[STATEMENT]
lemma finiteExpand:
  fixes P :: pi
  and   Q :: pi

  shows "finite(expandSet P Q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (expandSet P Q)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. finite (expandSet P Q)
[PROOF STEP]
have "finite {\<tau>.(P' \<parallel> Q) | P'. \<tau>.(P') \<in> summands P}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {\<tau>.(P' \<parallel> Q) |P'. \<tau>.P' \<in> summands P}
[PROOF STEP]
by(induct P rule: pi.induct, auto simp add: pi.inject Collect_ex_eq conj_disj_distribL
                                                           Collect_disj_eq UN_Un_distrib)
[PROOF STATE]
proof (state)
this:
finite {\<tau>.(P' \<parallel> Q) |P'. \<tau>.P' \<in> summands P}

goal (1 subgoal):
 1. finite (expandSet P Q)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
finite {\<tau>.(P' \<parallel> Q) |P'. \<tau>.P' \<in> summands P}

goal (1 subgoal):
 1. finite (expandSet P Q)
[PROOF STEP]
have "finite {\<tau>.(P \<parallel> Q') | Q'. \<tau>.(Q') \<in> summands Q}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {\<tau>.(P \<parallel> Q') |Q'. \<tau>.Q' \<in> summands Q}
[PROOF STEP]
by(induct Q rule: pi.induct, auto simp add: pi.inject Collect_ex_eq conj_disj_distribL
                                                           Collect_disj_eq UN_Un_distrib)
[PROOF STATE]
proof (state)
this:
finite {\<tau>.(P \<parallel> Q') |Q'. \<tau>.Q' \<in> summands Q}

goal (1 subgoal):
 1. finite (expandSet P Q)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
finite {\<tau>.(P \<parallel> Q') |Q'. \<tau>.Q' \<in> summands Q}

goal (1 subgoal):
 1. finite (expandSet P Q)
[PROOF STEP]
have "finite {a{b}.(P' \<parallel> Q) | a b P'. a{b}.P' \<in> summands P}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {a{b}.(P' \<parallel> Q) |a b P'. a{b}.P' \<in> summands P}
[PROOF STEP]
by(induct P rule: pi.induct, auto simp add: pi.inject Collect_ex_eq conj_disj_distribL
                                                           Collect_disj_eq UN_Un_distrib)
[PROOF STATE]
proof (state)
this:
finite {a{b}.(P' \<parallel> Q) |a b P'. a{b}.P' \<in> summands P}

goal (1 subgoal):
 1. finite (expandSet P Q)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
finite {a{b}.(P' \<parallel> Q) |a b P'. a{b}.P' \<in> summands P}

goal (1 subgoal):
 1. finite (expandSet P Q)
[PROOF STEP]
have "finite {a{b}.(P \<parallel> Q') | a b Q'. a{b}.Q' \<in> summands Q}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {a{b}.(P \<parallel> Q') |a b Q'. a{b}.Q' \<in> summands Q}
[PROOF STEP]
by(induct Q rule: pi.induct, auto simp add: pi.inject Collect_ex_eq conj_disj_distribL
                                                           Collect_disj_eq UN_Un_distrib)
[PROOF STATE]
proof (state)
this:
finite {a{b}.(P \<parallel> Q') |a b Q'. a{b}.Q' \<in> summands Q}

goal (1 subgoal):
 1. finite (expandSet P Q)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
finite {a{b}.(P \<parallel> Q') |a b Q'. a{b}.Q' \<in> summands Q}

goal (1 subgoal):
 1. finite (expandSet P Q)
[PROOF STEP]
have "finite {a<x>.(P' \<parallel> Q) | a x P'. a<x>.P' \<in> summands P \<and> x \<sharp> Q}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {a<x>.(P' \<parallel> Q) |a x P'. a<x>.P' \<in> summands P \<and> x \<sharp> Q}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. finite {a<x>.(P' \<parallel> Q) |a x P'. a<x>.P' \<in> summands P \<and> x \<sharp> Q}
[PROOF STEP]
have Aux: "\<And>a x P Q. (x::name) \<sharp> Q \<Longrightarrow> {a'<x'>.(P' \<parallel> Q) |a' x' P'. a'<x'>.P' = a<x>.P \<and> x' \<sharp> Q} = {a<x>.(P \<parallel> Q)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a x P Q. x \<sharp> Q \<Longrightarrow> {a'<x'>.(P' \<parallel> Q) |a' x' P'. a'<x'>.P' = a<x>.P \<and> x' \<sharp> Q} = {a<x>.(P \<parallel> Q)}
[PROOF STEP]
by(auto simp add: pi.inject name_abs_eq name_fresh_fresh)
[PROOF STATE]
proof (state)
this:
?x \<sharp> ?Q \<Longrightarrow> {a'<x'>.(P' \<parallel> ?Q) |a' x' P'. a'<x'>.P' = ?a<?x>.?P \<and> x' \<sharp> ?Q} = {?a<?x>.(?P \<parallel> ?Q)}

goal (1 subgoal):
 1. finite {a<x>.(P' \<parallel> Q) |a x P'. a<x>.P' \<in> summands P \<and> x \<sharp> Q}
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
?x \<sharp> ?Q \<Longrightarrow> {a'<x'>.(P' \<parallel> ?Q) |a' x' P'. a'<x'>.P' = ?a<?x>.?P \<and> x' \<sharp> ?Q} = {?a<?x>.(?P \<parallel> ?Q)}

goal (1 subgoal):
 1. finite {a<x>.(P' \<parallel> Q) |a x P'. a<x>.P' \<in> summands P \<and> x \<sharp> Q}
[PROOF STEP]
by(nominal_induct P avoiding: Q rule: pi.strong_induct,
         auto simp add: Collect_ex_eq conj_disj_distribL conj_disj_distribR
                        Collect_disj_eq UN_Un_distrib)
[PROOF STATE]
proof (state)
this:
finite {a<x>.(P' \<parallel> Q) |a x P'. a<x>.P' \<in> summands P \<and> x \<sharp> Q}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
finite {a<x>.(P' \<parallel> Q) |a x P'. a<x>.P' \<in> summands P \<and> x \<sharp> Q}

goal (1 subgoal):
 1. finite (expandSet P Q)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
finite {a<x>.(P' \<parallel> Q) |a x P'. a<x>.P' \<in> summands P \<and> x \<sharp> Q}

goal (1 subgoal):
 1. finite (expandSet P Q)
[PROOF STEP]
have "finite {a<x>.(P \<parallel> Q') | a x Q'. a<x>.Q' \<in> summands Q \<and> x \<sharp> P}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {a<x>.(P \<parallel> Q') |a x Q'. a<x>.Q' \<in> summands Q \<and> x \<sharp> P}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. finite {a<x>.(P \<parallel> Q') |a x Q'. a<x>.Q' \<in> summands Q \<and> x \<sharp> P}
[PROOF STEP]
have Aux: "\<And>a x P Q. (x::name) \<sharp> P \<Longrightarrow> {a'<x'>.(P \<parallel> Q') |a' x' Q'. a'<x'>.Q' = a<x>.Q \<and> x' \<sharp> P} = {a<x>.(P \<parallel> Q)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a x P Q. x \<sharp> P \<Longrightarrow> {a'<x'>.(P \<parallel> Q') |a' x' Q'. a'<x'>.Q' = a<x>.Q \<and> x' \<sharp> P} = {a<x>.(P \<parallel> Q)}
[PROOF STEP]
by(auto simp add: pi.inject name_abs_eq name_fresh_fresh)
[PROOF STATE]
proof (state)
this:
?x \<sharp> ?P \<Longrightarrow> {a'<x'>.(?P \<parallel> Q') |a' x' Q'. a'<x'>.Q' = ?a<?x>.?Q \<and> x' \<sharp> ?P} = {?a<?x>.(?P \<parallel> ?Q)}

goal (1 subgoal):
 1. finite {a<x>.(P \<parallel> Q') |a x Q'. a<x>.Q' \<in> summands Q \<and> x \<sharp> P}
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
?x \<sharp> ?P \<Longrightarrow> {a'<x'>.(?P \<parallel> Q') |a' x' Q'. a'<x'>.Q' = ?a<?x>.?Q \<and> x' \<sharp> ?P} = {?a<?x>.(?P \<parallel> ?Q)}

goal (1 subgoal):
 1. finite {a<x>.(P \<parallel> Q') |a x Q'. a<x>.Q' \<in> summands Q \<and> x \<sharp> P}
[PROOF STEP]
by(nominal_induct Q avoiding: P rule: pi.strong_induct,
         auto simp add: Collect_ex_eq conj_disj_distribL conj_disj_distribR
                        Collect_disj_eq UN_Un_distrib)
[PROOF STATE]
proof (state)
this:
finite {a<x>.(P \<parallel> Q') |a x Q'. a<x>.Q' \<in> summands Q \<and> x \<sharp> P}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
finite {a<x>.(P \<parallel> Q') |a x Q'. a<x>.Q' \<in> summands Q \<and> x \<sharp> P}

goal (1 subgoal):
 1. finite (expandSet P Q)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
finite {a<x>.(P \<parallel> Q') |a x Q'. a<x>.Q' \<in> summands Q \<and> x \<sharp> P}

goal (1 subgoal):
 1. finite (expandSet P Q)
[PROOF STEP]
have "finite {<\<nu>x>a{x}.(P' \<parallel> Q) | a x P'. <\<nu>x>a{x}.P' \<in> summands P \<and> x \<sharp> Q}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {<\<nu>x>a{x}.(P' \<parallel> Q) |a x P'. <\<nu>x>a{x}.P' \<in> summands P \<and> x \<sharp> Q}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. finite {<\<nu>x>a{x}.(P' \<parallel> Q) |a x P'. <\<nu>x>a{x}.P' \<in> summands P \<and> x \<sharp> Q}
[PROOF STEP]
have Aux: "\<And>a x P Q. \<lbrakk>x \<sharp> Q; a \<noteq> x\<rbrakk> \<Longrightarrow> {<\<nu>x'>a'{x'}.(P' \<parallel> Q) |a' x' P'. <\<nu>x'>a'{x'}.P' = <\<nu>x>a{x}.P \<and> x' \<sharp> Q} =
                                             {<\<nu>x>a{x}.(P \<parallel> Q)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a x P Q. \<lbrakk>x \<sharp> Q; a \<noteq> x\<rbrakk> \<Longrightarrow> {<\<nu>x'>a'{x'}.(P' \<parallel> Q) |a' x' P'. <\<nu>x'>a'{x'}.P' = <\<nu>x>a{x}.P \<and> x' \<sharp> Q} = {<\<nu>x>a{x}.(P \<parallel> Q)}
[PROOF STEP]
by(auto simp add: pi.inject name_abs_eq name_fresh_fresh)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?x \<sharp> ?Q; ?a \<noteq> ?x\<rbrakk> \<Longrightarrow> {<\<nu>x'>a'{x'}.(P' \<parallel> ?Q) |a' x' P'. <\<nu>x'>a'{x'}.P' = <\<nu>?x>?a{?x}.?P \<and> x' \<sharp> ?Q} = {<\<nu>?x>?a{?x}.(?P \<parallel> ?Q)}

goal (1 subgoal):
 1. finite {<\<nu>x>a{x}.(P' \<parallel> Q) |a x P'. <\<nu>x>a{x}.P' \<in> summands P \<and> x \<sharp> Q}
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x \<sharp> ?Q; ?a \<noteq> ?x\<rbrakk> \<Longrightarrow> {<\<nu>x'>a'{x'}.(P' \<parallel> ?Q) |a' x' P'. <\<nu>x'>a'{x'}.P' = <\<nu>?x>?a{?x}.?P \<and> x' \<sharp> ?Q} = {<\<nu>?x>?a{?x}.(?P \<parallel> ?Q)}

goal (1 subgoal):
 1. finite {<\<nu>x>a{x}.(P' \<parallel> Q) |a x P'. <\<nu>x>a{x}.P' \<in> summands P \<and> x \<sharp> Q}
[PROOF STEP]
by(nominal_induct P avoiding: Q rule: pi.strong_induct,
         auto simp add: Collect_ex_eq conj_disj_distribL conj_disj_distribR
                        Collect_disj_eq UN_Un_distrib)
[PROOF STATE]
proof (state)
this:
finite {<\<nu>x>a{x}.(P' \<parallel> Q) |a x P'. <\<nu>x>a{x}.P' \<in> summands P \<and> x \<sharp> Q}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
finite {<\<nu>x>a{x}.(P' \<parallel> Q) |a x P'. <\<nu>x>a{x}.P' \<in> summands P \<and> x \<sharp> Q}

goal (1 subgoal):
 1. finite (expandSet P Q)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
finite {<\<nu>x>a{x}.(P' \<parallel> Q) |a x P'. <\<nu>x>a{x}.P' \<in> summands P \<and> x \<sharp> Q}

goal (1 subgoal):
 1. finite (expandSet P Q)
[PROOF STEP]
have "finite {<\<nu>x>a{x}.(P \<parallel> Q') | a x Q'. <\<nu>x>a{x}.Q' \<in> summands Q \<and> x \<sharp> P}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {<\<nu>x>a{x}.(P \<parallel> Q') |a x Q'. <\<nu>x>a{x}.Q' \<in> summands Q \<and> x \<sharp> P}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. finite {<\<nu>x>a{x}.(P \<parallel> Q') |a x Q'. <\<nu>x>a{x}.Q' \<in> summands Q \<and> x \<sharp> P}
[PROOF STEP]
have Aux: "\<And>a x P Q. \<lbrakk>x \<sharp> P; a \<noteq> x\<rbrakk> \<Longrightarrow> {<\<nu>x'>a'{x'}.(P \<parallel> Q') |a' x' Q'. <\<nu>x'>a'{x'}.Q' = <\<nu>x>a{x}.Q \<and> x' \<sharp> P} =
                                             {<\<nu>x>a{x}.(P \<parallel> Q)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a x P Q. \<lbrakk>x \<sharp> P; a \<noteq> x\<rbrakk> \<Longrightarrow> {<\<nu>x'>a'{x'}.(P \<parallel> Q') |a' x' Q'. <\<nu>x'>a'{x'}.Q' = <\<nu>x>a{x}.Q \<and> x' \<sharp> P} = {<\<nu>x>a{x}.(P \<parallel> Q)}
[PROOF STEP]
by(auto simp add: pi.inject name_abs_eq name_fresh_fresh)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?x \<sharp> ?P; ?a \<noteq> ?x\<rbrakk> \<Longrightarrow> {<\<nu>x'>a'{x'}.(?P \<parallel> Q') |a' x' Q'. <\<nu>x'>a'{x'}.Q' = <\<nu>?x>?a{?x}.?Q \<and> x' \<sharp> ?P} = {<\<nu>?x>?a{?x}.(?P \<parallel> ?Q)}

goal (1 subgoal):
 1. finite {<\<nu>x>a{x}.(P \<parallel> Q') |a x Q'. <\<nu>x>a{x}.Q' \<in> summands Q \<and> x \<sharp> P}
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x \<sharp> ?P; ?a \<noteq> ?x\<rbrakk> \<Longrightarrow> {<\<nu>x'>a'{x'}.(?P \<parallel> Q') |a' x' Q'. <\<nu>x'>a'{x'}.Q' = <\<nu>?x>?a{?x}.?Q \<and> x' \<sharp> ?P} = {<\<nu>?x>?a{?x}.(?P \<parallel> ?Q)}

goal (1 subgoal):
 1. finite {<\<nu>x>a{x}.(P \<parallel> Q') |a x Q'. <\<nu>x>a{x}.Q' \<in> summands Q \<and> x \<sharp> P}
[PROOF STEP]
by(nominal_induct Q avoiding: P rule: pi.strong_induct,
         auto simp add: Collect_ex_eq conj_disj_distribL conj_disj_distribR
                        Collect_disj_eq UN_Un_distrib)
[PROOF STATE]
proof (state)
this:
finite {<\<nu>x>a{x}.(P \<parallel> Q') |a x Q'. <\<nu>x>a{x}.Q' \<in> summands Q \<and> x \<sharp> P}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
finite {<\<nu>x>a{x}.(P \<parallel> Q') |a x Q'. <\<nu>x>a{x}.Q' \<in> summands Q \<and> x \<sharp> P}

goal (1 subgoal):
 1. finite (expandSet P Q)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
finite {<\<nu>x>a{x}.(P \<parallel> Q') |a x Q'. <\<nu>x>a{x}.Q' \<in> summands Q \<and> x \<sharp> P}

goal (1 subgoal):
 1. finite (expandSet P Q)
[PROOF STEP]
have "finite {\<tau>.(P'[x::=b] \<parallel> Q') | x P' b Q'. \<exists>a. a<x>.P' \<in> summands P \<and> a{b}.Q' \<in> summands Q}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {\<tau>.(P'[x::=b] \<parallel> Q') |x P' b Q'. \<exists>a. a<x>.P' \<in> summands P \<and> a{b}.Q' \<in> summands Q}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. finite {\<tau>.(P'[x::=b] \<parallel> Q') |x P' b Q'. \<exists>a. a<x>.P' \<in> summands P \<and> a{b}.Q' \<in> summands Q}
[PROOF STEP]
have Aux: "\<And>a x P b Q. {\<tau>.(P'[x'::=b'] \<parallel> Q') | a' x' P' b' Q'. a'<x'>.P' = a<x>.P \<and> a'{b'}.Q' = a{b}.Q} = {\<tau>.(P[x::=b] \<parallel> Q)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a x P b Q. {uu_. \<exists>a' x' P' b' Q'. uu_ = \<tau>.(P'[x'::=b'] \<parallel> Q') \<and> a'<x'>.P' = a<x>.P \<and> a'{b'}.Q' = a{b}.Q} = {\<tau>.(P[x::=b] \<parallel> Q)}
[PROOF STEP]
by(auto simp add: name_abs_eq pi.inject renaming)
[PROOF STATE]
proof (state)
this:
{uu_. \<exists>a' x' P' b' Q'. uu_ = \<tau>.(P'[x'::=b'] \<parallel> Q') \<and> a'<x'>.P' = ?a<?x>.?P \<and> a'{b'}.Q' = ?a{?b}.?Q} = {\<tau>.(?P[?x::=?b] \<parallel> ?Q)}

goal (1 subgoal):
 1. finite {\<tau>.(P'[x::=b] \<parallel> Q') |x P' b Q'. \<exists>a. a<x>.P' \<in> summands P \<and> a{b}.Q' \<in> summands Q}
[PROOF STEP]
have "\<And>a x P Q b::'a::{}. finite {\<tau>.(P'[x'::=b] \<parallel> Q') | a' x' P' b Q'. a'<x'>.P' = a<x>.P \<and> a'{b}.Q' \<in> summands Q}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a x P Q b. finite {uu_. \<exists>a' x' P' b Q'. uu_ = \<tau>.(P'[x'::=b] \<parallel> Q') \<and> a'<x'>.P' = a<x>.P \<and> a'{b}.Q' \<in> summands Q}
[PROOF STEP]
apply(induct rule: pi.induct, simp_all)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a x P name1 name2 pi. finite {uu_. \<exists>a' x' P' b Q'. uu_ = \<tau>.(P'[x'::=b] \<parallel> Q') \<and> a'<x'>.P' = a<x>.P \<and> a'{b}.Q' \<in> summands pi} \<Longrightarrow> finite {uu_. \<exists>a' x' P' b Q'. uu_ = \<tau>.(P'[x'::=b] \<parallel> Q') \<and> a'<x'>.P' = a<x>.P \<and> a'{b}.Q' = name1{name2}.pi}
 2. \<And>a x P pi1 pi2. \<lbrakk>finite {uu_. \<exists>a' x' P' b Q'. uu_ = \<tau>.(P'[x'::=b] \<parallel> Q') \<and> a'<x'>.P' = a<x>.P \<and> a'{b}.Q' \<in> summands pi1}; finite {uu_. \<exists>a' x' P' b Q'. uu_ = \<tau>.(P'[x'::=b] \<parallel> Q') \<and> a'<x'>.P' = a<x>.P \<and> a'{b}.Q' \<in> summands pi2}\<rbrakk> \<Longrightarrow> finite {uu_. \<exists>a' x' P' b Q'. uu_ = \<tau>.(P'[x'::=b] \<parallel> Q') \<and> a'<x'>.P' = a<x>.P \<and> (a'{b}.Q' \<in> summands pi1 \<or> a'{b}.Q' \<in> summands pi2)}
[PROOF STEP]
apply(case_tac "a=name1")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a x P name1 name2 pi. \<lbrakk>finite {uu_. \<exists>a' x' P' b Q'. uu_ = \<tau>.(P'[x'::=b] \<parallel> Q') \<and> a'<x'>.P' = a<x>.P \<and> a'{b}.Q' \<in> summands pi}; a = name1\<rbrakk> \<Longrightarrow> finite {uu_. \<exists>a' x' P' b Q'. uu_ = \<tau>.(P'[x'::=b] \<parallel> Q') \<and> a'<x'>.P' = a<x>.P \<and> a'{b}.Q' = name1{name2}.pi}
 2. \<And>a x P name1 name2 pi. \<lbrakk>finite {uu_. \<exists>a' x' P' b Q'. uu_ = \<tau>.(P'[x'::=b] \<parallel> Q') \<and> a'<x'>.P' = a<x>.P \<and> a'{b}.Q' \<in> summands pi}; a \<noteq> name1\<rbrakk> \<Longrightarrow> finite {uu_. \<exists>a' x' P' b Q'. uu_ = \<tau>.(P'[x'::=b] \<parallel> Q') \<and> a'<x'>.P' = a<x>.P \<and> a'{b}.Q' = name1{name2}.pi}
 3. \<And>a x P pi1 pi2. \<lbrakk>finite {uu_. \<exists>a' x' P' b Q'. uu_ = \<tau>.(P'[x'::=b] \<parallel> Q') \<and> a'<x'>.P' = a<x>.P \<and> a'{b}.Q' \<in> summands pi1}; finite {uu_. \<exists>a' x' P' b Q'. uu_ = \<tau>.(P'[x'::=b] \<parallel> Q') \<and> a'<x'>.P' = a<x>.P \<and> a'{b}.Q' \<in> summands pi2}\<rbrakk> \<Longrightarrow> finite {uu_. \<exists>a' x' P' b Q'. uu_ = \<tau>.(P'[x'::=b] \<parallel> Q') \<and> a'<x'>.P' = a<x>.P \<and> (a'{b}.Q' \<in> summands pi1 \<or> a'{b}.Q' \<in> summands pi2)}
[PROOF STEP]
apply(simp add: Aux)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a x P name1 name2 pi. \<lbrakk>finite {uu_. \<exists>a' x' P' b Q'. uu_ = \<tau>.(P'[x'::=b] \<parallel> Q') \<and> a'<x'>.P' = a<x>.P \<and> a'{b}.Q' \<in> summands pi}; a \<noteq> name1\<rbrakk> \<Longrightarrow> finite {uu_. \<exists>a' x' P' b Q'. uu_ = \<tau>.(P'[x'::=b] \<parallel> Q') \<and> a'<x'>.P' = a<x>.P \<and> a'{b}.Q' = name1{name2}.pi}
 2. \<And>a x P pi1 pi2. \<lbrakk>finite {uu_. \<exists>a' x' P' b Q'. uu_ = \<tau>.(P'[x'::=b] \<parallel> Q') \<and> a'<x'>.P' = a<x>.P \<and> a'{b}.Q' \<in> summands pi1}; finite {uu_. \<exists>a' x' P' b Q'. uu_ = \<tau>.(P'[x'::=b] \<parallel> Q') \<and> a'<x'>.P' = a<x>.P \<and> a'{b}.Q' \<in> summands pi2}\<rbrakk> \<Longrightarrow> finite {uu_. \<exists>a' x' P' b Q'. uu_ = \<tau>.(P'[x'::=b] \<parallel> Q') \<and> a'<x'>.P' = a<x>.P \<and> (a'{b}.Q' \<in> summands pi1 \<or> a'{b}.Q' \<in> summands pi2)}
[PROOF STEP]
apply(simp add: pi.inject)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a x P pi1 pi2. \<lbrakk>finite {uu_. \<exists>a' x' P' b Q'. uu_ = \<tau>.(P'[x'::=b] \<parallel> Q') \<and> a'<x'>.P' = a<x>.P \<and> a'{b}.Q' \<in> summands pi1}; finite {uu_. \<exists>a' x' P' b Q'. uu_ = \<tau>.(P'[x'::=b] \<parallel> Q') \<and> a'<x'>.P' = a<x>.P \<and> a'{b}.Q' \<in> summands pi2}\<rbrakk> \<Longrightarrow> finite {uu_. \<exists>a' x' P' b Q'. uu_ = \<tau>.(P'[x'::=b] \<parallel> Q') \<and> a'<x'>.P' = a<x>.P \<and> (a'{b}.Q' \<in> summands pi1 \<or> a'{b}.Q' \<in> summands pi2)}
[PROOF STEP]
by(simp add: Collect_ex_eq conj_disj_distribL conj_disj_distribR
                   Collect_disj_eq UN_Un_distrib)
[PROOF STATE]
proof (state)
this:
finite {uu_. \<exists>a' x' P' b Q'. uu_ = \<tau>.(P'[x'::=b] \<parallel> Q') \<and> a'<x'>.P' = ?a<?x>.?P \<and> a'{b}.Q' \<in> summands ?Q}

goal (1 subgoal):
 1. finite {\<tau>.(P'[x::=b] \<parallel> Q') |x P' b Q'. \<exists>a. a<x>.P' \<in> summands P \<and> a{b}.Q' \<in> summands Q}
[PROOF STEP]
hence "finite {\<tau>.(P'[x::=b] \<parallel> Q') | a x P' b Q'. a<x>.P' \<in> summands P \<and> a{b}.Q' \<in> summands Q}"
[PROOF STATE]
proof (prove)
using this:
finite {uu_. \<exists>a' x' P' b Q'. uu_ = \<tau>.(P'[x'::=b] \<parallel> Q') \<and> a'<x'>.P' = ?a<?x>.?P \<and> a'{b}.Q' \<in> summands ?Q}

goal (1 subgoal):
 1. finite {uu_. \<exists>a x P' b Q'. uu_ = \<tau>.(P'[x::=b] \<parallel> Q') \<and> a<x>.P' \<in> summands P \<and> a{b}.Q' \<in> summands Q}
[PROOF STEP]
by(nominal_induct P avoiding: Q rule: pi.strong_induct,
         auto simp add: Collect_ex_eq conj_disj_distribL conj_disj_distribR
                        Collect_disj_eq UN_Un_distrib name_abs_eq)
[PROOF STATE]
proof (state)
this:
finite {uu_. \<exists>a x P' b Q'. uu_ = \<tau>.(P'[x::=b] \<parallel> Q') \<and> a<x>.P' \<in> summands P \<and> a{b}.Q' \<in> summands Q}

goal (1 subgoal):
 1. finite {\<tau>.(P'[x::=b] \<parallel> Q') |x P' b Q'. \<exists>a. a<x>.P' \<in> summands P \<and> a{b}.Q' \<in> summands Q}
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
finite {uu_. \<exists>a x P' b Q'. uu_ = \<tau>.(P'[x::=b] \<parallel> Q') \<and> a<x>.P' \<in> summands P \<and> a{b}.Q' \<in> summands Q}

goal (1 subgoal):
 1. finite {\<tau>.(P'[x::=b] \<parallel> Q') |x P' b Q'. \<exists>a. a<x>.P' \<in> summands P \<and> a{b}.Q' \<in> summands Q}
[PROOF STEP]
apply(rule_tac finite_subset)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. finite {uu_. \<exists>a x P' b Q'. uu_ = \<tau>.(P'[x::=b] \<parallel> Q') \<and> a<x>.P' \<in> summands P \<and> a{b}.Q' \<in> summands Q} \<Longrightarrow> {\<tau>.(P'[x::=b] \<parallel> Q') |x P' b Q'. \<exists>a. a<x>.P' \<in> summands P \<and> a{b}.Q' \<in> summands Q} \<subseteq> ?B1
 2. finite {uu_. \<exists>a x P' b Q'. uu_ = \<tau>.(P'[x::=b] \<parallel> Q') \<and> a<x>.P' \<in> summands P \<and> a{b}.Q' \<in> summands Q} \<Longrightarrow> finite ?B1
[PROOF STEP]
defer
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. finite {uu_. \<exists>a x P' b Q'. uu_ = \<tau>.(P'[x::=b] \<parallel> Q') \<and> a<x>.P' \<in> summands P \<and> a{b}.Q' \<in> summands Q} \<Longrightarrow> finite ?B1
 2. finite {uu_. \<exists>a x P' b Q'. uu_ = \<tau>.(P'[x::=b] \<parallel> Q') \<and> a<x>.P' \<in> summands P \<and> a{b}.Q' \<in> summands Q} \<Longrightarrow> {\<tau>.(P'[x::=b] \<parallel> Q') |x P' b Q'. \<exists>a. a<x>.P' \<in> summands P \<and> a{b}.Q' \<in> summands Q} \<subseteq> ?B1
[PROOF STEP]
by blast+
[PROOF STATE]
proof (state)
this:
finite {\<tau>.(P'[x::=b] \<parallel> Q') |x P' b Q'. \<exists>a. a<x>.P' \<in> summands P \<and> a{b}.Q' \<in> summands Q}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
finite {\<tau>.(P'[x::=b] \<parallel> Q') |x P' b Q'. \<exists>a. a<x>.P' \<in> summands P \<and> a{b}.Q' \<in> summands Q}

goal (1 subgoal):
 1. finite (expandSet P Q)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
finite {\<tau>.(P'[x::=b] \<parallel> Q') |x P' b Q'. \<exists>a. a<x>.P' \<in> summands P \<and> a{b}.Q' \<in> summands Q}

goal (1 subgoal):
 1. finite (expandSet P Q)
[PROOF STEP]
have "finite {\<tau>.(P' \<parallel> (Q'[x::=b])) | b P' x Q'. \<exists>a. a{b}.P' \<in> summands P \<and> a<x>.Q' \<in> summands Q}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {\<tau>.(P' \<parallel> Q'[x::=b]) |b P' x Q'. \<exists>a. a{b}.P' \<in> summands P \<and> a<x>.Q' \<in> summands Q}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. finite {\<tau>.(P' \<parallel> Q'[x::=b]) |b P' x Q'. \<exists>a. a{b}.P' \<in> summands P \<and> a<x>.Q' \<in> summands Q}
[PROOF STEP]
have Aux: "\<And>a x P b Q. {\<tau>.(P' \<parallel> (Q'[x'::=b'])) | a' b' P' x' Q'. a'{b'}.P' = a{b}.P \<and> a'<x'>.Q' = a<x>.Q} = {\<tau>.(P \<parallel> (Q[x::=b]))}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a x P b Q. {uu_. \<exists>a' b' P' x' Q'. uu_ = \<tau>.(P' \<parallel> Q'[x'::=b']) \<and> a'{b'}.P' = a{b}.P \<and> a'<x'>.Q' = a<x>.Q} = {\<tau>.(P \<parallel> Q[x::=b])}
[PROOF STEP]
by(auto simp add: name_abs_eq pi.inject renaming)
[PROOF STATE]
proof (state)
this:
{uu_. \<exists>a' b' P' x' Q'. uu_ = \<tau>.(P' \<parallel> Q'[x'::=b']) \<and> a'{b'}.P' = ?a{?b}.?P \<and> a'<x'>.Q' = ?a<?x>.?Q} = {\<tau>.(?P \<parallel> ?Q[?x::=?b])}

goal (1 subgoal):
 1. finite {\<tau>.(P' \<parallel> Q'[x::=b]) |b P' x Q'. \<exists>a. a{b}.P' \<in> summands P \<and> a<x>.Q' \<in> summands Q}
[PROOF STEP]
have "\<And>a b P Q x::'a::{}. finite {\<tau>.(P' \<parallel> (Q'[x::=b'])) | a' b' P' x Q'. a'{b'}.P' = a{b}.P \<and> a'<x>.Q' \<in> summands Q}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b P Q x. finite {uu_. \<exists>a' b' P' x Q'. uu_ = \<tau>.(P' \<parallel> Q'[x::=b']) \<and> a'{b'}.P' = a{b}.P \<and> a'<x>.Q' \<in> summands Q}
[PROOF STEP]
apply(induct rule: pi.induct, simp_all)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b P name1 name2 pi. finite {uu_. \<exists>a' b' P' x Q'. uu_ = \<tau>.(P' \<parallel> Q'[x::=b']) \<and> a'{b'}.P' = a{b}.P \<and> a'<x>.Q' \<in> summands pi} \<Longrightarrow> finite {uu_. \<exists>a' b' P' x Q'. uu_ = \<tau>.(P' \<parallel> Q'[x::=b']) \<and> a'{b'}.P' = a{b}.P \<and> a'<x>.Q' = name1<name2>.pi}
 2. \<And>a b P pi1 pi2. \<lbrakk>finite {uu_. \<exists>a' b' P' x Q'. uu_ = \<tau>.(P' \<parallel> Q'[x::=b']) \<and> a'{b'}.P' = a{b}.P \<and> a'<x>.Q' \<in> summands pi1}; finite {uu_. \<exists>a' b' P' x Q'. uu_ = \<tau>.(P' \<parallel> Q'[x::=b']) \<and> a'{b'}.P' = a{b}.P \<and> a'<x>.Q' \<in> summands pi2}\<rbrakk> \<Longrightarrow> finite {uu_. \<exists>a' b' P' x Q'. uu_ = \<tau>.(P' \<parallel> Q'[x::=b']) \<and> a'{b'}.P' = a{b}.P \<and> (a'<x>.Q' \<in> summands pi1 \<or> a'<x>.Q' \<in> summands pi2)}
[PROOF STEP]
apply(case_tac "a=name1")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a b P name1 name2 pi. \<lbrakk>finite {uu_. \<exists>a' b' P' x Q'. uu_ = \<tau>.(P' \<parallel> Q'[x::=b']) \<and> a'{b'}.P' = a{b}.P \<and> a'<x>.Q' \<in> summands pi}; a = name1\<rbrakk> \<Longrightarrow> finite {uu_. \<exists>a' b' P' x Q'. uu_ = \<tau>.(P' \<parallel> Q'[x::=b']) \<and> a'{b'}.P' = a{b}.P \<and> a'<x>.Q' = name1<name2>.pi}
 2. \<And>a b P name1 name2 pi. \<lbrakk>finite {uu_. \<exists>a' b' P' x Q'. uu_ = \<tau>.(P' \<parallel> Q'[x::=b']) \<and> a'{b'}.P' = a{b}.P \<and> a'<x>.Q' \<in> summands pi}; a \<noteq> name1\<rbrakk> \<Longrightarrow> finite {uu_. \<exists>a' b' P' x Q'. uu_ = \<tau>.(P' \<parallel> Q'[x::=b']) \<and> a'{b'}.P' = a{b}.P \<and> a'<x>.Q' = name1<name2>.pi}
 3. \<And>a b P pi1 pi2. \<lbrakk>finite {uu_. \<exists>a' b' P' x Q'. uu_ = \<tau>.(P' \<parallel> Q'[x::=b']) \<and> a'{b'}.P' = a{b}.P \<and> a'<x>.Q' \<in> summands pi1}; finite {uu_. \<exists>a' b' P' x Q'. uu_ = \<tau>.(P' \<parallel> Q'[x::=b']) \<and> a'{b'}.P' = a{b}.P \<and> a'<x>.Q' \<in> summands pi2}\<rbrakk> \<Longrightarrow> finite {uu_. \<exists>a' b' P' x Q'. uu_ = \<tau>.(P' \<parallel> Q'[x::=b']) \<and> a'{b'}.P' = a{b}.P \<and> (a'<x>.Q' \<in> summands pi1 \<or> a'<x>.Q' \<in> summands pi2)}
[PROOF STEP]
apply(simp add: Aux)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b P name1 name2 pi. \<lbrakk>finite {uu_. \<exists>a' b' P' x Q'. uu_ = \<tau>.(P' \<parallel> Q'[x::=b']) \<and> a'{b'}.P' = a{b}.P \<and> a'<x>.Q' \<in> summands pi}; a \<noteq> name1\<rbrakk> \<Longrightarrow> finite {uu_. \<exists>a' b' P' x Q'. uu_ = \<tau>.(P' \<parallel> Q'[x::=b']) \<and> a'{b'}.P' = a{b}.P \<and> a'<x>.Q' = name1<name2>.pi}
 2. \<And>a b P pi1 pi2. \<lbrakk>finite {uu_. \<exists>a' b' P' x Q'. uu_ = \<tau>.(P' \<parallel> Q'[x::=b']) \<and> a'{b'}.P' = a{b}.P \<and> a'<x>.Q' \<in> summands pi1}; finite {uu_. \<exists>a' b' P' x Q'. uu_ = \<tau>.(P' \<parallel> Q'[x::=b']) \<and> a'{b'}.P' = a{b}.P \<and> a'<x>.Q' \<in> summands pi2}\<rbrakk> \<Longrightarrow> finite {uu_. \<exists>a' b' P' x Q'. uu_ = \<tau>.(P' \<parallel> Q'[x::=b']) \<and> a'{b'}.P' = a{b}.P \<and> (a'<x>.Q' \<in> summands pi1 \<or> a'<x>.Q' \<in> summands pi2)}
[PROOF STEP]
apply(simp add: pi.inject)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b P pi1 pi2. \<lbrakk>finite {uu_. \<exists>a' b' P' x Q'. uu_ = \<tau>.(P' \<parallel> Q'[x::=b']) \<and> a'{b'}.P' = a{b}.P \<and> a'<x>.Q' \<in> summands pi1}; finite {uu_. \<exists>a' b' P' x Q'. uu_ = \<tau>.(P' \<parallel> Q'[x::=b']) \<and> a'{b'}.P' = a{b}.P \<and> a'<x>.Q' \<in> summands pi2}\<rbrakk> \<Longrightarrow> finite {uu_. \<exists>a' b' P' x Q'. uu_ = \<tau>.(P' \<parallel> Q'[x::=b']) \<and> a'{b'}.P' = a{b}.P \<and> (a'<x>.Q' \<in> summands pi1 \<or> a'<x>.Q' \<in> summands pi2)}
[PROOF STEP]
by(simp add: Collect_ex_eq conj_disj_distribL conj_disj_distribR
                     Collect_disj_eq UN_Un_distrib)
[PROOF STATE]
proof (state)
this:
finite {uu_. \<exists>a' b' P' x Q'. uu_ = \<tau>.(P' \<parallel> Q'[x::=b']) \<and> a'{b'}.P' = ?a{?b}.?P \<and> a'<x>.Q' \<in> summands ?Q}

goal (1 subgoal):
 1. finite {\<tau>.(P' \<parallel> Q'[x::=b]) |b P' x Q'. \<exists>a. a{b}.P' \<in> summands P \<and> a<x>.Q' \<in> summands Q}
[PROOF STEP]
hence "finite {\<tau>.(P' \<parallel> (Q'[x::=b])) | a b P' x Q'. a{b}.P' \<in> summands P \<and> a<x>.Q' \<in> summands Q}"
[PROOF STATE]
proof (prove)
using this:
finite {uu_. \<exists>a' b' P' x Q'. uu_ = \<tau>.(P' \<parallel> Q'[x::=b']) \<and> a'{b'}.P' = ?a{?b}.?P \<and> a'<x>.Q' \<in> summands ?Q}

goal (1 subgoal):
 1. finite {uu_. \<exists>a b P' x Q'. uu_ = \<tau>.(P' \<parallel> Q'[x::=b]) \<and> a{b}.P' \<in> summands P \<and> a<x>.Q' \<in> summands Q}
[PROOF STEP]
by(nominal_induct P avoiding: Q rule: pi.strong_induct,
         auto simp add: Collect_ex_eq conj_disj_distribL conj_disj_distribR
                        Collect_disj_eq UN_Un_distrib name_abs_eq)
[PROOF STATE]
proof (state)
this:
finite {uu_. \<exists>a b P' x Q'. uu_ = \<tau>.(P' \<parallel> Q'[x::=b]) \<and> a{b}.P' \<in> summands P \<and> a<x>.Q' \<in> summands Q}

goal (1 subgoal):
 1. finite {\<tau>.(P' \<parallel> Q'[x::=b]) |b P' x Q'. \<exists>a. a{b}.P' \<in> summands P \<and> a<x>.Q' \<in> summands Q}
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
finite {uu_. \<exists>a b P' x Q'. uu_ = \<tau>.(P' \<parallel> Q'[x::=b]) \<and> a{b}.P' \<in> summands P \<and> a<x>.Q' \<in> summands Q}

goal (1 subgoal):
 1. finite {\<tau>.(P' \<parallel> Q'[x::=b]) |b P' x Q'. \<exists>a. a{b}.P' \<in> summands P \<and> a<x>.Q' \<in> summands Q}
[PROOF STEP]
apply(rule_tac finite_subset)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. finite {uu_. \<exists>a b P' x Q'. uu_ = \<tau>.(P' \<parallel> Q'[x::=b]) \<and> a{b}.P' \<in> summands P \<and> a<x>.Q' \<in> summands Q} \<Longrightarrow> {\<tau>.(P' \<parallel> Q'[x::=b]) |b P' x Q'. \<exists>a. a{b}.P' \<in> summands P \<and> a<x>.Q' \<in> summands Q} \<subseteq> ?B1
 2. finite {uu_. \<exists>a b P' x Q'. uu_ = \<tau>.(P' \<parallel> Q'[x::=b]) \<and> a{b}.P' \<in> summands P \<and> a<x>.Q' \<in> summands Q} \<Longrightarrow> finite ?B1
[PROOF STEP]
defer
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. finite {uu_. \<exists>a b P' x Q'. uu_ = \<tau>.(P' \<parallel> Q'[x::=b]) \<and> a{b}.P' \<in> summands P \<and> a<x>.Q' \<in> summands Q} \<Longrightarrow> finite ?B1
 2. finite {uu_. \<exists>a b P' x Q'. uu_ = \<tau>.(P' \<parallel> Q'[x::=b]) \<and> a{b}.P' \<in> summands P \<and> a<x>.Q' \<in> summands Q} \<Longrightarrow> {\<tau>.(P' \<parallel> Q'[x::=b]) |b P' x Q'. \<exists>a. a{b}.P' \<in> summands P \<and> a<x>.Q' \<in> summands Q} \<subseteq> ?B1
[PROOF STEP]
by blast+
[PROOF STATE]
proof (state)
this:
finite {\<tau>.(P' \<parallel> Q'[x::=b]) |b P' x Q'. \<exists>a. a{b}.P' \<in> summands P \<and> a<x>.Q' \<in> summands Q}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
finite {\<tau>.(P' \<parallel> Q'[x::=b]) |b P' x Q'. \<exists>a. a{b}.P' \<in> summands P \<and> a<x>.Q' \<in> summands Q}

goal (1 subgoal):
 1. finite (expandSet P Q)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
finite {\<tau>.(P' \<parallel> Q'[x::=b]) |b P' x Q'. \<exists>a. a{b}.P' \<in> summands P \<and> a<x>.Q' \<in> summands Q}

goal (1 subgoal):
 1. finite (expandSet P Q)
[PROOF STEP]
have "finite {\<tau>.(<\<nu>y>(P'[x::=y] \<parallel> Q')) | x P' y Q'. \<exists>a. a<x>.P' \<in> summands P \<and> <\<nu>y>a{y}.Q' \<in> summands Q \<and> y \<sharp> P}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {\<tau>.(<\<nu>y>(P'[x::=y] \<parallel> Q')) |x P' y Q'. \<exists>a. a<x>.P' \<in> summands P \<and> <\<nu>y>a{y}.Q' \<in> summands Q \<and> y \<sharp> P}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. finite {\<tau>.(<\<nu>y>(P'[x::=y] \<parallel> Q')) |x P' y Q'. \<exists>a. a<x>.P' \<in> summands P \<and> <\<nu>y>a{y}.Q' \<in> summands Q \<and> y \<sharp> P}
[PROOF STEP]
have Aux: "\<And>a x P y Q. y \<sharp> P \<and> y \<noteq> a \<Longrightarrow> {\<tau>.(<\<nu>y'>(P'[x'::=y'] \<parallel> Q')) | a' x' P' y' Q'. a'<x'>.P' = a<x>.P \<and> <\<nu>y'>a'{y'}.Q' = <\<nu>y>a{y}.Q \<and> y' \<sharp> a<x>.P} = {\<tau>.(<\<nu>y>(P[x::=y] \<parallel> Q))}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a x P y Q. y \<sharp> P \<and> y \<noteq> a \<Longrightarrow> {uu_. \<exists>a' x' P' y' Q'. uu_ = \<tau>.(<\<nu>y'>(P'[x'::=y'] \<parallel> Q')) \<and> a'<x'>.P' = a<x>.P \<and> <\<nu>y'>a'{y'}.Q' = <\<nu>y>a{y}.Q \<and> y' \<sharp> a<x>.P} = {\<tau>.(<\<nu>y>(P[x::=y] \<parallel> Q))}
[PROOF STEP]
apply(auto simp add: pi.inject name_abs_eq name_fresh_abs name_calc fresh_fact2 fresh_fact1 eqvts forget)
[PROOF STATE]
proof (prove)
goal (9 subgoals):
 1. \<And>a x P y Q. \<lbrakk>y \<sharp> P; y \<noteq> a; x \<noteq> y; x \<noteq> a; x \<sharp> Q\<rbrakk> \<Longrightarrow> P = ([(x, y)] \<bullet> P)[y::=x]
 2. \<And>a x P y Q x'. \<lbrakk>y \<sharp> P; y \<noteq> a; x \<noteq> y; x \<noteq> a; x \<sharp> Q; x' \<noteq> x; x' \<sharp> P\<rbrakk> \<Longrightarrow> ([(x, x')] \<bullet> P)[x'::=x] = ([(x, y)] \<bullet> P)[y::=x]
 3. \<And>a x P y Q x' y'. \<lbrakk>y \<sharp> P; y \<noteq> a; y' \<noteq> y; y' \<noteq> a; y' \<sharp> Q; x' \<noteq> x; x' \<sharp> P; y' \<sharp> P; y \<noteq> x; y' \<noteq> x\<rbrakk> \<Longrightarrow> ([(x, x')] \<bullet> P)[x'::=y'] = P[x::=y']
 4. \<And>a x P y x'. \<lbrakk>y \<sharp> P; y \<noteq> a; x' \<noteq> x; x' \<sharp> P; ([(x, x')] \<bullet> P)[x'::=y] \<noteq> P[x::=y]\<rbrakk> \<Longrightarrow> False
 5. \<And>a x P y Q x'. \<lbrakk>y \<sharp> P; y \<noteq> a; x \<noteq> a; x \<sharp> Q; x' \<noteq> x; x' \<sharp> P; y \<noteq> x; ([(x, x')] \<bullet> P)[x'::=y] = ([(x, y)] \<bullet> [(x, x')] \<bullet> P)[x'::=y]; y \<sharp> ([(x, x')] \<bullet> P)[x'::=x]; y \<sharp> [(x, y)] \<bullet> Q; y \<noteq> x'\<rbrakk> \<Longrightarrow> ([(x, y)] \<bullet> [(x, x')] \<bullet> P)[x'::=y] = P[x::=y]
 6. \<And>a x P Q x' y'. \<lbrakk>y' \<noteq> a; y' \<sharp> Q; x' \<noteq> x; x' \<sharp> P; y' \<sharp> P\<rbrakk> \<Longrightarrow> ([(x, x')] \<bullet> P)[x'::=y'] = P[x::=y']
 7. \<And>a x P y Q x'. \<lbrakk>y \<sharp> P; y \<noteq> a; x' \<noteq> a; x' \<sharp> Q; x' \<noteq> x; x' \<sharp> P; ([(x, x')] \<bullet> P)[x'::=y] = [(y, x')] \<bullet> [(x, x')] \<bullet> P; y \<sharp> [(x, x')] \<bullet> P; y \<sharp> [(y, x')] \<bullet> Q; y \<noteq> x'\<rbrakk> \<Longrightarrow> [(y, x')] \<bullet> [(x, x')] \<bullet> P = P[x::=y]
 8. \<And>a x P Q x' y'. \<lbrakk>x' \<noteq> a; y' \<noteq> a; y' \<sharp> Q; x' \<noteq> x; x' \<sharp> P; y' \<sharp> P; [(x, x')] \<bullet> P = ([(x', y')] \<bullet> [(x, x')] \<bullet> P)[y'::=x']; x' \<sharp> [(x', y')] \<bullet> Q; y' \<noteq> x'\<rbrakk> \<Longrightarrow> [(x, x')] \<bullet> P = P[x::=x']
 9. \<And>a x P y Q x' y'. \<lbrakk>y \<sharp> P; y \<noteq> a; y' \<noteq> a; y' \<sharp> Q; x' \<noteq> x; x' \<sharp> P; y' \<sharp> P; y \<noteq> y'; ([(x, x')] \<bullet> P)[x'::=y] = ([(y, y')] \<bullet> [(x, x')] \<bullet> P)[x'::=y]; y \<sharp> ([(x, x')] \<bullet> P)[x'::=y']; y \<sharp> [(y, y')] \<bullet> Q; y' \<noteq> x'; y \<noteq> x'\<rbrakk> \<Longrightarrow> ([(y, y')] \<bullet> [(x, x')] \<bullet> P)[x'::=y] = P[x::=y]
[PROOF STEP]
apply(subst name_swap, simp add: injPermSubst fresh_fact1 fresh_fact2)+
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>a x P y x'. \<lbrakk>y \<sharp> P; y \<noteq> a; x' \<noteq> x; x' \<sharp> P; ([(x, x')] \<bullet> P)[x'::=y] \<noteq> P[x::=y]\<rbrakk> \<Longrightarrow> False
 2. \<And>a x P y Q x'. \<lbrakk>y \<sharp> P; y \<noteq> a; x \<noteq> a; x \<sharp> Q; x' \<noteq> x; x' \<sharp> P; y \<noteq> x; ([(x, x')] \<bullet> P)[x'::=y] = ([(x, y)] \<bullet> [(x, x')] \<bullet> P)[x'::=y]; y \<sharp> ([(x, x')] \<bullet> P)[x'::=x]; y \<sharp> [(x, y)] \<bullet> Q; y \<noteq> x'\<rbrakk> \<Longrightarrow> ([(x, y)] \<bullet> [(x, x')] \<bullet> P)[x'::=y] = P[x::=y]
 3. \<And>a x P Q x' y'. \<lbrakk>y' \<noteq> a; y' \<sharp> Q; x' \<noteq> x; x' \<sharp> P; y' \<sharp> P\<rbrakk> \<Longrightarrow> ([(x, x')] \<bullet> P)[x'::=y'] = P[x::=y']
 4. \<And>a x P y Q x'. \<lbrakk>y \<sharp> P; y \<noteq> a; x' \<noteq> a; x' \<sharp> Q; x' \<noteq> x; x' \<sharp> P; ([(x, x')] \<bullet> P)[x'::=y] = [(y, x')] \<bullet> [(x, x')] \<bullet> P; y \<sharp> [(x, x')] \<bullet> P; y \<sharp> [(y, x')] \<bullet> Q; y \<noteq> x'\<rbrakk> \<Longrightarrow> [(y, x')] \<bullet> [(x, x')] \<bullet> P = P[x::=y]
 5. \<And>a x P Q x' y'. \<lbrakk>x' \<noteq> a; y' \<noteq> a; y' \<sharp> Q; x' \<noteq> x; x' \<sharp> P; y' \<sharp> P; [(x, x')] \<bullet> P = ([(x', y')] \<bullet> [(x, x')] \<bullet> P)[y'::=x']; x' \<sharp> [(x', y')] \<bullet> Q; y' \<noteq> x'\<rbrakk> \<Longrightarrow> [(x, x')] \<bullet> P = P[x::=x']
 6. \<And>a x P y Q x' y'. \<lbrakk>y \<sharp> P; y \<noteq> a; y' \<noteq> a; y' \<sharp> Q; x' \<noteq> x; x' \<sharp> P; y' \<sharp> P; y \<noteq> y'; ([(x, x')] \<bullet> P)[x'::=y] = ([(y, y')] \<bullet> [(x, x')] \<bullet> P)[x'::=y]; y \<sharp> ([(x, x')] \<bullet> P)[x'::=y']; y \<sharp> [(y, y')] \<bullet> Q; y' \<noteq> x'; y \<noteq> x'\<rbrakk> \<Longrightarrow> ([(y, y')] \<bullet> [(x, x')] \<bullet> P)[x'::=y] = P[x::=y]
[PROOF STEP]
by(simp add: name_swap injPermSubst)+
[PROOF STATE]
proof (state)
this:
?y \<sharp> ?P \<and> ?y \<noteq> ?a \<Longrightarrow> {uu_. \<exists>a' x' P' y' Q'. uu_ = \<tau>.(<\<nu>y'>(P'[x'::=y'] \<parallel> Q')) \<and> a'<x'>.P' = ?a<?x>.?P \<and> <\<nu>y'>a'{y'}.Q' = <\<nu>?y>?a{?y}.?Q \<and> y' \<sharp> ?a<?x>.?P} = {\<tau>.(<\<nu>?y>(?P[?x::=?y] \<parallel> ?Q))}

goal (1 subgoal):
 1. finite {\<tau>.(<\<nu>y>(P'[x::=y] \<parallel> Q')) |x P' y Q'. \<exists>a. a<x>.P' \<in> summands P \<and> <\<nu>y>a{y}.Q' \<in> summands Q \<and> y \<sharp> P}
[PROOF STEP]
have BC: "\<And>a x P Q. finite {\<tau>.(<\<nu>y>(P'[x'::=y] \<parallel> Q')) | a' x' P' y Q'. a'<x'>.P' = a<x>.P \<and> <\<nu>y>a'{y}.Q' \<in> summands Q \<and> y \<sharp> a<x>.P}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a x P Q. finite {uu_. \<exists>a' x' P' y Q'. uu_ = \<tau>.(<\<nu>y>(P'[x'::=y] \<parallel> Q')) \<and> a'<x'>.P' = a<x>.P \<and> <\<nu>y>a'{y}.Q' \<in> summands Q \<and> y \<sharp> a<x>.P}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a x P Q. finite {uu_. \<exists>a' x' P' y Q'. uu_ = \<tau>.(<\<nu>y>(P'[x'::=y] \<parallel> Q')) \<and> a'<x'>.P' = a<x>.P \<and> <\<nu>y>a'{y}.Q' \<in> summands Q \<and> y \<sharp> a<x>.P}
[PROOF STEP]
fix a x P Q
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a x P Q. finite {uu_. \<exists>a' x' P' y Q'. uu_ = \<tau>.(<\<nu>y>(P'[x'::=y] \<parallel> Q')) \<and> a'<x'>.P' = a<x>.P \<and> <\<nu>y>a'{y}.Q' \<in> summands Q \<and> y \<sharp> a<x>.P}
[PROOF STEP]
show "finite {\<tau>.(<\<nu>y>(P'[x'::=y] \<parallel> Q')) | a' x' P' y Q'. a'<x'>.P' = a<x>.P \<and> <\<nu>y>a'{y}.Q' \<in> summands Q \<and> y \<sharp> a<x>.P}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {uu_. \<exists>a' x' P' y Q'. uu_ = \<tau>.(<\<nu>y>(P'[x'::=y] \<parallel> Q')) \<and> a'<x'>.P' = a<x>.P \<and> <\<nu>y>a'{y}.Q' \<in> summands Q \<and> y \<sharp> a<x>.P}
[PROOF STEP]
apply(nominal_induct Q avoiding: a P rule: pi.strong_induct, simp_all)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>pi1 pi2 a P. \<lbrakk>\<And>b ba. finite {uu_. \<exists>a' x' P' y Q'. uu_ = \<tau>.(<\<nu>y>(P'[x'::=y] \<parallel> Q')) \<and> a'<x'>.P' = b<x>.ba \<and> <\<nu>y>a'{y}.Q' \<in> summands pi1 \<and> y \<noteq> b \<and> y \<sharp> [x].ba}; \<And>b ba. finite {uu_. \<exists>a' x' P' y Q'. uu_ = \<tau>.(<\<nu>y>(P'[x'::=y] \<parallel> Q')) \<and> a'<x'>.P' = b<x>.ba \<and> <\<nu>y>a'{y}.Q' \<in> summands pi2 \<and> y \<noteq> b \<and> y \<sharp> [x].ba}\<rbrakk> \<Longrightarrow> finite {uu_. \<exists>a' x' P' y Q'. uu_ = \<tau>.(<\<nu>y>(P'[x'::=y] \<parallel> Q')) \<and> a'<x'>.P' = a<x>.P \<and> (<\<nu>y>a'{y}.Q' \<in> summands pi1 \<or> <\<nu>y>a'{y}.Q' \<in> summands pi2) \<and> y \<noteq> a \<and> y \<sharp> [x].P}
 2. \<And>name pi a P. \<lbrakk>name \<noteq> a; name \<sharp> P; \<And>b ba. finite {uu_. \<exists>a' x' P' y Q'. uu_ = \<tau>.(<\<nu>y>(P'[x'::=y] \<parallel> Q')) \<and> a'<x'>.P' = b<x>.ba \<and> <\<nu>y>a'{y}.Q' \<in> summands pi \<and> y \<noteq> b \<and> y \<sharp> [x].ba}\<rbrakk> \<Longrightarrow> (\<exists>a. a \<noteq> name \<and> (\<exists>P'. pi = a{name}.P')) \<longrightarrow> finite {uu_. \<exists>a' x' P' y Q'. uu_ = \<tau>.(<\<nu>y>(P'[x'::=y] \<parallel> Q')) \<and> a'<x'>.P' = a<x>.P \<and> <\<nu>y>a'{y}.Q' = <\<nu>name>pi \<and> y \<noteq> a \<and> y \<sharp> [x].P}
[PROOF STEP]
apply(simp add: Collect_ex_eq conj_disj_distribL conj_disj_distribR
                        Collect_disj_eq UN_Un_distrib)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>name pi a P. \<lbrakk>name \<noteq> a; name \<sharp> P; \<And>b ba. finite {uu_. \<exists>a' x' P' y Q'. uu_ = \<tau>.(<\<nu>y>(P'[x'::=y] \<parallel> Q')) \<and> a'<x'>.P' = b<x>.ba \<and> <\<nu>y>a'{y}.Q' \<in> summands pi \<and> y \<noteq> b \<and> y \<sharp> [x].ba}\<rbrakk> \<Longrightarrow> (\<exists>a. a \<noteq> name \<and> (\<exists>P'. pi = a{name}.P')) \<longrightarrow> finite {uu_. \<exists>a' x' P' y Q'. uu_ = \<tau>.(<\<nu>y>(P'[x'::=y] \<parallel> Q')) \<and> a'<x'>.P' = a<x>.P \<and> <\<nu>y>a'{y}.Q' = <\<nu>name>pi \<and> y \<noteq> a \<and> y \<sharp> [x].P}
[PROOF STEP]
apply(clarsimp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>name a P aa P'. \<lbrakk>name \<noteq> a; name \<sharp> P; aa \<noteq> name\<rbrakk> \<Longrightarrow> finite {uu_. \<exists>a' x' P'a y Q'. uu_ = \<tau>.(<\<nu>y>(P'a[x'::=y] \<parallel> Q')) \<and> a'<x'>.P'a = a<x>.P \<and> <\<nu>y>a'{y}.Q' = <\<nu>name>aa{name}.P' \<and> y \<noteq> a \<and> y \<sharp> [x].P}
[PROOF STEP]
apply(case_tac "a=aa")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>name a P aa P'. \<lbrakk>name \<noteq> a; name \<sharp> P; aa \<noteq> name; a = aa\<rbrakk> \<Longrightarrow> finite {uu_. \<exists>a' x' P'a y Q'. uu_ = \<tau>.(<\<nu>y>(P'a[x'::=y] \<parallel> Q')) \<and> a'<x'>.P'a = a<x>.P \<and> <\<nu>y>a'{y}.Q' = <\<nu>name>aa{name}.P' \<and> y \<noteq> a \<and> y \<sharp> [x].P}
 2. \<And>name a P aa P'. \<lbrakk>name \<noteq> a; name \<sharp> P; aa \<noteq> name; a \<noteq> aa\<rbrakk> \<Longrightarrow> finite {uu_. \<exists>a' x' P'a y Q'. uu_ = \<tau>.(<\<nu>y>(P'a[x'::=y] \<parallel> Q')) \<and> a'<x'>.P'a = a<x>.P \<and> <\<nu>y>a'{y}.Q' = <\<nu>name>aa{name}.P' \<and> y \<noteq> a \<and> y \<sharp> [x].P}
[PROOF STEP]
apply(insert Aux, auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>name a P aa P'. \<lbrakk>name \<noteq> a; name \<sharp> P; aa \<noteq> name; a \<noteq> aa; \<And>y P a x Q. y \<sharp> P \<and> y \<noteq> a \<Longrightarrow> {uu_. \<exists>a' x' P' y' Q'. uu_ = \<tau>.(<\<nu>y'>(P'[x'::=y'] \<parallel> Q')) \<and> a'<x'>.P' = a<x>.P \<and> <\<nu>y'>a'{y'}.Q' = <\<nu>y>a{y}.Q \<and> y' \<noteq> a \<and> y' \<sharp> [x].P} = {\<tau>.(<\<nu>y>(P[x::=y] \<parallel> Q))}\<rbrakk> \<Longrightarrow> finite {uu_. \<exists>a' x' P'a y Q'. uu_ = \<tau>.(<\<nu>y>(P'a[x'::=y] \<parallel> Q')) \<and> a'<x'>.P'a = a<x>.P \<and> <\<nu>y>a'{y}.Q' = <\<nu>name>aa{name}.P' \<and> y \<noteq> a \<and> y \<sharp> [x].P}
[PROOF STEP]
by(simp add: pi.inject name_abs_eq name_calc)
[PROOF STATE]
proof (state)
this:
finite {uu_. \<exists>a' x' P' y Q'. uu_ = \<tau>.(<\<nu>y>(P'[x'::=y] \<parallel> Q')) \<and> a'<x'>.P' = a<x>.P \<and> <\<nu>y>a'{y}.Q' \<in> summands Q \<and> y \<sharp> a<x>.P}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
finite {uu_. \<exists>a' x' P' y Q'. uu_ = \<tau>.(<\<nu>y>(P'[x'::=y] \<parallel> Q')) \<and> a'<x'>.P' = ?a<?x>.?P \<and> <\<nu>y>a'{y}.Q' \<in> summands ?Q \<and> y \<sharp> ?a<?x>.?P}

goal (1 subgoal):
 1. finite {\<tau>.(<\<nu>y>(P'[x::=y] \<parallel> Q')) |x P' y Q'. \<exists>a. a<x>.P' \<in> summands P \<and> <\<nu>y>a{y}.Q' \<in> summands Q \<and> y \<sharp> P}
[PROOF STEP]
have IH: "\<And>P P' Q. {\<tau>.(<\<nu>y>(P''[x::=y] \<parallel> Q')) | a x P'' y Q'. (a<x>.P'' \<in> summands P \<or> a<x>.P'' \<in> summands P') \<and> <\<nu>y>a{y}.Q' \<in> summands Q \<and> y \<sharp> P \<and> y \<sharp> P'} = {\<tau>.(<\<nu>y>(P''[x::=y] \<parallel> Q')) | a x P'' y Q'. a<x>.P'' \<in> summands P \<and> <\<nu>y>a{y}.Q' \<in> summands Q \<and> y \<sharp> P \<and> y \<sharp> P'} \<union> {\<tau>.(<\<nu>y>(P''[x::=y] \<parallel> Q')) | a x P'' y Q'. a<x>.P'' \<in> summands P' \<and> <\<nu>y>a{y}.Q' \<in> summands Q \<and> y \<sharp> P \<and> y \<sharp> P'}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>P P' Q. {uu_. \<exists>a x P'' y Q'. uu_ = \<tau>.(<\<nu>y>(P''[x::=y] \<parallel> Q')) \<and> (a<x>.P'' \<in> summands P \<or> a<x>.P'' \<in> summands P') \<and> <\<nu>y>a{y}.Q' \<in> summands Q \<and> y \<sharp> P \<and> y \<sharp> P'} = {uu_. \<exists>a x P'' y Q'. uu_ = \<tau>.(<\<nu>y>(P''[x::=y] \<parallel> Q')) \<and> a<x>.P'' \<in> summands P \<and> <\<nu>y>a{y}.Q' \<in> summands Q \<and> y \<sharp> P \<and> y \<sharp> P'} \<union> {uu_. \<exists>a x P'' y Q'. uu_ = \<tau>.(<\<nu>y>(P''[x::=y] \<parallel> Q')) \<and> a<x>.P'' \<in> summands P' \<and> <\<nu>y>a{y}.Q' \<in> summands Q \<and> y \<sharp> P \<and> y \<sharp> P'}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
{uu_. \<exists>a x P'' y Q'. uu_ = \<tau>.(<\<nu>y>(P''[x::=y] \<parallel> Q')) \<and> (a<x>.P'' \<in> summands ?P \<or> a<x>.P'' \<in> summands ?P') \<and> <\<nu>y>a{y}.Q' \<in> summands ?Q \<and> y \<sharp> ?P \<and> y \<sharp> ?P'} = {uu_. \<exists>a x P'' y Q'. uu_ = \<tau>.(<\<nu>y>(P''[x::=y] \<parallel> Q')) \<and> a<x>.P'' \<in> summands ?P \<and> <\<nu>y>a{y}.Q' \<in> summands ?Q \<and> y \<sharp> ?P \<and> y \<sharp> ?P'} \<union> {uu_. \<exists>a x P'' y Q'. uu_ = \<tau>.(<\<nu>y>(P''[x::=y] \<parallel> Q')) \<and> a<x>.P'' \<in> summands ?P' \<and> <\<nu>y>a{y}.Q' \<in> summands ?Q \<and> y \<sharp> ?P \<and> y \<sharp> ?P'}

goal (1 subgoal):
 1. finite {\<tau>.(<\<nu>y>(P'[x::=y] \<parallel> Q')) |x P' y Q'. \<exists>a. a<x>.P' \<in> summands P \<and> <\<nu>y>a{y}.Q' \<in> summands Q \<and> y \<sharp> P}
[PROOF STEP]
have IH': "\<And>P Q P'. {\<tau>.(<\<nu>y>(P''[x::=y] \<parallel> Q')) | a x P'' y Q'. a<x>.P'' \<in> summands P \<and> <\<nu>y>a{y}.Q' \<in> summands Q \<and> y \<sharp> P \<and> y \<sharp> P'} \<subseteq> {\<tau>.(<\<nu>y>(P''[x::=y] \<parallel> Q')) | a x P'' y Q'. a<x>.P'' \<in> summands P \<and> <\<nu>y>a{y}.Q' \<in> summands Q \<and> y \<sharp> P}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>P Q P'. {uu_. \<exists>a x P'' y Q'. uu_ = \<tau>.(<\<nu>y>(P''[x::=y] \<parallel> Q')) \<and> a<x>.P'' \<in> summands P \<and> <\<nu>y>a{y}.Q' \<in> summands Q \<and> y \<sharp> P \<and> y \<sharp> P'} \<subseteq> {uu_. \<exists>a x P'' y Q'. uu_ = \<tau>.(<\<nu>y>(P''[x::=y] \<parallel> Q')) \<and> a<x>.P'' \<in> summands P \<and> <\<nu>y>a{y}.Q' \<in> summands Q \<and> y \<sharp> P}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
{uu_. \<exists>a x P'' y Q'. uu_ = \<tau>.(<\<nu>y>(P''[x::=y] \<parallel> Q')) \<and> a<x>.P'' \<in> summands ?P \<and> <\<nu>y>a{y}.Q' \<in> summands ?Q \<and> y \<sharp> ?P \<and> y \<sharp> ?P'} \<subseteq> {uu_. \<exists>a x P'' y Q'. uu_ = \<tau>.(<\<nu>y>(P''[x::=y] \<parallel> Q')) \<and> a<x>.P'' \<in> summands ?P \<and> <\<nu>y>a{y}.Q' \<in> summands ?Q \<and> y \<sharp> ?P}

goal (1 subgoal):
 1. finite {\<tau>.(<\<nu>y>(P'[x::=y] \<parallel> Q')) |x P' y Q'. \<exists>a. a<x>.P' \<in> summands P \<and> <\<nu>y>a{y}.Q' \<in> summands Q \<and> y \<sharp> P}
[PROOF STEP]
have IH'': "\<And>P Q P'. {\<tau>.(<\<nu>y>(P''[x::=y] \<parallel> Q')) | a x P'' y Q'. a<x>.P'' \<in> summands P' \<and> <\<nu>y>a{y}.Q' \<in> summands Q \<and> y \<sharp> P \<and> y \<sharp> P'} \<subseteq> {\<tau>.(<\<nu>y>(P''[x::=y] \<parallel> Q')) | a x P'' y Q'. a<x>.P'' \<in> summands P' \<and> <\<nu>y>a{y}.Q' \<in> summands Q \<and> y \<sharp> P'}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>P Q P'. {uu_. \<exists>a x P'' y Q'. uu_ = \<tau>.(<\<nu>y>(P''[x::=y] \<parallel> Q')) \<and> a<x>.P'' \<in> summands P' \<and> <\<nu>y>a{y}.Q' \<in> summands Q \<and> y \<sharp> P \<and> y \<sharp> P'} \<subseteq> {uu_. \<exists>a x P'' y Q'. uu_ = \<tau>.(<\<nu>y>(P''[x::=y] \<parallel> Q')) \<and> a<x>.P'' \<in> summands P' \<and> <\<nu>y>a{y}.Q' \<in> summands Q \<and> y \<sharp> P'}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
{uu_. \<exists>a x P'' y Q'. uu_ = \<tau>.(<\<nu>y>(P''[x::=y] \<parallel> Q')) \<and> a<x>.P'' \<in> summands ?P'1 \<and> <\<nu>y>a{y}.Q' \<in> summands ?Q1 \<and> y \<sharp> ?P1 \<and> y \<sharp> ?P'1} \<subseteq> {uu_. \<exists>a x P'' y Q'. uu_ = \<tau>.(<\<nu>y>(P''[x::=y] \<parallel> Q')) \<and> a<x>.P'' \<in> summands ?P'1 \<and> <\<nu>y>a{y}.Q' \<in> summands ?Q1 \<and> y \<sharp> ?P'1}

goal (1 subgoal):
 1. finite {\<tau>.(<\<nu>y>(P'[x::=y] \<parallel> Q')) |x P' y Q'. \<exists>a. a<x>.P' \<in> summands P \<and> <\<nu>y>a{y}.Q' \<in> summands Q \<and> y \<sharp> P}
[PROOF STEP]
have "finite {\<tau>.(<\<nu>y>(P'[x::=y] \<parallel> Q')) | a x P' y Q'. a<x>.P' \<in> summands P \<and> <\<nu>y>a{y}.Q' \<in> summands Q \<and> y \<sharp> P}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {uu_. \<exists>a x P' y Q'. uu_ = \<tau>.(<\<nu>y>(P'[x::=y] \<parallel> Q')) \<and> a<x>.P' \<in> summands P \<and> <\<nu>y>a{y}.Q' \<in> summands Q \<and> y \<sharp> P}
[PROOF STEP]
apply(nominal_induct P avoiding: Q rule: pi.strong_induct, simp_all)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>name1 name2 pi Q. \<lbrakk>name2 \<sharp> Q; name2 \<noteq> name1; \<And>b. finite {uu_. \<exists>a x P' y Q'. uu_ = \<tau>.(<\<nu>y>(P'[x::=y] \<parallel> Q')) \<and> a<x>.P' \<in> summands pi \<and> <\<nu>y>a{y}.Q' \<in> summands b \<and> y \<sharp> pi}\<rbrakk> \<Longrightarrow> finite {uu_. \<exists>a x P' y Q'. uu_ = \<tau>.(<\<nu>y>(P'[x::=y] \<parallel> Q')) \<and> a<x>.P' = name1<name2>.pi \<and> <\<nu>y>a{y}.Q' \<in> summands Q \<and> y \<noteq> name1 \<and> y \<sharp> [name2].pi}
 2. \<And>pi1 pi2 Q. \<lbrakk>\<And>b. finite {uu_. \<exists>a x P' y Q'. uu_ = \<tau>.(<\<nu>y>(P'[x::=y] \<parallel> Q')) \<and> a<x>.P' \<in> summands pi1 \<and> <\<nu>y>a{y}.Q' \<in> summands b \<and> y \<sharp> pi1}; \<And>b. finite {uu_. \<exists>a x P' y Q'. uu_ = \<tau>.(<\<nu>y>(P'[x::=y] \<parallel> Q')) \<and> a<x>.P' \<in> summands pi2 \<and> <\<nu>y>a{y}.Q' \<in> summands b \<and> y \<sharp> pi2}\<rbrakk> \<Longrightarrow> finite {uu_. \<exists>a x P' y Q'. uu_ = \<tau>.(<\<nu>y>(P'[x::=y] \<parallel> Q')) \<and> (a<x>.P' \<in> summands pi1 \<or> a<x>.P' \<in> summands pi2) \<and> <\<nu>y>a{y}.Q' \<in> summands Q \<and> y \<sharp> pi1 \<and> y \<sharp> pi2}
[PROOF STEP]
apply(insert BC, force)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>pi1 pi2 Q. \<lbrakk>\<And>b. finite {uu_. \<exists>a x P' y Q'. uu_ = \<tau>.(<\<nu>y>(P'[x::=y] \<parallel> Q')) \<and> a<x>.P' \<in> summands pi1 \<and> <\<nu>y>a{y}.Q' \<in> summands b \<and> y \<sharp> pi1}; \<And>b. finite {uu_. \<exists>a x P' y Q'. uu_ = \<tau>.(<\<nu>y>(P'[x::=y] \<parallel> Q')) \<and> a<x>.P' \<in> summands pi2 \<and> <\<nu>y>a{y}.Q' \<in> summands b \<and> y \<sharp> pi2}; \<And>a x P Q. finite {uu_. \<exists>a' x' P' y Q'. uu_ = \<tau>.(<\<nu>y>(P'[x'::=y] \<parallel> Q')) \<and> a'<x'>.P' = a<x>.P \<and> <\<nu>y>a'{y}.Q' \<in> summands Q \<and> y \<sharp> a<x>.P}\<rbrakk> \<Longrightarrow> finite {uu_. \<exists>a x P' y Q'. uu_ = \<tau>.(<\<nu>y>(P'[x::=y] \<parallel> Q')) \<and> (a<x>.P' \<in> summands pi1 \<or> a<x>.P' \<in> summands pi2) \<and> <\<nu>y>a{y}.Q' \<in> summands Q \<and> y \<sharp> pi1 \<and> y \<sharp> pi2}
[PROOF STEP]
apply(insert IH, auto)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>pi1 pi2 Q. \<lbrakk>\<And>b. finite {uu_. \<exists>a x P' y Q'. uu_ = \<tau>.(<\<nu>y>(P'[x::=y] \<parallel> Q')) \<and> a<x>.P' \<in> summands pi1 \<and> <\<nu>y>a{y}.Q' \<in> summands b \<and> y \<sharp> pi1}; \<And>b. finite {uu_. \<exists>a x P' y Q'. uu_ = \<tau>.(<\<nu>y>(P'[x::=y] \<parallel> Q')) \<and> a<x>.P' \<in> summands pi2 \<and> <\<nu>y>a{y}.Q' \<in> summands b \<and> y \<sharp> pi2}; \<And>a x P Q. finite {uu_. \<exists>a' x' P' y Q'. uu_ = \<tau>.(<\<nu>y>(P'[x'::=y] \<parallel> Q')) \<and> a'<x'>.P' = a<x>.P \<and> <\<nu>y>a'{y}.Q' \<in> summands Q \<and> y \<noteq> a \<and> y \<sharp> [x].P}; \<And>P P' Q. {uu_. \<exists>a x P'' y Q'. uu_ = \<tau>.(<\<nu>y>(P''[x::=y] \<parallel> Q')) \<and> (a<x>.P'' \<in> summands P \<or> a<x>.P'' \<in> summands P') \<and> <\<nu>y>a{y}.Q' \<in> summands Q \<and> y \<sharp> P \<and> y \<sharp> P'} = {uu_. \<exists>a x P'' y Q'. uu_ = \<tau>.(<\<nu>y>(P''[x::=y] \<parallel> Q')) \<and> a<x>.P'' \<in> summands P \<and> <\<nu>y>a{y}.Q' \<in> summands Q \<and> y \<sharp> P \<and> y \<sharp> P'} \<union> {uu_. \<exists>a x P'' y Q'. uu_ = \<tau>.(<\<nu>y>(P''[x::=y] \<parallel> Q')) \<and> a<x>.P'' \<in> summands P' \<and> <\<nu>y>a{y}.Q' \<in> summands Q \<and> y \<sharp> P \<and> y \<sharp> P'}\<rbrakk> \<Longrightarrow> finite {uu_. \<exists>a x P' y Q'. uu_ = \<tau>.(<\<nu>y>(P'[x::=y] \<parallel> Q')) \<and> a<x>.P' \<in> summands pi1 \<and> <\<nu>y>a{y}.Q' \<in> summands Q \<and> y \<sharp> pi1 \<and> y \<sharp> pi2}
 2. \<And>pi1 pi2 Q. \<lbrakk>\<And>b. finite {uu_. \<exists>a x P' y Q'. uu_ = \<tau>.(<\<nu>y>(P'[x::=y] \<parallel> Q')) \<and> a<x>.P' \<in> summands pi1 \<and> <\<nu>y>a{y}.Q' \<in> summands b \<and> y \<sharp> pi1}; \<And>b. finite {uu_. \<exists>a x P' y Q'. uu_ = \<tau>.(<\<nu>y>(P'[x::=y] \<parallel> Q')) \<and> a<x>.P' \<in> summands pi2 \<and> <\<nu>y>a{y}.Q' \<in> summands b \<and> y \<sharp> pi2}; \<And>a x P Q. finite {uu_. \<exists>a' x' P' y Q'. uu_ = \<tau>.(<\<nu>y>(P'[x'::=y] \<parallel> Q')) \<and> a'<x'>.P' = a<x>.P \<and> <\<nu>y>a'{y}.Q' \<in> summands Q \<and> y \<noteq> a \<and> y \<sharp> [x].P}; \<And>P P' Q. {uu_. \<exists>a x P'' y Q'. uu_ = \<tau>.(<\<nu>y>(P''[x::=y] \<parallel> Q')) \<and> (a<x>.P'' \<in> summands P \<or> a<x>.P'' \<in> summands P') \<and> <\<nu>y>a{y}.Q' \<in> summands Q \<and> y \<sharp> P \<and> y \<sharp> P'} = {uu_. \<exists>a x P'' y Q'. uu_ = \<tau>.(<\<nu>y>(P''[x::=y] \<parallel> Q')) \<and> a<x>.P'' \<in> summands P \<and> <\<nu>y>a{y}.Q' \<in> summands Q \<and> y \<sharp> P \<and> y \<sharp> P'} \<union> {uu_. \<exists>a x P'' y Q'. uu_ = \<tau>.(<\<nu>y>(P''[x::=y] \<parallel> Q')) \<and> a<x>.P'' \<in> summands P' \<and> <\<nu>y>a{y}.Q' \<in> summands Q \<and> y \<sharp> P \<and> y \<sharp> P'}\<rbrakk> \<Longrightarrow> finite {uu_. \<exists>a x P' y Q'. uu_ = \<tau>.(<\<nu>y>(P'[x::=y] \<parallel> Q')) \<and> a<x>.P' \<in> summands pi2 \<and> <\<nu>y>a{y}.Q' \<in> summands Q \<and> y \<sharp> pi1 \<and> y \<sharp> pi2}
[PROOF STEP]
apply(blast intro: finite_subset[OF IH'])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>pi1 pi2 Q. \<lbrakk>\<And>b. finite {uu_. \<exists>a x P' y Q'. uu_ = \<tau>.(<\<nu>y>(P'[x::=y] \<parallel> Q')) \<and> a<x>.P' \<in> summands pi1 \<and> <\<nu>y>a{y}.Q' \<in> summands b \<and> y \<sharp> pi1}; \<And>b. finite {uu_. \<exists>a x P' y Q'. uu_ = \<tau>.(<\<nu>y>(P'[x::=y] \<parallel> Q')) \<and> a<x>.P' \<in> summands pi2 \<and> <\<nu>y>a{y}.Q' \<in> summands b \<and> y \<sharp> pi2}; \<And>a x P Q. finite {uu_. \<exists>a' x' P' y Q'. uu_ = \<tau>.(<\<nu>y>(P'[x'::=y] \<parallel> Q')) \<and> a'<x'>.P' = a<x>.P \<and> <\<nu>y>a'{y}.Q' \<in> summands Q \<and> y \<noteq> a \<and> y \<sharp> [x].P}; \<And>P P' Q. {uu_. \<exists>a x P'' y Q'. uu_ = \<tau>.(<\<nu>y>(P''[x::=y] \<parallel> Q')) \<and> (a<x>.P'' \<in> summands P \<or> a<x>.P'' \<in> summands P') \<and> <\<nu>y>a{y}.Q' \<in> summands Q \<and> y \<sharp> P \<and> y \<sharp> P'} = {uu_. \<exists>a x P'' y Q'. uu_ = \<tau>.(<\<nu>y>(P''[x::=y] \<parallel> Q')) \<and> a<x>.P'' \<in> summands P \<and> <\<nu>y>a{y}.Q' \<in> summands Q \<and> y \<sharp> P \<and> y \<sharp> P'} \<union> {uu_. \<exists>a x P'' y Q'. uu_ = \<tau>.(<\<nu>y>(P''[x::=y] \<parallel> Q')) \<and> a<x>.P'' \<in> summands P' \<and> <\<nu>y>a{y}.Q' \<in> summands Q \<and> y \<sharp> P \<and> y \<sharp> P'}\<rbrakk> \<Longrightarrow> finite {uu_. \<exists>a x P' y Q'. uu_ = \<tau>.(<\<nu>y>(P'[x::=y] \<parallel> Q')) \<and> a<x>.P' \<in> summands pi2 \<and> <\<nu>y>a{y}.Q' \<in> summands Q \<and> y \<sharp> pi1 \<and> y \<sharp> pi2}
[PROOF STEP]
by(blast intro: finite_subset[OF IH''])
[PROOF STATE]
proof (state)
this:
finite {uu_. \<exists>a x P' y Q'. uu_ = \<tau>.(<\<nu>y>(P'[x::=y] \<parallel> Q')) \<and> a<x>.P' \<in> summands P \<and> <\<nu>y>a{y}.Q' \<in> summands Q \<and> y \<sharp> P}

goal (1 subgoal):
 1. finite {\<tau>.(<\<nu>y>(P'[x::=y] \<parallel> Q')) |x P' y Q'. \<exists>a. a<x>.P' \<in> summands P \<and> <\<nu>y>a{y}.Q' \<in> summands Q \<and> y \<sharp> P}
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
finite {uu_. \<exists>a x P' y Q'. uu_ = \<tau>.(<\<nu>y>(P'[x::=y] \<parallel> Q')) \<and> a<x>.P' \<in> summands P \<and> <\<nu>y>a{y}.Q' \<in> summands Q \<and> y \<sharp> P}

goal (1 subgoal):
 1. finite {\<tau>.(<\<nu>y>(P'[x::=y] \<parallel> Q')) |x P' y Q'. \<exists>a. a<x>.P' \<in> summands P \<and> <\<nu>y>a{y}.Q' \<in> summands Q \<and> y \<sharp> P}
[PROOF STEP]
apply(rule_tac finite_subset)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. finite {uu_. \<exists>a x P' y Q'. uu_ = \<tau>.(<\<nu>y>(P'[x::=y] \<parallel> Q')) \<and> a<x>.P' \<in> summands P \<and> <\<nu>y>a{y}.Q' \<in> summands Q \<and> y \<sharp> P} \<Longrightarrow> {\<tau>.(<\<nu>y>(P'[x::=y] \<parallel> Q')) |x P' y Q'. \<exists>a. a<x>.P' \<in> summands P \<and> <\<nu>y>a{y}.Q' \<in> summands Q \<and> y \<sharp> P} \<subseteq> ?B1
 2. finite {uu_. \<exists>a x P' y Q'. uu_ = \<tau>.(<\<nu>y>(P'[x::=y] \<parallel> Q')) \<and> a<x>.P' \<in> summands P \<and> <\<nu>y>a{y}.Q' \<in> summands Q \<and> y \<sharp> P} \<Longrightarrow> finite ?B1
[PROOF STEP]
defer
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. finite {uu_. \<exists>a x P' y Q'. uu_ = \<tau>.(<\<nu>y>(P'[x::=y] \<parallel> Q')) \<and> a<x>.P' \<in> summands P \<and> <\<nu>y>a{y}.Q' \<in> summands Q \<and> y \<sharp> P} \<Longrightarrow> finite ?B1
 2. finite {uu_. \<exists>a x P' y Q'. uu_ = \<tau>.(<\<nu>y>(P'[x::=y] \<parallel> Q')) \<and> a<x>.P' \<in> summands P \<and> <\<nu>y>a{y}.Q' \<in> summands Q \<and> y \<sharp> P} \<Longrightarrow> {\<tau>.(<\<nu>y>(P'[x::=y] \<parallel> Q')) |x P' y Q'. \<exists>a. a<x>.P' \<in> summands P \<and> <\<nu>y>a{y}.Q' \<in> summands Q \<and> y \<sharp> P} \<subseteq> ?B1
[PROOF STEP]
by(blast)+
[PROOF STATE]
proof (state)
this:
finite {\<tau>.(<\<nu>y>(P'[x::=y] \<parallel> Q')) |x P' y Q'. \<exists>a. a<x>.P' \<in> summands P \<and> <\<nu>y>a{y}.Q' \<in> summands Q \<and> y \<sharp> P}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
finite {\<tau>.(<\<nu>y>(P'[x::=y] \<parallel> Q')) |x P' y Q'. \<exists>a. a<x>.P' \<in> summands P \<and> <\<nu>y>a{y}.Q' \<in> summands Q \<and> y \<sharp> P}

goal (1 subgoal):
 1. finite (expandSet P Q)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
finite {\<tau>.(<\<nu>y>(P'[x::=y] \<parallel> Q')) |x P' y Q'. \<exists>a. a<x>.P' \<in> summands P \<and> <\<nu>y>a{y}.Q' \<in> summands Q \<and> y \<sharp> P}

goal (1 subgoal):
 1. finite (expandSet P Q)
[PROOF STEP]
have "finite {\<tau>.(<\<nu>y>(P' \<parallel> (Q'[x::=y]))) | y P' x Q'. \<exists>a. <\<nu>y>a{y}.P' \<in> summands P \<and> a<x>.Q' \<in> summands Q \<and> y \<sharp> Q}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {\<tau>.(<\<nu>y>(P' \<parallel> Q'[x::=y])) |y P' x Q'. \<exists>a. <\<nu>y>a{y}.P' \<in> summands P \<and> a<x>.Q' \<in> summands Q \<and> y \<sharp> Q}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. finite {\<tau>.(<\<nu>y>(P' \<parallel> Q'[x::=y])) |y P' x Q'. \<exists>a. <\<nu>y>a{y}.P' \<in> summands P \<and> a<x>.Q' \<in> summands Q \<and> y \<sharp> Q}
[PROOF STEP]
have Aux: "\<And>a y P x Q. \<lbrakk>y \<sharp> Q; y \<noteq> a\<rbrakk> \<Longrightarrow> {\<tau>.(<\<nu>y'>(P' \<parallel> (Q'[x'::=y']))) | a' y' P' x' Q'. <\<nu>y'>a'{y'}.P' = <\<nu>y>a{y}.P \<and> a'<x'>.Q' = a<x>.Q \<and> y' \<sharp> a<x>.Q} = {\<tau>.(<\<nu>y>(P \<parallel> (Q[x::=y])))}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a y P x Q. \<lbrakk>y \<sharp> Q; y \<noteq> a\<rbrakk> \<Longrightarrow> {uu_. \<exists>a' y' P' x' Q'. uu_ = \<tau>.(<\<nu>y'>(P' \<parallel> Q'[x'::=y'])) \<and> <\<nu>y'>a'{y'}.P' = <\<nu>y>a{y}.P \<and> a'<x'>.Q' = a<x>.Q \<and> y' \<sharp> a<x>.Q} = {\<tau>.(<\<nu>y>(P \<parallel> Q[x::=y]))}
[PROOF STEP]
apply(auto simp add: pi.inject name_abs_eq name_fresh_abs name_calc fresh_fact2 fresh_fact1 forget eqvts fresh_left renaming[symmetric])
[PROOF STATE]
proof (prove)
goal (9 subgoals):
 1. \<And>a y P x Q x'. \<lbrakk>y \<sharp> Q; y \<noteq> a; x \<noteq> y; x \<noteq> a; x \<sharp> P; x' \<noteq> x; x' \<sharp> Q\<rbrakk> \<Longrightarrow> ([(x, x')] \<bullet> Q)[x'::=x] = Q
 2. \<And>a y P x Q y' x'. \<lbrakk>y \<sharp> Q; y \<noteq> a; y' \<noteq> y; y' \<noteq> a; y' \<sharp> P; x' \<noteq> x; x' \<sharp> Q; y' \<sharp> Q; y \<noteq> x; y' \<noteq> x\<rbrakk> \<Longrightarrow> ([(x, x')] \<bullet> Q)[x'::=y'] = Q[x::=y']
 3. \<And>a y x Q x'. \<lbrakk>y \<sharp> Q; y \<noteq> a; x' \<noteq> x; x' \<sharp> Q; ([(x, x')] \<bullet> Q)[x'::=y] \<noteq> Q[x::=y]\<rbrakk> \<Longrightarrow> False
 4. \<And>a y P x Q x'. \<lbrakk>y \<sharp> Q; y \<noteq> a; x' \<noteq> x; x' \<sharp> Q; x \<noteq> a; x \<sharp> P; y \<noteq> x; ([(x, x')] \<bullet> Q)[x'::=y] = [(y, x)] \<bullet> Q\<rbrakk> \<Longrightarrow> [(y, x)] \<bullet> Q = Q[x::=y]
 5. \<And>a y P x Q x' x'a. \<lbrakk>y \<sharp> Q; y \<noteq> a; x' \<noteq> x; x' \<sharp> Q; x \<noteq> a; x \<sharp> P; x'a \<noteq> x; x'a \<sharp> Q; y \<noteq> x; ([(x, x')] \<bullet> Q)[x'::=y] = ([(x, x'a)] \<bullet> Q)[x'a::=y]; y \<noteq> x'a\<rbrakk> \<Longrightarrow> ([(x, x'a)] \<bullet> Q)[x'a::=y] = Q[x::=y]
 6. \<And>a P x Q y' x' x'a. \<lbrakk>x' \<noteq> x; x' \<sharp> Q; y' \<noteq> a; y' \<sharp> P; x'a \<noteq> x; x'a \<sharp> Q; y' \<sharp> Q; ([(x, x')] \<bullet> Q)[x'::=y'] = ([(x, x'a)] \<bullet> Q)[x'a::=y']\<rbrakk> \<Longrightarrow> ([(x, x'a)] \<bullet> Q)[x'a::=y'] = Q[x::=y']
 7. \<And>a y P x Q x' x'a. \<lbrakk>y \<sharp> Q; y \<noteq> a; x' \<noteq> x; x' \<sharp> Q; x'a \<noteq> a; x'a \<sharp> P; x'a \<noteq> x; x'a \<sharp> Q; ([(x, x')] \<bullet> Q)[x'::=y] = [(y, x'a)] \<bullet> [(x, x'a)] \<bullet> Q; (if x = y then x'a else if x'a = y then x else y) \<sharp> Q; y \<noteq> x'a\<rbrakk> \<Longrightarrow> [(y, x'a)] \<bullet> [(x, x'a)] \<bullet> Q = Q[x::=y]
 8. \<And>a P x Q y' x' x'a. \<lbrakk>x'a \<noteq> a; x' \<noteq> x; x' \<sharp> Q; y' \<noteq> a; y' \<sharp> P; x'a \<noteq> x; x'a \<sharp> Q; y' \<sharp> Q; ([(x, x')] \<bullet> Q)[x'::=x'a] = [(x, x'a)] \<bullet> Q; y' \<noteq> x'a\<rbrakk> \<Longrightarrow> [(x, x'a)] \<bullet> Q = Q[x::=x'a]
 9. \<And>a y P x Q y' x' x'a. \<lbrakk>y \<sharp> Q; y \<noteq> a; x' \<noteq> x; x' \<sharp> Q; y' \<noteq> a; y' \<sharp> P; x'a \<noteq> x; x'a \<sharp> Q; y' \<sharp> Q; y \<noteq> y'; ([(x, x')] \<bullet> Q)[x'::=y] = ([(x, x'a)] \<bullet> Q)[x'a::=y]; y' \<noteq> x'a; y \<noteq> x'a\<rbrakk> \<Longrightarrow> ([(x, x'a)] \<bullet> Q)[x'a::=y] = Q[x::=y]
[PROOF STEP]
apply(subst name_swap, simp add: injPermSubst fresh_fact1 fresh_fact2)+
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<And>a y x Q x'. \<lbrakk>y \<sharp> Q; y \<noteq> a; x' \<noteq> x; x' \<sharp> Q; ([(x, x')] \<bullet> Q)[x'::=y] \<noteq> Q[x::=y]\<rbrakk> \<Longrightarrow> False
 2. \<And>a y P x Q x'. \<lbrakk>y \<sharp> Q; y \<noteq> a; x' \<noteq> x; x' \<sharp> Q; x \<noteq> a; x \<sharp> P; y \<noteq> x; ([(x, x')] \<bullet> Q)[x'::=y] = [(y, x)] \<bullet> Q\<rbrakk> \<Longrightarrow> [(y, x)] \<bullet> Q = Q[x::=y]
 3. \<And>a y P x Q x' x'a. \<lbrakk>y \<sharp> Q; y \<noteq> a; x' \<noteq> x; x' \<sharp> Q; x \<noteq> a; x \<sharp> P; x'a \<noteq> x; x'a \<sharp> Q; y \<noteq> x; ([(x, x')] \<bullet> Q)[x'::=y] = ([(x, x'a)] \<bullet> Q)[x'a::=y]; y \<noteq> x'a\<rbrakk> \<Longrightarrow> ([(x, x'a)] \<bullet> Q)[x'a::=y] = Q[x::=y]
 4. \<And>a P x Q y' x' x'a. \<lbrakk>x' \<noteq> x; x' \<sharp> Q; y' \<noteq> a; y' \<sharp> P; x'a \<noteq> x; x'a \<sharp> Q; y' \<sharp> Q; ([(x, x')] \<bullet> Q)[x'::=y'] = ([(x, x'a)] \<bullet> Q)[x'a::=y']\<rbrakk> \<Longrightarrow> ([(x, x'a)] \<bullet> Q)[x'a::=y'] = Q[x::=y']
 5. \<And>a y P x Q x' x'a. \<lbrakk>y \<sharp> Q; y \<noteq> a; x' \<noteq> x; x' \<sharp> Q; x'a \<noteq> a; x'a \<sharp> P; x'a \<noteq> x; x'a \<sharp> Q; ([(x, x')] \<bullet> Q)[x'::=y] = [(y, x'a)] \<bullet> [(x, x'a)] \<bullet> Q; (if x = y then x'a else if x'a = y then x else y) \<sharp> Q; y \<noteq> x'a\<rbrakk> \<Longrightarrow> [(y, x'a)] \<bullet> [(x, x'a)] \<bullet> Q = Q[x::=y]
 6. \<And>a P x Q y' x' x'a. \<lbrakk>x'a \<noteq> a; x' \<noteq> x; x' \<sharp> Q; y' \<noteq> a; y' \<sharp> P; x'a \<noteq> x; x'a \<sharp> Q; y' \<sharp> Q; ([(x, x')] \<bullet> Q)[x'::=x'a] = [(x, x'a)] \<bullet> Q; y' \<noteq> x'a\<rbrakk> \<Longrightarrow> [(x, x'a)] \<bullet> Q = Q[x::=x'a]
 7. \<And>a y P x Q y' x' x'a. \<lbrakk>y \<sharp> Q; y \<noteq> a; x' \<noteq> x; x' \<sharp> Q; y' \<noteq> a; y' \<sharp> P; x'a \<noteq> x; x'a \<sharp> Q; y' \<sharp> Q; y \<noteq> y'; ([(x, x')] \<bullet> Q)[x'::=y] = ([(x, x'a)] \<bullet> Q)[x'a::=y]; y' \<noteq> x'a; y \<noteq> x'a\<rbrakk> \<Longrightarrow> ([(x, x'a)] \<bullet> Q)[x'a::=y] = Q[x::=y]
[PROOF STEP]
by(simp add: name_swap injPermSubst)+
[PROOF STATE]
proof (state)
this:
\<lbrakk>?y \<sharp> ?Q; ?y \<noteq> ?a\<rbrakk> \<Longrightarrow> {uu_. \<exists>a' y' P' x' Q'. uu_ = \<tau>.(<\<nu>y'>(P' \<parallel> Q'[x'::=y'])) \<and> <\<nu>y'>a'{y'}.P' = <\<nu>?y>?a{?y}.?P \<and> a'<x'>.Q' = ?a<?x>.?Q \<and> y' \<sharp> ?a<?x>.?Q} = {\<tau>.(<\<nu>?y>(?P \<parallel> ?Q[?x::=?y]))}

goal (1 subgoal):
 1. finite {\<tau>.(<\<nu>y>(P' \<parallel> Q'[x::=y])) |y P' x Q'. \<exists>a. <\<nu>y>a{y}.P' \<in> summands P \<and> a<x>.Q' \<in> summands Q \<and> y \<sharp> Q}
[PROOF STEP]
have IH: "\<And>P y a Q Q'. {\<tau>.(<\<nu>y'>(P' \<parallel> (Q''[x::=y']))) | a' y' P' x Q''. <\<nu>y'>a'{y'}.P' = <\<nu>y>a{y}.P \<and> (a'<x>.Q'' \<in> summands Q \<or> a'<x>.Q'' \<in> summands Q') \<and> y' \<sharp> Q \<and> y' \<sharp> Q'} = {\<tau>.(<\<nu>y'>(P' \<parallel> (Q''[x::=y']))) | a' y' P' x Q''. <\<nu>y'>a'{y'}.P' = <\<nu>y>a{y}.P \<and> a'<x>.Q'' \<in> summands Q \<and> y' \<sharp> Q \<and> y' \<sharp> Q'} \<union> {\<tau>.(<\<nu>y'>(P' \<parallel> (Q''[x::=y']))) | a' y' P' x Q''. <\<nu>y'>a'{y'}.P' = <\<nu>y>a{y}.P \<and> a'<x>.Q'' \<in> summands Q' \<and> y' \<sharp> Q \<and> y' \<sharp> Q'}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>P y a Q Q'. {uu_. \<exists>a' y' P' x Q''. uu_ = \<tau>.(<\<nu>y'>(P' \<parallel> Q''[x::=y'])) \<and> <\<nu>y'>a'{y'}.P' = <\<nu>y>a{y}.P \<and> (a'<x>.Q'' \<in> summands Q \<or> a'<x>.Q'' \<in> summands Q') \<and> y' \<sharp> Q \<and> y' \<sharp> Q'} = {uu_. \<exists>a' y' P' x Q''. uu_ = \<tau>.(<\<nu>y'>(P' \<parallel> Q''[x::=y'])) \<and> <\<nu>y'>a'{y'}.P' = <\<nu>y>a{y}.P \<and> a'<x>.Q'' \<in> summands Q \<and> y' \<sharp> Q \<and> y' \<sharp> Q'} \<union> {uu_. \<exists>a' y' P' x Q''. uu_ = \<tau>.(<\<nu>y'>(P' \<parallel> Q''[x::=y'])) \<and> <\<nu>y'>a'{y'}.P' = <\<nu>y>a{y}.P \<and> a'<x>.Q'' \<in> summands Q' \<and> y' \<sharp> Q \<and> y' \<sharp> Q'}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
{uu_. \<exists>a' y' P' x Q''. uu_ = \<tau>.(<\<nu>y'>(P' \<parallel> Q''[x::=y'])) \<and> <\<nu>y'>a'{y'}.P' = <\<nu>?y>?a{?y}.?P \<and> (a'<x>.Q'' \<in> summands ?Q \<or> a'<x>.Q'' \<in> summands ?Q') \<and> y' \<sharp> ?Q \<and> y' \<sharp> ?Q'} = {uu_. \<exists>a' y' P' x Q''. uu_ = \<tau>.(<\<nu>y'>(P' \<parallel> Q''[x::=y'])) \<and> <\<nu>y'>a'{y'}.P' = <\<nu>?y>?a{?y}.?P \<and> a'<x>.Q'' \<in> summands ?Q \<and> y' \<sharp> ?Q \<and> y' \<sharp> ?Q'} \<union> {uu_. \<exists>a' y' P' x Q''. uu_ = \<tau>.(<\<nu>y'>(P' \<parallel> Q''[x::=y'])) \<and> <\<nu>y'>a'{y'}.P' = <\<nu>?y>?a{?y}.?P \<and> a'<x>.Q'' \<in> summands ?Q' \<and> y' \<sharp> ?Q \<and> y' \<sharp> ?Q'}

goal (1 subgoal):
 1. finite {\<tau>.(<\<nu>y>(P' \<parallel> Q'[x::=y])) |y P' x Q'. \<exists>a. <\<nu>y>a{y}.P' \<in> summands P \<and> a<x>.Q' \<in> summands Q \<and> y \<sharp> Q}
[PROOF STEP]
have IH': "\<And>a y P Q Q'. {\<tau>.(<\<nu>y'>(P' \<parallel> (Q''[x::=y']))) | a' y' P' x Q''. <\<nu>y'>a'{y'}.P' = <\<nu>y>a{y}.P \<and> a'<x>.Q'' \<in> summands Q \<and> y' \<sharp> Q \<and> y' \<sharp> Q'} \<subseteq> {\<tau>.(<\<nu>y'>(P' \<parallel> (Q''[x::=y']))) | a' y' P' x Q''. <\<nu>y'>a'{y'}.P' = <\<nu>y>a{y}.P \<and> a'<x>.Q'' \<in> summands Q \<and> y' \<sharp> Q}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a y P Q Q'. {uu_. \<exists>a' y' P' x Q''. uu_ = \<tau>.(<\<nu>y'>(P' \<parallel> Q''[x::=y'])) \<and> <\<nu>y'>a'{y'}.P' = <\<nu>y>a{y}.P \<and> a'<x>.Q'' \<in> summands Q \<and> y' \<sharp> Q \<and> y' \<sharp> Q'} \<subseteq> {uu_. \<exists>a' y' P' x Q''. uu_ = \<tau>.(<\<nu>y'>(P' \<parallel> Q''[x::=y'])) \<and> <\<nu>y'>a'{y'}.P' = <\<nu>y>a{y}.P \<and> a'<x>.Q'' \<in> summands Q \<and> y' \<sharp> Q}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
{uu_. \<exists>a' y' P' x Q''. uu_ = \<tau>.(<\<nu>y'>(P' \<parallel> Q''[x::=y'])) \<and> <\<nu>y'>a'{y'}.P' = <\<nu>?y>?a{?y}.?P \<and> a'<x>.Q'' \<in> summands ?Q \<and> y' \<sharp> ?Q \<and> y' \<sharp> ?Q'} \<subseteq> {uu_. \<exists>a' y' P' x Q''. uu_ = \<tau>.(<\<nu>y'>(P' \<parallel> Q''[x::=y'])) \<and> <\<nu>y'>a'{y'}.P' = <\<nu>?y>?a{?y}.?P \<and> a'<x>.Q'' \<in> summands ?Q \<and> y' \<sharp> ?Q}

goal (1 subgoal):
 1. finite {\<tau>.(<\<nu>y>(P' \<parallel> Q'[x::=y])) |y P' x Q'. \<exists>a. <\<nu>y>a{y}.P' \<in> summands P \<and> a<x>.Q' \<in> summands Q \<and> y \<sharp> Q}
[PROOF STEP]
have IH'': "\<And>a y P Q Q'. {\<tau>.(<\<nu>y'>(P' \<parallel> (Q''[x::=y']))) | a' y' P' x Q''. <\<nu>y'>a'{y'}.P' = <\<nu>y>a{y}.P \<and> a'<x>.Q'' \<in> summands Q' \<and> y' \<sharp> Q \<and> y' \<sharp> Q'} \<subseteq> {\<tau>.(<\<nu>y'>(P' \<parallel> (Q''[x::=y']))) | a' y' P' x Q''. <\<nu>y'>a'{y'}.P' = <\<nu>y>a{y}.P \<and> a'<x>.Q'' \<in> summands Q' \<and> y' \<sharp> Q'}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a y P Q Q'. {uu_. \<exists>a' y' P' x Q''. uu_ = \<tau>.(<\<nu>y'>(P' \<parallel> Q''[x::=y'])) \<and> <\<nu>y'>a'{y'}.P' = <\<nu>y>a{y}.P \<and> a'<x>.Q'' \<in> summands Q' \<and> y' \<sharp> Q \<and> y' \<sharp> Q'} \<subseteq> {uu_. \<exists>a' y' P' x Q''. uu_ = \<tau>.(<\<nu>y'>(P' \<parallel> Q''[x::=y'])) \<and> <\<nu>y'>a'{y'}.P' = <\<nu>y>a{y}.P \<and> a'<x>.Q'' \<in> summands Q' \<and> y' \<sharp> Q'}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
{uu_. \<exists>a' y' P' x Q''. uu_ = \<tau>.(<\<nu>y'>(P' \<parallel> Q''[x::=y'])) \<and> <\<nu>y'>a'{y'}.P' = <\<nu>?y1>?a1{?y1}.?P1 \<and> a'<x>.Q'' \<in> summands ?Q'1 \<and> y' \<sharp> ?Q1 \<and> y' \<sharp> ?Q'1} \<subseteq> {uu_. \<exists>a' y' P' x Q''. uu_ = \<tau>.(<\<nu>y'>(P' \<parallel> Q''[x::=y'])) \<and> <\<nu>y'>a'{y'}.P' = <\<nu>?y1>?a1{?y1}.?P1 \<and> a'<x>.Q'' \<in> summands ?Q'1 \<and> y' \<sharp> ?Q'1}

goal (1 subgoal):
 1. finite {\<tau>.(<\<nu>y>(P' \<parallel> Q'[x::=y])) |y P' x Q'. \<exists>a. <\<nu>y>a{y}.P' \<in> summands P \<and> a<x>.Q' \<in> summands Q \<and> y \<sharp> Q}
[PROOF STEP]
have BC: "\<And>a y P Q. \<lbrakk>y \<sharp> Q; y \<noteq> a\<rbrakk> \<Longrightarrow> finite {\<tau>.(<\<nu>y'>(P' \<parallel> (Q'[x::=y']))) | a' y' P' x Q'. <\<nu>y'>a'{y'}.P' = <\<nu>y>a{y}.P \<and> a'<x>.Q' \<in> summands Q \<and> y' \<sharp> Q}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a y P Q. \<lbrakk>y \<sharp> Q; y \<noteq> a\<rbrakk> \<Longrightarrow> finite {uu_. \<exists>a' y' P' x Q'. uu_ = \<tau>.(<\<nu>y'>(P' \<parallel> Q'[x::=y'])) \<and> <\<nu>y'>a'{y'}.P' = <\<nu>y>a{y}.P \<and> a'<x>.Q' \<in> summands Q \<and> y' \<sharp> Q}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a y P Q. \<lbrakk>y \<sharp> Q; y \<noteq> a\<rbrakk> \<Longrightarrow> finite {uu_. \<exists>a' y' P' x Q'. uu_ = \<tau>.(<\<nu>y'>(P' \<parallel> Q'[x::=y'])) \<and> <\<nu>y'>a'{y'}.P' = <\<nu>y>a{y}.P \<and> a'<x>.Q' \<in> summands Q \<and> y' \<sharp> Q}
[PROOF STEP]
fix a y P Q
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a y P Q. \<lbrakk>y \<sharp> Q; y \<noteq> a\<rbrakk> \<Longrightarrow> finite {uu_. \<exists>a' y' P' x Q'. uu_ = \<tau>.(<\<nu>y'>(P' \<parallel> Q'[x::=y'])) \<and> <\<nu>y'>a'{y'}.P' = <\<nu>y>a{y}.P \<and> a'<x>.Q' \<in> summands Q \<and> y' \<sharp> Q}
[PROOF STEP]
assume "(y::name) \<sharp> (Q::pi)" and "y \<noteq> a"
[PROOF STATE]
proof (state)
this:
y \<sharp> Q
y \<noteq> a

goal (1 subgoal):
 1. \<And>a y P Q. \<lbrakk>y \<sharp> Q; y \<noteq> a\<rbrakk> \<Longrightarrow> finite {uu_. \<exists>a' y' P' x Q'. uu_ = \<tau>.(<\<nu>y'>(P' \<parallel> Q'[x::=y'])) \<and> <\<nu>y'>a'{y'}.P' = <\<nu>y>a{y}.P \<and> a'<x>.Q' \<in> summands Q \<and> y' \<sharp> Q}
[PROOF STEP]
thus "finite {\<tau>.(<\<nu>y'>(P' \<parallel> (Q'[x::=y']))) | a' y' P' x Q'. <\<nu>y'>a'{y'}.P' = <\<nu>y>a{y}.P \<and> a'<x>.Q' \<in> summands Q \<and> y' \<sharp> Q}"
[PROOF STATE]
proof (prove)
using this:
y \<sharp> Q
y \<noteq> a

goal (1 subgoal):
 1. finite {uu_. \<exists>a' y' P' x Q'. uu_ = \<tau>.(<\<nu>y'>(P' \<parallel> Q'[x::=y'])) \<and> <\<nu>y'>a'{y'}.P' = <\<nu>y>a{y}.P \<and> a'<x>.Q' \<in> summands Q \<and> y' \<sharp> Q}
[PROOF STEP]
apply(nominal_induct Q avoiding: y rule: pi.strong_induct, simp_all)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>name1 name2 pi ya. \<lbrakk>name2 \<noteq> ya; name2 \<noteq> name1; \<And>b. \<lbrakk>b \<sharp> pi; b \<noteq> a\<rbrakk> \<Longrightarrow> finite {uu_. \<exists>a' y' P' x Q'. uu_ = \<tau>.(<\<nu>y'>(P' \<parallel> Q'[x::=y'])) \<and> <\<nu>y'>a'{y'}.P' = <\<nu>b>a{b}.P \<and> a'<x>.Q' \<in> summands pi \<and> y' \<sharp> pi}; ya \<noteq> name1 \<and> ya \<sharp> [name2].pi; ya \<noteq> a; y \<sharp> Q; y \<noteq> a\<rbrakk> \<Longrightarrow> finite {uu_. \<exists>a' y' P' x Q'. uu_ = \<tau>.(<\<nu>y'>(P' \<parallel> Q'[x::=y'])) \<and> <\<nu>y'>a'{y'}.P' = <\<nu>ya>a{ya}.P \<and> a'<x>.Q' = name1<name2>.pi \<and> y' \<noteq> name1 \<and> y' \<sharp> [name2].pi}
 2. \<And>pi1 pi2 ya. \<lbrakk>\<And>b. \<lbrakk>b \<sharp> pi1; b \<noteq> a\<rbrakk> \<Longrightarrow> finite {uu_. \<exists>a' y' P' x Q'. uu_ = \<tau>.(<\<nu>y'>(P' \<parallel> Q'[x::=y'])) \<and> <\<nu>y'>a'{y'}.P' = <\<nu>b>a{b}.P \<and> a'<x>.Q' \<in> summands pi1 \<and> y' \<sharp> pi1}; \<And>b. \<lbrakk>b \<sharp> pi2; b \<noteq> a\<rbrakk> \<Longrightarrow> finite {uu_. \<exists>a' y' P' x Q'. uu_ = \<tau>.(<\<nu>y'>(P' \<parallel> Q'[x::=y'])) \<and> <\<nu>y'>a'{y'}.P' = <\<nu>b>a{b}.P \<and> a'<x>.Q' \<in> summands pi2 \<and> y' \<sharp> pi2}; ya \<sharp> pi1 \<and> ya \<sharp> pi2; ya \<noteq> a; y \<sharp> Q; y \<noteq> a\<rbrakk> \<Longrightarrow> finite {uu_. \<exists>a' y' P' x Q'. uu_ = \<tau>.(<\<nu>y'>(P' \<parallel> Q'[x::=y'])) \<and> <\<nu>y'>a'{y'}.P' = <\<nu>ya>a{ya}.P \<and> (a'<x>.Q' \<in> summands pi1 \<or> a'<x>.Q' \<in> summands pi2) \<and> y' \<sharp> pi1 \<and> y' \<sharp> pi2}
[PROOF STEP]
apply(case_tac "a=name1")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>name1 name2 pi ya. \<lbrakk>name2 \<noteq> ya; name2 \<noteq> name1; \<And>b. \<lbrakk>b \<sharp> pi; b \<noteq> a\<rbrakk> \<Longrightarrow> finite {uu_. \<exists>a' y' P' x Q'. uu_ = \<tau>.(<\<nu>y'>(P' \<parallel> Q'[x::=y'])) \<and> <\<nu>y'>a'{y'}.P' = <\<nu>b>a{b}.P \<and> a'<x>.Q' \<in> summands pi \<and> y' \<sharp> pi}; ya \<noteq> name1 \<and> ya \<sharp> [name2].pi; ya \<noteq> a; y \<sharp> Q; y \<noteq> a; a = name1\<rbrakk> \<Longrightarrow> finite {uu_. \<exists>a' y' P' x Q'. uu_ = \<tau>.(<\<nu>y'>(P' \<parallel> Q'[x::=y'])) \<and> <\<nu>y'>a'{y'}.P' = <\<nu>ya>a{ya}.P \<and> a'<x>.Q' = name1<name2>.pi \<and> y' \<noteq> name1 \<and> y' \<sharp> [name2].pi}
 2. \<And>name1 name2 pi ya. \<lbrakk>name2 \<noteq> ya; name2 \<noteq> name1; \<And>b. \<lbrakk>b \<sharp> pi; b \<noteq> a\<rbrakk> \<Longrightarrow> finite {uu_. \<exists>a' y' P' x Q'. uu_ = \<tau>.(<\<nu>y'>(P' \<parallel> Q'[x::=y'])) \<and> <\<nu>y'>a'{y'}.P' = <\<nu>b>a{b}.P \<and> a'<x>.Q' \<in> summands pi \<and> y' \<sharp> pi}; ya \<noteq> name1 \<and> ya \<sharp> [name2].pi; ya \<noteq> a; y \<sharp> Q; y \<noteq> a; a \<noteq> name1\<rbrakk> \<Longrightarrow> finite {uu_. \<exists>a' y' P' x Q'. uu_ = \<tau>.(<\<nu>y'>(P' \<parallel> Q'[x::=y'])) \<and> <\<nu>y'>a'{y'}.P' = <\<nu>ya>a{ya}.P \<and> a'<x>.Q' = name1<name2>.pi \<and> y' \<noteq> name1 \<and> y' \<sharp> [name2].pi}
 3. \<And>pi1 pi2 ya. \<lbrakk>\<And>b. \<lbrakk>b \<sharp> pi1; b \<noteq> a\<rbrakk> \<Longrightarrow> finite {uu_. \<exists>a' y' P' x Q'. uu_ = \<tau>.(<\<nu>y'>(P' \<parallel> Q'[x::=y'])) \<and> <\<nu>y'>a'{y'}.P' = <\<nu>b>a{b}.P \<and> a'<x>.Q' \<in> summands pi1 \<and> y' \<sharp> pi1}; \<And>b. \<lbrakk>b \<sharp> pi2; b \<noteq> a\<rbrakk> \<Longrightarrow> finite {uu_. \<exists>a' y' P' x Q'. uu_ = \<tau>.(<\<nu>y'>(P' \<parallel> Q'[x::=y'])) \<and> <\<nu>y'>a'{y'}.P' = <\<nu>b>a{b}.P \<and> a'<x>.Q' \<in> summands pi2 \<and> y' \<sharp> pi2}; ya \<sharp> pi1 \<and> ya \<sharp> pi2; ya \<noteq> a; y \<sharp> Q; y \<noteq> a\<rbrakk> \<Longrightarrow> finite {uu_. \<exists>a' y' P' x Q'. uu_ = \<tau>.(<\<nu>y'>(P' \<parallel> Q'[x::=y'])) \<and> <\<nu>y'>a'{y'}.P' = <\<nu>ya>a{ya}.P \<and> (a'<x>.Q' \<in> summands pi1 \<or> a'<x>.Q' \<in> summands pi2) \<and> y' \<sharp> pi1 \<and> y' \<sharp> pi2}
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>name2 pi ya. \<lbrakk>name2 \<noteq> ya; name2 \<noteq> a; \<And>b. \<lbrakk>b \<sharp> pi; b \<noteq> a\<rbrakk> \<Longrightarrow> finite {uu_. \<exists>a' y' P' x Q'. uu_ = \<tau>.(<\<nu>y'>(P' \<parallel> Q'[x::=y'])) \<and> <\<nu>y'>a'{y'}.P' = <\<nu>b>a{b}.P \<and> a'<x>.Q' \<in> summands pi \<and> y' \<sharp> pi}; y \<sharp> Q; y \<noteq> a; ya \<noteq> a; ya \<sharp> [name2].pi\<rbrakk> \<Longrightarrow> finite {uu_. \<exists>a' y' P' x Q'. uu_ = \<tau>.(<\<nu>y'>(P' \<parallel> Q'[x::=y'])) \<and> <\<nu>y'>a'{y'}.P' = <\<nu>ya>a{ya}.P \<and> a'<x>.Q' = a<name2>.pi \<and> y' \<noteq> a \<and> y' \<sharp> [name2].pi}
 2. \<And>name1 name2 pi ya. \<lbrakk>name2 \<noteq> ya; name2 \<noteq> name1; \<And>b. \<lbrakk>b \<sharp> pi; b \<noteq> a\<rbrakk> \<Longrightarrow> finite {uu_. \<exists>a' y' P' x Q'. uu_ = \<tau>.(<\<nu>y'>(P' \<parallel> Q'[x::=y'])) \<and> <\<nu>y'>a'{y'}.P' = <\<nu>b>a{b}.P \<and> a'<x>.Q' \<in> summands pi \<and> y' \<sharp> pi}; ya \<noteq> a; y \<sharp> Q; y \<noteq> a; a \<noteq> name1; ya \<noteq> name1; ya \<sharp> [name2].pi\<rbrakk> \<Longrightarrow> finite {uu_. \<exists>a' y' P' x Q'. uu_ = \<tau>.(<\<nu>y'>(P' \<parallel> Q'[x::=y'])) \<and> <\<nu>y'>a'{y'}.P' = <\<nu>ya>a{ya}.P \<and> a'<x>.Q' = name1<name2>.pi \<and> y' \<noteq> name1 \<and> y' \<sharp> [name2].pi}
 3. \<And>pi1 pi2 ya. \<lbrakk>\<And>b. \<lbrakk>b \<sharp> pi1; b \<noteq> a\<rbrakk> \<Longrightarrow> finite {uu_. \<exists>a' y' P' x Q'. uu_ = \<tau>.(<\<nu>y'>(P' \<parallel> Q'[x::=y'])) \<and> <\<nu>y'>a'{y'}.P' = <\<nu>b>a{b}.P \<and> a'<x>.Q' \<in> summands pi1 \<and> y' \<sharp> pi1}; \<And>b. \<lbrakk>b \<sharp> pi2; b \<noteq> a\<rbrakk> \<Longrightarrow> finite {uu_. \<exists>a' y' P' x Q'. uu_ = \<tau>.(<\<nu>y'>(P' \<parallel> Q'[x::=y'])) \<and> <\<nu>y'>a'{y'}.P' = <\<nu>b>a{b}.P \<and> a'<x>.Q' \<in> summands pi2 \<and> y' \<sharp> pi2}; ya \<noteq> a; y \<sharp> Q; y \<noteq> a; ya \<sharp> pi1; ya \<sharp> pi2\<rbrakk> \<Longrightarrow> finite {uu_. \<exists>a' y' P' x Q'. uu_ = \<tau>.(<\<nu>y'>(P' \<parallel> Q'[x::=y'])) \<and> <\<nu>y'>a'{y'}.P' = <\<nu>ya>a{ya}.P \<and> (a'<x>.Q' \<in> summands pi1 \<or> a'<x>.Q' \<in> summands pi2) \<and> y' \<sharp> pi1 \<and> y' \<sharp> pi2}
[PROOF STEP]
apply(subgoal_tac "ya \<sharp> (pi::pi)")
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>name2 pi ya. \<lbrakk>name2 \<noteq> ya; name2 \<noteq> a; \<And>b. \<lbrakk>b \<sharp> pi; b \<noteq> a\<rbrakk> \<Longrightarrow> finite {uu_. \<exists>a' y' P' x Q'. uu_ = \<tau>.(<\<nu>y'>(P' \<parallel> Q'[x::=y'])) \<and> <\<nu>y'>a'{y'}.P' = <\<nu>b>a{b}.P \<and> a'<x>.Q' \<in> summands pi \<and> y' \<sharp> pi}; y \<sharp> Q; y \<noteq> a; ya \<noteq> a; ya \<sharp> [name2].pi; ya \<sharp> pi\<rbrakk> \<Longrightarrow> finite {uu_. \<exists>a' y' P' x Q'. uu_ = \<tau>.(<\<nu>y'>(P' \<parallel> Q'[x::=y'])) \<and> <\<nu>y'>a'{y'}.P' = <\<nu>ya>a{ya}.P \<and> a'<x>.Q' = a<name2>.pi \<and> y' \<noteq> a \<and> y' \<sharp> [name2].pi}
 2. \<And>name2 pi ya. \<lbrakk>name2 \<noteq> ya; name2 \<noteq> a; \<And>b. \<lbrakk>b \<sharp> pi; b \<noteq> a\<rbrakk> \<Longrightarrow> finite {uu_. \<exists>a' y' P' x Q'. uu_ = \<tau>.(<\<nu>y'>(P' \<parallel> Q'[x::=y'])) \<and> <\<nu>y'>a'{y'}.P' = <\<nu>b>a{b}.P \<and> a'<x>.Q' \<in> summands pi \<and> y' \<sharp> pi}; y \<sharp> Q; y \<noteq> a; ya \<noteq> a; ya \<sharp> [name2].pi\<rbrakk> \<Longrightarrow> ya \<sharp> pi
 3. \<And>name1 name2 pi ya. \<lbrakk>name2 \<noteq> ya; name2 \<noteq> name1; \<And>b. \<lbrakk>b \<sharp> pi; b \<noteq> a\<rbrakk> \<Longrightarrow> finite {uu_. \<exists>a' y' P' x Q'. uu_ = \<tau>.(<\<nu>y'>(P' \<parallel> Q'[x::=y'])) \<and> <\<nu>y'>a'{y'}.P' = <\<nu>b>a{b}.P \<and> a'<x>.Q' \<in> summands pi \<and> y' \<sharp> pi}; ya \<noteq> a; y \<sharp> Q; y \<noteq> a; a \<noteq> name1; ya \<noteq> name1; ya \<sharp> [name2].pi\<rbrakk> \<Longrightarrow> finite {uu_. \<exists>a' y' P' x Q'. uu_ = \<tau>.(<\<nu>y'>(P' \<parallel> Q'[x::=y'])) \<and> <\<nu>y'>a'{y'}.P' = <\<nu>ya>a{ya}.P \<and> a'<x>.Q' = name1<name2>.pi \<and> y' \<noteq> name1 \<and> y' \<sharp> [name2].pi}
 4. \<And>pi1 pi2 ya. \<lbrakk>\<And>b. \<lbrakk>b \<sharp> pi1; b \<noteq> a\<rbrakk> \<Longrightarrow> finite {uu_. \<exists>a' y' P' x Q'. uu_ = \<tau>.(<\<nu>y'>(P' \<parallel> Q'[x::=y'])) \<and> <\<nu>y'>a'{y'}.P' = <\<nu>b>a{b}.P \<and> a'<x>.Q' \<in> summands pi1 \<and> y' \<sharp> pi1}; \<And>b. \<lbrakk>b \<sharp> pi2; b \<noteq> a\<rbrakk> \<Longrightarrow> finite {uu_. \<exists>a' y' P' x Q'. uu_ = \<tau>.(<\<nu>y'>(P' \<parallel> Q'[x::=y'])) \<and> <\<nu>y'>a'{y'}.P' = <\<nu>b>a{b}.P \<and> a'<x>.Q' \<in> summands pi2 \<and> y' \<sharp> pi2}; ya \<noteq> a; y \<sharp> Q; y \<noteq> a; ya \<sharp> pi1; ya \<sharp> pi2\<rbrakk> \<Longrightarrow> finite {uu_. \<exists>a' y' P' x Q'. uu_ = \<tau>.(<\<nu>y'>(P' \<parallel> Q'[x::=y'])) \<and> <\<nu>y'>a'{y'}.P' = <\<nu>ya>a{ya}.P \<and> (a'<x>.Q' \<in> summands pi1 \<or> a'<x>.Q' \<in> summands pi2) \<and> y' \<sharp> pi1 \<and> y' \<sharp> pi2}
[PROOF STEP]
apply(insert Aux)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>name2 pi ya. \<lbrakk>name2 \<noteq> ya; name2 \<noteq> a; \<And>b. \<lbrakk>b \<sharp> pi; b \<noteq> a\<rbrakk> \<Longrightarrow> finite {uu_. \<exists>a' y' P' x Q'. uu_ = \<tau>.(<\<nu>y'>(P' \<parallel> Q'[x::=y'])) \<and> <\<nu>y'>a'{y'}.P' = <\<nu>b>a{b}.P \<and> a'<x>.Q' \<in> summands pi \<and> y' \<sharp> pi}; y \<sharp> Q; y \<noteq> a; ya \<noteq> a; ya \<sharp> [name2].pi; ya \<sharp> pi; \<And>y Q a P x. \<lbrakk>y \<sharp> Q; y \<noteq> a\<rbrakk> \<Longrightarrow> {uu_. \<exists>a' y' P' x' Q'. uu_ = \<tau>.(<\<nu>y'>(P' \<parallel> Q'[x'::=y'])) \<and> <\<nu>y'>a'{y'}.P' = <\<nu>y>a{y}.P \<and> a'<x'>.Q' = a<x>.Q \<and> y' \<sharp> a<x>.Q} = {\<tau>.(<\<nu>y>(P \<parallel> Q[x::=y]))}\<rbrakk> \<Longrightarrow> finite {uu_. \<exists>a' y' P' x Q'. uu_ = \<tau>.(<\<nu>y'>(P' \<parallel> Q'[x::=y'])) \<and> <\<nu>y'>a'{y'}.P' = <\<nu>ya>a{ya}.P \<and> a'<x>.Q' = a<name2>.pi \<and> y' \<noteq> a \<and> y' \<sharp> [name2].pi}
 2. \<And>name2 pi ya. \<lbrakk>name2 \<noteq> ya; name2 \<noteq> a; \<And>b. \<lbrakk>b \<sharp> pi; b \<noteq> a\<rbrakk> \<Longrightarrow> finite {uu_. \<exists>a' y' P' x Q'. uu_ = \<tau>.(<\<nu>y'>(P' \<parallel> Q'[x::=y'])) \<and> <\<nu>y'>a'{y'}.P' = <\<nu>b>a{b}.P \<and> a'<x>.Q' \<in> summands pi \<and> y' \<sharp> pi}; y \<sharp> Q; y \<noteq> a; ya \<noteq> a; ya \<sharp> [name2].pi; \<And>y Q a P x. \<lbrakk>y \<sharp> Q; y \<noteq> a\<rbrakk> \<Longrightarrow> {uu_. \<exists>a' y' P' x' Q'. uu_ = \<tau>.(<\<nu>y'>(P' \<parallel> Q'[x'::=y'])) \<and> <\<nu>y'>a'{y'}.P' = <\<nu>y>a{y}.P \<and> a'<x'>.Q' = a<x>.Q \<and> y' \<sharp> a<x>.Q} = {\<tau>.(<\<nu>y>(P \<parallel> Q[x::=y]))}\<rbrakk> \<Longrightarrow> ya \<sharp> pi
 3. \<And>name1 name2 pi ya. \<lbrakk>name2 \<noteq> ya; name2 \<noteq> name1; \<And>b. \<lbrakk>b \<sharp> pi; b \<noteq> a\<rbrakk> \<Longrightarrow> finite {uu_. \<exists>a' y' P' x Q'. uu_ = \<tau>.(<\<nu>y'>(P' \<parallel> Q'[x::=y'])) \<and> <\<nu>y'>a'{y'}.P' = <\<nu>b>a{b}.P \<and> a'<x>.Q' \<in> summands pi \<and> y' \<sharp> pi}; ya \<noteq> a; y \<sharp> Q; y \<noteq> a; a \<noteq> name1; ya \<noteq> name1; ya \<sharp> [name2].pi; \<And>y Q a P x. \<lbrakk>y \<sharp> Q; y \<noteq> a\<rbrakk> \<Longrightarrow> {uu_. \<exists>a' y' P' x' Q'. uu_ = \<tau>.(<\<nu>y'>(P' \<parallel> Q'[x'::=y'])) \<and> <\<nu>y'>a'{y'}.P' = <\<nu>y>a{y}.P \<and> a'<x'>.Q' = a<x>.Q \<and> y' \<sharp> a<x>.Q} = {\<tau>.(<\<nu>y>(P \<parallel> Q[x::=y]))}\<rbrakk> \<Longrightarrow> finite {uu_. \<exists>a' y' P' x Q'. uu_ = \<tau>.(<\<nu>y'>(P' \<parallel> Q'[x::=y'])) \<and> <\<nu>y'>a'{y'}.P' = <\<nu>ya>a{ya}.P \<and> a'<x>.Q' = name1<name2>.pi \<and> y' \<noteq> name1 \<and> y' \<sharp> [name2].pi}
 4. \<And>pi1 pi2 ya. \<lbrakk>\<And>b. \<lbrakk>b \<sharp> pi1; b \<noteq> a\<rbrakk> \<Longrightarrow> finite {uu_. \<exists>a' y' P' x Q'. uu_ = \<tau>.(<\<nu>y'>(P' \<parallel> Q'[x::=y'])) \<and> <\<nu>y'>a'{y'}.P' = <\<nu>b>a{b}.P \<and> a'<x>.Q' \<in> summands pi1 \<and> y' \<sharp> pi1}; \<And>b. \<lbrakk>b \<sharp> pi2; b \<noteq> a\<rbrakk> \<Longrightarrow> finite {uu_. \<exists>a' y' P' x Q'. uu_ = \<tau>.(<\<nu>y'>(P' \<parallel> Q'[x::=y'])) \<and> <\<nu>y'>a'{y'}.P' = <\<nu>b>a{b}.P \<and> a'<x>.Q' \<in> summands pi2 \<and> y' \<sharp> pi2}; ya \<noteq> a; y \<sharp> Q; y \<noteq> a; ya \<sharp> pi1; ya \<sharp> pi2; \<And>y Q a P x. \<lbrakk>y \<sharp> Q; y \<noteq> a\<rbrakk> \<Longrightarrow> {uu_. \<exists>a' y' P' x' Q'. uu_ = \<tau>.(<\<nu>y'>(P' \<parallel> Q'[x'::=y'])) \<and> <\<nu>y'>a'{y'}.P' = <\<nu>y>a{y}.P \<and> a'<x'>.Q' = a<x>.Q \<and> y' \<sharp> a<x>.Q} = {\<tau>.(<\<nu>y>(P \<parallel> Q[x::=y]))}\<rbrakk> \<Longrightarrow> finite {uu_. \<exists>a' y' P' x Q'. uu_ = \<tau>.(<\<nu>y'>(P' \<parallel> Q'[x::=y'])) \<and> <\<nu>y'>a'{y'}.P' = <\<nu>ya>a{ya}.P \<and> (a'<x>.Q' \<in> summands pi1 \<or> a'<x>.Q' \<in> summands pi2) \<and> y' \<sharp> pi1 \<and> y' \<sharp> pi2}
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>name2 pi ya. \<lbrakk>name2 \<noteq> ya; name2 \<noteq> a; \<And>b. \<lbrakk>b \<sharp> pi; b \<noteq> a\<rbrakk> \<Longrightarrow> finite {uu_. \<exists>a' y' P' x Q'. uu_ = \<tau>.(<\<nu>y'>(P' \<parallel> Q'[x::=y'])) \<and> <\<nu>y'>a'{y'}.P' = <\<nu>b>a{b}.P \<and> a'<x>.Q' \<in> summands pi \<and> y' \<sharp> pi}; y \<sharp> Q; y \<noteq> a; ya \<noteq> a; ya \<sharp> [name2].pi; \<And>y Q a P x. \<lbrakk>y \<sharp> Q; y \<noteq> a\<rbrakk> \<Longrightarrow> {uu_. \<exists>a' y' P' x' Q'. uu_ = \<tau>.(<\<nu>y'>(P' \<parallel> Q'[x'::=y'])) \<and> <\<nu>y'>a'{y'}.P' = <\<nu>y>a{y}.P \<and> a'<x'>.Q' = a<x>.Q \<and> y' \<noteq> a \<and> y' \<sharp> [x].Q} = {\<tau>.(<\<nu>y>(P \<parallel> Q[x::=y]))}\<rbrakk> \<Longrightarrow> ya \<sharp> pi
 2. \<And>name1 name2 pi ya. \<lbrakk>name2 \<noteq> ya; name2 \<noteq> name1; \<And>b. \<lbrakk>b \<sharp> pi; b \<noteq> a\<rbrakk> \<Longrightarrow> finite {uu_. \<exists>a' y' P' x Q'. uu_ = \<tau>.(<\<nu>y'>(P' \<parallel> Q'[x::=y'])) \<and> <\<nu>y'>a'{y'}.P' = <\<nu>b>a{b}.P \<and> a'<x>.Q' \<in> summands pi \<and> y' \<sharp> pi}; ya \<noteq> a; y \<sharp> Q; y \<noteq> a; a \<noteq> name1; ya \<noteq> name1; ya \<sharp> [name2].pi; \<And>y Q a P x. \<lbrakk>y \<sharp> Q; y \<noteq> a\<rbrakk> \<Longrightarrow> {uu_. \<exists>a' y' P' x' Q'. uu_ = \<tau>.(<\<nu>y'>(P' \<parallel> Q'[x'::=y'])) \<and> <\<nu>y'>a'{y'}.P' = <\<nu>y>a{y}.P \<and> a'<x'>.Q' = a<x>.Q \<and> y' \<noteq> a \<and> y' \<sharp> [x].Q} = {\<tau>.(<\<nu>y>(P \<parallel> Q[x::=y]))}\<rbrakk> \<Longrightarrow> finite {uu_. \<exists>a' y' P' x Q'. uu_ = \<tau>.(<\<nu>y'>(P' \<parallel> Q'[x::=y'])) \<and> <\<nu>y'>a'{y'}.P' = <\<nu>ya>a{ya}.P \<and> a'<x>.Q' = name1<name2>.pi \<and> y' \<noteq> name1 \<and> y' \<sharp> [name2].pi}
 3. \<And>pi1 pi2 ya. \<lbrakk>\<And>b. \<lbrakk>b \<sharp> pi1; b \<noteq> a\<rbrakk> \<Longrightarrow> finite {uu_. \<exists>a' y' P' x Q'. uu_ = \<tau>.(<\<nu>y'>(P' \<parallel> Q'[x::=y'])) \<and> <\<nu>y'>a'{y'}.P' = <\<nu>b>a{b}.P \<and> a'<x>.Q' \<in> summands pi1 \<and> y' \<sharp> pi1}; \<And>b. \<lbrakk>b \<sharp> pi2; b \<noteq> a\<rbrakk> \<Longrightarrow> finite {uu_. \<exists>a' y' P' x Q'. uu_ = \<tau>.(<\<nu>y'>(P' \<parallel> Q'[x::=y'])) \<and> <\<nu>y'>a'{y'}.P' = <\<nu>b>a{b}.P \<and> a'<x>.Q' \<in> summands pi2 \<and> y' \<sharp> pi2}; ya \<noteq> a; y \<sharp> Q; y \<noteq> a; ya \<sharp> pi1; ya \<sharp> pi2; \<And>y Q a P x. \<lbrakk>y \<sharp> Q; y \<noteq> a\<rbrakk> \<Longrightarrow> {uu_. \<exists>a' y' P' x' Q'. uu_ = \<tau>.(<\<nu>y'>(P' \<parallel> Q'[x'::=y'])) \<and> <\<nu>y'>a'{y'}.P' = <\<nu>y>a{y}.P \<and> a'<x'>.Q' = a<x>.Q \<and> y' \<noteq> a \<and> y' \<sharp> [x].Q} = {\<tau>.(<\<nu>y>(P \<parallel> Q[x::=y]))}\<rbrakk> \<Longrightarrow> finite {uu_. \<exists>a' y' P' x Q'. uu_ = \<tau>.(<\<nu>y'>(P' \<parallel> Q'[x::=y'])) \<and> <\<nu>y'>a'{y'}.P' = <\<nu>ya>a{ya}.P \<and> (a'<x>.Q' \<in> summands pi1 \<or> a'<x>.Q' \<in> summands pi2) \<and> y' \<sharp> pi1 \<and> y' \<sharp> pi2}
[PROOF STEP]
apply(simp add: name_fresh_abs)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>name1 name2 pi ya. \<lbrakk>name2 \<noteq> ya; name2 \<noteq> name1; \<And>b. \<lbrakk>b \<sharp> pi; b \<noteq> a\<rbrakk> \<Longrightarrow> finite {uu_. \<exists>a' y' P' x Q'. uu_ = \<tau>.(<\<nu>y'>(P' \<parallel> Q'[x::=y'])) \<and> <\<nu>y'>a'{y'}.P' = <\<nu>b>a{b}.P \<and> a'<x>.Q' \<in> summands pi \<and> y' \<sharp> pi}; ya \<noteq> a; y \<sharp> Q; y \<noteq> a; a \<noteq> name1; ya \<noteq> name1; ya \<sharp> [name2].pi; \<And>y Q a P x. \<lbrakk>y \<sharp> Q; y \<noteq> a\<rbrakk> \<Longrightarrow> {uu_. \<exists>a' y' P' x' Q'. uu_ = \<tau>.(<\<nu>y'>(P' \<parallel> Q'[x'::=y'])) \<and> <\<nu>y'>a'{y'}.P' = <\<nu>y>a{y}.P \<and> a'<x'>.Q' = a<x>.Q \<and> y' \<noteq> a \<and> y' \<sharp> [x].Q} = {\<tau>.(<\<nu>y>(P \<parallel> Q[x::=y]))}\<rbrakk> \<Longrightarrow> finite {uu_. \<exists>a' y' P' x Q'. uu_ = \<tau>.(<\<nu>y'>(P' \<parallel> Q'[x::=y'])) \<and> <\<nu>y'>a'{y'}.P' = <\<nu>ya>a{ya}.P \<and> a'<x>.Q' = name1<name2>.pi \<and> y' \<noteq> name1 \<and> y' \<sharp> [name2].pi}
 2. \<And>pi1 pi2 ya. \<lbrakk>\<And>b. \<lbrakk>b \<sharp> pi1; b \<noteq> a\<rbrakk> \<Longrightarrow> finite {uu_. \<exists>a' y' P' x Q'. uu_ = \<tau>.(<\<nu>y'>(P' \<parallel> Q'[x::=y'])) \<and> <\<nu>y'>a'{y'}.P' = <\<nu>b>a{b}.P \<and> a'<x>.Q' \<in> summands pi1 \<and> y' \<sharp> pi1}; \<And>b. \<lbrakk>b \<sharp> pi2; b \<noteq> a\<rbrakk> \<Longrightarrow> finite {uu_. \<exists>a' y' P' x Q'. uu_ = \<tau>.(<\<nu>y'>(P' \<parallel> Q'[x::=y'])) \<and> <\<nu>y'>a'{y'}.P' = <\<nu>b>a{b}.P \<and> a'<x>.Q' \<in> summands pi2 \<and> y' \<sharp> pi2}; ya \<noteq> a; y \<sharp> Q; y \<noteq> a; ya \<sharp> pi1; ya \<sharp> pi2; \<And>y Q a P x. \<lbrakk>y \<sharp> Q; y \<noteq> a\<rbrakk> \<Longrightarrow> {uu_. \<exists>a' y' P' x' Q'. uu_ = \<tau>.(<\<nu>y'>(P' \<parallel> Q'[x'::=y'])) \<and> <\<nu>y'>a'{y'}.P' = <\<nu>y>a{y}.P \<and> a'<x'>.Q' = a<x>.Q \<and> y' \<noteq> a \<and> y' \<sharp> [x].Q} = {\<tau>.(<\<nu>y>(P \<parallel> Q[x::=y]))}\<rbrakk> \<Longrightarrow> finite {uu_. \<exists>a' y' P' x Q'. uu_ = \<tau>.(<\<nu>y'>(P' \<parallel> Q'[x::=y'])) \<and> <\<nu>y'>a'{y'}.P' = <\<nu>ya>a{ya}.P \<and> (a'<x>.Q' \<in> summands pi1 \<or> a'<x>.Q' \<in> summands pi2) \<and> y' \<sharp> pi1 \<and> y' \<sharp> pi2}
[PROOF STEP]
apply(simp add: pi.inject name_abs_eq name_calc)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>pi1 pi2 ya. \<lbrakk>\<And>b. \<lbrakk>b \<sharp> pi1; b \<noteq> a\<rbrakk> \<Longrightarrow> finite {uu_. \<exists>a' y' P' x Q'. uu_ = \<tau>.(<\<nu>y'>(P' \<parallel> Q'[x::=y'])) \<and> <\<nu>y'>a'{y'}.P' = <\<nu>b>a{b}.P \<and> a'<x>.Q' \<in> summands pi1 \<and> y' \<sharp> pi1}; \<And>b. \<lbrakk>b \<sharp> pi2; b \<noteq> a\<rbrakk> \<Longrightarrow> finite {uu_. \<exists>a' y' P' x Q'. uu_ = \<tau>.(<\<nu>y'>(P' \<parallel> Q'[x::=y'])) \<and> <\<nu>y'>a'{y'}.P' = <\<nu>b>a{b}.P \<and> a'<x>.Q' \<in> summands pi2 \<and> y' \<sharp> pi2}; ya \<noteq> a; y \<sharp> Q; y \<noteq> a; ya \<sharp> pi1; ya \<sharp> pi2; \<And>y Q a P x. \<lbrakk>y \<sharp> Q; y \<noteq> a\<rbrakk> \<Longrightarrow> {uu_. \<exists>a' y' P' x' Q'. uu_ = \<tau>.(<\<nu>y'>(P' \<parallel> Q'[x'::=y'])) \<and> <\<nu>y'>a'{y'}.P' = <\<nu>y>a{y}.P \<and> a'<x'>.Q' = a<x>.Q \<and> y' \<noteq> a \<and> y' \<sharp> [x].Q} = {\<tau>.(<\<nu>y>(P \<parallel> Q[x::=y]))}\<rbrakk> \<Longrightarrow> finite {uu_. \<exists>a' y' P' x Q'. uu_ = \<tau>.(<\<nu>y'>(P' \<parallel> Q'[x::=y'])) \<and> <\<nu>y'>a'{y'}.P' = <\<nu>ya>a{ya}.P \<and> (a'<x>.Q' \<in> summands pi1 \<or> a'<x>.Q' \<in> summands pi2) \<and> y' \<sharp> pi1 \<and> y' \<sharp> pi2}
[PROOF STEP]
apply(insert IH)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>pi1 pi2 ya. \<lbrakk>\<And>b. \<lbrakk>b \<sharp> pi1; b \<noteq> a\<rbrakk> \<Longrightarrow> finite {uu_. \<exists>a' y' P' x Q'. uu_ = \<tau>.(<\<nu>y'>(P' \<parallel> Q'[x::=y'])) \<and> <\<nu>y'>a'{y'}.P' = <\<nu>b>a{b}.P \<and> a'<x>.Q' \<in> summands pi1 \<and> y' \<sharp> pi1}; \<And>b. \<lbrakk>b \<sharp> pi2; b \<noteq> a\<rbrakk> \<Longrightarrow> finite {uu_. \<exists>a' y' P' x Q'. uu_ = \<tau>.(<\<nu>y'>(P' \<parallel> Q'[x::=y'])) \<and> <\<nu>y'>a'{y'}.P' = <\<nu>b>a{b}.P \<and> a'<x>.Q' \<in> summands pi2 \<and> y' \<sharp> pi2}; ya \<noteq> a; y \<sharp> Q; y \<noteq> a; ya \<sharp> pi1; ya \<sharp> pi2; \<And>y Q a P x. \<lbrakk>y \<sharp> Q; y \<noteq> a\<rbrakk> \<Longrightarrow> {uu_. \<exists>a' y' P' x' Q'. uu_ = \<tau>.(<\<nu>y'>(P' \<parallel> Q'[x'::=y'])) \<and> <\<nu>y'>a'{y'}.P' = <\<nu>y>a{y}.P \<and> a'<x'>.Q' = a<x>.Q \<and> y' \<noteq> a \<and> y' \<sharp> [x].Q} = {\<tau>.(<\<nu>y>(P \<parallel> Q[x::=y]))}; \<And>y a P Q Q'. {uu_. \<exists>a' y' P' x Q''. uu_ = \<tau>.(<\<nu>y'>(P' \<parallel> Q''[x::=y'])) \<and> <\<nu>y'>a'{y'}.P' = <\<nu>y>a{y}.P \<and> (a'<x>.Q'' \<in> summands Q \<or> a'<x>.Q'' \<in> summands Q') \<and> y' \<sharp> Q \<and> y' \<sharp> Q'} = {uu_. \<exists>a' y' P' x Q''. uu_ = \<tau>.(<\<nu>y'>(P' \<parallel> Q''[x::=y'])) \<and> <\<nu>y'>a'{y'}.P' = <\<nu>y>a{y}.P \<and> a'<x>.Q'' \<in> summands Q \<and> y' \<sharp> Q \<and> y' \<sharp> Q'} \<union> {uu_. \<exists>a' y' P' x Q''. uu_ = \<tau>.(<\<nu>y'>(P' \<parallel> Q''[x::=y'])) \<and> <\<nu>y'>a'{y'}.P' = <\<nu>y>a{y}.P \<and> a'<x>.Q'' \<in> summands Q' \<and> y' \<sharp> Q \<and> y' \<sharp> Q'}\<rbrakk> \<Longrightarrow> finite {uu_. \<exists>a' y' P' x Q'. uu_ = \<tau>.(<\<nu>y'>(P' \<parallel> Q'[x::=y'])) \<and> <\<nu>y'>a'{y'}.P' = <\<nu>ya>a{ya}.P \<and> (a'<x>.Q' \<in> summands pi1 \<or> a'<x>.Q' \<in> summands pi2) \<and> y' \<sharp> pi1 \<and> y' \<sharp> pi2}
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>pi1 pi2 ya. \<lbrakk>\<And>b. \<lbrakk>b \<sharp> pi1; b \<noteq> a\<rbrakk> \<Longrightarrow> finite {uu_. \<exists>a' y' P' x Q'. uu_ = \<tau>.(<\<nu>y'>(P' \<parallel> Q'[x::=y'])) \<and> <\<nu>y'>a'{y'}.P' = <\<nu>b>a{b}.P \<and> a'<x>.Q' \<in> summands pi1 \<and> y' \<sharp> pi1}; \<And>b. \<lbrakk>b \<sharp> pi2; b \<noteq> a\<rbrakk> \<Longrightarrow> finite {uu_. \<exists>a' y' P' x Q'. uu_ = \<tau>.(<\<nu>y'>(P' \<parallel> Q'[x::=y'])) \<and> <\<nu>y'>a'{y'}.P' = <\<nu>b>a{b}.P \<and> a'<x>.Q' \<in> summands pi2 \<and> y' \<sharp> pi2}; ya \<noteq> a; y \<sharp> Q; y \<noteq> a; ya \<sharp> pi1; ya \<sharp> pi2; \<And>y Q a P x. \<lbrakk>y \<sharp> Q; y \<noteq> a\<rbrakk> \<Longrightarrow> {uu_. \<exists>a' y' P' x' Q'. uu_ = \<tau>.(<\<nu>y'>(P' \<parallel> Q'[x'::=y'])) \<and> <\<nu>y'>a'{y'}.P' = <\<nu>y>a{y}.P \<and> a'<x'>.Q' = a<x>.Q \<and> y' \<noteq> a \<and> y' \<sharp> [x].Q} = {\<tau>.(<\<nu>y>(P \<parallel> Q[x::=y]))}; \<And>y a P Q Q'. {uu_. \<exists>a' y' P' x Q''. uu_ = \<tau>.(<\<nu>y'>(P' \<parallel> Q''[x::=y'])) \<and> <\<nu>y'>a'{y'}.P' = <\<nu>y>a{y}.P \<and> (a'<x>.Q'' \<in> summands Q \<or> a'<x>.Q'' \<in> summands Q') \<and> y' \<sharp> Q \<and> y' \<sharp> Q'} = {uu_. \<exists>a' y' P' x Q''. uu_ = \<tau>.(<\<nu>y'>(P' \<parallel> Q''[x::=y'])) \<and> <\<nu>y'>a'{y'}.P' = <\<nu>y>a{y}.P \<and> a'<x>.Q'' \<in> summands Q \<and> y' \<sharp> Q \<and> y' \<sharp> Q'} \<union> {uu_. \<exists>a' y' P' x Q''. uu_ = \<tau>.(<\<nu>y'>(P' \<parallel> Q''[x::=y'])) \<and> <\<nu>y'>a'{y'}.P' = <\<nu>y>a{y}.P \<and> a'<x>.Q'' \<in> summands Q' \<and> y' \<sharp> Q \<and> y' \<sharp> Q'}\<rbrakk> \<Longrightarrow> finite {uu_. \<exists>a' y' P' x Q'. uu_ = \<tau>.(<\<nu>y'>(P' \<parallel> Q'[x::=y'])) \<and> <\<nu>y'>a'{y'}.P' = <\<nu>ya>a{ya}.P \<and> a'<x>.Q' \<in> summands pi1 \<and> y' \<sharp> pi1 \<and> y' \<sharp> pi2}
 2. \<And>pi1 pi2 ya. \<lbrakk>\<And>b. \<lbrakk>b \<sharp> pi1; b \<noteq> a\<rbrakk> \<Longrightarrow> finite {uu_. \<exists>a' y' P' x Q'. uu_ = \<tau>.(<\<nu>y'>(P' \<parallel> Q'[x::=y'])) \<and> <\<nu>y'>a'{y'}.P' = <\<nu>b>a{b}.P \<and> a'<x>.Q' \<in> summands pi1 \<and> y' \<sharp> pi1}; \<And>b. \<lbrakk>b \<sharp> pi2; b \<noteq> a\<rbrakk> \<Longrightarrow> finite {uu_. \<exists>a' y' P' x Q'. uu_ = \<tau>.(<\<nu>y'>(P' \<parallel> Q'[x::=y'])) \<and> <\<nu>y'>a'{y'}.P' = <\<nu>b>a{b}.P \<and> a'<x>.Q' \<in> summands pi2 \<and> y' \<sharp> pi2}; ya \<noteq> a; y \<sharp> Q; y \<noteq> a; ya \<sharp> pi1; ya \<sharp> pi2; \<And>y Q a P x. \<lbrakk>y \<sharp> Q; y \<noteq> a\<rbrakk> \<Longrightarrow> {uu_. \<exists>a' y' P' x' Q'. uu_ = \<tau>.(<\<nu>y'>(P' \<parallel> Q'[x'::=y'])) \<and> <\<nu>y'>a'{y'}.P' = <\<nu>y>a{y}.P \<and> a'<x'>.Q' = a<x>.Q \<and> y' \<noteq> a \<and> y' \<sharp> [x].Q} = {\<tau>.(<\<nu>y>(P \<parallel> Q[x::=y]))}; \<And>y a P Q Q'. {uu_. \<exists>a' y' P' x Q''. uu_ = \<tau>.(<\<nu>y'>(P' \<parallel> Q''[x::=y'])) \<and> <\<nu>y'>a'{y'}.P' = <\<nu>y>a{y}.P \<and> (a'<x>.Q'' \<in> summands Q \<or> a'<x>.Q'' \<in> summands Q') \<and> y' \<sharp> Q \<and> y' \<sharp> Q'} = {uu_. \<exists>a' y' P' x Q''. uu_ = \<tau>.(<\<nu>y'>(P' \<parallel> Q''[x::=y'])) \<and> <\<nu>y'>a'{y'}.P' = <\<nu>y>a{y}.P \<and> a'<x>.Q'' \<in> summands Q \<and> y' \<sharp> Q \<and> y' \<sharp> Q'} \<union> {uu_. \<exists>a' y' P' x Q''. uu_ = \<tau>.(<\<nu>y'>(P' \<parallel> Q''[x::=y'])) \<and> <\<nu>y'>a'{y'}.P' = <\<nu>y>a{y}.P \<and> a'<x>.Q'' \<in> summands Q' \<and> y' \<sharp> Q \<and> y' \<sharp> Q'}\<rbrakk> \<Longrightarrow> finite {uu_. \<exists>a' y' P' x Q'. uu_ = \<tau>.(<\<nu>y'>(P' \<parallel> Q'[x::=y'])) \<and> <\<nu>y'>a'{y'}.P' = <\<nu>ya>a{ya}.P \<and> a'<x>.Q' \<in> summands pi2 \<and> y' \<sharp> pi1 \<and> y' \<sharp> pi2}
[PROOF STEP]
apply(blast intro: finite_subset[OF IH'])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>pi1 pi2 ya. \<lbrakk>\<And>b. \<lbrakk>b \<sharp> pi1; b \<noteq> a\<rbrakk> \<Longrightarrow> finite {uu_. \<exists>a' y' P' x Q'. uu_ = \<tau>.(<\<nu>y'>(P' \<parallel> Q'[x::=y'])) \<and> <\<nu>y'>a'{y'}.P' = <\<nu>b>a{b}.P \<and> a'<x>.Q' \<in> summands pi1 \<and> y' \<sharp> pi1}; \<And>b. \<lbrakk>b \<sharp> pi2; b \<noteq> a\<rbrakk> \<Longrightarrow> finite {uu_. \<exists>a' y' P' x Q'. uu_ = \<tau>.(<\<nu>y'>(P' \<parallel> Q'[x::=y'])) \<and> <\<nu>y'>a'{y'}.P' = <\<nu>b>a{b}.P \<and> a'<x>.Q' \<in> summands pi2 \<and> y' \<sharp> pi2}; ya \<noteq> a; y \<sharp> Q; y \<noteq> a; ya \<sharp> pi1; ya \<sharp> pi2; \<And>y Q a P x. \<lbrakk>y \<sharp> Q; y \<noteq> a\<rbrakk> \<Longrightarrow> {uu_. \<exists>a' y' P' x' Q'. uu_ = \<tau>.(<\<nu>y'>(P' \<parallel> Q'[x'::=y'])) \<and> <\<nu>y'>a'{y'}.P' = <\<nu>y>a{y}.P \<and> a'<x'>.Q' = a<x>.Q \<and> y' \<noteq> a \<and> y' \<sharp> [x].Q} = {\<tau>.(<\<nu>y>(P \<parallel> Q[x::=y]))}; \<And>y a P Q Q'. {uu_. \<exists>a' y' P' x Q''. uu_ = \<tau>.(<\<nu>y'>(P' \<parallel> Q''[x::=y'])) \<and> <\<nu>y'>a'{y'}.P' = <\<nu>y>a{y}.P \<and> (a'<x>.Q'' \<in> summands Q \<or> a'<x>.Q'' \<in> summands Q') \<and> y' \<sharp> Q \<and> y' \<sharp> Q'} = {uu_. \<exists>a' y' P' x Q''. uu_ = \<tau>.(<\<nu>y'>(P' \<parallel> Q''[x::=y'])) \<and> <\<nu>y'>a'{y'}.P' = <\<nu>y>a{y}.P \<and> a'<x>.Q'' \<in> summands Q \<and> y' \<sharp> Q \<and> y' \<sharp> Q'} \<union> {uu_. \<exists>a' y' P' x Q''. uu_ = \<tau>.(<\<nu>y'>(P' \<parallel> Q''[x::=y'])) \<and> <\<nu>y'>a'{y'}.P' = <\<nu>y>a{y}.P \<and> a'<x>.Q'' \<in> summands Q' \<and> y' \<sharp> Q \<and> y' \<sharp> Q'}\<rbrakk> \<Longrightarrow> finite {uu_. \<exists>a' y' P' x Q'. uu_ = \<tau>.(<\<nu>y'>(P' \<parallel> Q'[x::=y'])) \<and> <\<nu>y'>a'{y'}.P' = <\<nu>ya>a{ya}.P \<and> a'<x>.Q' \<in> summands pi2 \<and> y' \<sharp> pi1 \<and> y' \<sharp> pi2}
[PROOF STEP]
by(blast intro: finite_subset[OF IH''])
[PROOF STATE]
proof (state)
this:
finite {uu_. \<exists>a' y' P' x Q'. uu_ = \<tau>.(<\<nu>y'>(P' \<parallel> Q'[x::=y'])) \<and> <\<nu>y'>a'{y'}.P' = <\<nu>y>a{y}.P \<and> a'<x>.Q' \<in> summands Q \<and> y' \<sharp> Q}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>?y2 \<sharp> ?Q2; ?y2 \<noteq> ?a2\<rbrakk> \<Longrightarrow> finite {uu_. \<exists>a' y' P' x Q'. uu_ = \<tau>.(<\<nu>y'>(P' \<parallel> Q'[x::=y'])) \<and> <\<nu>y'>a'{y'}.P' = <\<nu>?y2>?a2{?y2}.?P2 \<and> a'<x>.Q' \<in> summands ?Q2 \<and> y' \<sharp> ?Q2}

goal (1 subgoal):
 1. finite {\<tau>.(<\<nu>y>(P' \<parallel> Q'[x::=y])) |y P' x Q'. \<exists>a. <\<nu>y>a{y}.P' \<in> summands P \<and> a<x>.Q' \<in> summands Q \<and> y \<sharp> Q}
[PROOF STEP]
have "finite {\<tau>.(<\<nu>y>(P' \<parallel> (Q'[x::=y]))) | a y P' x Q'. <\<nu>y>a{y}.P' \<in> summands P \<and> a<x>.Q' \<in> summands Q \<and> y \<sharp> Q}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {uu_. \<exists>a y P' x Q'. uu_ = \<tau>.(<\<nu>y>(P' \<parallel> Q'[x::=y])) \<and> <\<nu>y>a{y}.P' \<in> summands P \<and> a<x>.Q' \<in> summands Q \<and> y \<sharp> Q}
[PROOF STEP]
apply(nominal_induct P avoiding: Q rule: pi.strong_induct, simp_all)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>pi1 pi2 Q. \<lbrakk>\<And>b. finite {uu_. \<exists>a y P' x Q'. uu_ = \<tau>.(<\<nu>y>(P' \<parallel> Q'[x::=y])) \<and> <\<nu>y>a{y}.P' \<in> summands pi1 \<and> a<x>.Q' \<in> summands b \<and> y \<sharp> b}; \<And>b. finite {uu_. \<exists>a y P' x Q'. uu_ = \<tau>.(<\<nu>y>(P' \<parallel> Q'[x::=y])) \<and> <\<nu>y>a{y}.P' \<in> summands pi2 \<and> a<x>.Q' \<in> summands b \<and> y \<sharp> b}\<rbrakk> \<Longrightarrow> finite {uu_. \<exists>a y P' x Q'. uu_ = \<tau>.(<\<nu>y>(P' \<parallel> Q'[x::=y])) \<and> (<\<nu>y>a{y}.P' \<in> summands pi1 \<or> <\<nu>y>a{y}.P' \<in> summands pi2) \<and> a<x>.Q' \<in> summands Q \<and> y \<sharp> Q}
 2. \<And>name pi Q. \<lbrakk>name \<sharp> Q; \<And>b. finite {uu_. \<exists>a y P' x Q'. uu_ = \<tau>.(<\<nu>y>(P' \<parallel> Q'[x::=y])) \<and> <\<nu>y>a{y}.P' \<in> summands pi \<and> a<x>.Q' \<in> summands b \<and> y \<sharp> b}\<rbrakk> \<Longrightarrow> (\<exists>a. a \<noteq> name \<and> (\<exists>P'. pi = a{name}.P')) \<longrightarrow> finite {uu_. \<exists>a y P' x Q'. uu_ = \<tau>.(<\<nu>y>(P' \<parallel> Q'[x::=y])) \<and> <\<nu>y>a{y}.P' = <\<nu>name>pi \<and> a<x>.Q' \<in> summands Q \<and> y \<sharp> Q}
[PROOF STEP]
apply(simp add: Collect_ex_eq conj_disj_distribL conj_disj_distribR name_fresh_abs
                      Collect_disj_eq UN_Un_distrib)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>name pi Q. \<lbrakk>name \<sharp> Q; \<And>b. finite {uu_. \<exists>a y P' x Q'. uu_ = \<tau>.(<\<nu>y>(P' \<parallel> Q'[x::=y])) \<and> <\<nu>y>a{y}.P' \<in> summands pi \<and> a<x>.Q' \<in> summands b \<and> y \<sharp> b}\<rbrakk> \<Longrightarrow> (\<exists>a. a \<noteq> name \<and> (\<exists>P'. pi = a{name}.P')) \<longrightarrow> finite {uu_. \<exists>a y P' x Q'. uu_ = \<tau>.(<\<nu>y>(P' \<parallel> Q'[x::=y])) \<and> <\<nu>y>a{y}.P' = <\<nu>name>pi \<and> a<x>.Q' \<in> summands Q \<and> y \<sharp> Q}
[PROOF STEP]
by(auto intro: BC)
[PROOF STATE]
proof (state)
this:
finite {uu_. \<exists>a y P' x Q'. uu_ = \<tau>.(<\<nu>y>(P' \<parallel> Q'[x::=y])) \<and> <\<nu>y>a{y}.P' \<in> summands P \<and> a<x>.Q' \<in> summands Q \<and> y \<sharp> Q}

goal (1 subgoal):
 1. finite {\<tau>.(<\<nu>y>(P' \<parallel> Q'[x::=y])) |y P' x Q'. \<exists>a. <\<nu>y>a{y}.P' \<in> summands P \<and> a<x>.Q' \<in> summands Q \<and> y \<sharp> Q}
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
finite {uu_. \<exists>a y P' x Q'. uu_ = \<tau>.(<\<nu>y>(P' \<parallel> Q'[x::=y])) \<and> <\<nu>y>a{y}.P' \<in> summands P \<and> a<x>.Q' \<in> summands Q \<and> y \<sharp> Q}

goal (1 subgoal):
 1. finite {\<tau>.(<\<nu>y>(P' \<parallel> Q'[x::=y])) |y P' x Q'. \<exists>a. <\<nu>y>a{y}.P' \<in> summands P \<and> a<x>.Q' \<in> summands Q \<and> y \<sharp> Q}
[PROOF STEP]
apply(rule_tac finite_subset)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. finite {uu_. \<exists>a y P' x Q'. uu_ = \<tau>.(<\<nu>y>(P' \<parallel> Q'[x::=y])) \<and> <\<nu>y>a{y}.P' \<in> summands P \<and> a<x>.Q' \<in> summands Q \<and> y \<sharp> Q} \<Longrightarrow> {\<tau>.(<\<nu>y>(P' \<parallel> Q'[x::=y])) |y P' x Q'. \<exists>a. <\<nu>y>a{y}.P' \<in> summands P \<and> a<x>.Q' \<in> summands Q \<and> y \<sharp> Q} \<subseteq> ?B1
 2. finite {uu_. \<exists>a y P' x Q'. uu_ = \<tau>.(<\<nu>y>(P' \<parallel> Q'[x::=y])) \<and> <\<nu>y>a{y}.P' \<in> summands P \<and> a<x>.Q' \<in> summands Q \<and> y \<sharp> Q} \<Longrightarrow> finite ?B1
[PROOF STEP]
defer
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. finite {uu_. \<exists>a y P' x Q'. uu_ = \<tau>.(<\<nu>y>(P' \<parallel> Q'[x::=y])) \<and> <\<nu>y>a{y}.P' \<in> summands P \<and> a<x>.Q' \<in> summands Q \<and> y \<sharp> Q} \<Longrightarrow> finite ?B1
 2. finite {uu_. \<exists>a y P' x Q'. uu_ = \<tau>.(<\<nu>y>(P' \<parallel> Q'[x::=y])) \<and> <\<nu>y>a{y}.P' \<in> summands P \<and> a<x>.Q' \<in> summands Q \<and> y \<sharp> Q} \<Longrightarrow> {\<tau>.(<\<nu>y>(P' \<parallel> Q'[x::=y])) |y P' x Q'. \<exists>a. <\<nu>y>a{y}.P' \<in> summands P \<and> a<x>.Q' \<in> summands Q \<and> y \<sharp> Q} \<subseteq> ?B1
[PROOF STEP]
by blast+
[PROOF STATE]
proof (state)
this:
finite {\<tau>.(<\<nu>y>(P' \<parallel> Q'[x::=y])) |y P' x Q'. \<exists>a. <\<nu>y>a{y}.P' \<in> summands P \<and> a<x>.Q' \<in> summands Q \<and> y \<sharp> Q}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
finite {\<tau>.(<\<nu>y>(P' \<parallel> Q'[x::=y])) |y P' x Q'. \<exists>a. <\<nu>y>a{y}.P' \<in> summands P \<and> a<x>.Q' \<in> summands Q \<and> y \<sharp> Q}

goal (1 subgoal):
 1. finite (expandSet P Q)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
finite {\<tau>.(P' \<parallel> Q) |P'. \<tau>.P' \<in> summands P}
finite {\<tau>.(P \<parallel> Q') |Q'. \<tau>.Q' \<in> summands Q}
finite {a{b}.(P' \<parallel> Q) |a b P'. a{b}.P' \<in> summands P}
finite {a{b}.(P \<parallel> Q') |a b Q'. a{b}.Q' \<in> summands Q}
finite {a<x>.(P' \<parallel> Q) |a x P'. a<x>.P' \<in> summands P \<and> x \<sharp> Q}
finite {a<x>.(P \<parallel> Q') |a x Q'. a<x>.Q' \<in> summands Q \<and> x \<sharp> P}
finite {<\<nu>x>a{x}.(P' \<parallel> Q) |a x P'. <\<nu>x>a{x}.P' \<in> summands P \<and> x \<sharp> Q}
finite {<\<nu>x>a{x}.(P \<parallel> Q') |a x Q'. <\<nu>x>a{x}.Q' \<in> summands Q \<and> x \<sharp> P}
finite {\<tau>.(P'[x::=b] \<parallel> Q') |x P' b Q'. \<exists>a. a<x>.P' \<in> summands P \<and> a{b}.Q' \<in> summands Q}
finite {\<tau>.(P' \<parallel> Q'[x::=b]) |b P' x Q'. \<exists>a. a{b}.P' \<in> summands P \<and> a<x>.Q' \<in> summands Q}
finite {\<tau>.(<\<nu>y>(P'[x::=y] \<parallel> Q')) |x P' y Q'. \<exists>a. a<x>.P' \<in> summands P \<and> <\<nu>y>a{y}.Q' \<in> summands Q \<and> y \<sharp> P}
finite {\<tau>.(<\<nu>y>(P' \<parallel> Q'[x::=y])) |y P' x Q'. \<exists>a. <\<nu>y>a{y}.P' \<in> summands P \<and> a<x>.Q' \<in> summands Q \<and> y \<sharp> Q}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
finite {\<tau>.(P' \<parallel> Q) |P'. \<tau>.P' \<in> summands P}
finite {\<tau>.(P \<parallel> Q') |Q'. \<tau>.Q' \<in> summands Q}
finite {a{b}.(P' \<parallel> Q) |a b P'. a{b}.P' \<in> summands P}
finite {a{b}.(P \<parallel> Q') |a b Q'. a{b}.Q' \<in> summands Q}
finite {a<x>.(P' \<parallel> Q) |a x P'. a<x>.P' \<in> summands P \<and> x \<sharp> Q}
finite {a<x>.(P \<parallel> Q') |a x Q'. a<x>.Q' \<in> summands Q \<and> x \<sharp> P}
finite {<\<nu>x>a{x}.(P' \<parallel> Q) |a x P'. <\<nu>x>a{x}.P' \<in> summands P \<and> x \<sharp> Q}
finite {<\<nu>x>a{x}.(P \<parallel> Q') |a x Q'. <\<nu>x>a{x}.Q' \<in> summands Q \<and> x \<sharp> P}
finite {\<tau>.(P'[x::=b] \<parallel> Q') |x P' b Q'. \<exists>a. a<x>.P' \<in> summands P \<and> a{b}.Q' \<in> summands Q}
finite {\<tau>.(P' \<parallel> Q'[x::=b]) |b P' x Q'. \<exists>a. a{b}.P' \<in> summands P \<and> a<x>.Q' \<in> summands Q}
finite {\<tau>.(<\<nu>y>(P'[x::=y] \<parallel> Q')) |x P' y Q'. \<exists>a. a<x>.P' \<in> summands P \<and> <\<nu>y>a{y}.Q' \<in> summands Q \<and> y \<sharp> P}
finite {\<tau>.(<\<nu>y>(P' \<parallel> Q'[x::=y])) |y P' x Q'. \<exists>a. <\<nu>y>a{y}.P' \<in> summands P \<and> a<x>.Q' \<in> summands Q \<and> y \<sharp> Q}

goal (1 subgoal):
 1. finite (expandSet P Q)
[PROOF STEP]
by(simp add: expandSet_def)
[PROOF STATE]
proof (state)
this:
finite (expandSet P Q)

goal:
No subgoals!
[PROOF STEP]
qed