Quelle Class2.thy
Sprache: Isabelle
theory Class2
imports Class1
begin
text ‹ Reduction›
lemma fin_not_Cut:
assumes a:
"fin M x"
shows "¬ (∃ a M' x N'. M = Cut .M' (x).N')"
using a
by (induct) (auto)
lemma fresh_not_fin:
assumes a:
"x♯ M"
shows "¬ fin M x"
proof -
have "fin M x ==> x♯ M ==> False" by (induct rule: fin.induct) (auto simp add: abs_fresh fr
esh_atm)with a show "¬ fin M x" by blastqed lemma fresh_not_fic:assumes a: "a♯ M" shows "¬ fic M a" proof -have "fic M a ==> a♯ M ==> False" by (induct rule: fic.induct) (auto simp add: abs_fresh fresh_atm)with a show "¬ fic M a" by blastqed lemma c_redu_subst1:assumes a: "M ⟶ 🪙 c M'" "c♯ M" "y♯ P" shows "M{y:=.P} ⟶ 🪙 c M'{y:=.P}" using aproof (nominal_induct avoiding: y c P rule: c_redu.strong_induct)case (left M a N x)then show ?case apply -apply (simp)apply (rule conjI)apply (force)apply (auto)apply (subgoal_tac "M{a:=(x).N}{y:=.P} = M{y:=.P}{a:=(x).(N{y:=.P})}" )(*A*) apply (simp)apply (rule c_redu.intros )apply (rule not_fic_subst1)apply (simp)apply (simp add: subst_fresh)apply (simp add: subst_fresh)apply (simp add: abs_fresh fresh_atm)apply (rule subst_subst2)apply (simp add: fresh_prod fresh_atm)apply (simp add: fresh_prod fresh_atm)apply (simp add: fresh_prod fresh_atm)apply (simp)done next case (right N x a M)then show ?case apply -apply (simp)apply (rule conjI)(* case M = Ax y a *) apply (rule impI)apply (subgoal_tac "N{x:=.Ax y a}{y:=.P} = N{y:=.P}{x:=.P}" )apply (simp)apply (rule c_redu.right)apply (rule not_fin_subst2)apply (simp)apply (rule subst_fresh)apply (simp add: abs_fresh)apply (simp add: abs_fresh)apply (rule sym)apply (rule interesting_subst1')apply (simp add: fresh_atm)apply (simp)apply (simp)(* case M \<noteq> Ax y a*) apply (rule impI)apply (subgoal_tac "N{x:=.M}{y:=.P} = N{y:=.P}{x:=.(M{y:=.P})}" )apply (simp)apply (rule c_redu.right)apply (rule not_fin_subst2)apply (simp)apply (simp add: subst_fresh)apply (simp add: subst_fresh)apply (simp add: abs_fresh fresh_atm)apply (rule subst_subst3)apply (simp_all add: fresh_atm fresh_prod)done qed lemma c_redu_subst2:assumes a: "M ⟶ 🪙 c M'" "c♯ P" "y♯ M" shows "M{c:=(y).P} ⟶ 🪙 c M'{c:=(y).P}" using aproof (nominal_induct avoiding: y c P rule: c_redu.strong_induct)case (right N x a M)then show ?case apply -apply (simp)apply (rule conjI)apply (force)apply (auto)apply (subgoal_tac "N{x:=.M}{c:=(y).P} = N{c:=(y).P}{x:= .(M{c:=(y).P})}" )(*A*) apply (simp)apply (rule c_redu.intros )apply (rule not_fin_subst1)apply (simp)apply (simp add: subst_fresh)apply (simp add: subst_fresh)apply (simp add: abs_fresh fresh_atm)apply (rule subst_subst1)apply (simp add: fresh_prod fresh_atm)apply (simp add: fresh_prod fresh_atm)apply (simp add: fresh_prod fresh_atm)apply (simp)done next case (left M a N x)then show ?case apply -apply (simp)apply (rule conjI)(* case N = Ax x c *) apply (rule impI)apply (subgoal_tac "M{a:=(x).Ax x c}{c:=(y).P} = M{c:=(y).P}{a:=(y).P}" )apply (simp)apply (rule c_redu.left)apply (rule not_fic_subst2)apply (simp)apply (simp)apply (rule subst_fresh)apply (simp add: abs_fresh)apply (rule sym)apply (rule interesting_subst2')apply (simp add: fresh_atm)apply (simp)apply (simp)(* case M \<noteq> Ax y a*) apply (rule impI)apply (subgoal_tac "M{a:=(x).N}{c:=(y).P} = M{c:=(y).P}{a:=(x).(N{c:=(y).P})}" )apply (simp)apply (rule c_redu.left)apply (rule not_fic_subst2)apply (simp)apply (simp add: subst_fresh)apply (simp add: subst_fresh)apply (simp add: abs_fresh fresh_atm)apply (rule subst_subst4)apply (simp add: fresh_prod fresh_atm)apply (simp add: fresh_prod fresh_atm)apply (simp add: fresh_prod fresh_atm)apply (simp add: fresh_prod fresh_atm)apply (simp)done qed lemma c_redu_subst1':assumes a: "M ⟶ 🪙 c M'" shows "M{y:=.P} ⟶ 🪙 c M'{y:=.P}" using aproof -obtain y'::"name" where fs1: "y'♯ (M,M',P,P,y)" by (rule exists_fresh(1), rule fin_supp, blast)obtain c'::"coname" where fs2: "c'♯ (M,M',P,P,c)" by (rule exists_fresh(2), rule fin_supp, blast)have "M{y:=.P} = ([(y',y)]∙ M){y':=.([(c',c)]∙ P)}" using fs1 fs2apply -apply (rule trans)apply (rule_tac y="y'" in subst_rename(3))apply (simp)apply (rule subst_rename(4))apply (simp)done also have "… ⟶ 🪙 c ([(y',y)]∙ M'){y':=.([(c',c)]∙ P)}" using fs1 fs2apply -apply (rule c_redu_subst1)apply (simp add: c_redu.eqvt a)apply (simp_all add: fresh_left calc_atm fresh_prod)done also have "… = M'{y:=.P}" using fs1 fs2apply -apply (rule sym)apply (rule trans)apply (rule_tac y="y'" in subst_rename(3))apply (simp)apply (rule subst_rename(4))apply (simp)done finally show ?thesis by simpqed lemma c_redu_subst2':assumes a: "M ⟶ 🪙 c M'" shows "M{c:=(y).P} ⟶ 🪙 c M'{c:=(y).P}" using aproof -obtain y'::"name" where fs1: "y'♯ (M,M',P,P,y)" by (rule exists_fresh(1), rule fin_supp, blast)obtain c'::"coname" where fs2: "c'♯ (M,M',P,P,c)" by (rule exists_fresh(2), rule fin_supp, blast)have "M{c:=(y).P} = ([(c',c)]∙ M){c':=(y').([(y',y)]∙ P)}" using fs1 fs2apply -apply (rule trans)apply (rule_tac c="c'" in subst_rename(1))apply (simp)apply (rule subst_rename(2))apply (simp)done also have "… ⟶ 🪙 c ([(c',c)]∙ M'){c':=(y').([(y',y)]∙ P)}" using fs1 fs2apply -apply (rule c_redu_subst2)apply (simp add: c_redu.eqvt a)apply (simp_all add: fresh_left calc_atm fresh_prod)done also have "… = M'{c:=(y).P}" using fs1 fs2apply -apply (rule sym)apply (rule trans)apply (rule_tac c="c'" in subst_rename(1))apply (simp)apply (rule subst_rename(2))apply (simp)done finally show ?thesis by simpqed lemma aux1:assumes a: "M = M'" "M' ⟶ 🪙 l M''" shows "M ⟶ 🪙 l M''" using a by simplemma aux2:assumes a: "M ⟶ 🪙 l M'" "M' = M''" shows "M ⟶ 🪙 l M''" using a by simplemma aux3:assumes a: "M = M'" "M' ⟶ 🪙 a* M''" shows "M ⟶ 🪙 a* M''" using a by simplemma aux4:assumes a: "M = M'" shows "M ⟶ 🪙 a* M'" using a by blastlemma l_redu_subst1:assumes a: "M ⟶ 🪙 l M'" shows "M{y:=.P} ⟶ 🪙 a* M'{y:=.P}" using aproof (nominal_induct M M' avoiding: y c P rule: l_redu.strong_induct)case LAxRthen show ?case apply -apply (rule aux3)apply (rule better_Cut_substn)apply (simp add: abs_fresh)apply (simp)apply (simp add: fresh_atm)apply (auto)apply (rule aux4)apply (simp add: trm.inject alpha calc_atm fresh_atm)apply (rule rtranclp_trans)apply (rule a_starI)apply (rule al_redu)apply (rule l_redu.intros )apply (simp add: subst_fresh)apply (simp add: fresh_atm)apply (rule fic_subst2)apply (simp_all)apply (rule aux4)apply (rule subst_comm')apply (simp_all)done next case LAxLthen show ?case apply -apply (rule aux3)apply (rule better_Cut_substn)apply (simp add: abs_fresh)apply (simp)apply (simp add: trm.inject fresh_atm)apply (auto)apply (rule aux4)apply (rule sym)apply (rule fin_substn_nrename)apply (simp_all)apply (rule a_starI)apply (rule al_redu)apply (rule aux2)apply (rule l_redu.intros )apply (simp add: subst_fresh)apply (simp add: fresh_atm)apply (rule fin_subst1)apply (simp_all)apply (rule subst_comm')apply (simp_all)done next case (LNot v M N u a b)then show ?case proof -assume asm: "N≠ Ax y b" have "(Cut .NotR (u).M a (v).NotL .N v){y:=.P} = (Cut .NotR (u).(M{y:=.P}) a (v).NotL .(N{y:=.P}) v)" using LNotby (simp add: subst_fresh abs_fresh fresh_atm)also have "… ⟶ 🪙 l (Cut .(N{y:=.P}) (u).(M{y:=.P}))" using LNotby (auto intro: l_redu.intros simp add: subst_fresh)also have "… = (Cut .N (u).M){y:=.P}" using LNot asmby (simp add: subst_fresh abs_fresh fresh_atm)finally have ?thesis by automoreover assume asm: "N=Ax y b" have "(Cut .NotR (u).M a (v).NotL .N v){y:=.P} = (Cut .NotR (u).(M{y:=.P}) a (v).NotL .(N{y:=.P}) v)" using LNotby (simp add: subst_fresh abs_fresh fresh_atm)also have "… ⟶ 🪙 a* (Cut .(N{y:=.P}) (u).(M{y:=.P}))" using LNotapply -apply (rule a_starI)apply (rule al_redu)apply (auto intro: l_redu.intros simp add: subst_fresh abs_fresh)done also have "… = (Cut .(Cut .P (y).Ax y b) (u).(M{y:=.P}))" using LNot asmby simpalso have "… ⟶ 🪙 a* (Cut .(P[c⊨ c>b]) (u).(M{y:=.P}))" proof (cases "fic P c" )case True assume "fic P c" then show ?thesis using LNotapply -apply (rule a_starI)apply (rule better_CutL_intro)apply (rule al_redu)apply (rule better_LAxR_intro)apply (simp)done next case False assume "¬ fic P c" then show ?thesisapply -apply (rule a_star_CutL)apply (rule rtranclp_trans)apply (rule a_starI)apply (rule ac_redu)apply (rule better_left)apply (simp)apply (simp add: subst_with_ax2)done qed also have "… = (Cut .N (u).M){y:=.P}" using LNot asmapply -apply (auto simp add: subst_fresh abs_fresh)apply (simp add: trm.inject)apply (simp add: alpha fresh_atm)apply (rule sym)apply (rule crename_swap)apply (simp)done finally have "(Cut .NotR (u).M a (v).NotL .N v){y:=.P} ⟶ 🪙 a* (Cut .N (u).M){y:=.P}" by simpultimately show ?thesis by blastqed next case (LAnd1 b a1 M1 a2 M2 N z u)then show ?case proof -assume asm: "M1≠ Ax y a1" have "(Cut .AndR .M1 .M2 b (z).AndL1 (u).N z){y:=.P} = Cut .AndR .(M1{y:=.P}) .(M2{y:=.P}) b (z).AndL1 (u).(N{y:=.P}) z" using LAnd1 by (simp add: subst_fresh abs_fresh fresh_atm)also have "… ⟶ 🪙 a* Cut .(M1{y:=.P}) (u).(N{y:=.P})" using LAnd1apply -apply (rule a_starI)apply (rule al_redu)apply (auto intro: l_redu.intros simp add: subst_fresh abs_fresh)done also have "… = (Cut .M1 (u).N){y:=.P}" using LAnd1 asmby (simp add: subst_fresh abs_fresh fresh_atm)finally have "(Cut .AndR .M1 .M2 b (z).AndL1 (u).N z){y:=.P} ⟶ 🪙 a* (Cut .M1 (u).N){y:=.P}" by simpmoreover assume asm: "M1=Ax y a1" have "(Cut .AndR .M1 .M2 b (z).AndL1 (u).N z){y:=.P} = Cut .AndR .(M1{y:=.P}) .(M2{y:=.P}) b (z).AndL1 (u).(N{y:=.P}) z" using LAnd1 by (simp add: subst_fresh abs_fresh fresh_atm)also have "… ⟶ 🪙 a* Cut .(M1{y:=.P}) (u).(N{y:=.P})" using LAnd1apply -apply (rule a_starI)apply (rule al_redu)apply (auto intro: l_redu.intros simp add: subst_fresh abs_fresh)done also have "… = Cut .(Cut .P (y). Ax y a1) (u).(N{y:=.P})" using LAnd1 asm by simpalso have "… ⟶ 🪙 a* Cut .P[c⊨ c>a1] (u).(N{y:=.P})" proof (cases "fic P c" )case True assume "fic P c" then show ?thesis using LAnd1apply -apply (rule a_starI)apply (rule better_CutL_intro)apply (rule al_redu)apply (rule better_LAxR_intro)apply (simp)done next case False assume "¬ fic P c" then show ?thesisapply -apply (rule a_star_CutL)apply (rule rtranclp_trans)apply (rule a_starI)apply (rule ac_redu)apply (rule better_left)apply (simp)apply (simp add: subst_with_ax2)done qed also have "… = (Cut .M1 (u).N){y:=.P}" using LAnd1 asmapply -apply (auto simp add: subst_fresh abs_fresh)apply (simp add: trm.inject)apply (simp add: alpha fresh_atm)apply (rule sym)apply (rule crename_swap)apply (simp)done finally have "(Cut .AndR .M1 .M2 b (z).AndL1 (u).N z){y:=.P} ⟶ 🪙 a* (Cut .M1 (u).N){y:=.P}" by simpultimately show ?thesis by blastqed next case (LAnd2 b a1 M1 a2 M2 N z u)then show ?case proof -assume asm: "M2≠ Ax y a2" have "(Cut .AndR .M1 .M2 b (z).AndL2 (u).N z){y:=.P} = Cut .AndR .(M1{y:=.P}) .(M2{y:=.P}) b (z).AndL2 (u).(N{y:=.P}) z" using LAnd2 by (simp add: subst_fresh abs_fresh fresh_atm)also have "… ⟶ 🪙 a* Cut .(M2{y:=.P}) (u).(N{y:=.P})" using LAnd2apply -apply (rule a_starI)apply (rule al_redu)apply (auto intro: l_redu.intros simp add: subst_fresh abs_fresh)done also have "… = (Cut .M2 (u).N){y:=.P}" using LAnd2 asmby (simp add: subst_fresh abs_fresh fresh_atm)finally have "(Cut .AndR .M1 .M2 b (z).AndL2 (u).N z){y:=.P} ⟶ 🪙 a* (Cut .M2 (u).N){y:=.P}" by simpmoreover assume asm: "M2=Ax y a2" have "(Cut .AndR .M1 .M2 b (z).AndL2 (u).N z){y:=.P} = Cut .AndR .(M1{y:=.P}) .(M2{y:=.P}) b (z).AndL2 (u).(N{y:=.P}) z" using LAnd2 by (simp add: subst_fresh abs_fresh fresh_atm)also have "… ⟶ 🪙 a* Cut .(M2{y:=.P}) (u).(N{y:=.P})" using LAnd2apply -apply (rule a_starI)apply (rule al_redu)apply (auto intro: l_redu.intros simp add: subst_fresh abs_fresh)done also have "… = Cut .(Cut .P (y). Ax y a2) (u).(N{y:=.P})" using LAnd2 asm by simpalso have "… ⟶ 🪙 a* Cut .P[c⊨ c>a2] (u).(N{y:=.P})" proof (cases "fic P c" )case True assume "fic P c" then show ?thesis using LAnd2 asmapply -apply (rule a_starI)apply (rule better_CutL_intro)apply (rule al_redu)apply (rule better_LAxR_intro)apply (simp)done next case False assume "¬ fic P c" then show ?thesisapply -apply (rule a_star_CutL)apply (rule rtranclp_trans)apply (rule a_starI)apply (rule ac_redu)apply (rule better_left)apply (simp)apply (simp add: subst_with_ax2)done qed also have "… = (Cut .M2 (u).N){y:=.P}" using LAnd2 asmapply -apply (auto simp add: subst_fresh abs_fresh)apply (simp add: trm.inject)apply (simp add: alpha fresh_atm)apply (rule sym)apply (rule crename_swap)apply (simp)done finally have "(Cut .AndR .M1 .M2 b (z).AndL2 (u).N z){y:=.P} ⟶ 🪙 a* (Cut .M2 (u).N){y:=.P}" by simpultimately show ?thesis by blastqed next case (LOr1 b a M N1 N2 z x1 x2 y c P)then show ?case proof -assume asm: "M≠ Ax y a" have "(Cut .OrR1 .M b (z).OrL (x1).N1 (x2).N2 z){y:=.P} = Cut .OrR1 .(M{y:=.P}) b (z).OrL (x1).(N1{y:=.P}) (x2).(N2{y:=.P}) z" using LOr1 by (simp add: subst_fresh abs_fresh fresh_atm)also have "… ⟶ 🪙 a* Cut .(M{y:=.P}) (x1).(N1{y:=.P})" using LOr1apply -apply (rule a_starI)apply (rule al_redu)apply (auto intro: l_redu.intros simp add: subst_fresh abs_fresh)done also have "… = (Cut .M (x1).N1){y:=.P}" using LOr1 asmby (simp add: subst_fresh abs_fresh fresh_atm)finally have "(Cut .OrR1 .M b (z).OrL (x1).N1 (x2).N2 z){y:=.P} ⟶ 🪙 a* (Cut .M (x1).N1){y:=.P}" by simpmoreover assume asm: "M=Ax y a" have "(Cut .OrR1 .M b (z).OrL (x1).N1 (x2).N2 z){y:=.P} = Cut .OrR1 .(M{y:=.P}) b (z).OrL (x1).(N1{y:=.P}) (x2).(N2{y:=.P}) z" using LOr1 by (simp add: subst_fresh abs_fresh fresh_atm)also have "… ⟶ 🪙 a* Cut .(M{y:=.P}) (x1).(N1{y:=.P})" using LOr1apply -apply (rule a_starI)apply (rule al_redu)apply (auto intro: l_redu.intros simp add: subst_fresh abs_fresh)done also have "… = Cut .(Cut .P (y). Ax y a) (x1).(N1{y:=.P})" using LOr1 asm by simpalso have "… ⟶ 🪙 a* Cut .P[c⊨ c>a] (x1).(N1{y:=.P})" proof (cases "fic P c" )case True assume "fic P c" then show ?thesis using LOr1apply -apply (rule a_starI)apply (rule better_CutL_intro)apply (rule al_redu)apply (rule better_LAxR_intro)apply (simp)done next case False assume "¬ fic P c" then show ?thesisapply -apply (rule a_star_CutL)apply (rule rtranclp_trans)apply (rule a_starI)apply (rule ac_redu)apply (rule better_left)apply (simp)apply (simp add: subst_with_ax2)done qed also have "… = (Cut .M (x1).N1){y:=.P}" using LOr1 asmapply -apply (auto simp add: subst_fresh abs_fresh)apply (simp add: trm.inject)apply (simp add: alpha fresh_atm)apply (rule sym)apply (rule crename_swap)apply (simp)done finally have "(Cut .OrR1 .M b (z).OrL (x1).N1 (x2).N2 z){y:=.P} ⟶ 🪙 a* (Cut .M (x1).N1){y:=.P}" by simpultimately show ?thesis by blastqed next case (LOr2 b a M N1 N2 z x1 x2 y c P)then show ?case proof -assume asm: "M≠ Ax y a" have "(Cut .OrR2 .M b (z).OrL (x1).N1 (x2).N2 z){y:=.P} = Cut .OrR2 .(M{y:=.P}) b (z).OrL (x1).(N1{y:=.P}) (x2).(N2{y:=.P}) z" using LOr2 by (simp add: subst_fresh abs_fresh fresh_atm)also have "… ⟶ 🪙 a* Cut .(M{y:=.P}) (x2).(N2{y:=.P})" using LOr2apply -apply (rule a_starI)apply (rule al_redu)apply (auto intro: l_redu.intros simp add: subst_fresh abs_fresh)done also have "… = (Cut .M (x2).N2){y:=.P}" using LOr2 asmby (simp add: subst_fresh abs_fresh fresh_atm)finally have "(Cut .OrR2 .M b (z).OrL (x1).N1 (x2).N2 z){y:=.P} ⟶ 🪙 a* (Cut .M (x2).N2){y:=.P}" by simpmoreover assume asm: "M=Ax y a" have "(Cut .OrR2 .M b (z).OrL (x1).N1 (x2).N2 z){y:=.P} = Cut .OrR2 .(M{y:=.P}) b (z).OrL (x1).(N1{y:=.P}) (x2).(N2{y:=.P}) z" using LOr2 by (simp add: subst_fresh abs_fresh fresh_atm)also have "… ⟶ 🪙 a* Cut .(M{y:=.P}) (x2).(N2{y:=.P})" using LOr2apply -apply (rule a_starI)apply (rule al_redu)apply (auto intro: l_redu.intros simp add: subst_fresh abs_fresh)done also have "… = Cut .(Cut .P (y). Ax y a) (x2).(N2{y:=.P})" using LOr2 asm by simpalso have "… ⟶ 🪙 a* Cut .P[c⊨ c>a] (x2).(N2{y:=.P})" proof (cases "fic P c" )case True assume "fic P c" then show ?thesis using LOr2apply -apply (rule a_starI)apply (rule better_CutL_intro)apply (rule al_redu)apply (rule better_LAxR_intro)apply (simp)done next case False assume "¬ fic P c" then show ?thesisapply -apply (rule a_star_CutL)apply (rule rtranclp_trans)apply (rule a_starI)apply (rule ac_redu)apply (rule better_left)apply (simp)apply (simp add: subst_with_ax2)done qed also have "… = (Cut .M (x2).N2){y:=.P}" using LOr2 asmapply -apply (auto simp add: subst_fresh abs_fresh)apply (simp add: trm.inject)apply (simp add: alpha fresh_atm)apply (rule sym)apply (rule crename_swap)apply (simp)done finally have "(Cut .OrR2 .M b (z).OrL (x1).N1 (x2).N2 z){y:=.P} ⟶ 🪙 a* (Cut .M (x2).N2){y:=.P}" by simpultimately show ?thesis by blastqed next case (LImp z N u Q x M b a d y c P)then show ?case proof -assume asm: "N≠ Ax y d" have "(Cut .ImpR (x)..M b (z).ImpL .N (u).Q z){y:=.P} = Cut .ImpR (x)..(M{y:=.P}) b (z).ImpL .(N{y:=.P}) (u).(Q{y:=.P}) z" using LImp by (simp add: fresh_prod abs_fresh fresh_atm)also have "… ⟶ 🪙 a* Cut .(Cut .(N{y:=.P}) (x).(M{y:=.P})) (u).(Q{y:=.P})" using LImpapply -apply (rule a_starI)apply (rule al_redu)apply (auto intro: l_redu.intros simp add: subst_fresh abs_fresh)done also have "… = (Cut .(Cut .N (x).M) (u).Q){y:=.P}" using LImp asmby (simp add: subst_fresh abs_fresh fresh_atm)finally have "(Cut .ImpR (x)..M b (z).ImpL .N (u).Q z){y:=.P} ⟶ 🪙 a* (Cut .(Cut .N (x).M) (u).Q){y:=.P}" by simpmoreover assume asm: "N=Ax y d" have "(Cut .ImpR (x)..M b (z).ImpL .N (u).Q z){y:=.P} = Cut .ImpR (x)..(M{y:=.P}) b (z).ImpL .(N{y:=.P}) (u).(Q{y:=.P}) z" using LImp by (simp add: subst_fresh abs_fresh fresh_atm fresh_prod)also have "… ⟶ 🪙 a* Cut .(Cut .(N{y:=.P}) (x).(M{y:=.P})) (u).(Q{y:=.P})" using LImpapply -apply (rule a_starI)apply (rule al_redu)apply (auto intro: l_redu.intros simp add: subst_fresh abs_fresh)done also have "… = Cut .(Cut .(Cut .P (y).Ax y d) (x).(M{y:=.P})) (u).(Q{y:=.P})" using LImp asm by simpalso have "… ⟶ 🪙 a* Cut .(Cut .(P[c⊨ c>d]) (x).(M{y:=.P})) (u).(Q{y:=.P})" proof (cases "fic P c" )case True assume "fic P c" then show ?thesis using LImpapply -apply (rule a_starI)apply (rule better_CutL_intro)apply (rule a_Cut_l)apply (simp add: subst_fresh abs_fresh)apply (simp add: abs_fresh fresh_atm)apply (rule al_redu)apply (rule better_LAxR_intro)apply (simp)done next case False assume "¬ fic P c" then show ?thesis using LImpapply -apply (rule a_star_CutL)apply (rule a_star_CutL)apply (rule rtranclp_trans)apply (rule a_starI)apply (rule ac_redu)apply (rule better_left)apply (simp)apply (simp add: subst_with_ax2)done qed also have "… = (Cut .(Cut .N (x).M) (u).Q){y:=.P}" using LImp asmapply -apply (auto simp add: subst_fresh abs_fresh)apply (simp add: trm.inject)apply (simp add: alpha fresh_atm)apply (simp add: trm.inject)apply (simp add: alpha)apply (rule sym)apply (rule crename_swap)apply (simp)done finally have "(Cut .ImpR (x)..M b (z).ImpL .N (u).Q z){y:=.P} ⟶ 🪙 a* (Cut .(Cut .N (x).M) (u).Q){y:=.P}" by simpultimately show ?thesis by blastqed qed lemma l_redu_subst2:assumes a: "M ⟶ 🪙 l M'" shows "M{c:=(y).P} ⟶ 🪙 a* M'{c:=(y).P}" using aproof (nominal_induct M M' avoiding: y c P rule: l_redu.strong_induct)case LAxRthen show ?case apply -apply (rule aux3)apply (rule better_Cut_substc)apply (simp add: abs_fresh)apply (simp add: abs_fresh)apply (simp add: trm.inject fresh_atm)apply (auto)apply (rule aux4)apply (rule sym)apply (rule fic_substc_crename)apply (simp_all)apply (rule a_starI)apply (rule al_redu)apply (rule aux2)apply (rule l_redu.intros )apply (simp add: subst_fresh)apply (simp add: fresh_atm)apply (rule fic_subst1)apply (simp_all)apply (rule subst_comm')apply (simp_all)done next case LAxLthen show ?case apply -apply (rule aux3)apply (rule better_Cut_substc)apply (simp)apply (simp add: abs_fresh)apply (simp add: fresh_atm)apply (auto)apply (rule aux4)apply (simp add: trm.inject alpha calc_atm fresh_atm)apply (rule rtranclp_trans)apply (rule a_starI)apply (rule al_redu)apply (rule l_redu.intros )apply (simp add: subst_fresh)apply (simp add: fresh_atm)apply (rule fin_subst2)apply (simp_all)apply (rule aux4)apply (rule subst_comm')apply (simp_all)done next case (LNot v M N u a b)then show ?case proof -assume asm: "M≠ Ax u c" have "(Cut .NotR (u).M a (v).NotL .N v){c:=(y).P} = (Cut .NotR (u).(M{c:=(y).P}) a (v).NotL .(N{c:=(y).P}) v)" using LNotby (simp add: subst_fresh abs_fresh fresh_atm)also have "… ⟶ 🪙 l (Cut .(N{c:=(y).P}) (u).(M{c:=(y).P}))" using LNotby (auto intro: l_redu.intros simp add: subst_fresh)also have "… = (Cut .N (u).M){c:=(y).P}" using LNot asmby (simp add: subst_fresh abs_fresh fresh_atm)finally have ?thesis by automoreover assume asm: "M=Ax u c" have "(Cut .NotR (u).M a (v).NotL .N v){c:=(y).P} = (Cut .NotR (u).(M{c:=(y).P}) a (v).NotL .(N{c:=(y).P}) v)" using LNotby (simp add: subst_fresh abs_fresh fresh_atm)also have "… ⟶ 🪙 a* (Cut .(N{c:=(y).P}) (u).(M{c:=(y).P}))" using LNotapply -apply (rule a_starI)apply (rule al_redu)apply (auto intro: l_redu.intros simp add: subst_fresh abs_fresh)done also have "… = (Cut .(N{c:=(y).P}) (u).(Cut .(Ax u c) (y).P))" using LNot asmby simpalso have "… ⟶ 🪙 a* (Cut .(N{c:=(y).P}) (u).(P[y⊨ n>u]))" proof (cases "fin P y" )case True assume "fin P y" then show ?thesis using LNotapply -apply (rule a_starI)apply (rule better_CutR_intro)apply (rule al_redu)apply (rule better_LAxL_intro)apply (simp)done next case False assume "¬ fin P y" then show ?thesisapply -apply (rule a_star_CutR)apply (rule rtranclp_trans)apply (rule a_starI)apply (rule ac_redu)apply (rule better_right)apply (simp)apply (simp add: subst_with_ax1)done qed also have "… = (Cut .N (u).M){c:=(y).P}" using LNot asmapply -apply (auto simp add: subst_fresh abs_fresh)apply (simp add: trm.inject)apply (simp add: alpha fresh_atm)apply (rule sym)apply (rule nrename_swap)apply (simp)done finally have "(Cut .NotR (u).M a (v).NotL .N v){c:=(y).P} ⟶ 🪙 a* (Cut .N (u).M){c:=(y).P}" by simpultimately show ?thesis by blastqed next case (LAnd1 b a1 M1 a2 M2 N z u)then show ?case proof -assume asm: "N≠ Ax u c" have "(Cut .AndR .M1 .M2 b (z).AndL1 (u).N z){c:=(y).P} = Cut .AndR .(M1{c:=(y).P}) .(M2{c:=(y).P}) b (z).AndL1 (u).(N{c:=(y).P}) z" using LAnd1 by (simp add: subst_fresh abs_fresh fresh_atm)also have "… ⟶ 🪙 a* Cut .(M1{c:=(y).P}) (u).(N{c:=(y).P})" using LAnd1apply -apply (rule a_starI)apply (rule al_redu)apply (auto intro: l_redu.intros simp add: subst_fresh abs_fresh)done also have "… = (Cut .M1 (u).N){c:=(y).P}" using LAnd1 asmby (simp add: subst_fresh abs_fresh fresh_atm)finally have "(Cut .AndR .M1 .M2 b (z).AndL1 (u).N z){c:=(y).P} ⟶ 🪙 a* (Cut .M1 (u).N){c:=(y).P}" by simpmoreover assume asm: "N=Ax u c" have "(Cut .AndR .M1 .M2 b (z).AndL1 (u).N z){c:=(y).P} = Cut .AndR .(M1{c:=(y).P}) .(M2{c:=(y).P}) b (z).AndL1 (u).(N{c:=(y).P}) z" using LAnd1 by (simp add: subst_fresh abs_fresh fresh_atm)also have "… ⟶ 🪙 a* Cut .(M1{c:=(y).P}) (u).(N{c:=(y).P})" using LAnd1apply -apply (rule a_starI)apply (rule al_redu)apply (auto intro: l_redu.intros simp add: subst_fresh abs_fresh)done also have "… = Cut .(M1{c:=(y).P}) (u).(Cut .(Ax u c) (y).P)" using LAnd1 asm by simpalso have "… ⟶ 🪙 a* Cut .(M1{c:=(y).P}) (u).(P[y⊨ n>u])" proof (cases "fin P y" )case True assume "fin P y" then show ?thesis using LAnd1apply -apply (rule a_starI)apply (rule better_CutR_intro)apply (rule al_redu)apply (rule better_LAxL_intro)apply (simp)done next case False assume "¬ fin P y" then show ?thesisapply -apply (rule a_star_CutR)apply (rule rtranclp_trans)apply (rule a_starI)apply (rule ac_redu)apply (rule better_right)apply (simp)apply (simp add: subst_with_ax1)done qed also have "… = (Cut .M1 (u).N){c:=(y).P}" using LAnd1 asmapply -apply (auto simp add: subst_fresh abs_fresh)apply (simp add: trm.inject)apply (simp add: alpha fresh_atm)apply (rule sym)apply (rule nrename_swap)apply (simp)done finally have "(Cut .AndR .M1 .M2 b (z).AndL1 (u).N z){c:=(y).P} ⟶ 🪙 a* (Cut .M1 (u).N){c:=(y).P}" by simpultimately show ?thesis by blastqed next case (LAnd2 b a1 M1 a2 M2 N z u)then show ?case proof -assume asm: "N≠ Ax u c" have "(Cut .AndR .M1 .M2 b (z).AndL2 (u).N z){c:=(y).P} = Cut .AndR .(M1{c:=(y).P}) .(M2{c:=(y).P}) b (z).AndL2 (u).(N{c:=(y).P}) z" using LAnd2 by (simp add: subst_fresh abs_fresh fresh_atm)also have "… ⟶ 🪙 a* Cut .(M2{c:=(y).P}) (u).(N{c:=(y).P})" using LAnd2apply -apply (rule a_starI)apply (rule al_redu)apply (auto intro: l_redu.intros simp add: subst_fresh abs_fresh)done also have "… = (Cut .M2 (u).N){c:=(y).P}" using LAnd2 asmby (simp add: subst_fresh abs_fresh fresh_atm)finally have "(Cut .AndR .M1 .M2 b (z).AndL2 (u).N z){c:=(y).P} ⟶ 🪙 a* (Cut .M2 (u).N){c:=(y).P}" by simpmoreover assume asm: "N=Ax u c" have "(Cut .AndR .M1 .M2 b (z).AndL2 (u).N z){c:=(y).P} = Cut .AndR .(M1{c:=(y).P}) .(M2{c:=(y).P}) b (z).AndL2 (u).(N{c:=(y).P}) z" using LAnd2 by (simp add: subst_fresh abs_fresh fresh_atm)also have "… ⟶ 🪙 a* Cut .(M2{c:=(y).P}) (u).(N{c:=(y).P})" using LAnd2apply -apply (rule a_starI)apply (rule al_redu)apply (auto intro: l_redu.intros simp add: subst_fresh abs_fresh)done also have "… = Cut .(M2{c:=(y).P}) (u).(Cut .(Ax u c) (y).P)" using LAnd2 asm by simpalso have "… ⟶ 🪙 a* Cut .(M2{c:=(y).P}) (u).(P[y⊨ n>u])" proof (cases "fin P y" )case True assume "fin P y" then show ?thesis using LAnd2apply -apply (rule a_starI)apply (rule better_CutR_intro)apply (rule al_redu)apply (rule better_LAxL_intro)apply (simp)done next case False assume "¬ fin P y" then show ?thesisapply -apply (rule a_star_CutR)apply (rule rtranclp_trans)apply (rule a_starI)apply (rule ac_redu)apply (rule better_right)apply (simp)apply (simp add: subst_with_ax1)done qed also have "… = (Cut .M2 (u).N){c:=(y).P}" using LAnd2 asmapply -apply (auto simp add: subst_fresh abs_fresh)apply (simp add: trm.inject)apply (simp add: alpha fresh_atm)apply (rule sym)apply (rule nrename_swap)apply (simp)done finally have "(Cut .AndR .M1 .M2 b (z).AndL2 (u).N z){c:=(y).P} ⟶ 🪙 a* (Cut .M2 (u).N){c:=(y).P}" by simpultimately show ?thesis by blastqed next case (LOr1 b a M N1 N2 z x1 x2 y c P)then show ?case proof -assume asm: "N1≠ Ax x1 c" have "(Cut .OrR1 .M b (z).OrL (x1).N1 (x2).N2 z){c:=(y).P} = Cut .OrR1 .(M{c:=(y).P}) b (z).OrL (x1).(N1{c:=(y).P}) (x2).(N2{c:=(y).P}) z" using LOr1 by (simp add: subst_fresh abs_fresh fresh_atm)also have "… ⟶ 🪙 a* Cut .(M{c:=(y).P}) (x1).(N1{c:=(y).P})" using LOr1apply -apply (rule a_starI)apply (rule al_redu)apply (auto intro: l_redu.intros simp add: subst_fresh abs_fresh)done also have "… = (Cut .M (x1).N1){c:=(y).P}" using LOr1 asmby (simp add: subst_fresh abs_fresh fresh_atm)finally have "(Cut .OrR1 .M b (z).OrL (x1).N1 (x2).N2 z){c:=(y).P} ⟶ 🪙 a* (Cut .M (x1).N1){c:=(y).P}" by simpmoreover assume asm: "N1=Ax x1 c" have "(Cut .OrR1 .M b (z).OrL (x1).N1 (x2).N2 z){c:=(y).P} = Cut .OrR1 .(M{c:=(y).P}) b (z).OrL (x1).(N1{c:=(y).P}) (x2).(N2{c:=(y).P}) z" using LOr1 by (simp add: subst_fresh abs_fresh fresh_atm)also have "… ⟶ 🪙 a* Cut .(M{c:=(y).P}) (x1).(N1{c:=(y).P})" using LOr1apply -apply (rule a_starI)apply (rule al_redu)apply (auto intro: l_redu.intros simp add: subst_fresh abs_fresh)done also have "… = Cut .(M{c:=(y).P}) (x1).(Cut .(Ax x1 c) (y).P)" using LOr1 asm by simpalso have "… ⟶ 🪙 a* Cut .(M{c:=(y).P}) (x1).(P[y⊨ n>x1])" proof (cases "fin P y" )case True assume "fin P y" then show ?thesis using LOr1apply -apply (rule a_starI)apply (rule better_CutR_intro)apply (rule al_redu)apply (rule better_LAxL_intro)apply (simp)done next case False assume "¬ fin P y" then show ?thesisapply -apply (rule a_star_CutR)apply (rule rtranclp_trans)apply (rule a_starI)apply (rule ac_redu)apply (rule better_right)apply (simp)apply (simp add: subst_with_ax1)done qed also have "… = (Cut .M (x1).N1){c:=(y).P}" using LOr1 asmapply -apply (auto simp add: subst_fresh abs_fresh)apply (simp add: trm.inject)apply (simp add: alpha fresh_atm)apply (rule sym)apply (rule nrename_swap)apply (simp)done finally have "(Cut .OrR1 .M b (z).OrL (x1).N1 (x2).N2 z){c:=(y).P} ⟶ 🪙 a* (Cut .M (x1).N1){c:=(y).P}" by simpultimately show ?thesis by blastqed next case (LOr2 b a M N1 N2 z x1 x2 y c P)then show ?case proof -assume asm: "N2≠ Ax x2 c" have "(Cut .OrR2 .M b (z).OrL (x1).N1 (x2).N2 z){c:=(y).P} = Cut .OrR2 .(M{c:=(y).P}) b (z).OrL (x1).(N1{c:=(y).P}) (x2).(N2{c:=(y).P}) z" using LOr2 by (simp add: subst_fresh abs_fresh fresh_atm)also have "… ⟶ 🪙 a* Cut .(M{c:=(y).P}) (x2).(N2{c:=(y).P})" using LOr2apply -apply (rule a_starI)apply (rule al_redu)apply (auto intro: l_redu.intros simp add: subst_fresh abs_fresh)done also have "… = (Cut .M (x2).N2){c:=(y).P}" using LOr2 asmby (simp add: subst_fresh abs_fresh fresh_atm)finally have "(Cut .OrR2 .M b (z).OrL (x1).N1 (x2).N2 z){c:=(y).P} ⟶ 🪙 a* (Cut .M (x2).N2){c:=(y).P}" by simpmoreover assume asm: "N2=Ax x2 c" have "(Cut .OrR2 .M b (z).OrL (x1).N1 (x2).N2 z){c:=(y).P} = Cut .OrR2 .(M{c:=(y).P}) b (z).OrL (x1).(N1{c:=(y).P}) (x2).(N2{c:=(y).P}) z" using LOr2 by (simp add: subst_fresh abs_fresh fresh_atm)also have "… ⟶ 🪙 a* Cut .(M{c:=(y).P}) (x2).(N2{c:=(y).P})" using LOr2apply -apply (rule a_starI)apply (rule al_redu)apply (auto intro: l_redu.intros simp add: subst_fresh abs_fresh)done also have "… = Cut .(M{c:=(y).P}) (x2).(Cut .(Ax x2 c) (y).P)" using LOr2 asm by simpalso have "… ⟶ 🪙 a* Cut .(M{c:=(y).P}) (x2).(P[y⊨ n>x2])" proof (cases "fin P y" )case True assume "fin P y" then show ?thesis using LOr2apply -apply (rule a_starI)apply (rule better_CutR_intro)apply (rule al_redu)apply (rule better_LAxL_intro)apply (simp)done next case False assume "¬ fin P y" then show ?thesisapply -apply (rule a_star_CutR)apply (rule rtranclp_trans)apply (rule a_starI)apply (rule ac_redu)apply (rule better_right)apply (simp)apply (simp add: subst_with_ax1)done qed also have "… = (Cut .M (x2).N2){c:=(y).P}" using LOr2 asmapply -apply (auto simp add: subst_fresh abs_fresh)apply (simp add: trm.inject)apply (simp add: alpha fresh_atm)apply (rule sym)apply (rule nrename_swap)apply (simp)done finally have "(Cut .OrR2 .M b (z).OrL (x1).N1 (x2).N2 z){c:=(y).P} ⟶ 🪙 a* (Cut .M (x2).N2){c:=(y).P}" by simpultimately show ?thesis by blastqed next case (LImp z N u Q x M b a d y c P)then show ?case proof -assume asm: "M≠ Ax x c ∧ Q≠ Ax u c" have "(Cut .ImpR (x)..M b (z).ImpL .N (u).Q z){c:=(y).P} = Cut .ImpR (x)..(M{c:=(y).P}) b (z).ImpL .(N{c:=(y).P}) (u).(Q{c:=(y).P}) z" using LImp by (simp add: fresh_prod abs_fresh fresh_atm)also have "… ⟶ 🪙 a* Cut .(Cut .(N{c:=(y).P}) (x).(M{c:=(y).P})) (u).(Q{c:=(y).P})" using LImpapply -apply (rule a_starI)apply (rule al_redu)apply (auto intro: l_redu.intros simp add: subst_fresh abs_fresh)done also have "… = (Cut .(Cut .N (x).M) (u).Q){c:=(y).P}" using LImp asmby (simp add: subst_fresh abs_fresh fresh_atm)finally have "(Cut .ImpR (x)..M b (z).ImpL .N (u).Q z){c:=(y).P} ⟶ 🪙 a* (Cut .(Cut .N (x).M) (u).Q){c:=(y).P}" by simpmoreover assume asm: "M=Ax x c ∧ Q≠ Ax u c" have "(Cut .ImpR (x)..M b (z).ImpL .N (u).Q z){c:=(y).P} = Cut .ImpR (x)..(M{c:=(y).P}) b (z).ImpL .(N{c:=(y).P}) (u).(Q{c:=(y).P}) z" using LImp by (simp add: subst_fresh abs_fresh fresh_atm fresh_prod)also have "… ⟶ 🪙 a* Cut .(Cut .(N{c:=(y).P}) (x).(M{c:=(y).P})) (u).(Q{c:=(y).P})" using LImpapply -apply (rule a_starI)apply (rule al_redu)apply (auto intro: l_redu.intros simp add: subst_fresh abs_fresh)done also have "… = Cut .(Cut .(N{c:=(y).P}) (x).(Cut .Ax x c (y).P)) (u).(Q{c:=(y).P})" using LImp asm by simpalso have "… ⟶ 🪙 a* Cut .(Cut .(N{c:=(y).P}) (x).(P[y⊨ n>x])) (u).(Q{c:=(y).P})" proof (cases "fin P y" )case True assume "fin P y" then show ?thesis using LImpapply -apply (rule a_star_CutL)apply (rule a_star_CutR)apply (rule rtranclp_trans)apply (rule a_starI)apply (rule al_redu)apply (rule better_LAxL_intro)apply (simp)apply (simp)done next case False assume "¬ fin P y" then show ?thesis using LImpapply -apply (rule a_star_CutL)apply (rule a_star_CutR)apply (rule rtranclp_trans)apply (rule a_starI)apply (rule ac_redu)apply (rule better_right)apply (simp)apply (simp add: subst_with_ax1)done qed also have "… = (Cut .(Cut .N (x).M) (u).Q){c:=(y).P}" using LImp asmapply -apply (auto simp add: subst_fresh abs_fresh)apply (simp add: trm.inject)apply (simp add: alpha fresh_atm)apply (simp add: trm.inject)apply (simp add: alpha)apply (simp add: nrename_swap)done finally have "(Cut .ImpR (x)..M b (z).ImpL .N (u).Q z){c:=(y).P} ⟶ 🪙 a* (Cut .(Cut .N (x).M) (u).Q){c:=(y).P}" by simpmoreover assume asm: "M≠ Ax x c ∧ Q=Ax u c" have "(Cut .ImpR (x)..M b (z).ImpL .N (u).Q z){c:=(y).P} = Cut .ImpR (x)..(M{c:=(y).P}) b (z).ImpL .(N{c:=(y).P}) (u).(Q{c:=(y).P}) z" using LImp by (simp add: subst_fresh abs_fresh fresh_atm fresh_prod)also have "… ⟶ 🪙 a* Cut .(Cut .(N{c:=(y).P}) (x).(M{c:=(y).P})) (u).(Q{c:=(y).P})" using LImpapply -apply (rule a_starI)apply (rule al_redu)apply (auto intro: l_redu.intros simp add: subst_fresh abs_fresh)done also have "… = Cut .(Cut .(N{c:=(y).P}) (x).(M{c:=(y).P})) (u).(Cut .Ax u c (y).P)" using LImp asm by simpalso have "… ⟶ 🪙 a* Cut .(Cut .(N{c:=(y).P}) (x).(M{c:=(y).P})) (u).(P[y⊨ n>u])" proof (cases "fin P y" )case True assume "fin P y" then show ?thesis using LImpapply -apply (rule a_star_CutR)apply (rule a_starI)apply (rule al_redu)apply (rule better_LAxL_intro)apply (simp)done next case False assume "¬ fin P y" then show ?thesis using LImpapply -apply (rule a_star_CutR)apply (rule rtranclp_trans)apply (rule a_starI)apply (rule ac_redu)apply (rule better_right)apply (simp)apply (simp add: subst_with_ax1)done qed also have "… = (Cut .(Cut .N (x).M) (u).Q){c:=(y).P}" using LImp asmapply -apply (auto simp add: subst_fresh abs_fresh)apply (simp add: trm.inject)apply (simp add: alpha fresh_atm)apply (simp add: nrename_swap)done finally have "(Cut .ImpR (x)..M b (z).ImpL .N (u).Q z){c:=(y).P} ⟶ 🪙 a* (Cut .(Cut .N (x).M) (u).Q){c:=(y).P}" by simpmoreover assume asm: "M=Ax x c ∧ Q=Ax u c" have "(Cut .ImpR (x)..M b (z).ImpL .N (u).Q z){c:=(y).P} = Cut .ImpR (x)..(M{c:=(y).P}) b (z).ImpL .(N{c:=(y).P}) (u).(Q{c:=(y).P}) z" using LImp by (simp add: subst_fresh abs_fresh fresh_atm fresh_prod)also have "… ⟶ 🪙 a* Cut .(Cut .(N{c:=(y).P}) (x).(M{c:=(y).P})) (u).(Q{c:=(y).P})" using LImpapply -apply (rule a_starI)apply (rule al_redu)apply (auto intro: l_redu.intros simp add: subst_fresh abs_fresh)done also have "… = Cut .(Cut .(N{c:=(y).P}) (x).(Cut .Ax x c (y).P)) (u).(Cut .Ax u c (y).P)" using LImp asm by simpalso have "… ⟶ 🪙 a* Cut .(Cut .(N{c:=(y).P}) (x).(Cut .Ax x c (y).P)) (u).(P[y⊨ n>u])" proof (cases "fin P y" )case True assume "fin P y" then show ?thesis using LImpapply -apply (rule a_star_CutR)apply (rule a_starI)apply (rule al_redu)apply (rule better_LAxL_intro)apply (simp)done next case False assume "¬ fin P y" then show ?thesis using LImpapply -apply (rule a_star_CutR)apply (rule rtranclp_trans)apply (rule a_starI)apply (rule ac_redu)apply (rule better_right)apply (simp)apply (simp add: subst_with_ax1)done qed also have "… ⟶ 🪙 a* Cut .(Cut .(N{c:=(y).P}) (x).(P[y⊨ n>x])) (u).(P[y⊨ n>u])" proof (cases "fin P y" )case True assume "fin P y" then show ?thesis using LImpapply -apply (rule a_star_CutL)apply (rule a_star_CutR)apply (rule a_starI)apply (rule al_redu)apply (rule better_LAxL_intro)apply (simp)done next case False assume "¬ fin P y" then show ?thesis using LImpapply -apply (rule a_star_CutL)apply (rule a_star_CutR)apply (rule rtranclp_trans)apply (rule a_starI)apply (rule ac_redu)apply (rule better_right)apply (simp)apply (simp add: subst_with_ax1)done qed also have "… = (Cut .(Cut .N (x).M) (u).Q){c:=(y).P}" using LImp asmapply -apply (auto simp add: subst_fresh abs_fresh)apply (simp add: trm.inject)apply (rule conjI)apply (simp add: alpha fresh_atm trm.inject)apply (simp add: nrename_swap)apply (simp add: alpha fresh_atm trm.inject)apply (simp add: nrename_swap)done finally have "(Cut .ImpR (x)..M b (z).ImpL .N (u).Q z){c:=(y).P} ⟶ 🪙 a* (Cut .(Cut .N (x).M) (u).Q){c:=(y).P}" by simpultimately show ?thesis by blastqed qed lemma a_redu_subst1:assumes a: "M ⟶ 🪙 a M'" shows "M{y:=.P} ⟶ 🪙 a* M'{y:=.P}" using aproof (nominal_induct avoiding: y c P rule: a_redu.strong_induct)case al_reduthen show ?case by (simp only: l_redu_subst1)next case ac_reduthen show ?case apply -apply (rule a_starI)apply (rule a_redu.ac_redu)apply (simp only: c_redu_subst1')done next case (a_Cut_l a N x M M' y c P)then show ?case apply (simp add: subst_fresh fresh_a_redu)apply (rule conjI)apply (rule impI)+apply (simp)apply (drule ax_do_not_a_reduce)apply (simp)apply (rule impI)apply (rule conjI)apply (rule impI)apply (simp)apply (drule_tac x="y" in meta_spec)apply (drule_tac x="c" in meta_spec)apply (drule_tac x="P" in meta_spec)apply (simp)apply (rule rtranclp_trans)apply (rule a_star_CutL)apply (assumption)apply (rule rtranclp_trans)apply (rule_tac M'="P[c⊨ c>a]" in a_star_CutL)apply (case_tac "fic P c" )apply (rule a_starI)apply (rule al_redu)apply (rule better_LAxR_intro)apply (simp)apply (rule rtranclp_trans)apply (rule a_starI)apply (rule ac_redu)apply (rule better_left)apply (simp)apply (rule subst_with_ax2)apply (rule aux4)apply (simp add: trm.inject)apply (simp add: alpha fresh_atm)apply (simp add: crename_swap)apply (rule impI)apply (rule a_star_CutL)apply (auto)done next case (a_Cut_r a N x M M' y c P)then show ?case apply (auto simp add: subst_fresh fresh_a_redu)apply (rule a_star_CutR)apply (auto)[1]apply (rule a_star_CutR)apply (auto)[1]done next case a_NotLthen show ?case apply (auto)apply (generate_fresh "name" )apply (fresh_fun_simp)apply (fresh_fun_simp)apply (simp add: subst_fresh)apply (rule a_star_CutR)apply (rule a_star_NotL)apply (auto)[1]apply (rule a_star_NotL)apply (auto)[1]done next case a_NotRthen show ?case apply (auto)apply (rule a_star_NotR)apply (auto)[1]done next case a_AndR_lthen show ?case apply (auto simp add: subst_fresh fresh_a_redu)apply (rule a_star_AndR)apply (auto)done next case a_AndR_rthen show ?case apply (auto simp add: subst_fresh fresh_a_redu)apply (rule a_star_AndR)apply (auto)done next case a_AndL1then show ?case apply (auto)apply (generate_fresh "name" )apply (fresh_fun_simp)apply (fresh_fun_simp)apply (simp add: subst_fresh)apply (rule a_star_CutR)apply (rule a_star_AndL1)apply (auto)[1]apply (rule a_star_AndL1)apply (auto)[1]done next case a_AndL2then show ?case apply (auto)apply (generate_fresh "name" )apply (fresh_fun_simp)apply (fresh_fun_simp)apply (simp add: subst_fresh)apply (rule a_star_CutR)apply (rule a_star_AndL2)apply (auto)[1]apply (rule a_star_AndL2)apply (auto)[1]done next case a_OrR1then show ?case apply (auto simp add: subst_fresh fresh_a_redu)apply (rule a_star_OrR1)apply (auto)done next case a_OrR2then show ?case apply (auto simp add: subst_fresh fresh_a_redu)apply (rule a_star_OrR2)apply (auto)done next case a_OrL_lthen show ?case apply (auto simp add: subst_fresh fresh_a_redu)apply (generate_fresh "name" )apply (fresh_fun_simp)apply (fresh_fun_simp)apply (simp add: subst_fresh)apply (rule a_star_CutR)apply (rule a_star_OrL)apply (auto)apply (rule a_star_OrL)apply (auto)done next case a_OrL_rthen show ?case apply (auto simp add: subst_fresh fresh_a_redu)apply (generate_fresh "name" )apply (fresh_fun_simp)apply (fresh_fun_simp)apply (simp add: subst_fresh)apply (rule a_star_CutR)apply (rule a_star_OrL)apply (auto)apply (rule a_star_OrL)apply (auto)done next case a_ImpRthen show ?case apply (auto simp add: subst_fresh fresh_a_redu)apply (rule a_star_ImpR)apply (auto)done next case a_ImpL_rthen show ?case apply (auto simp add: subst_fresh fresh_a_redu)apply (generate_fresh "name" )apply (fresh_fun_simp)apply (fresh_fun_simp)apply (simp add: subst_fresh)apply (rule a_star_CutR)apply (rule a_star_ImpL)apply (auto)apply (rule a_star_ImpL)apply (auto)done next case a_ImpL_lthen show ?case apply (auto simp add: subst_fresh fresh_a_redu)apply (generate_fresh "name" )apply (fresh_fun_simp)apply (fresh_fun_simp)apply (simp add: subst_fresh)apply (rule a_star_CutR)apply (rule a_star_ImpL)apply (auto)apply (rule a_star_ImpL)apply (auto)done qed lemma a_redu_subst2:assumes a: "M ⟶ 🪙 a M'" shows "M{c:=(y).P} ⟶ 🪙 a* M'{c:=(y).P}" using aproof (nominal_induct avoiding: y c P rule: a_redu.strong_induct)case al_reduthen show ?case by (simp only: l_redu_subst2)next case ac_reduthen show ?case apply -apply (rule a_starI)apply (rule a_redu.ac_redu)apply (simp only: c_redu_subst2')done next case (a_Cut_r a N x M M' y c P)then show ?case apply (simp add: subst_fresh fresh_a_redu)apply (rule conjI)apply (rule impI)+apply (simp)apply (drule ax_do_not_a_reduce)apply (simp)apply (rule impI)apply (rule conjI)apply (rule impI)apply (simp)apply (drule_tac x="c" in meta_spec)apply (drule_tac x="y" in meta_spec)apply (drule_tac x="P" in meta_spec)apply (simp)apply (rule rtranclp_trans)apply (rule a_star_CutR)apply (assumption)apply (rule rtranclp_trans)apply (rule_tac N'="P[y⊨ n>x]" in a_star_CutR)apply (case_tac "fin P y" )apply (rule a_starI)apply (rule al_redu)apply (rule better_LAxL_intro)apply (simp)apply (rule rtranclp_trans)apply (rule a_starI)apply (rule ac_redu)apply (rule better_right)apply (simp)apply (rule subst_with_ax1)apply (rule aux4)apply (simp add: trm.inject)apply (simp add: alpha fresh_atm)apply (simp add: nrename_swap)apply (rule impI)apply (rule a_star_CutR)apply (auto)done next case (a_Cut_l a N x M M' y c P)then show ?case apply (auto simp add: subst_fresh fresh_a_redu)apply (rule a_star_CutL)apply (auto)[1]apply (rule a_star_CutL)apply (auto)[1]done next case a_NotRthen show ?case apply (auto)apply (generate_fresh "coname" )apply (fresh_fun_simp)apply (fresh_fun_simp)apply (simp add: subst_fresh)apply (rule a_star_CutL)apply (rule a_star_NotR)apply (auto)[1]apply (rule a_star_NotR)apply (auto)[1]done next case a_NotLthen show ?case apply (auto)apply (rule a_star_NotL)apply (auto)[1]done next case a_AndR_lthen show ?case apply (auto simp add: subst_fresh fresh_a_redu)apply (generate_fresh "coname" )apply (fresh_fun_simp)apply (fresh_fun_simp)apply (simp add: subst_fresh)apply (rule a_star_CutL)apply (rule a_star_AndR)apply (auto)apply (rule a_star_AndR)apply (auto)done next case a_AndR_rthen show ?case apply (auto simp add: subst_fresh fresh_a_redu)apply (generate_fresh "coname" )apply (fresh_fun_simp)apply (fresh_fun_simp)apply (simp add: subst_fresh)apply (rule a_star_CutL)apply (rule a_star_AndR)apply (auto)apply (rule a_star_AndR)apply (auto)done next case a_AndL1then show ?case apply (auto simp add: subst_fresh fresh_a_redu)apply (rule a_star_AndL1)apply (auto)done next case a_AndL2then show ?case apply (auto simp add: subst_fresh fresh_a_redu)apply (rule a_star_AndL2)apply (auto)done next case a_OrR1then show ?case apply (auto)apply (generate_fresh "coname" )apply (fresh_fun_simp)apply (fresh_fun_simp)apply (simp add: subst_fresh)apply (rule a_star_CutL)apply (rule a_star_OrR1)apply (auto)[1]apply (rule a_star_OrR1)apply (auto)[1]done next case a_OrR2then show ?case apply (auto)apply (generate_fresh "coname" )apply (fresh_fun_simp)apply (fresh_fun_simp)apply (simp add: subst_fresh)apply (rule a_star_CutL)apply (rule a_star_OrR2)apply (auto)[1]apply (rule a_star_OrR2)apply (auto)[1]done next case a_OrL_lthen show ?case apply (auto simp add: subst_fresh fresh_a_redu)apply (rule a_star_OrL)apply (auto)done next case a_OrL_rthen show ?case apply (auto simp add: subst_fresh fresh_a_redu)apply (rule a_star_OrL)apply (auto)done next case a_ImpRthen show ?case apply (auto simp add: subst_fresh fresh_a_redu)apply (generate_fresh "coname" )apply (fresh_fun_simp)apply (fresh_fun_simp)apply (simp add: subst_fresh)apply (rule a_star_CutL)apply (rule a_star_ImpR)apply (auto)apply (rule a_star_ImpR)apply (auto)done next case a_ImpL_lthen show ?case apply (auto simp add: subst_fresh fresh_a_redu)apply (rule a_star_ImpL)apply (auto)done next case a_ImpL_rthen show ?case apply (auto simp add: subst_fresh fresh_a_redu)apply (rule a_star_ImpL)apply (auto)done qed lemma a_star_subst1:assumes a: "M ⟶ 🪙 a* M'" shows "M{y:=.P} ⟶ 🪙 a* M'{y:=.P}" using aapply (induct)apply (blast)apply (drule_tac y="y" and c="c" and P="P" in a_redu_subst1)apply (auto)done lemma a_star_subst2:assumes a: "M ⟶ 🪙 a* M'" shows "M{c:=(y).P} ⟶ 🪙 a* M'{c:=(y).P}" using aapply (induct)apply (blast)apply (drule_tac y="y" and c="c" and P="P" in a_redu_subst2)apply (auto)done text ‹ Candidates and SN› text ‹ SNa› inductive "trm ==> where "(∧ ⟶ 🪙 a M' ==> SNa M') ==> SNa M" lemma SNa_induct[consumes 1]:assumes major: "SNa M" assumes hyp: "∧ ==> (∀ M''. M'⟶ 🪙 a M'' ⟶ P M'' ==> P M')" shows "P M" apply (rule major[THEN SNa.induct])apply (rule hyp)apply (rule SNaI)apply (blast)+done lemma double_SNa_aux:assumes a_SNa: "SNa a" and b_SNa: "SNa b" and hyp: "∧ (∧ ⟶ 🪙 a y ==> SNa y) ==> (∧ ⟶ 🪙 a y ==> P y z) ==> (∧ ⟶ 🪙 a u ==> SNa u) ==> (∧ ⟶ 🪙 a u ==> P x u) ==> P x z" shows "P a b" proof -from a_SNahave r: "∧ ==> P a b" proof (induct a rule: SNa.induct)case (SNaI x)note SNa' = thishave "SNa b" by factthus ?case proof (induct b rule: SNa.induct)case (SNaI y)show ?case apply (rule hyp)apply (erule SNa')apply (erule SNa')apply (rule SNa.SNaI)apply (erule SNaI)+done qed qed from b_SNa show ?thesis by (rule r)qed lemma double_SNa:"[ SNa a; SNa b; ∀ x z. ((∀ y. x⟶ 🪙 ay ⟶ P y z) ∧ (∀ u. z⟶ 🪙 a u ⟶ P x u)) ⟶ P x z] ==> P a b" apply (rule_tac double_SNa_aux)apply (assumption)+apply (blast)done lemma a_preserves_SNa:assumes a: "SNa M" "M⟶ 🪙 a M'" shows "SNa M'" using a by (erule_tac SNa.cases) (simp)lemma a_star_preserves_SNa:assumes a: "SNa M" and b: "M⟶ 🪙 a* M'" shows "SNa M'" using b aby (induct) (auto simp add: a_preserves_SNa)lemma Ax_in_SNa:shows "SNa (Ax x a)" apply (rule SNaI)apply (erule a_redu.cases, auto)apply (erule l_redu.cases, auto)apply (erule c_redu.cases, auto)done lemma NotL_in_SNa:assumes a: "SNa M" shows "SNa (NotL .M x)" using aapply (induct)apply (rule SNaI)apply (erule a_redu.cases, auto)apply (erule l_redu.cases, auto)apply (erule c_redu.cases, auto)apply (auto simp add: trm.inject alpha)apply (rotate_tac 1)apply (drule_tac x="[(a,aa)]∙ M'a" in meta_spec)apply (simp add: a_redu.eqvt)apply (subgoal_tac "NotL .([(a,aa)]∙ M'a) x = NotL .M'a x" )apply (simp)apply (simp add: trm.inject alpha fresh_a_redu)done lemma NotR_in_SNa:assumes a: "SNa M" shows "SNa (NotR (x).M a)" using aapply (induct)apply (rule SNaI)apply (erule a_redu.cases, auto)apply (erule l_redu.cases, auto)apply (erule c_redu.cases, auto)apply (auto simp add: trm.inject alpha)apply (rotate_tac 1)apply (drule_tac x="[(x,xa)]∙ M'a" in meta_spec)apply (simp add: a_redu.eqvt)apply (rule_tac s="NotR (x).([(x,xa)]∙ M'a) a" in subst)apply (simp add: trm.inject alpha fresh_a_redu)apply (simp)done lemma AndL1_in_SNa:assumes a: "SNa M" shows "SNa (AndL1 (x).M y)" using aapply (induct)apply (rule SNaI)apply (erule a_redu.cases, auto)apply (erule l_redu.cases, auto)apply (erule c_redu.cases, auto)apply (auto simp add: trm.inject alpha)apply (rotate_tac 1)apply (drule_tac x="[(x,xa)]∙ M'a" in meta_spec)apply (simp add: a_redu.eqvt)apply (rule_tac s="AndL1 x.([(x,xa)]∙ M'a) y" in subst)apply (simp add: trm.inject alpha fresh_a_redu)apply (simp)done lemma AndL2_in_SNa:assumes a: "SNa M" shows "SNa (AndL2 (x).M y)" using aapply (induct)apply (rule SNaI)apply (erule a_redu.cases, auto)apply (erule l_redu.cases, auto)apply (erule c_redu.cases, auto)apply (auto simp add: trm.inject alpha)apply (rotate_tac 1)apply (drule_tac x="[(x,xa)]∙ M'a" in meta_spec)apply (simp add: a_redu.eqvt)apply (rule_tac s="AndL2 x.([(x,xa)]∙ M'a) y" in subst)apply (simp add: trm.inject alpha fresh_a_redu)apply (simp)done lemma OrR1_in_SNa:assumes a: "SNa M" shows "SNa (OrR1 .M b)" using aapply (induct)apply (rule SNaI)apply (erule a_redu.cases, auto)apply (erule l_redu.cases, auto)apply (erule c_redu.cases, auto)apply (auto simp add: trm.inject alpha)apply (rotate_tac 1)apply (drule_tac x="[(a,aa)]∙ M'a" in meta_spec)apply (simp add: a_redu.eqvt)apply (rule_tac s="OrR1 .([(a,aa)]∙ M'a) b" in subst)apply (simp add: trm.inject alpha fresh_a_redu)apply (simp)done lemma OrR2_in_SNa:assumes a: "SNa M" shows "SNa (OrR2 .M b)" using aapply (induct)apply (rule SNaI)apply (erule a_redu.cases, auto)apply (erule l_redu.cases, auto)apply (erule c_redu.cases, auto)apply (auto simp add: trm.inject alpha)apply (rotate_tac 1)apply (drule_tac x="[(a,aa)]∙ M'a" in meta_spec)apply (simp add: a_redu.eqvt)apply (rule_tac s="OrR2 .([(a,aa)]∙ M'a) b" in subst)apply (simp add: trm.inject alpha fresh_a_redu)apply (simp)done lemma ImpR_in_SNa:assumes a: "SNa M" shows "SNa (ImpR (x)..M b)" using aapply (induct)apply (rule SNaI)apply (erule a_redu.cases, auto)apply (erule l_redu.cases, auto)apply (erule c_redu.cases, auto)apply (auto simp add: trm.inject alpha abs_fresh abs_perm calc_atm)apply (rotate_tac 1)apply (drule_tac x="[(a,aa)]∙ M'a" in meta_spec)apply (simp add: a_redu.eqvt)apply (rule_tac s="ImpR (x)..([(a,aa)]∙ M'a) b" in subst)apply (simp add: trm.inject alpha fresh_a_redu)apply (simp)apply (rotate_tac 1)apply (drule_tac x="[(x,xa)]∙ M'a" in meta_spec)apply (simp add: a_redu.eqvt)apply (rule_tac s="ImpR (x)..([(x,xa)]∙ M'a) b" in subst)apply (simp add: trm.inject alpha fresh_a_redu abs_fresh abs_perm calc_atm)apply (simp)apply (rotate_tac 1)apply (drule_tac x="[(a,aa)]∙ [(x,xa)]∙ M'a" in meta_spec)apply (simp add: a_redu.eqvt)apply (rule_tac s="ImpR (x)..([(a,aa)]∙ [(x,xa)]∙ M'a) b" in subst)apply (simp add: trm.inject alpha fresh_a_redu abs_fresh abs_perm calc_atm)apply (simp add: fresh_left calc_atm fresh_a_redu)apply (simp)done lemma AndR_in_SNa:assumes a: "SNa M" "SNa N" shows "SNa (AndR .M .N c)" apply (rule_tac a="M" and b="N" in double_SNa)apply (rule a)+apply (auto)apply (rule SNaI)apply (drule a_redu_AndR_elim)apply (auto)done lemma OrL_in_SNa:assumes a: "SNa M" "SNa N" shows "SNa (OrL (x).M (y).N z)" apply (rule_tac a="M" and b="N" in double_SNa)apply (rule a)+apply (auto)apply (rule SNaI)apply (drule a_redu_OrL_elim)apply (auto)done lemma ImpL_in_SNa:assumes a: "SNa M" "SNa N" shows "SNa (ImpL .M (y).N z)" apply (rule_tac a="M" and b="N" in double_SNa)apply (rule a)+apply (auto)apply (rule SNaI)apply (drule a_redu_ImpL_elim)apply (auto)done lemma SNa_eqvt:fixes pi1::"name prm" and pi2::"coname prm" shows "SNa M ==> SNa (pi1∙ M)" and "SNa M ==> SNa (pi2∙ M)" apply -apply (induct rule: SNa.induct)apply (rule SNaI)apply (drule_tac pi="(rev pi1)" in a_redu.eqvt(1))apply (rotate_tac 1)apply (drule_tac x="(rev pi1)∙ M'" in meta_spec)apply (perm_simp)apply (induct rule: SNa.induct)apply (rule SNaI)apply (drule_tac pi="(rev pi2)" in a_redu.eqvt(2))apply (rotate_tac 1)apply (drule_tac x="(rev pi2)∙ M'" in meta_spec)apply (perm_simp)done text ‹ set operators› definition AXIOMSn :: "ty ==> where "AXIOMSn B ≡ { (x):(Ax y b) | x y b. True }" definition AXIOMSc::"ty ==> where "AXIOMSc B ≡ { :(Ax y b) | a y b. True }" definition BINDINGn::"ty ==> ==> where "BINDINGn B X ≡ { (x):M | x M. ∀ a P. :P∈ X ⟶ SNa (M{x:= .P})}" definition BINDINGc::"ty ==> ==> where "BINDINGc B X ≡ { :M | a M. ∀ x P. (x):P∈ X ⟶ SNa (M{a:=(x).P})}" lemma BINDINGn_decreasing:shows "X⊆ Y ==> BINDINGn B Y ⊆ BINDINGn B X" by (simp add: BINDINGn_def) (blast) lemma BINDINGc_decreasing:shows "X⊆ Y ==> BINDINGc B Y ⊆ BINDINGc B X" by (simp add: BINDINGc_def) (blast) nominal_primrec "ty ==> ==> where "NOTRIGHT (NOT B) X = { :NotR (x).M a | a x M. fic (NotR (x).M a) a ∧ (x):M ∈ X }" apply (rule TrueI)+done lemma NOTRIGHT_eqvt_name:fixes pi::"name prm" shows "(pi∙ (NOTRIGHT (NOT B) X)) = NOTRIGHT (NOT B) (pi∙ X)" apply (auto simp add: perm_set_def)apply (rule_tac x="pi∙ a" in exI) apply (rule_tac x="pi∙ xb" in exI) apply (rule_tac x="pi∙ M" in exI)apply (simp)apply (rule conjI)apply (drule_tac pi="pi" in fic.eqvt(1))apply (simp)apply (rule_tac x="(xb):M" in exI)apply (simp)apply (rule_tac x="(rev pi)∙ (:NotR (xa).M a)" in exI)apply (perm_simp)apply (rule_tac x="(rev pi)∙ a" in exI) apply (rule_tac x="(rev pi)∙ xa" in exI) apply (rule_tac x="(rev pi)∙ M" in exI)apply (simp add: swap_simps)apply (drule_tac pi="rev pi" in fic.eqvt(1))apply (simp)apply (drule sym)apply (drule pt_bij1[OF pt_name_inst, OF at_name_inst])apply (simp add: swap_simps)done lemma NOTRIGHT_eqvt_coname:fixes pi::"coname prm" shows "(pi∙ (NOTRIGHT (NOT B) X)) = NOTRIGHT (NOT B) (pi∙ X)" apply (auto simp add: perm_set_def)apply (rule_tac x="pi∙ a" in exI) apply (rule_tac x="pi∙ xb" in exI) apply (rule_tac x="pi∙ M" in exI)apply (simp)apply (rule conjI)apply (drule_tac pi="pi" in fic.eqvt(2))apply (simp)apply (rule_tac x="(xb):M" in exI)apply (simp)apply (rule_tac x="<((rev pi)∙ a)>:NotR ((rev pi)∙ xa).((rev pi)∙ M) ((rev pi)∙ a)" in exI)apply (perm_simp)apply (rule_tac x="(rev pi)∙ a" in exI) apply (rule_tac x="(rev pi)∙ xa" in exI) apply (rule_tac x="(rev pi)∙ M" in exI)apply (simp add: swap_simps)apply (drule_tac pi="rev pi" in fic.eqvt(2))apply (simp)apply (drule sym)apply (drule pt_bij1[OF pt_coname_inst, OF at_coname_inst])apply (simp add: swap_simps)done nominal_primrec "ty ==> ==> where "NOTLEFT (NOT B) X = { (x):NotL .M x | a x M. fin (NotL .M x) x ∧ :M ∈ X }" apply (rule TrueI)+done lemma NOTLEFT_eqvt_name:fixes pi::"name prm" shows "(pi∙ (NOTLEFT (NOT B) X)) = NOTLEFT (NOT B) (pi∙ X)" apply (auto simp add: perm_set_def)apply (rule_tac x="pi∙ a" in exI) apply (rule_tac x="pi∙ xb" in exI) apply (rule_tac x="pi∙ M" in exI)apply (simp)apply (rule conjI)apply (drule_tac pi="pi" in fin.eqvt(1))apply (simp)apply (rule_tac x=":M" in exI)apply (simp)apply (rule_tac x="(((rev pi)∙ xa)):NotL <((rev pi)∙ a)>.((rev pi)∙ M) ((rev pi)∙ xa)" in exI)apply (perm_simp)apply (rule_tac x="(rev pi)∙ a" in exI) apply (rule_tac x="(rev pi)∙ xa" in exI) apply (rule_tac x="(rev pi)∙ M" in exI)apply (simp add: swap_simps)apply (drule_tac pi="rev pi" in fin.eqvt(1))apply (simp)apply (drule sym)apply (drule pt_bij1[OF pt_name_inst, OF at_name_inst])apply (simp add: swap_simps)done lemma NOTLEFT_eqvt_coname:fixes pi::"coname prm" shows "(pi∙ (NOTLEFT (NOT B) X)) = NOTLEFT (NOT B) (pi∙ X)" apply (auto simp add: perm_set_def)apply (rule_tac x="pi∙ a" in exI) apply (rule_tac x="pi∙ xb" in exI) apply (rule_tac x="pi∙ M" in exI)apply (simp)apply (rule conjI)apply (drule_tac pi="pi" in fin.eqvt(2))apply (simp)apply (rule_tac x=":M" in exI)apply (simp)apply (rule_tac x="(((rev pi)∙ xa)):NotL <((rev pi)∙ a)>.((rev pi)∙ M) ((rev pi)∙ xa)" in exI)apply (perm_simp)apply (rule_tac x="(rev pi)∙ a" in exI) apply (rule_tac x="(rev pi)∙ xa" in exI) apply (rule_tac x="(rev pi)∙ M" in exI)apply (simp add: swap_simps)apply (drule_tac pi="rev pi" in fin.eqvt(2))apply (simp)apply (drule sym)apply (drule pt_bij1[OF pt_coname_inst, OF at_coname_inst])apply (simp add: swap_simps)done nominal_primrec "ty ==> ==> ==> where "ANDRIGHT (B AND C) X Y = { :AndR .M .N c | c a b M N. fic (AndR .M .N c) c ∧ :M ∈ X ∧ :N ∈ Y }" apply (rule TrueI)+done lemma ANDRIGHT_eqvt_name:fixes pi::"name prm" shows "(pi∙ (ANDRIGHT (A AND B) X Y)) = ANDRIGHT (A AND B) (pi∙ X) (pi∙ Y)" apply (auto simp add: perm_set_def)apply (rule_tac x="pi∙ c" in exI)apply (rule_tac x="pi∙ a" in exI)apply (rule_tac x="pi∙ b" in exI)apply (rule_tac x="pi∙ M" in exI)apply (rule_tac x="pi∙ N" in exI)apply (simp)apply (rule conjI)apply (drule_tac pi="pi" in fic.eqvt(1))apply (simp)apply (rule conjI)apply (rule_tac x=":M" in exI)apply (simp)apply (rule_tac x=":N" in exI)apply (simp)apply (rule_tac x="(rev pi)∙ (:AndR .M .N c)" in exI)apply (perm_simp)apply (rule_tac x="(rev pi)∙ c" in exI)apply (rule_tac x="(rev pi)∙ a" in exI)apply (rule_tac x="(rev pi)∙ b" in exI)apply (rule_tac x="(rev pi)∙ M" in exI)apply (rule_tac x="(rev pi)∙ N" in exI)apply (simp add: swap_simps)apply (drule_tac pi="rev pi" in fic.eqvt(1))apply (simp)apply (drule sym)apply (drule sym)apply (drule pt_bij1[OF pt_name_inst, OF at_name_inst])apply (drule pt_bij1[OF pt_name_inst, OF at_name_inst])apply (simp add: swap_simps)done lemma ANDRIGHT_eqvt_coname:fixes pi::"coname prm" shows "(pi∙ (ANDRIGHT (A AND B) X Y)) = ANDRIGHT (A AND B) (pi∙ X) (pi∙ Y)" apply (auto simp add: perm_set_def)apply (rule_tac x="pi∙ c" in exI)apply (rule_tac x="pi∙ a" in exI)apply (rule_tac x="pi∙ b" in exI)apply (rule_tac x="pi∙ M" in exI)apply (rule_tac x="pi∙ N" in exI)apply (simp)apply (rule conjI)apply (drule_tac pi="pi" in fic.eqvt(2))apply (simp)apply (rule conjI)apply (rule_tac x=":M" in exI)apply (simp)apply (rule_tac x=":N" in exI)apply (simp)apply (rule_tac x="(rev pi)∙ (:AndR .M .N c)" in exI)apply (perm_simp)apply (rule_tac x="(rev pi)∙ c" in exI)apply (rule_tac x="(rev pi)∙ a" in exI)apply (rule_tac x="(rev pi)∙ b" in exI)apply (rule_tac x="(rev pi)∙ M" in exI)apply (rule_tac x="(rev pi)∙ N" in exI)apply (simp)apply (drule_tac pi="rev pi" in fic.eqvt(2))apply (simp)apply (drule sym)apply (drule sym)apply (drule pt_bij1[OF pt_coname_inst, OF at_coname_inst])apply (drule pt_bij1[OF pt_coname_inst, OF at_coname_inst])apply (simp)done nominal_primrec "ty ==> ==> where "ANDLEFT1 (B AND C) X = { (y):AndL1 (x).M y | x y M. fin (AndL1 (x).M y) y ∧ (x):M ∈ X }" apply (rule TrueI)+done lemma ANDLEFT1_eqvt_name:fixes pi::"name prm" shows "(pi∙ (ANDLEFT1 (A AND B) X)) = ANDLEFT1 (A AND B) (pi∙ X)" apply (auto simp add: perm_set_def)apply (rule_tac x="pi∙ xb" in exI) apply (rule_tac x="pi∙ y" in exI) apply (rule_tac x="pi∙ M" in exI)apply (simp)apply (rule conjI)apply (drule_tac pi="pi" in fin.eqvt(1))apply (simp)apply (rule_tac x="(xb):M" in exI)apply (simp)apply (rule_tac x="(rev pi)∙ ((y):AndL1 (xa).M y)" in exI)apply (perm_simp)apply (rule_tac x="(rev pi)∙ xa" in exI) apply (rule_tac x="(rev pi)∙ y" in exI) apply (rule_tac x="(rev pi)∙ M" in exI)apply (simp)apply (drule_tac pi="rev pi" in fin.eqvt(1))apply (simp)apply (drule sym)apply (drule pt_bij1[OF pt_name_inst, OF at_name_inst])apply (simp)done lemma ANDLEFT1_eqvt_coname:fixes pi::"coname prm" shows "(pi∙ (ANDLEFT1 (A AND B) X)) = ANDLEFT1 (A AND B) (pi∙ X)" apply (auto simp add: perm_set_def)apply (rule_tac x="pi∙ xb" in exI) apply (rule_tac x="pi∙ y" in exI) apply (rule_tac x="pi∙ M" in exI)apply (simp)apply (rule conjI)apply (drule_tac pi="pi" in fin.eqvt(2))apply (simp)apply (rule_tac x="(xb):M" in exI)apply (simp)apply (rule_tac x="(rev pi)∙ ((y):AndL1 (xa).M y)" in exI)apply (perm_simp)apply (rule_tac x="(rev pi)∙ xa" in exI) apply (rule_tac x="(rev pi)∙ y" in exI) apply (rule_tac x="(rev pi)∙ M" in exI)apply (simp add: swap_simps)apply (drule_tac pi="rev pi" in fin.eqvt(2))apply (simp)apply (drule sym)apply (drule pt_bij1[OF pt_coname_inst, OF at_coname_inst])apply (simp add: swap_simps)done nominal_primrec "ty ==> ==> where "ANDLEFT2 (B AND C) X = { (y):AndL2 (x).M y | x y M. fin (AndL2 (x).M y) y ∧ (x):M ∈ X }" apply (rule TrueI)+done lemma ANDLEFT2_eqvt_name:fixes pi::"name prm" shows "(pi∙ (ANDLEFT2 (A AND B) X)) = ANDLEFT2 (A AND B) (pi∙ X)" apply (auto simp add: perm_set_def)apply (rule_tac x="pi∙ xb" in exI) apply (rule_tac x="pi∙ y" in exI) apply (rule_tac x="pi∙ M" in exI)apply (simp)apply (rule conjI)apply (drule_tac pi="pi" in fin.eqvt(1))apply (simp)apply (rule_tac x="(xb):M" in exI)apply (simp)apply (rule_tac x="(rev pi)∙ ((y):AndL2 (xa).M y)" in exI)apply (perm_simp)apply (rule_tac x="(rev pi)∙ xa" in exI) apply (rule_tac x="(rev pi)∙ y" in exI) apply (rule_tac x="(rev pi)∙ M" in exI)apply (simp)apply (drule_tac pi="rev pi" in fin.eqvt(1))apply (simp)apply (drule sym)apply (drule pt_bij1[OF pt_name_inst, OF at_name_inst])apply (simp)done lemma ANDLEFT2_eqvt_coname:fixes pi::"coname prm" shows "(pi∙ (ANDLEFT2 (A AND B) X)) = ANDLEFT2 (A AND B) (pi∙ X)" apply (auto simp add: perm_set_def)apply (rule_tac x="pi∙ xb" in exI) apply (rule_tac x="pi∙ y" in exI) apply (rule_tac x="pi∙ M" in exI)apply (simp)apply (rule conjI)apply (drule_tac pi="pi" in fin.eqvt(2))apply (simp)apply (rule_tac x="(xb):M" in exI)apply (simp)apply (rule_tac x="(rev pi)∙ ((y):AndL2 (xa).M y)" in exI)apply (perm_simp)apply (rule_tac x="(rev pi)∙ xa" in exI) apply (rule_tac x="(rev pi)∙ y" in exI) apply (rule_tac x="(rev pi)∙ M" in exI)apply (simp add: swap_simps)apply (drule_tac pi="rev pi" in fin.eqvt(2))apply (simp)apply (drule sym)apply (drule pt_bij1[OF pt_coname_inst, OF at_coname_inst])apply (simp add: swap_simps)done nominal_primrec "ty ==> ==> ==> where "ORLEFT (B OR C) X Y = { (z):OrL (x).M (y).N z | x y z M N. fin (OrL (x).M (y).N z) z ∧ (x):M ∈ X ∧ (y):N ∈ Y }" apply (rule TrueI)+done lemma ORLEFT_eqvt_name:fixes pi::"name prm" shows "(pi∙ (ORLEFT (A OR B) X Y)) = ORLEFT (A OR B) (pi∙ X) (pi∙ Y)" apply (auto simp add: perm_set_def)apply (rule_tac x="pi∙ xb" in exI)apply (rule_tac x="pi∙ y" in exI)apply (rule_tac x="pi∙ z" in exI)apply (rule_tac x="pi∙ M" in exI)apply (rule_tac x="pi∙ N" in exI)apply (simp)apply (rule conjI)apply (drule_tac pi="pi" in fin.eqvt(1))apply (simp)apply (rule conjI)apply (rule_tac x="(xb):M" in exI)apply (simp)apply (rule_tac x="(y):N" in exI)apply (simp)apply (rule_tac x="(rev pi)∙ ((z):OrL (xa).M (y).N z)" in exI)apply (perm_simp)apply (rule_tac x="(rev pi)∙ xa" in exI)apply (rule_tac x="(rev pi)∙ y" in exI)apply (rule_tac x="(rev pi)∙ z" in exI)apply (rule_tac x="(rev pi)∙ M" in exI)apply (rule_tac x="(rev pi)∙ N" in exI)apply (simp)apply (drule_tac pi="rev pi" in fin.eqvt(1))apply (simp)apply (drule sym)apply (drule sym)apply (drule pt_bij1[OF pt_name_inst, OF at_name_inst])apply (drule pt_bij1[OF pt_name_inst, OF at_name_inst])apply (simp)done lemma ORLEFT_eqvt_coname:fixes pi::"coname prm" shows "(pi∙ (ORLEFT (A OR B) X Y)) = ORLEFT (A OR B) (pi∙ X) (pi∙ Y)" apply (auto simp add: perm_set_def)apply (rule_tac x="pi∙ xb" in exI)apply (rule_tac x="pi∙ y" in exI)apply (rule_tac x="pi∙ z" in exI)apply (rule_tac x="pi∙ M" in exI)apply (rule_tac x="pi∙ N" in exI)apply (simp)apply (rule conjI)apply (drule_tac pi="pi" in fin.eqvt(2))apply (simp)apply (rule conjI)apply (rule_tac x="(xb):M" in exI)apply (simp)apply (rule_tac x="(y):N" in exI)apply (simp)apply (rule_tac x="(rev pi)∙ ((z):OrL (xa).M (y).N z)" in exI)apply (perm_simp)apply (rule_tac x="(rev pi)∙ xa" in exI)apply (rule_tac x="(rev pi)∙ y" in exI)apply (rule_tac x="(rev pi)∙ z" in exI)apply (rule_tac x="(rev pi)∙ M" in exI)apply (rule_tac x="(rev pi)∙ N" in exI)apply (simp add: swap_simps)apply (drule_tac pi="rev pi" in fin.eqvt(2))apply (simp)apply (drule sym)apply (drule sym)apply (drule pt_bij1[OF pt_coname_inst, OF at_coname_inst])apply (drule pt_bij1[OF pt_coname_inst, OF at_coname_inst])apply (simp add: swap_simps)done nominal_primrec "ty ==> ==> where "ORRIGHT1 (B OR C) X = { :OrR1 .M b | a b M. fic (OrR1 .M b) b ∧ :M ∈ X }" apply (rule TrueI)+done lemma ORRIGHT1_eqvt_name:fixes pi::"name prm" shows "(pi∙ (ORRIGHT1 (A OR B) X)) = ORRIGHT1 (A OR B) (pi∙ X)" apply (auto simp add: perm_set_def)apply (rule_tac x="pi∙ a" in exI) apply (rule_tac x="pi∙ b" in exI) apply (rule_tac x="pi∙ M" in exI)apply (simp)apply (rule conjI)apply (drule_tac pi="pi" in fic.eqvt(1))apply (simp)apply (rule_tac x=":M" in exI)apply (perm_simp)apply (rule_tac x="(rev pi)∙ (:OrR1 .M b)" in exI)apply (perm_simp)apply (rule_tac x="(rev pi)∙ a" in exI) apply (rule_tac x="(rev pi)∙ b" in exI) apply (rule_tac x="(rev pi)∙ M" in exI)apply (simp add: swap_simps)apply (drule_tac pi="rev pi" in fic.eqvt(1))apply (simp)apply (drule sym)apply (drule pt_bij1[OF pt_name_inst, OF at_name_inst])apply (simp add: swap_simps)done lemma ORRIGHT1_eqvt_coname:fixes pi::"coname prm" shows "(pi∙ (ORRIGHT1 (A OR B) X)) = ORRIGHT1 (A OR B) (pi∙ X)" apply (auto simp add: perm_set_def)apply (rule_tac x="pi∙ a" in exI) apply (rule_tac x="pi∙ b" in exI) apply (rule_tac x="pi∙ M" in exI)apply (simp)apply (rule conjI)apply (drule_tac pi="pi" in fic.eqvt(2))apply (simp)apply (rule_tac x=":M" in exI)apply (perm_simp)apply (rule_tac x="(rev pi)∙ (:OrR1 .M b)" in exI)apply (perm_simp)apply (rule_tac x="(rev pi)∙ a" in exI) apply (rule_tac x="(rev pi)∙ b" in exI) apply (rule_tac x="(rev pi)∙ M" in exI)apply (simp)apply (drule_tac pi="rev pi" in fic.eqvt(2))apply (simp)apply (drule sym)apply (drule pt_bij1[OF pt_coname_inst, OF at_coname_inst])apply (simp)done nominal_primrec "ty ==> ==> where "ORRIGHT2 (B OR C) X = { :OrR2 .M b | a b M. fic (OrR2 .M b) b ∧ :M ∈ X }" apply (rule TrueI)+done lemma ORRIGHT2_eqvt_name:fixes pi::"name prm" shows "(pi∙ (ORRIGHT2 (A OR B) X)) = ORRIGHT2 (A OR B) (pi∙ X)" apply (auto simp add: perm_set_def)apply (rule_tac x="pi∙ a" in exI) apply (rule_tac x="pi∙ b" in exI) apply (rule_tac x="pi∙ M" in exI)apply (simp)apply (rule conjI)apply (drule_tac pi="pi" in fic.eqvt(1))apply (simp)apply (rule_tac x=":M" in exI)apply (perm_simp)apply (rule_tac x="(rev pi)∙ (:OrR2 .M b)" in exI)apply (perm_simp)apply (rule_tac x="(rev pi)∙ a" in exI) apply (rule_tac x="(rev pi)∙ b" in exI) apply (rule_tac x="(rev pi)∙ M" in exI)apply (simp add: swap_simps)apply (drule_tac pi="rev pi" in fic.eqvt(1))apply (simp)apply (drule sym)apply (drule pt_bij1[OF pt_name_inst, OF at_name_inst])apply (simp add: swap_simps)done lemma ORRIGHT2_eqvt_coname:fixes pi::"coname prm" shows "(pi∙ (ORRIGHT2 (A OR B) X)) = ORRIGHT2 (A OR B) (pi∙ X)" apply (auto simp add: perm_set_def)apply (rule_tac x="pi∙ a" in exI) apply (rule_tac x="pi∙ b" in exI) apply (rule_tac x="pi∙ M" in exI)apply (simp)apply (rule conjI)apply (drule_tac pi="pi" in fic.eqvt(2))apply (simp)apply (rule_tac x=":M" in exI)apply (perm_simp)apply (rule_tac x="(rev pi)∙ (:OrR2 .M b)" in exI)apply (perm_simp)apply (rule_tac x="(rev pi)∙ a" in exI) apply (rule_tac x="(rev pi)∙ b" in exI) apply (rule_tac x="(rev pi)∙ M" in exI)apply (simp)apply (drule_tac pi="rev pi" in fic.eqvt(2))apply (simp)apply (drule sym)apply (drule pt_bij1[OF pt_coname_inst, OF at_coname_inst])apply (simp)done nominal_primrec "ty ==> ==> ==> ==> ==> where "IMPRIGHT (B IMP C) X Y Z U= { :ImpR (x)..M b | x a b M. fic (ImpR (x). .M b) b ∧ (∀ z P. x♯ (z,P) ∧ (z):P ∈ Z ⟶ (x):(M{a:=(z).P}) ∈ X) ∧ (∀ c Q. a♯ (c,Q) ∧ :Q ∈ U ⟶ :(M{x:=.Q}) ∈ Y)}" apply (rule TrueI)+done lemma IMPRIGHT_eqvt_name:fixes pi::"name prm" shows "(pi∙ (IMPRIGHT (A IMP B) X Y Z U)) = IMPRIGHT (A IMP B) (pi∙ X) (pi∙ Y) (pi∙ Z) (pi∙ U)" apply (auto simp add: perm_set_def)apply (rule_tac x="pi∙ xb" in exI)apply (rule_tac x="pi∙ a" in exI)apply (rule_tac x="pi∙ b" in exI)apply (rule_tac x="pi∙ M" in exI)apply (simp)apply (rule conjI)apply (drule_tac pi="pi" in fic.eqvt(1))apply (simp)apply (rule conjI)apply (auto)[1]apply (rule_tac x="(xb):(M{a:=((rev pi)∙ z).((rev pi)∙ P)})" in exI)apply (perm_simp add: csubst_eqvt)apply (drule sym)apply (drule pt_bij1[OF pt_name_inst, OF at_name_inst])apply (simp)apply (simp add: fresh_right)apply (auto)[1]apply (rule_tac x=":(M{xb:=<((rev pi)∙ c)>.((rev pi)∙ Q)})" in exI)apply (perm_simp add: nsubst_eqvt)apply (drule sym)apply (drule pt_bij1[OF pt_name_inst, OF at_name_inst])apply (simp add: swap_simps fresh_left)apply (rule_tac x="(rev pi)∙ (:ImpR xa..M b)" in exI)apply (perm_simp)apply (rule_tac x="(rev pi)∙ xa" in exI)apply (rule_tac x="(rev pi)∙ a" in exI)apply (rule_tac x="(rev pi)∙ b" in exI)apply (rule_tac x="(rev pi)∙ M" in exI)apply (simp add: swap_simps)apply (drule_tac pi="rev pi" in fic.eqvt(1))apply (simp add: swap_simps)apply (rule conjI)apply (auto)[1]apply (drule_tac x="pi∙ z" in spec)apply (drule_tac x="pi∙ P" in spec)apply (drule mp)apply (simp add: fresh_right)apply (rule_tac x="(z):P" in exI)apply (simp)apply (auto)[1]apply (drule sym)apply (drule pt_bij1[OF pt_name_inst, OF at_name_inst])apply (perm_simp add: csubst_eqvt fresh_right)apply (auto)[1]apply (drule_tac x="pi∙ c" in spec)apply (drule_tac x="pi∙ Q" in spec)apply (drule mp)apply (simp add: swap_simps fresh_left)apply (rule_tac x=":Q" in exI)apply (simp add: swap_simps)apply (auto)[1]apply (drule sym)apply (drule pt_bij1[OF pt_name_inst, OF at_name_inst])apply (perm_simp add: nsubst_eqvt)done lemma IMPRIGHT_eqvt_coname:fixes pi::"coname prm" shows "(pi∙ (IMPRIGHT (A IMP B) X Y Z U)) = IMPRIGHT (A IMP B) (pi∙ X) (pi∙ Y) (pi∙ Z) (pi∙ U)" apply (auto simp add: perm_set_def)apply (rule_tac x="pi∙ xb" in exI)apply (rule_tac x="pi∙ a" in exI)apply (rule_tac x="pi∙ b" in exI)apply (rule_tac x="pi∙ M" in exI)apply (simp)apply (rule conjI)apply (drule_tac pi="pi" in fic.eqvt(2))apply (simp)apply (rule conjI)apply (auto)[1]apply (rule_tac x="(xb):(M{a:=((rev pi)∙ z).((rev pi)∙ P)})" in exI)apply (perm_simp add: csubst_eqvt)apply (drule sym)apply (drule pt_bij1[OF pt_coname_inst, OF at_coname_inst])apply (simp add: swap_simps fresh_left)apply (auto)[1]apply (rule_tac x=":(M{xb:=<((rev pi)∙ c)>.((rev pi)∙ Q)})" in exI)apply (perm_simp add: nsubst_eqvt)apply (drule sym)apply (drule pt_bij1[OF pt_coname_inst, OF at_coname_inst])apply (simp add: fresh_right)apply (rule_tac x="(rev pi)∙ (:ImpR xa..M b)" in exI)apply (perm_simp)apply (rule_tac x="(rev pi)∙ xa" in exI)apply (rule_tac x="(rev pi)∙ a" in exI)apply (rule_tac x="(rev pi)∙ b" in exI)apply (rule_tac x="(rev pi)∙ M" in exI)apply (simp add: swap_simps)apply (drule_tac pi="rev pi" in fic.eqvt(2))apply (simp add: swap_simps)apply (rule conjI)apply (auto)[1]apply (drule_tac x="pi∙ z" in spec)apply (drule_tac x="pi∙ P" in spec)apply (simp add: swap_simps fresh_left)apply (drule mp)apply (rule_tac x="(z):P" in exI)apply (simp add: swap_simps)apply (auto)[1]apply (drule sym)apply (drule pt_bij1[OF pt_coname_inst, OF at_coname_inst])apply (perm_simp add: csubst_eqvt fresh_right)apply (auto)[1]apply (drule_tac x="pi∙ c" in spec)apply (drule_tac x="pi∙ Q" in spec)apply (simp add: fresh_right)apply (drule mp)apply (rule_tac x=":Q" in exI)apply (simp)apply (auto)[1]apply (drule sym)apply (drule pt_bij1[OF pt_coname_inst, OF at_coname_inst])apply (perm_simp add: nsubst_eqvt fresh_right)done nominal_primrec "ty ==> ==> ==> where "IMPLEFT (B IMP C) X Y = { (y):ImpL .M (x).N y | x a y M N. fin (ImpL .M (x).N y) y ∧ :M ∈ X ∧ (x):N ∈ Y }" apply (rule TrueI)+done lemma IMPLEFT_eqvt_name:fixes pi::"name prm" shows "(pi∙ (IMPLEFT (A IMP B) X Y)) = IMPLEFT (A IMP B) (pi∙ X) (pi∙ Y)" apply (auto simp add: perm_set_def)apply (rule_tac x="pi∙ xb" in exI) apply (rule_tac x="pi∙ a" in exI)apply (rule_tac x="pi∙ y" in exI) apply (rule_tac x="pi∙ M" in exI) apply (rule_tac x="pi∙ N" in exI)apply (simp)apply (rule conjI)apply (drule_tac pi="pi" in fin.eqvt(1))apply (simp)apply (rule conjI)apply (rule_tac x=":M" in exI)apply (simp)apply (rule_tac x="(xb):N" in exI)apply (simp)apply (rule_tac x="(rev pi)∙ ((y):ImpL .M (xa).N y)" in exI)apply (perm_simp)apply (rule_tac x="(rev pi)∙ xa" in exI) apply (rule_tac x="(rev pi)∙ a" in exI) apply (rule_tac x="(rev pi)∙ y" in exI) apply (rule_tac x="(rev pi)∙ M" in exI)apply (rule_tac x="(rev pi)∙ N" in exI)apply (simp add: swap_simps)apply (drule_tac pi="rev pi" in fin.eqvt(1))apply (simp)apply (drule sym)apply (drule sym)apply (drule pt_bij1[OF pt_name_inst, OF at_name_inst])apply (drule pt_bij1[OF pt_name_inst, OF at_name_inst])apply (simp add: swap_simps)done lemma IMPLEFT_eqvt_coname:fixes pi::"coname prm" shows "(pi∙ (IMPLEFT (A IMP B) X Y)) = IMPLEFT (A IMP B) (pi∙ X) (pi∙ Y)" apply (auto simp add: perm_set_def)apply (rule_tac x="pi∙ xb" in exI) apply (rule_tac x="pi∙ a" in exI)apply (rule_tac x="pi∙ y" in exI) apply (rule_tac x="pi∙ M" in exI) apply (rule_tac x="pi∙ N" in exI)apply (simp)apply (rule conjI)apply (drule_tac pi="pi" in fin.eqvt(2))apply (simp)apply (rule conjI)apply (rule_tac x=":M" in exI)apply (simp)apply (rule_tac x="(xb):N" in exI)apply (simp)apply (rule_tac x="(rev pi)∙ ((y):ImpL .M (xa).N y)" in exI)apply (perm_simp)apply (rule_tac x="(rev pi)∙ xa" in exI) apply (rule_tac x="(rev pi)∙ a" in exI) apply (rule_tac x="(rev pi)∙ y" in exI) apply (rule_tac x="(rev pi)∙ M" in exI)apply (rule_tac x="(rev pi)∙ N" in exI)apply (simp add: swap_simps)apply (drule_tac pi="rev pi" in fin.eqvt(2))apply (simp)apply (drule sym)apply (drule sym)apply (drule pt_bij1[OF pt_coname_inst, OF at_coname_inst])apply (drule pt_bij1[OF pt_coname_inst, OF at_coname_inst])apply (simp add: swap_simps)done lemma sum_cases:shows "(∃ y. x=Inl y) ∨ (∃ y. x=Inr y)" apply (rule_tac s="x" in sumE)apply (auto)done function "ty ==> ==> and "ty ==> ==> where "NEGc (PR A) X = AXIOMSc (PR A) ∪ BINDINGc (PR A) X" "NEGc (NOT C) X = AXIOMSc (NOT C) ∪ BINDINGc (NOT C) X ∪ NOTRIGHT (NOT C) (lfp (NEGn C ∘ NEGc C))" "NEGc (C AND D) X = AXIOMSc (C AND D) ∪ BINDINGc (C AND D) X ∪ ANDRIGHT (C AND D) (NEGc C (lfp (NEGn C ∘ NEGc C))) (NEGc D (lfp (NEGn D ∘ NEGc D)))" "NEGc (C OR D) X = AXIOMSc (C OR D) ∪ BINDINGc (C OR D) X ∪ ORRIGHT1 (C OR D) (NEGc C (lfp (NEGn C ∘ NEGc C))) ∪ ORRIGHT2 (C OR D) (NEGc D (lfp (NEGn D ∘ NEGc D)))" "NEGc (C IMP D) X = AXIOMSc (C IMP D) ∪ BINDINGc (C IMP D) X ∪ IMPRIGHT (C IMP D) (lfp (NEGn C ∘ NEGc C)) (NEGc D (lfp (NEGn D ∘ NEGc D))) (lfp (NEGn D ∘ NEGc D)) (NEGc C (lfp (NEGn C ∘ NEGc C)))" "NEGn (PR A) X = AXIOMSn (PR A) ∪ BINDINGn (PR A) X" "NEGn (NOT C) X = AXIOMSn (NOT C) ∪ BINDINGn (NOT C) X ∪ NOTLEFT (NOT C) (NEGc C (lfp (NEGn C ∘ NEGc C)))" "NEGn (C AND D) X = AXIOMSn (C AND D) ∪ BINDINGn (C AND D) X ∪ ANDLEFT1 (C AND D) (lfp (NEGn C ∘ NEGc C)) ∪ ANDLEFT2 (C AND D) (lfp (NEGn D ∘ NEGc D))" "NEGn (C OR D) X = AXIOMSn (C OR D) ∪ BINDINGn (C OR D) X ∪ ORLEFT (C OR D) (lfp (NEGn C ∘ NEGc C)) (lfp (NEGn D ∘ NEGc D))" "NEGn (C IMP D) X = AXIOMSn (C IMP D) ∪ BINDINGn (C IMP D) X ∪ IMPLEFT (C IMP D) (NEGc C (lfp (NEGn C ∘ NEGc C))) (lfp (NEGn D ∘ NEGc D))" using ty_cases sum_cases apply (auto simp add: ty.inject)apply (drule_tac x="x" in meta_spec)apply (fastforce simp add: ty.inject)done termination apply (relation "measure (case_sum (size∘ fst) (size∘ fst))" )apply (simp_all)done text ‹ Candidates› lemma test1:shows "x∈ (X∪ Y) = (x∈ X ∨ x∈ Y)" by blastlemma test2:shows "x∈ (X∩ Y) = (x∈ X ∧ x∈ Y)" by blastlemma big_inter_eqvt:fixes pi1::"name prm" and X::"('a::pt_name) set set" and pi2::"coname prm" and Y::"('b::pt_coname) set set" shows "(pi1∙ (∩ ∩ ∙ X)" and "(pi2∙ (∩ ∩ ∙ Y)" apply (auto simp add: perm_set_def)apply (rule_tac x="(rev pi1)∙ x" in exI)apply (perm_simp)apply (rule ballI)apply (drule_tac x="pi1∙ xa" in spec)apply (auto)apply (drule_tac x="xa" in spec)apply (auto)[1]apply (rule_tac x="(rev pi1)∙ xb" in exI)apply (perm_simp)apply (simp add: pt_set_bij1[OF pt_name_inst, OF at_name_inst])apply (simp add: pt_set_bij[OF pt_name_inst, OF at_name_inst])apply (simp add: pt_set_bij1[OF pt_name_inst, OF at_name_inst])apply (rule_tac x="(rev pi2)∙ x" in exI)apply (perm_simp)apply (rule ballI)apply (drule_tac x="pi2∙ xa" in spec)apply (auto)apply (drule_tac x="xa" in spec)apply (auto)[1]apply (rule_tac x="(rev pi2)∙ xb" in exI)apply (perm_simp)apply (simp add: pt_set_bij1[OF pt_coname_inst, OF at_coname_inst])apply (simp add: pt_set_bij[OF pt_coname_inst, OF at_coname_inst])apply (simp add: pt_set_bij1[OF pt_coname_inst, OF at_coname_inst])done lemma lfp_eqvt:fixes pi1::"name prm" and f::"'a set ==> and pi2::"coname prm" and g::"'b set ==> shows "pi1∙ (lfp f) = lfp (pi1∙ f)" and "pi2∙ (lfp g) = lfp (pi2∙ g)" apply (simp add: lfp_def)apply (simp add: big_inter_eqvt)apply (simp add: pt_Collect_eqvt[OF pt_name_inst, OF at_name_inst])apply (subgoal_tac "{u. (pi1∙ f) u ⊆ u} = {u. ((rev pi1)∙ ((pi1∙ f) u)) ⊆ ((rev pi1)∙ u)}" )apply (perm_simp)apply (rule Collect_cong)apply (rule iffI)apply (rule subseteq_eqvt(1)[THEN iffD1])apply (simp add: perm_bool)apply (drule subseteq_eqvt(1)[THEN iffD2])apply (simp add: perm_bool)apply (simp add: lfp_def)apply (simp add: big_inter_eqvt)apply (simp add: pt_Collect_eqvt[OF pt_coname_inst, OF at_coname_inst])apply (subgoal_tac "{u. (pi2∙ g) u ⊆ u} = {u. ((rev pi2)∙ ((pi2∙ g) u)) ⊆ ((rev pi2)∙ u)}" )apply (perm_simp)apply (rule Collect_cong)apply (rule iffI)apply (rule subseteq_eqvt(2)[THEN iffD1])apply (simp add: perm_bool)apply (drule subseteq_eqvt(2)[THEN iffD2])apply (simp add: perm_bool)done abbreviation "ty ==> (‹ ∥ '(_')∥ › [60] 60) where "∥ (B)∥ ≡ lfp (NEGn B ∘ NEGc B)" abbreviation "ty ==> (‹ ∥ 🪙 ∥ › [60] 60)where "∥ ∥ ≡ NEGc B (∥ (B)∥ )" lemma NEGn_decreasing:shows "X⊆ Y ==> NEGn B Y ⊆ NEGn B X" by (nominal_induct B rule: ty.strong_induct)lemma NEGc_decreasing:shows "X⊆ Y ==> NEGc B Y ⊆ NEGc B X" by (nominal_induct B rule: ty.strong_induct)lemma mono_NEGn_NEGc:shows "mono (NEGn B ∘ NEGc B)" and "mono (NEGc B ∘ NEGn B)" proof -have "∀ X Y. X⊆ Y ⟶ NEGn B (NEGc B X) ⊆ NEGn B (NEGc B Y)" proof (intro strip)fix X::"ntrm set" and Y::"ntrm set" assume "X⊆ Y" then have "NEGc B Y ⊆ NEGc B X" by (simp add: NEGc_decreasing)then show "NEGn B (NEGc B X) ⊆ NEGn B (NEGc B Y)" by (simp add: NEGn_decreasing)qed then show "mono (NEGn B ∘ NEGc B)" by (simp add: mono_def)next have "∀ X Y. X⊆ Y ⟶ NEGc B (NEGn B X) ⊆ NEGc B (NEGn B Y)" proof (intro strip)fix X::"ctrm set" and Y::"ctrm set" assume "X⊆ Y" then have "NEGn B Y ⊆ NEGn B X" by (simp add: NEGn_decreasing)then show "NEGc B (NEGn B X) ⊆ NEGc B (NEGn B Y)" by (simp add: NEGc_decreasing)qed then show "mono (NEGc B ∘ NEGn B)" by (simp add: mono_def)qed lemma NEG_simp:shows "∥ ∥ = NEGc B (∥ (B)∥ )" and "∥ (B)∥ = NEGn B (∥ ∥ )" proof -show "∥ ∥ = NEGc B (∥ (B)∥ )" by simpnext have "∥ (B)∥ ≡ lfp (NEGn B ∘ NEGc B)" by simpthen have "∥ (B)∥ = (NEGn B ∘ NEGc B) (∥ (B)∥ )" using mono_NEGn_NEGc def_lfp_unfold by blastthen show "∥ (B)∥ = NEGn B (∥ ∥ )" by simpqed lemma NEG_elim:shows "M ∈ ∥ ∥ ==> M ∈ NEGc B (∥ (B)∥ )" and "N ∈ ∥ (B)∥ ==> N ∈ NEGn B (∥ ∥ )" using NEG_simp by (blast)+lemma NEG_intro:shows "M ∈ NEGc B (∥ (B)∥ ) ==> M ∈ ∥ ∥ " and "N ∈ NEGn B (∥ ∥ ) ==> N ∈ ∥ (B)∥ " using NEG_simp by (blast)+lemma NEGc_simps:shows "NEGc (PR A) (∥ (PR A)∥ ) = AXIOMSc (PR A) ∪ BINDINGc (PR A) (∥ (PR A)∥ )" and "NEGc (NOT C) (∥ (NOT C)∥ ) = AXIOMSc (NOT C) ∪ BINDINGc (NOT C) (∥ (NOT C)∥ ) ∪ (NOTRIGHT (NOT C) (∥ (C)∥ ))" and "NEGc (C AND D) (∥ (C AND D)∥ ) = AXIOMSc (C AND D) ∪ BINDINGc (C AND D) (∥ (C AND D)∥ ) ∪ (ANDRIGHT (C AND D) (∥ ∥ ) (∥ ∥ ))" and "NEGc (C OR D) (∥ (C OR D)∥ ) = AXIOMSc (C OR D) ∪ BINDINGc (C OR D) (∥ (C OR D)∥ ) ∪ (ORRIGHT1 (C OR D) (∥ ∥ )) ∪ (ORRIGHT2 (C OR D) (∥ ∥ ))" and "NEGc (C IMP D) (∥ (C IMP D)∥ ) = AXIOMSc (C IMP D) ∪ BINDINGc (C IMP D) (∥ (C IMP D)∥ ) ∪ (IMPRIGHT (C IMP D) (∥ (C)∥ ) (∥ ∥ ) (∥ (D)∥ ) (∥ ∥ ))" by (simp_all only: NEGc.simps)lemma AXIOMS_in_CANDs:shows "AXIOMSn B ⊆ (∥ (B)∥ )" and "AXIOMSc B ⊆ (∥ ∥ )" proof -have "AXIOMSn B ⊆ NEGn B (∥ ∥ )" by (nominal_induct B rule: ty.strong_induct) (auto)then show "AXIOMSn B ⊆ ∥ (B)∥ " using NEG_simp by blastnext have "AXIOMSc B ⊆ NEGc B (∥ (B)∥ )" by (nominal_induct B rule: ty.strong_induct) (auto)then show "AXIOMSc B ⊆ ∥ ∥ " using NEG_simp by blastqed lemma Ax_in_CANDs:shows "(y):Ax x a ∈ ∥ (B)∥ " and ":Ax x a ∈ ∥ ∥ " proof -have "(y):Ax x a ∈ AXIOMSn B" by (auto simp add: AXIOMSn_def)also have "AXIOMSn B ⊆ ∥ (B)∥ " by (rule AXIOMS_in_CANDs)finally show "(y):Ax x a ∈ ∥ (B)∥ " by simpnext have ":Ax x a ∈ AXIOMSc B" by (auto simp add: AXIOMSc_def)also have "AXIOMSc B ⊆ ∥ ∥ " by (rule AXIOMS_in_CANDs)finally show ":Ax x a ∈ ∥ ∥ " by simpqed lemma AXIOMS_eqvt_aux_name:fixes pi::"name prm" shows "M ∈ AXIOMSn B ==> (pi∙ M) ∈ AXIOMSn B" and "N ∈ AXIOMSc B ==> (pi∙ N) ∈ AXIOMSc B" apply (auto simp add: AXIOMSn_def AXIOMSc_def)apply (rule_tac x="pi∙ x" in exI)apply (rule_tac x="pi∙ y" in exI)apply (rule_tac x="pi∙ b" in exI)apply (simp)apply (rule_tac x="pi∙ a" in exI)apply (rule_tac x="pi∙ y" in exI)apply (rule_tac x="pi∙ b" in exI)apply (simp)done lemma AXIOMS_eqvt_aux_coname:fixes pi::"coname prm" shows "M ∈ AXIOMSn B ==> (pi∙ M) ∈ AXIOMSn B" and "N ∈ AXIOMSc B ==> (pi∙ N) ∈ AXIOMSc B" apply (auto simp add: AXIOMSn_def AXIOMSc_def)apply (rule_tac x="pi∙ x" in exI)apply (rule_tac x="pi∙ y" in exI)apply (rule_tac x="pi∙ b" in exI)apply (simp)apply (rule_tac x="pi∙ a" in exI)apply (rule_tac x="pi∙ y" in exI)apply (rule_tac x="pi∙ b" in exI)apply (simp)done lemma AXIOMS_eqvt_name:fixes pi::"name prm" shows "(pi∙ AXIOMSn B) = AXIOMSn B" and "(pi∙ AXIOMSc B) = AXIOMSc B" apply (auto)apply (simp add: pt_set_bij1a[OF pt_name_inst, OF at_name_inst])apply (drule_tac pi="pi" in AXIOMS_eqvt_aux_name(1))apply (perm_simp)apply (drule_tac pi="rev pi" in AXIOMS_eqvt_aux_name(1))apply (simp add: pt_set_bij1[OF pt_name_inst, OF at_name_inst])apply (simp add: pt_set_bij1a[OF pt_name_inst, OF at_name_inst])apply (drule_tac pi="pi" in AXIOMS_eqvt_aux_name(2))apply (perm_simp)apply (drule_tac pi="rev pi" in AXIOMS_eqvt_aux_name(2))apply (simp add: pt_set_bij1[OF pt_name_inst, OF at_name_inst])done lemma AXIOMS_eqvt_coname:fixes pi::"coname prm" shows "(pi∙ AXIOMSn B) = AXIOMSn B" and "(pi∙ AXIOMSc B) = AXIOMSc B" apply (auto)apply (simp add: pt_set_bij1a[OF pt_coname_inst, OF at_coname_inst])apply (drule_tac pi="pi" in AXIOMS_eqvt_aux_coname(1))apply (perm_simp)apply (drule_tac pi="rev pi" in AXIOMS_eqvt_aux_coname(1))apply (simp add: pt_set_bij1[OF pt_coname_inst, OF at_coname_inst])apply (simp add: pt_set_bij1a[OF pt_coname_inst, OF at_coname_inst])apply (drule_tac pi="pi" in AXIOMS_eqvt_aux_coname(2))apply (perm_simp)apply (drule_tac pi="rev pi" in AXIOMS_eqvt_aux_coname(2))apply (simp add: pt_set_bij1[OF pt_coname_inst, OF at_coname_inst])done lemma BINDING_eqvt_name:fixes pi::"name prm" shows "(pi∙ (BINDINGn B X)) = BINDINGn B (pi∙ X)" and "(pi∙ (BINDINGc B Y)) = BINDINGc B (pi∙ Y)" apply (auto simp add: BINDINGn_def BINDINGc_def perm_set_def)apply (rule_tac x="pi∙ xb" in exI)apply (rule_tac x="pi∙ M" in exI)apply (simp)apply (auto)[1]apply (drule_tac x="(rev pi)∙ a" in spec)apply (drule_tac x="(rev pi)∙ P" in spec)apply (drule mp)apply (drule sym)apply (drule pt_bij1[OF pt_name_inst, OF at_name_inst])apply (simp)apply (drule_tac ?pi1.0="pi" in SNa_eqvt(1))apply (perm_simp add: nsubst_eqvt)apply (rule_tac x="(rev pi∙ xa):(rev pi∙ M)" in exI)apply (perm_simp)apply (rule_tac x="rev pi∙ xa" in exI)apply (rule_tac x="rev pi∙ M" in exI)apply (simp)apply (auto)[1]apply (drule_tac x="pi∙ a" in spec)apply (drule_tac x="pi∙ P" in spec)apply (drule mp)apply (force)apply (drule_tac ?pi1.0="rev pi" in SNa_eqvt(1))apply (perm_simp add: nsubst_eqvt)apply (rule_tac x="pi∙ a" in exI)apply (rule_tac x="pi∙ M" in exI)apply (simp)apply (auto)[1]apply (drule_tac x="(rev pi)∙ x" in spec)apply (drule_tac x="(rev pi)∙ P" in spec)apply (drule mp)apply (drule sym)apply (drule pt_bij1[OF pt_name_inst, OF at_name_inst])apply (simp)apply (drule_tac ?pi1.0="pi" in SNa_eqvt(1))apply (perm_simp add: csubst_eqvt)apply (rule_tac x="<(rev pi∙ a)>:(rev pi∙ M)" in exI)apply (perm_simp)apply (rule_tac x="rev pi∙ a" in exI)apply (rule_tac x="rev pi∙ M" in exI)apply (simp add: swap_simps)apply (auto)[1]apply (drule_tac x="pi∙ x" in spec)apply (drule_tac x="pi∙ P" in spec)apply (drule mp)apply (force)apply (drule_tac ?pi1.0="rev pi" in SNa_eqvt(1))apply (perm_simp add: csubst_eqvt)done lemma BINDING_eqvt_coname:fixes pi::"coname prm" shows "(pi∙ (BINDINGn B X)) = BINDINGn B (pi∙ X)" and "(pi∙ (BINDINGc B Y)) = BINDINGc B (pi∙ Y)" apply (auto simp add: BINDINGn_def BINDINGc_def perm_set_def)apply (rule_tac x="pi∙ xb" in exI)apply (rule_tac x="pi∙ M" in exI)apply (simp)apply (auto)[1]apply (drule_tac x="(rev pi)∙ a" in spec)apply (drule_tac x="(rev pi)∙ P" in spec)apply (drule mp)apply (drule sym)apply (drule pt_bij1[OF pt_coname_inst, OF at_coname_inst])apply (simp)apply (drule_tac ?pi2.0="pi" in SNa_eqvt(2))apply (perm_simp add: nsubst_eqvt)apply (rule_tac x="(rev pi∙ xa):(rev pi∙ M)" in exI)apply (perm_simp)apply (rule_tac x="rev pi∙ xa" in exI)apply (rule_tac x="rev pi∙ M" in exI)apply (simp add: swap_simps)apply (auto)[1]apply (drule_tac x="pi∙ a" in spec)apply (drule_tac x="pi∙ P" in spec)apply (drule mp)apply (force)apply (drule_tac ?pi2.0="rev pi" in SNa_eqvt(2))apply (perm_simp add: nsubst_eqvt)apply (rule_tac x="pi∙ a" in exI)apply (rule_tac x="pi∙ M" in exI)apply (simp)apply (auto)[1]apply (drule_tac x="(rev pi)∙ x" in spec)apply (drule_tac x="(rev pi)∙ P" in spec)apply (drule mp)apply (drule sym)apply (drule pt_bij1[OF pt_coname_inst, OF at_coname_inst])apply (simp)apply (drule_tac ?pi2.0="pi" in SNa_eqvt(2))apply (perm_simp add: csubst_eqvt)apply (rule_tac x="<(rev pi∙ a)>:(rev pi∙ M)" in exI)apply (perm_simp)apply (rule_tac x="rev pi∙ a" in exI)apply (rule_tac x="rev pi∙ M" in exI)apply (simp)apply (auto)[1]apply (drule_tac x="pi∙ x" in spec)apply (drule_tac x="pi∙ P" in spec)apply (drule mp)apply (force)apply (drule_tac ?pi2.0="rev pi" in SNa_eqvt(2))apply (perm_simp add: csubst_eqvt)done lemma CAND_eqvt_name:fixes pi::"name prm" shows "(pi∙ (∥ (B)∥ )) = (∥ (B)∥ )" and "(pi∙ (∥ ∥ )) = (∥ ∥ )" proof (nominal_induct B rule: ty.strong_induct)case (PR X)case 1 show ?case apply -apply (simp add: lfp_eqvt)apply (simp add: perm_fun_def)apply (simp add: union_eqvt AXIOMS_eqvt_name BINDING_eqvt_name)apply (perm_simp)done next case 2 show ?case apply -apply (simp only: NEGc_simps)apply (simp add: union_eqvt AXIOMS_eqvt_name BINDING_eqvt_name)apply (simp add: lfp_eqvt)apply (simp add: comp_def)apply (simp add: perm_fun_def)apply (simp add: union_eqvt AXIOMS_eqvt_name BINDING_eqvt_name)apply (perm_simp)done next case (NOT B)have ih1: "pi∙ (∥ (B)∥ ) = (∥ (B)∥ )" by facthave ih2: "pi∙ (∥ ∥ ) = (∥ ∥ )" by facthave g: "pi∙ (∥ (NOT B)∥ ) = (∥ (NOT B)∥ )" apply -apply (simp only: lfp_eqvt)apply (simp only: comp_def)apply (simp only: perm_fun_def)apply (simp only: NEGc.simps NEGn.simps)apply (simp only: union_eqvt AXIOMS_eqvt_name BINDING_eqvt_name NOTRIGHT_eqvt_name NOTLEFT_eqvt_name)apply (perm_simp add: ih1 ih2)done case 1 show ?case by (rule g)next case 2 show ?case by (simp only: NEGc_simps union_eqvt AXIOMS_eqvt_name BINDING_eqvt_name NOTRIGHT_eqvt_name ih1 ih2 g)next case (AND A B)have ih1: "pi∙ (∥ (A)∥ ) = (∥ (A)∥ )" by facthave ih2: "pi∙ (∥ ∥ ) = (∥ ∥ )" by facthave ih3: "pi∙ (∥ (B)∥ ) = (∥ (B)∥ )" by facthave ih4: "pi∙ (∥ ∥ ) = (∥ ∥ )" by facthave g: "pi∙ (∥ (A AND B)∥ ) = (∥ (A AND B)∥ )" apply -apply (simp only: lfp_eqvt)apply (simp only: comp_def)apply (simp only: perm_fun_def)apply (simp only: NEGc.simps NEGn.simps)apply (simp only: union_eqvt AXIOMS_eqvt_name BINDING_eqvt_name ANDRIGHT_eqvt_name apply (perm_simp add: ih1 ih2 ih3 ih4)done case 1 show ?case by (rule g)next case 2 show ?case by (simp only: NEGc_simps union_eqvt AXIOMS_eqvt_name BINDING_eqvt_name next case (OR A B)have ih1: "pi∙ (∥ (A)∥ ) = (∥ (A)∥ )" by facthave ih2: "pi∙ (∥ ∥ ) = (∥ ∥ )" by facthave ih3: "pi∙ (∥ (B)∥ ) = (∥ (B)∥ )" by facthave ih4: "pi∙ (∥ ∥ ) = (∥ ∥ )" by facthave g: "pi∙ (∥ (A OR B)∥ ) = (∥ (A OR B)∥ )" apply -apply (simp only: lfp_eqvt)apply (simp only: comp_def)apply (simp only: perm_fun_def)apply (simp only: NEGc.simps NEGn.simps)apply (simp only: union_eqvt AXIOMS_eqvt_name BINDING_eqvt_name ORRIGHT1_eqvt_name apply (perm_simp add: ih1 ih2 ih3 ih4)done case 1 show ?case by (rule g)next case 2 show ?case by (simp only: NEGc_simps union_eqvt AXIOMS_eqvt_name BINDING_eqvt_name next case (IMP A B)have ih1: "pi∙ (∥ (A)∥ ) = (∥ (A)∥ )" by facthave ih2: "pi∙ (∥ ∥ ) = (∥ ∥ )" by facthave ih3: "pi∙ (∥ (B)∥ ) = (∥ (B)∥ )" by facthave ih4: "pi∙ (∥ ∥ ) = (∥ ∥ )" by facthave g: "pi∙ (∥ (A IMP B)∥ ) = (∥ (A IMP B)∥ )" apply -apply (simp only: lfp_eqvt)apply (simp only: comp_def)apply (simp only: perm_fun_def)apply (simp only: NEGc.simps NEGn.simps)apply (simp only: union_eqvt AXIOMS_eqvt_name BINDING_eqvt_name IMPRIGHT_eqvt_name IMPLEFT_eqvt_name)apply (perm_simp add: ih1 ih2 ih3 ih4)done case 1 show ?case by (rule g)next case 2 show ?case by (simp only: NEGc_simps union_eqvt AXIOMS_eqvt_name BINDING_eqvt_name qed lemma CAND_eqvt_coname:fixes pi::"coname prm" shows "(pi∙ (∥ (B)∥ )) = (∥ (B)∥ )" and "(pi∙ (∥ ∥ )) = (∥ ∥ )" proof (nominal_induct B rule: ty.strong_induct)case (PR X)case 1 show ?case apply -apply (simp add: lfp_eqvt)apply (simp add: perm_fun_def)apply (simp add: union_eqvt AXIOMS_eqvt_coname BINDING_eqvt_coname)apply (perm_simp)done next case 2 show ?case apply -apply (simp only: NEGc_simps)apply (simp add: union_eqvt AXIOMS_eqvt_coname BINDING_eqvt_coname)apply (simp add: lfp_eqvt)apply (simp add: comp_def)apply (simp add: perm_fun_def)apply (simp add: union_eqvt AXIOMS_eqvt_coname BINDING_eqvt_coname)apply (perm_simp)done next case (NOT B)have ih1: "pi∙ (∥ (B)∥ ) = (∥ (B)∥ )" by facthave ih2: "pi∙ (∥ ∥ ) = (∥ ∥ )" by facthave g: "pi∙ (∥ (NOT B)∥ ) = (∥ (NOT B)∥ )" apply -apply (simp only: lfp_eqvt)apply (simp only: comp_def)apply (simp only: perm_fun_def)apply (simp only: NEGc.simps NEGn.simps)apply (simp only: union_eqvt AXIOMS_eqvt_coname BINDING_eqvt_coname apply (perm_simp add: ih1 ih2)done case 1 show ?case by (rule g)next case 2 show ?case by (simp only: NEGc_simps union_eqvt AXIOMS_eqvt_coname BINDING_eqvt_coname next case (AND A B)have ih1: "pi∙ (∥ (A)∥ ) = (∥ (A)∥ )" by facthave ih2: "pi∙ (∥ ∥ ) = (∥ ∥ )" by facthave ih3: "pi∙ (∥ (B)∥ ) = (∥ (B)∥ )" by facthave ih4: "pi∙ (∥ ∥ ) = (∥ ∥ )" by facthave g: "pi∙ (∥ (A AND B)∥ ) = (∥ (A AND B)∥ )" apply -apply (simp only: lfp_eqvt)apply (simp only: comp_def)apply (simp only: perm_fun_def)apply (simp only: NEGc.simps NEGn.simps)apply (simp only: union_eqvt AXIOMS_eqvt_coname BINDING_eqvt_coname ANDRIGHT_eqvt_coname apply (perm_simp add: ih1 ih2 ih3 ih4)done case 1 show ?case by (rule g)next case 2 show ?case by (simp only: NEGc_simps union_eqvt AXIOMS_eqvt_coname BINDING_eqvt_coname next case (OR A B)have ih1: "pi∙ (∥ (A)∥ ) = (∥ (A)∥ )" by facthave ih2: "pi∙ (∥ ∥ ) = (∥ ∥ )" by facthave ih3: "pi∙ (∥ (B)∥ ) = (∥ (B)∥ )" by facthave ih4: "pi∙ (∥ ∥ ) = (∥ ∥ )" by facthave g: "pi∙ (∥ (A OR B)∥ ) = (∥ (A OR B)∥ )" apply -apply (simp only: lfp_eqvt)apply (simp only: comp_def)apply (simp only: perm_fun_def)apply (simp only: NEGc.simps NEGn.simps)apply (simp only: union_eqvt AXIOMS_eqvt_coname BINDING_eqvt_coname ORRIGHT1_eqvt_coname apply (perm_simp add: ih1 ih2 ih3 ih4)done case 1 show ?case by (rule g)next case 2 show ?case by (simp only: NEGc_simps union_eqvt AXIOMS_eqvt_coname BINDING_eqvt_coname next case (IMP A B)have ih1: "pi∙ (∥ (A)∥ ) = (∥ (A)∥ )" by facthave ih2: "pi∙ (∥ ∥ ) = (∥ ∥ )" by facthave ih3: "pi∙ (∥ (B)∥ ) = (∥ (B)∥ )" by facthave ih4: "pi∙ (∥ ∥ ) = (∥ ∥ )" by facthave g: "pi∙ (∥ (A IMP B)∥ ) = (∥ (A IMP B)∥ )" apply -apply (simp only: lfp_eqvt)apply (simp only: comp_def)apply (simp only: perm_fun_def)apply (simp only: NEGc.simps NEGn.simps)apply (simp only: union_eqvt AXIOMS_eqvt_coname BINDING_eqvt_coname IMPRIGHT_eqvt_coname apply (perm_simp add: ih1 ih2 ih3 ih4)done case 1 show ?case by (rule g)next case 2 show ?case by (simp only: NEGc_simps union_eqvt AXIOMS_eqvt_coname BINDING_eqvt_coname qed text ‹ Elimination rules for the set-operators› lemma BINDINGc_elim:assumes a: ":M ∈ BINDINGc B (∥ (B)∥ )" shows "∀ x P. ((x):P)∈ (∥ (B)∥ ) ⟶ SNa (M{a:=(x).P})" using aapply (auto simp add: BINDINGc_def)apply (auto simp add: ctrm.inject alpha)apply (drule_tac x="[(a,aa)]∙ x" in spec)apply (drule_tac x="[(a,aa)]∙ P" in spec)apply (drule mp)apply (drule_tac pi="[(a,aa)]" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (simp add: CAND_eqvt_coname)apply (drule_tac ?pi2.0="[(a,aa)]" in SNa_eqvt(2))apply (perm_simp add: csubst_eqvt)done lemma BINDINGn_elim:assumes a: "(x):M ∈ BINDINGn B (∥ ∥ )" shows "∀ c P. (:P)∈ (∥ ∥ ) ⟶ SNa (M{x:=.P})" using aapply (auto simp add: BINDINGn_def)apply (auto simp add: ntrm.inject alpha)apply (drule_tac x="[(x,xa)]∙ c" in spec)apply (drule_tac x="[(x,xa)]∙ P" in spec)apply (drule mp)apply (drule_tac pi="[(x,xa)]" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])apply (simp add: CAND_eqvt_name)apply (drule_tac ?pi1.0="[(x,xa)]" in SNa_eqvt(1))apply (perm_simp add: nsubst_eqvt)done lemma NOTRIGHT_elim:assumes a: ":M ∈ NOTRIGHT (NOT B) (∥ (B)∥ )" obtains x' M' where "M = NotR (x').M' a" and "fic (NotR (x').M' a) a" and "(x'):M' ∈ (∥ (B)∥ )" using aapply (auto simp add: ctrm.inject alpha abs_fresh calc_atm)apply (drule_tac x="x" in meta_spec)apply (drule_tac x="[(a,aa)]∙ Ma" in meta_spec)apply (simp)apply (drule meta_mp)apply (drule_tac pi="[(a,aa)]" in fic.eqvt(2))apply (simp add: calc_atm)apply (drule meta_mp)apply (drule_tac pi="[(a,aa)]" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (simp add: calc_atm CAND_eqvt_coname)apply (simp)done lemma NOTLEFT_elim:assumes a: "(x):M ∈ NOTLEFT (NOT B) (∥ ∥ )" obtains a' M' where "M = NotL .M' x" and "fin (NotL .M' x) x" and ":M' ∈ (∥ ∥ )" using aapply (auto simp add: ntrm.inject alpha abs_fresh calc_atm)apply (drule_tac x="a" in meta_spec)apply (drule_tac x="[(x,xa)]∙ Ma" in meta_spec)apply (simp)apply (drule meta_mp)apply (drule_tac pi="[(x,xa)]" in fin.eqvt(1))apply (simp add: calc_atm)apply (drule meta_mp)apply (drule_tac pi="[(x,xa)]" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])apply (simp add: calc_atm CAND_eqvt_name)apply (simp)done lemma ANDRIGHT_elim:assumes a: ":M ∈ ANDRIGHT (B AND C) (∥ ∥ ) (∥ ∥ )" obtains d' M' e' N' where "M = AndR .M' .N' a" and "fic (AndR .M' .N' a) a" and ":M' ∈ (∥ ∥ )" and ":N' ∈ (∥ ∥ )" using aapply (auto simp add: ctrm.inject alpha abs_fresh calc_atm fresh_atm)apply (drule_tac x="c" in meta_spec)apply (drule_tac x="[(a,c)]∙ Ma" in meta_spec)apply (drule_tac x="c" in meta_spec)apply (drule_tac x="[(a,c)]∙ N" in meta_spec)apply (simp)apply (drule meta_mp)apply (drule_tac pi="[(a,c)]" in fic.eqvt(2))apply (simp add: calc_atm)apply (drule meta_mp)apply (drule_tac pi="[(a,c)]" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (simp add: calc_atm CAND_eqvt_coname)apply (drule meta_mp)apply (drule_tac pi="[(a,c)]" and x=":N" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (simp add: calc_atm CAND_eqvt_coname)apply (simp)apply (case_tac "a=b" )apply (simp)apply (drule_tac x="c" in meta_spec)apply (drule_tac x="[(b,c)]∙ Ma" in meta_spec)apply (drule_tac x="c" in meta_spec)apply (drule_tac x="[(b,c)]∙ N" in meta_spec)apply (simp)apply (drule meta_mp)apply (drule_tac pi="[(b,c)]" in fic.eqvt(2))apply (simp add: calc_atm)apply (drule meta_mp)apply (drule_tac pi="[(b,c)]" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (simp add: calc_atm CAND_eqvt_coname)apply (drule meta_mp)apply (drule_tac pi="[(b,c)]" and x=":N" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (simp add: calc_atm CAND_eqvt_coname)apply (simp)apply (simp)apply (case_tac "c=b" )apply (simp)apply (drule_tac x="b" in meta_spec)apply (drule_tac x="[(a,b)]∙ Ma" in meta_spec)apply (drule_tac x="a" in meta_spec)apply (drule_tac x="[(a,b)]∙ N" in meta_spec)apply (simp)apply (drule meta_mp)apply (drule_tac pi="[(a,b)]" in fic.eqvt(2))apply (simp add: calc_atm)apply (drule meta_mp)apply (drule_tac pi="[(a,b)]" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (simp add: calc_atm CAND_eqvt_coname)apply (drule meta_mp)apply (drule_tac pi="[(a,b)]" and x=":N" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (simp add: calc_atm CAND_eqvt_coname)apply (simp)apply (simp)apply (drule_tac x="c" in meta_spec)apply (drule_tac x="[(a,c)]∙ Ma" in meta_spec)apply (drule_tac x="b" in meta_spec)apply (drule_tac x="[(a,c)]∙ N" in meta_spec)apply (simp)apply (drule meta_mp)apply (drule_tac pi="[(a,c)]" in fic.eqvt(2))apply (simp add: calc_atm)apply (drule meta_mp)apply (drule_tac pi="[(a,c)]" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (simp add: calc_atm CAND_eqvt_coname)apply (drule meta_mp)apply (drule_tac pi="[(a,c)]" and x=":N" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (simp add: calc_atm CAND_eqvt_coname)apply (simp)apply (case_tac "a=aa" )apply (simp)apply (drule_tac x="c" in meta_spec)apply (drule_tac x="[(aa,c)]∙ Ma" in meta_spec)apply (drule_tac x="c" in meta_spec)apply (drule_tac x="[(aa,c)]∙ N" in meta_spec)apply (simp)apply (drule meta_mp)apply (drule_tac pi="[(aa,c)]" in fic.eqvt(2))apply (simp add: calc_atm)apply (drule meta_mp)apply (drule_tac pi="[(aa,c)]" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (simp add: calc_atm CAND_eqvt_coname)apply (drule meta_mp)apply (drule_tac pi="[(aa,c)]" and x=":N" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (simp add: calc_atm CAND_eqvt_coname)apply (simp)apply (simp)apply (case_tac "c=aa" )apply (simp)apply (drule_tac x="a" in meta_spec)apply (drule_tac x="[(a,aa)]∙ Ma" in meta_spec)apply (drule_tac x="aa" in meta_spec)apply (drule_tac x="[(a,aa)]∙ N" in meta_spec)apply (simp)apply (drule meta_mp)apply (drule_tac pi="[(a,aa)]" in fic.eqvt(2))apply (simp add: calc_atm)apply (drule meta_mp)apply (drule_tac pi="[(a,aa)]" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (simp add: calc_atm CAND_eqvt_coname)apply (drule meta_mp)apply (drule_tac pi="[(a,aa)]" and x=":N" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (simp add: calc_atm CAND_eqvt_coname)apply (simp)apply (simp)apply (drule_tac x="aa" in meta_spec)apply (drule_tac x="[(a,c)]∙ Ma" in meta_spec)apply (drule_tac x="c" in meta_spec)apply (drule_tac x="[(a,c)]∙ N" in meta_spec)apply (simp)apply (drule meta_mp)apply (drule_tac pi="[(a,c)]" in fic.eqvt(2))apply (simp add: calc_atm)apply (drule meta_mp)apply (drule_tac pi="[(a,c)]" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (simp add: calc_atm CAND_eqvt_coname)apply (drule meta_mp)apply (drule_tac pi="[(a,c)]" and x=":N" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (simp add: calc_atm CAND_eqvt_coname)apply (simp)apply (case_tac "a=aa" )apply (simp)apply (case_tac "aa=b" )apply (simp)apply (drule_tac x="c" in meta_spec)apply (drule_tac x="[(b,c)]∙ Ma" in meta_spec)apply (drule_tac x="c" in meta_spec)apply (drule_tac x="[(b,c)]∙ N" in meta_spec)apply (simp)apply (drule meta_mp)apply (drule_tac pi="[(b,c)]" in fic.eqvt(2))apply (simp add: calc_atm)apply (drule meta_mp)apply (drule_tac pi="[(b,c)]" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (simp add: calc_atm CAND_eqvt_coname)apply (drule meta_mp)apply (drule_tac pi="[(b,c)]" and x=":N" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (simp add: calc_atm CAND_eqvt_coname)apply (simp)apply (simp)apply (case_tac "c=b" )apply (simp)apply (drule_tac x="b" in meta_spec)apply (drule_tac x="[(aa,b)]∙ Ma" in meta_spec)apply (drule_tac x="aa" in meta_spec)apply (drule_tac x="[(aa,b)]∙ N" in meta_spec)apply (simp)apply (drule meta_mp)apply (drule_tac pi="[(aa,b)]" in fic.eqvt(2))apply (simp add: calc_atm)apply (drule meta_mp)apply (drule_tac pi="[(aa,b)]" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (simp add: calc_atm CAND_eqvt_coname)apply (drule meta_mp)apply (drule_tac pi="[(aa,b)]" and x=":N" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (simp add: calc_atm CAND_eqvt_coname)apply (simp)apply (simp)apply (drule_tac x="c" in meta_spec)apply (drule_tac x="[(aa,c)]∙ Ma" in meta_spec)apply (drule_tac x="b" in meta_spec)apply (drule_tac x="[(aa,c)]∙ N" in meta_spec)apply (simp)apply (drule meta_mp)apply (drule_tac pi="[(aa,c)]" in fic.eqvt(2))apply (simp add: calc_atm)apply (drule meta_mp)apply (drule_tac pi="[(aa,c)]" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (simp add: calc_atm CAND_eqvt_coname)apply (drule meta_mp)apply (drule_tac pi="[(aa,c)]" and x=":N" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (simp add: calc_atm CAND_eqvt_coname)apply (simp)apply (simp)apply (case_tac "c=aa" )apply (simp)apply (case_tac "a=b" )apply (simp)apply (drule_tac x="b" in meta_spec)apply (drule_tac x="[(b,aa)]∙ Ma" in meta_spec)apply (drule_tac x="aa" in meta_spec)apply (drule_tac x="[(b,aa)]∙ N" in meta_spec)apply (simp)apply (drule meta_mp)apply (drule_tac pi="[(b,aa)]" in fic.eqvt(2))apply (simp add: calc_atm)apply (drule meta_mp)apply (drule_tac pi="[(b,aa)]" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (simp add: calc_atm CAND_eqvt_coname)apply (drule meta_mp)apply (drule_tac pi="[(b,aa)]" and x=":N" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (simp add: calc_atm CAND_eqvt_coname)apply (simp)apply (simp)apply (case_tac "aa=b" )apply (simp)apply (drule_tac x="a" in meta_spec)apply (drule_tac x="[(a,b)]∙ Ma" in meta_spec)apply (drule_tac x="a" in meta_spec)apply (drule_tac x="[(a,b)]∙ N" in meta_spec)apply (simp)apply (drule meta_mp)apply (drule_tac pi="[(a,b)]" in fic.eqvt(2))apply (simp add: calc_atm)apply (drule meta_mp)apply (drule_tac pi="[(a,b)]" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (simp add: calc_atm CAND_eqvt_coname)apply (drule meta_mp)apply (drule_tac pi="[(a,b)]" and x=":N" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (simp add: calc_atm CAND_eqvt_coname)apply (simp)apply (simp)apply (drule_tac x="a" in meta_spec)apply (drule_tac x="[(a,aa)]∙ Ma" in meta_spec)apply (drule_tac x="b" in meta_spec)apply (drule_tac x="[(a,aa)]∙ N" in meta_spec)apply (simp)apply (drule meta_mp)apply (drule_tac pi="[(a,aa)]" in fic.eqvt(2))apply (simp add: calc_atm)apply (drule meta_mp)apply (drule_tac pi="[(a,aa)]" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (simp add: calc_atm CAND_eqvt_coname)apply (drule meta_mp)apply (drule_tac pi="[(a,aa)]" and x=":N" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (simp add: calc_atm CAND_eqvt_coname)apply (simp)apply (simp)apply (case_tac "a=b" )apply (simp)apply (drule_tac x="aa" in meta_spec)apply (drule_tac x="[(b,c)]∙ Ma" in meta_spec)apply (drule_tac x="c" in meta_spec)apply (drule_tac x="[(b,c)]∙ N" in meta_spec)apply (simp)apply (drule meta_mp)apply (drule_tac pi="[(b,c)]" in fic.eqvt(2))apply (simp add: calc_atm)apply (drule meta_mp)apply (drule_tac pi="[(b,c)]" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (simp add: calc_atm CAND_eqvt_coname)apply (drule meta_mp)apply (drule_tac pi="[(b,c)]" and x=":N" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (simp add: calc_atm CAND_eqvt_coname)apply (simp)apply (simp)apply (case_tac "c=b" )apply (simp)apply (drule_tac x="aa" in meta_spec)apply (drule_tac x="[(a,b)]∙ Ma" in meta_spec)apply (drule_tac x="a" in meta_spec)apply (drule_tac x="[(a,b)]∙ N" in meta_spec)apply (simp)apply (drule meta_mp)apply (drule_tac pi="[(a,b)]" in fic.eqvt(2))apply (simp add: calc_atm)apply (drule meta_mp)apply (drule_tac pi="[(a,b)]" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (simp add: calc_atm CAND_eqvt_coname)apply (drule meta_mp)apply (drule_tac pi="[(a,b)]" and x=":N" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (simp add: calc_atm CAND_eqvt_coname)apply (simp)apply (simp)apply (drule_tac x="aa" in meta_spec)apply (drule_tac x="[(a,c)]∙ Ma" in meta_spec)apply (drule_tac x="b" in meta_spec)apply (drule_tac x="[(a,c)]∙ N" in meta_spec)apply (simp)apply (drule meta_mp)apply (drule_tac pi="[(a,c)]" in fic.eqvt(2))apply (simp add: calc_atm)apply (drule meta_mp)apply (drule_tac pi="[(a,c)]" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (simp add: calc_atm CAND_eqvt_coname)apply (drule meta_mp)apply (drule_tac pi="[(a,c)]" and x=":N" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (simp add: calc_atm CAND_eqvt_coname)apply (simp)done lemma ANDLEFT1_elim:assumes a: "(x):M ∈ ANDLEFT1 (B AND C) (∥ (B)∥ )" obtains x' M' where "M = AndL1 (x').M' x" and "fin (AndL1 (x').M' x) x" and "(x'):M' ∈ (∥ ∥ )" using a [[ hypsubst_thin = true ]]apply (auto simp add: ntrm.inject alpha abs_fresh calc_atm)apply (drule_tac x="y" in meta_spec)apply (drule_tac x="[(x,y)]∙ M" in meta_spec)apply (simp)apply (drule meta_mp)apply (drule_tac pi="[(x,y)]" in fin.eqvt(1))apply (simp add: calc_atm)apply (drule meta_mp)apply (drule_tac pi="[(x,y)]" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])apply (simp add: calc_atm CAND_eqvt_name)apply (simp)apply (case_tac "x=xa" )apply (simp)apply (drule_tac x="y" in meta_spec)apply (drule_tac x="[(xa,y)]∙ M" in meta_spec)apply (simp)apply (drule meta_mp)apply (drule_tac pi="[(xa,y)]" in fin.eqvt(1))apply (simp add: calc_atm)apply (drule meta_mp)apply (drule_tac pi="[(xa,y)]" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])apply (simp add: calc_atm CAND_eqvt_name)apply (simp)apply (simp)apply (case_tac "y=xa" )apply (simp)apply (drule_tac x="x" in meta_spec)apply (drule_tac x="[(x,xa)]∙ M" in meta_spec)apply (simp)apply (drule meta_mp)apply (drule_tac pi="[(x,xa)]" in fin.eqvt(1))apply (simp add: calc_atm)apply (drule meta_mp)apply (drule_tac pi="[(x,xa)]" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])apply (simp add: calc_atm CAND_eqvt_name)apply (simp)apply (simp)apply (drule_tac x="xa" in meta_spec)apply (drule_tac x="[(x,y)]∙ M" in meta_spec)apply (simp)apply (drule meta_mp)apply (drule_tac pi="[(x,y)]" in fin.eqvt(1))apply (simp add: calc_atm)apply (drule meta_mp)apply (drule_tac pi="[(x,y)]" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])apply (simp add: calc_atm CAND_eqvt_name)apply (simp)done lemma ANDLEFT2_elim:assumes a: "(x):M ∈ ANDLEFT2 (B AND C) (∥ (C)∥ )" obtains x' M' where "M = AndL2 (x').M' x" and "fin (AndL2 (x').M' x) x" and "(x'):M' ∈ (∥ ∥ )" using a [[ hypsubst_thin = true ]]apply (auto simp add: ntrm.inject alpha abs_fresh calc_atm)apply (drule_tac x="y" in meta_spec)apply (drule_tac x="[(x,y)]∙ M" in meta_spec)apply (simp)apply (drule meta_mp)apply (drule_tac pi="[(x,y)]" in fin.eqvt(1))apply (simp add: calc_atm)apply (drule meta_mp)apply (drule_tac pi="[(x,y)]" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])apply (simp add: calc_atm CAND_eqvt_name)apply (simp)apply (case_tac "x=xa" )apply (simp)apply (drule_tac x="y" in meta_spec)apply (drule_tac x="[(xa,y)]∙ M" in meta_spec)apply (simp)apply (drule meta_mp)apply (drule_tac pi="[(xa,y)]" in fin.eqvt(1))apply (simp add: calc_atm)apply (drule meta_mp)apply (drule_tac pi="[(xa,y)]" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])apply (simp add: calc_atm CAND_eqvt_name)apply (simp)apply (simp)apply (case_tac "y=xa" )apply (simp)apply (drule_tac x="x" in meta_spec)apply (drule_tac x="[(x,xa)]∙ M" in meta_spec)apply (simp)apply (drule meta_mp)apply (drule_tac pi="[(x,xa)]" in fin.eqvt(1))apply (simp add: calc_atm)apply (drule meta_mp)apply (drule_tac pi="[(x,xa)]" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])apply (simp add: calc_atm CAND_eqvt_name)apply (simp)apply (simp)apply (drule_tac x="xa" in meta_spec)apply (drule_tac x="[(x,y)]∙ M" in meta_spec)apply (simp)apply (drule meta_mp)apply (drule_tac pi="[(x,y)]" in fin.eqvt(1))apply (simp add: calc_atm)apply (drule meta_mp)apply (drule_tac pi="[(x,y)]" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])apply (simp add: calc_atm CAND_eqvt_name)apply (simp)done lemma ORRIGHT1_elim:assumes a: ":M ∈ ORRIGHT1 (B OR C) (∥ ∥ )" obtains a' M' where "M = OrR1 .M' a" and "fic (OrR1 .M' a) a" and ":M' ∈ (∥ ∥ )" using aapply (auto simp add: ctrm.inject alpha abs_fresh calc_atm)apply (drule_tac x="b" in meta_spec)apply (drule_tac x="[(a,b)]∙ Ma" in meta_spec)apply (simp)apply (drule meta_mp)apply (drule_tac pi="[(a,b)]" in fic.eqvt(2))apply (simp add: calc_atm)apply (drule meta_mp)apply (drule_tac pi="[(a,b)]" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (simp add: calc_atm CAND_eqvt_coname)apply (simp)apply (case_tac "a=aa" )apply (simp)apply (drule_tac x="b" in meta_spec)apply (drule_tac x="[(aa,b)]∙ Ma" in meta_spec)apply (simp)apply (drule meta_mp)apply (drule_tac pi="[(aa,b)]" in fic.eqvt(2))apply (simp add: calc_atm)apply (drule meta_mp)apply (drule_tac pi="[(aa,b)]" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (simp add: calc_atm CAND_eqvt_coname)apply (simp)apply (simp)apply (case_tac "b=aa" )apply (simp)apply (drule_tac x="a" in meta_spec)apply (drule_tac x="[(a,aa)]∙ Ma" in meta_spec)apply (simp)apply (drule meta_mp)apply (drule_tac pi="[(a,aa)]" in fic.eqvt(2))apply (simp add: calc_atm)apply (drule meta_mp)apply (drule_tac pi="[(a,aa)]" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (simp add: calc_atm CAND_eqvt_coname)apply (simp)apply (simp)apply (drule_tac x="aa" in meta_spec)apply (drule_tac x="[(a,b)]∙ Ma" in meta_spec)apply (simp)apply (drule meta_mp)apply (drule_tac pi="[(a,b)]" in fic.eqvt(2))apply (simp add: calc_atm)apply (drule meta_mp)apply (drule_tac pi="[(a,b)]" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (simp add: calc_atm CAND_eqvt_coname)apply (simp)done lemma ORRIGHT2_elim:assumes a: ":M ∈ ORRIGHT2 (B OR C) (∥ ∥ )" obtains a' M' where "M = OrR2 .M' a" and "fic (OrR2 .M' a) a" and ":M' ∈ (∥ ∥ )" using aapply (auto simp add: ctrm.inject alpha abs_fresh calc_atm)apply (drule_tac x="b" in meta_spec)apply (drule_tac x="[(a,b)]∙ Ma" in meta_spec)apply (simp)apply (drule meta_mp)apply (drule_tac pi="[(a,b)]" in fic.eqvt(2))apply (simp add: calc_atm)apply (drule meta_mp)apply (drule_tac pi="[(a,b)]" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (simp add: calc_atm CAND_eqvt_coname)apply (simp)apply (case_tac "a=aa" )apply (simp)apply (drule_tac x="b" in meta_spec)apply (drule_tac x="[(aa,b)]∙ Ma" in meta_spec)apply (simp)apply (drule meta_mp)apply (drule_tac pi="[(aa,b)]" in fic.eqvt(2))apply (simp add: calc_atm)apply (drule meta_mp)apply (drule_tac pi="[(aa,b)]" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (simp add: calc_atm CAND_eqvt_coname)apply (simp)apply (simp)apply (case_tac "b=aa" )apply (simp)apply (drule_tac x="a" in meta_spec)apply (drule_tac x="[(a,aa)]∙ Ma" in meta_spec)apply (simp)apply (drule meta_mp)apply (drule_tac pi="[(a,aa)]" in fic.eqvt(2))apply (simp add: calc_atm)apply (drule meta_mp)apply (drule_tac pi="[(a,aa)]" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (simp add: calc_atm CAND_eqvt_coname)apply (simp)apply (simp)apply (drule_tac x="aa" in meta_spec)apply (drule_tac x="[(a,b)]∙ Ma" in meta_spec)apply (simp)apply (drule meta_mp)apply (drule_tac pi="[(a,b)]" in fic.eqvt(2))apply (simp add: calc_atm)apply (drule meta_mp)apply (drule_tac pi="[(a,b)]" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (simp add: calc_atm CAND_eqvt_coname)apply (simp)done lemma ORLEFT_elim:assumes a: "(x):M ∈ ORLEFT (B OR C) (∥ (B)∥ ) (∥ (C)∥ )" obtains y' M' z' N' where "M = OrL (y').M' (z').N' x" and "fin (OrL (y').M' (z').N' x) x" and "(y'):M' ∈ (∥ (B)∥ )" and "(z'):N' ∈ (∥ (C)∥ )" using aapply (auto simp add: ntrm.inject alpha abs_fresh calc_atm fresh_atm)apply (drule_tac x="z" in meta_spec)apply (drule_tac x="[(x,z)]∙ Ma" in meta_spec)apply (drule_tac x="z" in meta_spec)apply (drule_tac x="[(x,z)]∙ N" in meta_spec)apply (simp)apply (drule meta_mp)apply (drule_tac pi="[(x,z)]" in fin.eqvt(1))apply (simp add: calc_atm)apply (drule meta_mp)apply (drule_tac pi="[(x,z)]" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])apply (simp add: calc_atm CAND_eqvt_name)apply (drule meta_mp)apply (drule_tac pi="[(x,z)]" and x="(x):N" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])apply (simp add: calc_atm CAND_eqvt_name)apply (simp)apply (case_tac "x=y" )apply (simp)apply (drule_tac x="z" in meta_spec)apply (drule_tac x="[(y,z)]∙ Ma" in meta_spec)apply (drule_tac x="z" in meta_spec)apply (drule_tac x="[(y,z)]∙ N" in meta_spec)apply (simp)apply (drule meta_mp)apply (drule_tac pi="[(y,z)]" in fin.eqvt(1))apply (simp add: calc_atm)apply (drule meta_mp)apply (drule_tac pi="[(y,z)]" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])apply (simp add: calc_atm CAND_eqvt_name)apply (drule meta_mp)apply (drule_tac pi="[(y,z)]" and x="(y):N" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])apply (simp add: calc_atm CAND_eqvt_name)apply (simp)apply (simp)apply (case_tac "z=y" )apply (simp)apply (drule_tac x="y" in meta_spec)apply (drule_tac x="[(x,y)]∙ Ma" in meta_spec)apply (drule_tac x="x" in meta_spec)apply (drule_tac x="[(x,y)]∙ N" in meta_spec)apply (simp)apply (drule meta_mp)apply (drule_tac pi="[(x,y)]" in fin.eqvt(1))apply (simp add: calc_atm)apply (drule meta_mp)apply (drule_tac pi="[(x,y)]" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])apply (simp add: calc_atm CAND_eqvt_name)apply (drule meta_mp)apply (drule_tac pi="[(x,y)]" and x="(y):N" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])apply (simp add: calc_atm CAND_eqvt_name)apply (simp)apply (simp)apply (drule_tac x="z" in meta_spec)apply (drule_tac x="[(x,z)]∙ Ma" in meta_spec)apply (drule_tac x="y" in meta_spec)apply (drule_tac x="[(x,z)]∙ N" in meta_spec)apply (simp)apply (drule meta_mp)apply (drule_tac pi="[(x,z)]" in fin.eqvt(1))apply (simp add: calc_atm)apply (drule meta_mp)apply (drule_tac pi="[(x,z)]" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])apply (simp add: calc_atm CAND_eqvt_name)apply (drule meta_mp)apply (drule_tac pi="[(x,z)]" and x="(y):N" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])apply (simp add: calc_atm CAND_eqvt_name)apply (simp)apply (case_tac "x=xa" )apply (simp)apply (drule_tac x="z" in meta_spec)apply (drule_tac x="[(xa,z)]∙ Ma" in meta_spec)apply (drule_tac x="z" in meta_spec)apply (drule_tac x="[(xa,z)]∙ N" in meta_spec)apply (simp)apply (drule meta_mp)apply (drule_tac pi="[(xa,z)]" in fin.eqvt(1))apply (simp add: calc_atm)apply (drule meta_mp)apply (drule_tac pi="[(xa,z)]" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])apply (simp add: calc_atm CAND_eqvt_name)apply (drule meta_mp)apply (drule_tac pi="[(xa,z)]" and x="(xa):N" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])apply (simp add: calc_atm CAND_eqvt_name)apply (simp)apply (simp)apply (case_tac "z=xa" )apply (simp)apply (drule_tac x="x" in meta_spec)apply (drule_tac x="[(x,xa)]∙ Ma" in meta_spec)apply (drule_tac x="xa" in meta_spec)apply (drule_tac x="[(x,xa)]∙ N" in meta_spec)apply (simp)apply (drule meta_mp)apply (drule_tac pi="[(x,xa)]" in fin.eqvt(1))apply (simp add: calc_atm)apply (drule meta_mp)apply (drule_tac pi="[(x,xa)]" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])apply (simp add: calc_atm CAND_eqvt_name)apply (drule meta_mp)apply (drule_tac pi="[(x,xa)]" and x="(x):N" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])apply (simp add: calc_atm CAND_eqvt_name)apply (simp)apply (simp)apply (drule_tac x="xa" in meta_spec)apply (drule_tac x="[(x,z)]∙ Ma" in meta_spec)apply (drule_tac x="z" in meta_spec)apply (drule_tac x="[(x,z)]∙ N" in meta_spec)apply (simp)apply (drule meta_mp)apply (drule_tac pi="[(x,z)]" in fin.eqvt(1))apply (simp add: calc_atm)apply (drule meta_mp)apply (drule_tac pi="[(x,z)]" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])apply (simp add: calc_atm CAND_eqvt_name)apply (drule meta_mp)apply (drule_tac pi="[(x,z)]" and x="(x):N" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])apply (simp add: calc_atm CAND_eqvt_name)apply (simp)apply (case_tac "x=xa" )apply (simp)apply (case_tac "xa=y" )apply (simp)apply (drule_tac x="z" in meta_spec)apply (drule_tac x="[(y,z)]∙ Ma" in meta_spec)apply (drule_tac x="z" in meta_spec)apply (drule_tac x="[(y,z)]∙ N" in meta_spec)apply (simp)apply (drule meta_mp)apply (drule_tac pi="[(y,z)]" in fin.eqvt(1))apply (simp add: calc_atm)apply (drule meta_mp)apply (drule_tac pi="[(y,z)]" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])apply (simp add: calc_atm CAND_eqvt_name)apply (drule meta_mp)apply (drule_tac pi="[(y,z)]" and x="(y):N" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])apply (simp add: calc_atm CAND_eqvt_name)apply (simp)apply (simp)apply (case_tac "z=y" )apply (simp)apply (drule_tac x="y" in meta_spec)apply (drule_tac x="[(xa,y)]∙ Ma" in meta_spec)apply (drule_tac x="xa" in meta_spec)apply (drule_tac x="[(xa,y)]∙ N" in meta_spec)apply (simp)apply (drule meta_mp)apply (drule_tac pi="[(xa,y)]" in fin.eqvt(1))apply (simp add: calc_atm)apply (drule meta_mp)apply (drule_tac pi="[(xa,y)]" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])apply (simp add: calc_atm CAND_eqvt_name)apply (drule meta_mp)apply (drule_tac pi="[(xa,y)]" and x="(y):N" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])apply (simp add: calc_atm CAND_eqvt_name)apply (simp)apply (simp)apply (drule_tac x="z" in meta_spec)apply (drule_tac x="[(xa,z)]∙ Ma" in meta_spec)apply (drule_tac x="y" in meta_spec)apply (drule_tac x="[(xa,z)]∙ N" in meta_spec)apply (simp)apply (drule meta_mp)apply (drule_tac pi="[(xa,z)]" in fin.eqvt(1))apply (simp add: calc_atm)apply (drule meta_mp)apply (drule_tac pi="[(xa,z)]" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])apply (simp add: calc_atm CAND_eqvt_name)apply (drule meta_mp)apply (drule_tac pi="[(xa,z)]" and x="(y):N" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])apply (simp add: calc_atm CAND_eqvt_name)apply (simp)apply (simp)apply (case_tac "z=xa" )apply (simp)apply (case_tac "x=y" )apply (simp)apply (drule_tac x="y" in meta_spec)apply (drule_tac x="[(y,xa)]∙ Ma" in meta_spec)apply (drule_tac x="xa" in meta_spec)apply (drule_tac x="[(y,xa)]∙ N" in meta_spec)apply (simp)apply (drule meta_mp)apply (drule_tac pi="[(y,xa)]" in fin.eqvt(1))apply (simp add: calc_atm)apply (drule meta_mp)apply (drule_tac pi="[(y,xa)]" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])apply (simp add: calc_atm CAND_eqvt_name)apply (drule meta_mp)apply (drule_tac pi="[(y,xa)]" and x="(y):N" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])apply (simp add: calc_atm CAND_eqvt_name)apply (simp)apply (simp)apply (case_tac "xa=y" )apply (simp)apply (drule_tac x="x" in meta_spec)apply (drule_tac x="[(x,y)]∙ Ma" in meta_spec)apply (drule_tac x="x" in meta_spec)apply (drule_tac x="[(x,y)]∙ N" in meta_spec)apply (simp)apply (drule meta_mp)apply (drule_tac pi="[(x,y)]" in fin.eqvt(1))apply (simp add: calc_atm)apply (drule meta_mp)apply (drule_tac pi="[(x,y)]" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])apply (simp add: calc_atm CAND_eqvt_name)apply (drule meta_mp)apply (drule_tac pi="[(x,y)]" and x="(y):N" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])apply (simp add: calc_atm CAND_eqvt_name)apply (simp)apply (simp)apply (drule_tac x="x" in meta_spec)apply (drule_tac x="[(x,xa)]∙ Ma" in meta_spec)apply (drule_tac x="y" in meta_spec)apply (drule_tac x="[(x,xa)]∙ N" in meta_spec)apply (simp)apply (drule meta_mp)apply (drule_tac pi="[(x,xa)]" in fin.eqvt(1))apply (simp add: calc_atm)apply (drule meta_mp)apply (drule_tac pi="[(x,xa)]" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])apply (simp add: calc_atm CAND_eqvt_name)apply (drule meta_mp)apply (drule_tac pi="[(x,xa)]" and x="(y):N" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])apply (simp add: calc_atm CAND_eqvt_name)apply (simp)apply (simp)apply (case_tac "x=y" )apply (simp)apply (drule_tac x="xa" in meta_spec)apply (drule_tac x="[(y,z)]∙ Ma" in meta_spec)apply (drule_tac x="z" in meta_spec)apply (drule_tac x="[(y,z)]∙ N" in meta_spec)apply (simp)apply (drule meta_mp)apply (drule_tac pi="[(y,z)]" in fin.eqvt(1))apply (simp add: calc_atm)apply (drule meta_mp)apply (drule_tac pi="[(y,z)]" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])apply (simp add: calc_atm CAND_eqvt_name)apply (drule meta_mp)apply (drule_tac pi="[(y,z)]" and x="(y):N" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])apply (simp add: calc_atm CAND_eqvt_name)apply (simp)apply (simp)apply (case_tac "z=y" )apply (simp)apply (drule_tac x="xa" in meta_spec)apply (drule_tac x="[(x,y)]∙ Ma" in meta_spec)apply (drule_tac x="x" in meta_spec)apply (drule_tac x="[(x,y)]∙ N" in meta_spec)apply (simp)apply (drule meta_mp)apply (drule_tac pi="[(x,y)]" in fin.eqvt(1))apply (simp add: calc_atm)apply (drule meta_mp)apply (drule_tac pi="[(x,y)]" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])apply (simp add: calc_atm CAND_eqvt_name)apply (drule meta_mp)apply (drule_tac pi="[(x,y)]" and x="(y):N" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])apply (simp add: calc_atm CAND_eqvt_name)apply (simp)apply (simp)apply (drule_tac x="xa" in meta_spec)apply (drule_tac x="[(x,z)]∙ Ma" in meta_spec)apply (drule_tac x="y" in meta_spec)apply (drule_tac x="[(x,z)]∙ N" in meta_spec)apply (simp)apply (drule meta_mp)apply (drule_tac pi="[(x,z)]" in fin.eqvt(1))apply (simp add: calc_atm)apply (drule meta_mp)apply (drule_tac pi="[(x,z)]" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])apply (simp add: calc_atm CAND_eqvt_name)apply (drule meta_mp)apply (drule_tac pi="[(x,z)]" and x="(y):N" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])apply (simp add: calc_atm CAND_eqvt_name)apply (simp)done lemma IMPRIGHT_elim:assumes a: ":M ∈ IMPRIGHT (B IMP C) (∥ (B)∥ ) (∥ ∥ ) (∥ (C)∥ ) (∥ ∥ )" obtains x' a' M' where "M = ImpR (x')..M' a" and "fic (ImpR (x')..M' a) a" and "∀ z P. x'♯ (z,P) ∧ (z):P ∈ ∥ (C)∥ ⟶ (x'):(M'{a':=(z).P}) ∈ ∥ (B)∥ " and "∀ c Q. a'♯ (c,Q) ∧ :Q ∈ ∥ ∥ ⟶ :(M'{x':=.Q}) ∈ ∥ ∥ " using aapply (auto simp add: ctrm.inject alpha abs_fresh calc_atm)apply (drule_tac x="x" in meta_spec)apply (drule_tac x="b" in meta_spec)apply (drule_tac x="[(a,b)]∙ Ma" in meta_spec)apply (simp)apply (drule_tac pi="[(a,b)]" in fic.eqvt(2))apply (simp add: calc_atm)apply (drule meta_mp)apply (auto)[1]apply (drule_tac pi="[(a,b)]" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (simp add: calc_atm CAND_eqvt_coname)apply (drule_tac x="z" in spec)apply (drule_tac x="[(a,b)]∙ P" in spec)apply (simp add: fresh_prod fresh_left calc_atm)apply (drule_tac pi="[(a,b)]" and x="(x):Ma{a:=(z).([(a,b)]∙ P)}" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (perm_simp add: calc_atm csubst_eqvt CAND_eqvt_coname)apply (drule meta_mp)apply (auto)[1]apply (drule_tac pi="[(a,b)]" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (simp add: CAND_eqvt_coname)apply (rotate_tac 2)apply (drule_tac x="[(a,b)]∙ c" in spec)apply (drule_tac x="[(a,b)]∙ Q" in spec)apply (simp add: fresh_prod fresh_left)apply (drule mp)apply (simp add: calc_atm)apply (drule_tac pi="[(a,b)]" and x=":Ma{x:=<([(a,b)]∙ c)>.([(a,b)]∙ Q)}" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (perm_simp add: nsubst_eqvt CAND_eqvt_coname)apply (simp add: calc_atm)apply (case_tac "a=aa" )apply (simp)apply (drule_tac x="x" in meta_spec)apply (drule_tac x="b" in meta_spec)apply (drule_tac x="[(aa,b)]∙ Ma" in meta_spec)apply (simp)apply (drule meta_mp)apply (drule_tac pi="[(aa,b)]" in fic.eqvt(2))apply (simp add: calc_atm)apply (drule meta_mp)apply (auto)[1]apply (drule_tac pi="[(a,b)]" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (simp add: calc_atm CAND_eqvt_coname)apply (drule_tac x="z" in spec)apply (drule_tac x="[(a,b)]∙ P" in spec)apply (simp add: fresh_prod fresh_left calc_atm)apply (drule_tac pi="[(a,b)]" and x="(x):Ma{a:=(z).([(a,b)]∙ P)}" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (perm_simp add: calc_atm csubst_eqvt CAND_eqvt_coname)apply (drule meta_mp)apply (auto)[1]apply (drule_tac pi="[(a,b)]" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (simp add: CAND_eqvt_coname)apply (drule_tac x="[(a,b)]∙ c" in spec)apply (drule_tac x="[(a,b)]∙ Q" in spec)apply (simp)apply (simp add: fresh_prod fresh_left)apply (drule mp)apply (simp add: calc_atm)apply (drule_tac pi="[(a,b)]" and x=":Ma{x:=<([(a,b)]∙ c)>.([(a,b)]∙ Q)}" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (perm_simp add: nsubst_eqvt CAND_eqvt_coname)apply (simp add: calc_atm)apply (simp)apply (case_tac "b=aa" )apply (simp)apply (drule_tac x="x" in meta_spec)apply (drule_tac x="a" in meta_spec)apply (drule_tac x="[(a,aa)]∙ Ma" in meta_spec)apply (simp)apply (drule meta_mp)apply (drule_tac pi="[(a,aa)]" in fic.eqvt(2))apply (simp add: calc_atm)apply (drule meta_mp)apply (auto)[1]apply (drule_tac pi="[(a,aa)]" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (simp add: calc_atm CAND_eqvt_coname)apply (drule_tac x="z" in spec)apply (drule_tac x="[(a,aa)]∙ P" in spec)apply (simp add: fresh_prod fresh_left calc_atm)apply (drule_tac pi="[(a,aa)]" and x="(x):Ma{aa:=(z).([(a,aa)]∙ P)}" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (perm_simp add: calc_atm csubst_eqvt CAND_eqvt_coname)apply (drule meta_mp)apply (auto)[1]apply (drule_tac pi="[(a,aa)]" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (simp add: CAND_eqvt_coname)apply (drule_tac x="[(a,aa)]∙ c" in spec)apply (drule_tac x="[(a,aa)]∙ Q" in spec)apply (simp)apply (simp add: fresh_prod fresh_left)apply (drule mp)apply (simp add: calc_atm)apply (drule_tac pi="[(a,aa)]" and x=":Ma{x:=<([(a,aa)]∙ c)>.([(a,aa)]∙ Q)}" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (perm_simp add: nsubst_eqvt CAND_eqvt_coname)apply (simp add: calc_atm)apply (simp)apply (drule_tac x="x" in meta_spec)apply (drule_tac x="aa" in meta_spec)apply (drule_tac x="[(a,b)]∙ Ma" in meta_spec)apply (simp)apply (drule meta_mp)apply (drule_tac pi="[(a,b)]" in fic.eqvt(2))apply (simp add: calc_atm)apply (drule meta_mp)apply (auto)[1]apply (drule_tac pi="[(a,b)]" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (simp add: calc_atm CAND_eqvt_coname)apply (drule_tac x="z" in spec)apply (drule_tac x="[(a,b)]∙ P" in spec)apply (simp add: fresh_prod fresh_left calc_atm)apply (drule_tac pi="[(a,b)]" and x="(x):Ma{aa:=(z).([(a,b)]∙ P)}" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (perm_simp add: calc_atm csubst_eqvt CAND_eqvt_coname)apply (drule meta_mp)apply (auto)[1]apply (drule_tac pi="[(a,b)]" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (simp add: CAND_eqvt_coname)apply (drule_tac x="[(a,b)]∙ c" in spec)apply (drule_tac x="[(a,b)]∙ Q" in spec)apply (simp add: fresh_prod fresh_left)apply (drule mp)apply (simp add: calc_atm)apply (drule_tac pi="[(a,b)]" and x=":Ma{x:=<([(a,b)]∙ c)>.([(a,b)]∙ Q)}" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (perm_simp add: nsubst_eqvt CAND_eqvt_coname)apply (simp add: calc_atm)done lemma IMPLEFT_elim:assumes a: "(x):M ∈ IMPLEFT (B IMP C) (∥ ∥ ) (∥ (C)∥ )" obtains x' a' M' N' where "M = ImpL .M' (x').N' x" and "fin (ImpL .M' (x').N' x) x" and ":M' ∈ ∥ ∥ " and "(x'):N' ∈ ∥ (C)∥ " using aapply (auto simp add: ntrm.inject alpha abs_fresh calc_atm)apply (drule_tac x="a" in meta_spec)apply (drule_tac x="[(x,y)]∙ Ma" in meta_spec)apply (drule_tac x="y" in meta_spec)apply (drule_tac x="[(x,y)]∙ N" in meta_spec)apply (simp)apply (drule meta_mp)apply (drule_tac pi="[(x,y)]" in fin.eqvt(1))apply (simp add: calc_atm)apply (drule meta_mp)apply (drule_tac pi="[(x,y)]" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])apply (simp add: calc_atm CAND_eqvt_name)apply (drule meta_mp)apply (drule_tac pi="[(x,y)]" and x="(x):N" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])apply (perm_simp add: calc_atm CAND_eqvt_name)apply (simp)apply (case_tac "x=xa" )apply (simp)apply (drule_tac x="a" in meta_spec)apply (drule_tac x="[(xa,y)]∙ Ma" in meta_spec)apply (drule_tac x="y" in meta_spec)apply (drule_tac x="[(xa,y)]∙ N" in meta_spec)apply (simp)apply (drule meta_mp)apply (drule_tac pi="[(xa,y)]" in fin.eqvt(1))apply (simp add: calc_atm)apply (drule meta_mp)apply (drule_tac pi="[(xa,y)]" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])apply (simp add: calc_atm CAND_eqvt_name)apply (drule meta_mp)apply (drule_tac pi="[(xa,y)]" and x="(xa):N" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])apply (simp add: calc_atm CAND_eqvt_name)apply (simp)apply (simp)apply (case_tac "y=xa" )apply (simp)apply (drule_tac x="a" in meta_spec)apply (drule_tac x="[(x,xa)]∙ Ma" in meta_spec)apply (drule_tac x="x" in meta_spec)apply (drule_tac x="[(x,xa)]∙ N" in meta_spec)apply (simp)apply (drule meta_mp)apply (drule_tac pi="[(x,xa)]" in fin.eqvt(1))apply (simp add: calc_atm)apply (drule meta_mp)apply (drule_tac pi="[(x,xa)]" and x=":Ma" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])apply (simp add: calc_atm CAND_eqvt_name)apply (drule meta_mp)apply (drule_tac pi="[(x,xa)]" and x="(xa):N" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])apply (simp add: calc_atm CAND_eqvt_name)apply (simp)apply (simp)apply (drule_tac x="a" in meta_spec)apply (drule_tac x="[(x,y)]∙ Ma" in meta_spec)apply (drule_tac x="xa" in meta_spec)apply (drule_tac x="[(x,y)]∙ N" in meta_spec)apply (simp)apply (drule meta_mp)apply (drule_tac pi="[(x,y)]" in fin.eqvt(1))apply (simp add: calc_atm)apply (drule meta_mp)apply (drule_tac pi="[(x,y)]" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])apply (simp add: calc_atm CAND_eqvt_name)apply (drule meta_mp)apply (drule_tac pi="[(x,y)]" and x="(xa):N" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])apply (simp add: calc_atm CAND_eqvt_name)apply (simp)done lemma CANDs_alpha:shows ":M ∈ (∥ ∥ ) ==> [a].M = [b].N ==> :N ∈ (∥ ∥ )" and "(x):M ∈ (∥ (B)∥ ) ==> [x].M = [y].N ==> (y):N ∈ (∥ (B)∥ )" apply (auto simp add: alpha)apply (drule_tac pi="[(a,b)]" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (perm_simp add: CAND_eqvt_coname calc_atm)apply (drule_tac pi="[(x,y)]" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])apply (perm_simp add: CAND_eqvt_name calc_atm)done lemma CAND_NotR_elim:assumes a: ":NotR (x).M a ∈ (∥ ∥ )" ":NotR (x).M a ∉ BINDINGc B (∥ (B)∥ )" shows "∃ B'. B = NOT B' ∧ (x):M ∈ (∥ (B')∥ )" using aapply (nominal_induct B rule: ty.strong_induct)apply (simp_all add: ty.inject AXIOMSc_def ctrm.inject alpha)apply (auto intro: CANDs_alpha simp add: trm.inject calc_atm abs_fresh fresh_atm)apply (drule_tac pi="[(a,aa)]" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (auto simp add: CAND_eqvt_coname calc_atm intro: CANDs_alpha)done lemma CAND_NotL_elim_aux:assumes a: "(x):NotL .M x ∈ NEGn B (∥ ∥ )" "(x):NotL .M x ∉ BINDINGn B (∥ ∥ )" shows "∃ B'. B = NOT B' ∧ :M ∈ (∥ ∥ )" using aapply (nominal_induct B rule: ty.strong_induct)apply (simp_all add: ty.inject AXIOMSn_def ntrm.inject alpha)apply (auto intro: CANDs_alpha simp add: trm.inject calc_atm abs_fresh fresh_atm)apply (drule_tac pi="[(x,xa)]" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])apply (auto simp add: CAND_eqvt_name calc_atm intro: CANDs_alpha)done lemmas CAND_NotL_elim = CAND_NotL_elim_aux[OF NEG_elim(2)]lemma CAND_AndR_elim:assumes a: ":AndR .M .N a ∈ (∥ ∥ )" ":AndR .M .N a ∉ BINDINGc B (∥ (B)∥ )" shows "∃ B1 B2. B = B1 AND B2 ∧ :M ∈ (∥ ∥ ) ∧ :N ∈ (∥ ∥ )" using aapply (nominal_induct B rule: ty.strong_induct)apply (simp_all add: ty.inject AXIOMSc_def ctrm.inject alpha)apply (auto intro: CANDs_alpha simp add: trm.inject calc_atm abs_fresh fresh_atm)apply (drule_tac pi="[(a,ca)]" and x=":Ma" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (simp add: CAND_eqvt_coname calc_atm)apply (auto intro: CANDs_alpha)[1]apply (drule_tac pi="[(a,ca)]" and x=":Na" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (simp add: CAND_eqvt_coname calc_atm)apply (auto intro: CANDs_alpha)[1]apply (drule_tac pi="[(a,ca)]" and x=":Ma" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (simp add: CAND_eqvt_coname calc_atm)apply (auto intro: CANDs_alpha)[1]apply (case_tac "a=ba" )apply (simp)apply (drule_tac pi="[(ba,ca)]" and x=":Na" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (simp add: CAND_eqvt_coname calc_atm)apply (auto intro: CANDs_alpha)[1]apply (simp)apply (case_tac "ca=ba" )apply (simp)apply (drule_tac pi="[(a,ba)]" and x=":Na" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (simp add: CAND_eqvt_coname calc_atm)apply (auto intro: CANDs_alpha)[1]apply (simp)apply (drule_tac pi="[(a,ca)]" and x=":Na" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (simp add: CAND_eqvt_coname calc_atm)apply (auto intro: CANDs_alpha)[1]apply (case_tac "a=aa" )apply (simp)apply (drule_tac pi="[(aa,ca)]" and x=":Ma" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (simp add: CAND_eqvt_coname calc_atm)apply (auto intro: CANDs_alpha)[1]apply (simp)apply (case_tac "ca=aa" )apply (simp)apply (drule_tac pi="[(a,aa)]" and x=":Ma" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (simp add: CAND_eqvt_coname calc_atm)apply (auto intro: CANDs_alpha)[1]apply (simp)apply (drule_tac pi="[(a,ca)]" and x=":Ma" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (simp add: CAND_eqvt_coname calc_atm)apply (auto intro: CANDs_alpha)[1]apply (drule_tac pi="[(a,ca)]" and x=":Na" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (simp add: CAND_eqvt_coname calc_atm)apply (auto intro: CANDs_alpha)[1]apply (case_tac "a=aa" )apply (simp)apply (drule_tac pi="[(aa,ca)]" and x=":Ma" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (simp add: CAND_eqvt_coname calc_atm)apply (auto intro: CANDs_alpha)[1]apply (simp)apply (case_tac "ca=aa" )apply (simp)apply (drule_tac pi="[(a,aa)]" and x=":Ma" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (simp add: CAND_eqvt_coname calc_atm)apply (auto intro: CANDs_alpha)[1]apply (simp)apply (drule_tac pi="[(a,ca)]" and x=":Ma" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (simp add: CAND_eqvt_coname calc_atm)apply (auto intro: CANDs_alpha)[1]apply (case_tac "a=ba" )apply (simp)apply (drule_tac pi="[(ba,ca)]" and x=":Na" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (simp add: CAND_eqvt_coname calc_atm)apply (auto intro: CANDs_alpha)[1]apply (simp)apply (case_tac "ca=ba" )apply (simp)apply (drule_tac pi="[(a,ba)]" and x=":Na" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (simp add: CAND_eqvt_coname calc_atm)apply (auto intro: CANDs_alpha)[1]apply (simp)apply (drule_tac pi="[(a,ca)]" and x=":Na" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (simp add: CAND_eqvt_coname calc_atm)apply (auto intro: CANDs_alpha)[1]done lemma CAND_OrR1_elim:assumes a: ":OrR1 .M a ∈ (∥ ∥ )" ":OrR1 .M a ∉ BINDINGc B (∥ (B)∥ )" shows "∃ B1 B2. B = B1 OR B2 ∧ :M ∈ (∥ ∥ )" using aapply (nominal_induct B rule: ty.strong_induct)apply (simp_all add: ty.inject AXIOMSc_def ctrm.inject alpha)apply (auto intro: CANDs_alpha simp add: trm.inject calc_atm abs_fresh fresh_atm)apply (drule_tac pi="[(a,ba)]" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (auto simp add: CAND_eqvt_coname calc_atm intro: CANDs_alpha)apply (case_tac "a=aa" )apply (simp)apply (drule_tac pi="[(aa,ba)]" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (auto simp add: CAND_eqvt_coname calc_atm intro: CANDs_alpha)apply (case_tac "ba=aa" )apply (simp)apply (drule_tac pi="[(a,aa)]" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (auto simp add: CAND_eqvt_coname calc_atm intro: CANDs_alpha)apply (drule_tac pi="[(a,ba)]" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (auto simp add: CAND_eqvt_coname calc_atm intro: CANDs_alpha)done lemma CAND_OrR2_elim:assumes a: ":OrR2 .M a ∈ (∥ ∥ )" ":OrR2 .M a ∉ BINDINGc B (∥ (B)∥ )" shows "∃ B1 B2. B = B1 OR B2 ∧ :M ∈ (∥ ∥ )" using aapply (nominal_induct B rule: ty.strong_induct)apply (simp_all add: ty.inject AXIOMSc_def ctrm.inject alpha)apply (auto intro: CANDs_alpha simp add: trm.inject calc_atm abs_fresh fresh_atm)apply (drule_tac pi="[(a,ba)]" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (auto simp add: CAND_eqvt_coname calc_atm intro: CANDs_alpha)apply (case_tac "a=aa" )apply (simp)apply (drule_tac pi="[(aa,ba)]" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (auto simp add: CAND_eqvt_coname calc_atm intro: CANDs_alpha)apply (case_tac "ba=aa" )apply (simp)apply (drule_tac pi="[(a,aa)]" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (auto simp add: CAND_eqvt_coname calc_atm intro: CANDs_alpha)apply (drule_tac pi="[(a,ba)]" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (auto simp add: CAND_eqvt_coname calc_atm intro: CANDs_alpha)done lemma CAND_OrL_elim_aux:assumes a: "(x):(OrL (y).M (z).N x) ∈ NEGn B (∥ ∥ )" "(x):(OrL (y).M (z).N x) ∉ BINDINGn B (∥ ∥ )" shows "∃ B1 B2. B = B1 OR B2 ∧ (y):M ∈ (∥ (B1)∥ ) ∧ (z):N ∈ (∥ (B2)∥ )" using aapply (nominal_induct B rule: ty.strong_induct)apply (simp_all add: ty.inject AXIOMSn_def ntrm.inject alpha)apply (auto intro: CANDs_alpha simp add: trm.inject calc_atm abs_fresh fresh_atm)apply (drule_tac pi="[(x,za)]" and x="(x):Ma" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])apply (simp add: CAND_eqvt_name calc_atm)apply (auto intro: CANDs_alpha)[1]apply (drule_tac pi="[(x,za)]" and x="(x):Na" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])apply (simp add: CAND_eqvt_name calc_atm)apply (auto intro: CANDs_alpha)[1]apply (drule_tac pi="[(x,za)]" and x="(x):Ma" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])apply (simp add: CAND_eqvt_name calc_atm)apply (auto intro: CANDs_alpha)[1]apply (case_tac "x=ya" )apply (simp)apply (drule_tac pi="[(ya,za)]" and x="(ya):Na" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])apply (simp add: CAND_eqvt_name calc_atm)apply (auto intro: CANDs_alpha)[1]apply (simp)apply (case_tac "za=ya" )apply (simp)apply (drule_tac pi="[(x,ya)]" and x="(ya):Na" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])apply (simp add: CAND_eqvt_name calc_atm)apply (auto intro: CANDs_alpha)[1]apply (simp)apply (drule_tac pi="[(x,za)]" and x="(ya):Na" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])apply (simp add: CAND_eqvt_name calc_atm)apply (auto intro: CANDs_alpha)[1]apply (case_tac "x=xa" )apply (simp)apply (drule_tac pi="[(xa,za)]" and x="(xa):Ma" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])apply (simp add: CAND_eqvt_name calc_atm)apply (auto intro: CANDs_alpha)[1]apply (simp)apply (case_tac "za=xa" )apply (simp)apply (drule_tac pi="[(x,xa)]" and x="(xa):Ma" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])apply (simp add: CAND_eqvt_name calc_atm)apply (auto intro: CANDs_alpha)[1]apply (simp)apply (drule_tac pi="[(x,za)]" and x="(xa):Ma" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])apply (simp add: CAND_eqvt_name calc_atm)apply (auto intro: CANDs_alpha)[1]apply (drule_tac pi="[(x,za)]" and x="(x):Na" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])apply (simp add: CAND_eqvt_name calc_atm)apply (auto intro: CANDs_alpha)[1]apply (case_tac "x=xa" )apply (simp)apply (drule_tac pi="[(xa,za)]" and x="(xa):Ma" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])apply (simp add: CAND_eqvt_name calc_atm)apply (auto intro: CANDs_alpha)[1]apply (simp)apply (case_tac "za=xa" )apply (simp)apply (drule_tac pi="[(x,xa)]" and x="(xa):Ma" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])apply (simp add: CAND_eqvt_name calc_atm)apply (auto intro: CANDs_alpha)[1]apply (simp)apply (drule_tac pi="[(x,za)]" and x="(xa):Ma" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])apply (simp add: CAND_eqvt_name calc_atm)apply (auto intro: CANDs_alpha)[1]apply (case_tac "x=ya" )apply (simp)apply (drule_tac pi="[(ya,za)]" and x="(ya):Na" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])apply (simp add: CAND_eqvt_name calc_atm)apply (auto intro: CANDs_alpha)[1]apply (simp)apply (case_tac "za=ya" )apply (simp)apply (drule_tac pi="[(x,ya)]" and x="(ya):Na" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])apply (simp add: CAND_eqvt_name calc_atm)apply (auto intro: CANDs_alpha)[1]apply (simp)apply (drule_tac pi="[(x,za)]" and x="(ya):Na" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])apply (simp add: CAND_eqvt_name calc_atm)apply (auto intro: CANDs_alpha)[1]done lemmas CAND_OrL_elim = CAND_OrL_elim_aux[OF NEG_elim(2)]lemma CAND_AndL1_elim_aux:assumes a: "(x):(AndL1 (y).M x) ∈ NEGn B (∥ ∥ )" "(x):(AndL1 (y).M x) ∉ BINDINGn B (∥ ∥ shows "∃ B1 B2. B = B1 AND B2 ∧ (y):M ∈ (∥ (B1)∥ )" using aapply (nominal_induct B rule: ty.strong_induct)apply (simp_all add: ty.inject AXIOMSn_def ntrm.inject alpha)apply (auto intro: CANDs_alpha simp add: trm.inject calc_atm abs_fresh fresh_atm)apply (drule_tac pi="[(x,ya)]" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])apply (auto simp add: CAND_eqvt_name calc_atm intro: CANDs_alpha)apply (case_tac "x=xa" )apply (simp)apply (drule_tac pi="[(xa,ya)]" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])apply (auto simp add: CAND_eqvt_name calc_atm intro: CANDs_alpha)apply (case_tac "ya=xa" )apply (simp)apply (drule_tac pi="[(x,xa)]" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])apply (auto simp add: CAND_eqvt_name calc_atm intro: CANDs_alpha)apply (drule_tac pi="[(x,ya)]" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])apply (auto simp add: CAND_eqvt_name calc_atm intro: CANDs_alpha)done lemmas CAND_AndL1_elim = CAND_AndL1_elim_aux[OF NEG_elim(2)]lemma CAND_AndL2_elim_aux:assumes a: "(x):(AndL2 (y).M x) ∈ NEGn B (∥ ∥ )" "(x):(AndL2 (y).M x) ∉ BINDINGn B (∥ ∥ shows "∃ B1 B2. B = B1 AND B2 ∧ (y):M ∈ (∥ (B2)∥ )" using aapply (nominal_induct B rule: ty.strong_induct)apply (simp_all add: ty.inject AXIOMSn_def ntrm.inject alpha)apply (auto intro: CANDs_alpha simp add: trm.inject calc_atm abs_fresh fresh_atm)apply (drule_tac pi="[(x,ya)]" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])apply (auto simp add: CAND_eqvt_name calc_atm intro: CANDs_alpha)apply (case_tac "x=xa" )apply (simp)apply (drule_tac pi="[(xa,ya)]" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])apply (auto simp add: CAND_eqvt_name calc_atm intro: CANDs_alpha)apply (case_tac "ya=xa" )apply (simp)apply (drule_tac pi="[(x,xa)]" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])apply (auto simp add: CAND_eqvt_name calc_atm intro: CANDs_alpha)apply (drule_tac pi="[(x,ya)]" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])apply (auto simp add: CAND_eqvt_name calc_atm intro: CANDs_alpha)done lemmas CAND_AndL2_elim = CAND_AndL2_elim_aux[OF NEG_elim(2)]lemma CAND_ImpL_elim_aux:assumes a: "(x):(ImpL .M (z).N x) ∈ NEGn B (∥ ∥ )" "(x):(ImpL .M (z).N x) ∉ BINDINGn B (∥ ∥ )" shows "∃ B1 B2. B = B1 IMP B2 ∧ :M ∈ (∥ ∥ ) ∧ (z):N ∈ (∥ (B2)∥ )" using aapply (nominal_induct B rule: ty.strong_induct)apply (simp_all add: ty.inject AXIOMSn_def ntrm.inject alpha)apply (auto intro: CANDs_alpha simp add: trm.inject calc_atm abs_fresh fresh_atm)apply (drule_tac pi="[(x,y)]" and x=":Ma" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])apply (simp add: CAND_eqvt_name calc_atm)apply (auto intro: CANDs_alpha)[1]apply (drule_tac pi="[(x,y)]" and x="(x):Na" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])apply (simp add: CAND_eqvt_name calc_atm)apply (auto intro: CANDs_alpha)[1]apply (drule_tac pi="[(x,y)]" and x=":Ma" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])apply (simp add: CAND_eqvt_name calc_atm)apply (auto intro: CANDs_alpha)[1]apply (case_tac "x=xa" )apply (simp)apply (drule_tac pi="[(xa,y)]" and x="(xa):Na" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])apply (simp add: CAND_eqvt_name calc_atm)apply (auto intro: CANDs_alpha)[1]apply (simp)apply (case_tac "y=xa" )apply (simp)apply (drule_tac pi="[(x,xa)]" and x="(xa):Na" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])apply (simp add: CAND_eqvt_name calc_atm)apply (auto intro: CANDs_alpha)[1]apply (simp)apply (drule_tac pi="[(x,y)]" and x="(xa):Na" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])apply (simp add: CAND_eqvt_name calc_atm)apply (auto intro: CANDs_alpha)[1]done lemmas CAND_ImpL_elim = CAND_ImpL_elim_aux[OF NEG_elim(2)]lemma CAND_ImpR_elim:assumes a: ":ImpR (x)..M a ∈ (∥ ∥ )" ":ImpR (x)..M a ∉ BINDINGc B (∥ (B)∥ )" shows "∃ B1 B2. B = B1 IMP B2 ∧ (∀ z P. x♯ (z,P) ∧ (z):P ∈ ∥ (B2)∥ ⟶ (x):(M{b:=(z).P}) ∈ ∥ (B1)∥ ) ∧ (∀ c Q. b♯ (c,Q) ∧ :Q ∈ ∥ ∥ ⟶ :(M{x:=.Q}) ∈ ∥ ∥ )" using aapply (nominal_induct B rule: ty.strong_induct)apply (simp_all add: ty.inject AXIOMSc_def ctrm.inject alpha)apply (auto intro: CANDs_alpha simp add: trm.inject calc_atm abs_fresh fresh_atm fresh_prod fresh_bij)apply (generate_fresh "name" ) apply (generate_fresh "coname" )apply (drule_tac a="ca" and z="c" in alpha_name_coname)apply (simp) apply (simp) apply (simp) apply (drule_tac x="[(xa,c)]∙ [(aa,ca)]∙ [(b,ca)]∙ [(x,c)]∙ z" in spec)apply (drule_tac x="[(xa,c)]∙ [(aa,ca)]∙ [(b,ca)]∙ [(x,c)]∙ P" in spec)apply (drule mp)apply (rule conjI)apply (auto simp add: calc_atm fresh_prod fresh_atm)[1]apply (rule conjI)apply (auto simp add: fresh_left calc_atm fresh_prod fresh_atm)[1]apply (drule_tac pi="[(x,c)]" and X="∥ (ty2)∥ " in pt_set_bij2[OF pt_name_inst, OF at_name_inst])apply (simp add: CAND_eqvt_name CAND_eqvt_coname)apply (drule_tac pi="[(b,ca)]" and X="∥ (ty2)∥ " in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (simp add: CAND_eqvt_name CAND_eqvt_coname)apply (drule_tac pi="[(aa,ca)]" and X="∥ (ty2)∥ " in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (simp add: CAND_eqvt_name CAND_eqvt_coname)apply (drule_tac pi="[(xa,c)]" and X="∥ (ty2)∥ " in pt_set_bij2[OF pt_name_inst, OF at_name_inst])apply (simp add: CAND_eqvt_name CAND_eqvt_coname)apply (drule_tac pi="[(xa,c)]" and X="∥ (ty1)∥ " in pt_set_bij2[OF pt_name_inst, OF at_name_inst])apply (simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt)apply (drule_tac pi="[(aa,ca)]" and X="∥ (ty1)∥ " in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt)apply (drule_tac pi="[(b,ca)]" and X="∥ (ty1)∥ " in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (simp add: CAND_eqvt_name CAND_eqvt_coname)apply (drule_tac pi="[(x,c)]" and X="∥ (ty1)∥ " in pt_set_bij2[OF pt_name_inst, OF at_name_inst])apply (perm_simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt)apply (generate_fresh "name" )apply (generate_fresh "coname" )apply (drule_tac a="cb" and z="ca" in alpha_name_coname)apply (simp)apply (simp)apply (simp)apply (drule_tac x="[(xa,ca)]∙ [(aa,cb)]∙ [(b,cb)]∙ [(x,ca)]∙ c" in spec)apply (drule_tac x="[(xa,ca)]∙ [(aa,cb)]∙ [(b,cb)]∙ [(x,ca)]∙ Q" in spec)apply (drule mp)apply (rule conjI)apply (auto simp add: calc_atm fresh_prod fresh_atm)[1]apply (rule conjI)apply (auto simp add: fresh_left calc_atm fresh_prod fresh_atm)[1]apply (drule_tac pi="[(x,ca)]" and X="∥ ∥ " in pt_set_bij2[OF pt_name_inst, OF at_name_inst])apply (simp add: CAND_eqvt_name CAND_eqvt_coname)apply (drule_tac pi="[(b,cb)]" and X="∥ ∥ " in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (simp add: CAND_eqvt_name CAND_eqvt_coname)apply (drule_tac pi="[(aa,cb)]" and X="∥ ∥ " in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (simp add: CAND_eqvt_name CAND_eqvt_coname)apply (drule_tac pi="[(xa,ca)]" and X="∥ ∥ " in pt_set_bij2[OF pt_name_inst, OF at_name_inst])apply (simp add: CAND_eqvt_name CAND_eqvt_coname)apply (drule_tac pi="[(xa,ca)]" and X="∥ ∥ " in pt_set_bij2[OF pt_name_inst, OF at_name_inst])apply (simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt)apply (drule_tac pi="[(aa,cb)]" and X="∥ ∥ " in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt)apply (drule_tac pi="[(b,cb)]" and X="∥ ∥ " in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (simp add: CAND_eqvt_name CAND_eqvt_coname)apply (drule_tac pi="[(x,ca)]" and X="∥ ∥ " in pt_set_bij2[OF pt_name_inst, OF at_name_inst])apply (perm_simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt)apply (generate_fresh "name" )apply (generate_fresh "coname" )apply (drule_tac a="ca" and z="c" in alpha_name_coname)apply (simp add: fresh_left calc_atm fresh_prod fresh_atm)apply (simp add: fresh_left calc_atm fresh_prod fresh_atm)apply (auto)[1]apply (simp)apply (drule_tac x="[(a,ba)]∙ [(xa,c)]∙ [(ba,ca)]∙ [(b,ca)]∙ [(x,c)]∙ z" in spec)apply (drule_tac x="[(a,ba)]∙ [(xa,c)]∙ [(ba,ca)]∙ [(b,ca)]∙ [(x,c)]∙ P" in spec)apply (drule mp)apply (rule conjI)apply (auto simp add: calc_atm fresh_prod fresh_atm)[1]apply (rule conjI)apply (auto simp add: fresh_left calc_atm fresh_prod fresh_atm)[1]apply (drule_tac pi="[(x,c)]" and X="∥ (ty2)∥ " in pt_set_bij2[OF pt_name_inst, OF at_name_inst])apply (simp add: CAND_eqvt_name CAND_eqvt_coname)apply (drule_tac pi="[(b,ca)]" and X="∥ (ty2)∥ " in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (simp add: CAND_eqvt_name CAND_eqvt_coname)apply (drule_tac pi="[(ba,ca)]" and X="∥ (ty2)∥ " in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (simp add: CAND_eqvt_name CAND_eqvt_coname)apply (drule_tac pi="[(xa,c)]" and X="∥ (ty2)∥ " in pt_set_bij2[OF pt_name_inst, OF at_name_inst])apply (simp add: CAND_eqvt_name CAND_eqvt_coname)apply (drule_tac pi="[(a,ba)]" and X="∥ (ty2)∥ " in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (simp add: CAND_eqvt_name CAND_eqvt_coname)apply (drule_tac pi="[(a,ba)]" and X="∥ (ty1)∥ " in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt)apply (drule_tac pi="[(xa,c)]" and X="∥ (ty1)∥ " in pt_set_bij2[OF pt_name_inst, OF at_name_inst])apply (simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt)apply (drule_tac pi="[(ba,ca)]" and X="∥ (ty1)∥ " in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt)apply (drule_tac pi="[(b,ca)]" and X="∥ (ty1)∥ " in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (simp add: CAND_eqvt_name CAND_eqvt_coname)apply (drule_tac pi="[(x,c)]" and X="∥ (ty1)∥ " in pt_set_bij2[OF pt_name_inst, OF at_name_inst])apply (perm_simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt)apply (generate_fresh "name" )apply (generate_fresh "coname" )apply (drule_tac a="cb" and z="ca" in alpha_name_coname)apply (simp add: fresh_left calc_atm fresh_prod fresh_atm)apply (simp add: fresh_left calc_atm fresh_prod fresh_atm)apply (auto)[1]apply (simp)apply (drule_tac x="[(a,ba)]∙ [(xa,ca)]∙ [(ba,cb)]∙ [(b,cb)]∙ [(x,ca)]∙ c" in spec)apply (drule_tac x="[(a,ba)]∙ [(xa,ca)]∙ [(ba,cb)]∙ [(b,cb)]∙ [(x,ca)]∙ Q" in spec)apply (drule mp)apply (rule conjI)apply (auto simp add: calc_atm fresh_prod fresh_atm)[1]apply (rule conjI)apply (auto simp add: fresh_left calc_atm fresh_prod fresh_atm)[1]apply (drule_tac pi="[(x,ca)]" and X="∥ ∥ " in pt_set_bij2[OF pt_name_inst, OF at_name_inst])apply (simp add: CAND_eqvt_name CAND_eqvt_coname)apply (drule_tac pi="[(b,cb)]" and X="∥ ∥ " in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (simp add: CAND_eqvt_name CAND_eqvt_coname)apply (drule_tac pi="[(ba,cb)]" and X="∥ ∥ " in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (simp add: CAND_eqvt_name CAND_eqvt_coname)apply (drule_tac pi="[(xa,ca)]" and X="∥ ∥ " in pt_set_bij2[OF pt_name_inst, OF at_name_inst])apply (simp add: CAND_eqvt_name CAND_eqvt_coname)apply (drule_tac pi="[(a,ba)]" and X="∥ ∥ " in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (simp add: CAND_eqvt_name CAND_eqvt_coname)apply (drule_tac pi="[(a,ba)]" and X="∥ ∥ " in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt)apply (drule_tac pi="[(xa,ca)]" and X="∥ ∥ " in pt_set_bij2[OF pt_name_inst, OF at_name_inst])apply (simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt)apply (drule_tac pi="[(ba,cb)]" and X="∥ ∥ " in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt)apply (drule_tac pi="[(b,cb)]" and X="∥ ∥ " in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (simp add: CAND_eqvt_name CAND_eqvt_coname)apply (drule_tac pi="[(x,ca)]" and X="∥ ∥ " in pt_set_bij2[OF pt_name_inst, OF at_name_inst])apply (perm_simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt)apply (case_tac "a=aa" )apply (simp)apply (generate_fresh "name" )apply (generate_fresh "coname" )apply (drule_tac a="ca" and z="c" in alpha_name_coname)apply (simp add: fresh_left calc_atm fresh_prod fresh_atm)apply (simp add: fresh_left calc_atm fresh_prod fresh_atm)apply (auto)[1]apply (simp)apply (drule_tac x="[(aa,ba)]∙ [(xa,c)]∙ [(ba,ca)]∙ [(b,ca)]∙ [(x,c)]∙ z" in spec)apply (drule_tac x="[(aa,ba)]∙ [(xa,c)]∙ [(ba,ca)]∙ [(b,ca)]∙ [(x,c)]∙ P" in spec)apply (drule mp)apply (rule conjI)apply (auto simp add: calc_atm fresh_prod fresh_atm)[1]apply (rule conjI)apply (auto simp add: fresh_left calc_atm fresh_prod fresh_atm)[1]apply (drule_tac pi="[(x,c)]" and X="∥ (ty2)∥ " in pt_set_bij2[OF pt_name_inst, OF at_name_inst])apply (simp add: CAND_eqvt_name CAND_eqvt_coname)apply (drule_tac pi="[(b,ca)]" and X="∥ (ty2)∥ " in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (simp add: CAND_eqvt_name CAND_eqvt_coname)apply (drule_tac pi="[(ba,ca)]" and X="∥ (ty2)∥ " in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (simp add: CAND_eqvt_name CAND_eqvt_coname)apply (drule_tac pi="[(xa,c)]" and X="∥ (ty2)∥ " in pt_set_bij2[OF pt_name_inst, OF at_name_inst])apply (simp add: CAND_eqvt_name CAND_eqvt_coname)apply (drule_tac pi="[(aa,ba)]" and X="∥ (ty2)∥ " in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (simp add: CAND_eqvt_name CAND_eqvt_coname)apply (drule_tac pi="[(aa,ba)]" and X="∥ (ty1)∥ " in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt)apply (drule_tac pi="[(xa,c)]" and X="∥ (ty1)∥ " in pt_set_bij2[OF pt_name_inst, OF at_name_inst])apply (simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt)apply (drule_tac pi="[(ba,ca)]" and X="∥ (ty1)∥ " in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt)apply (drule_tac pi="[(b,ca)]" and X="∥ (ty1)∥ " in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (simp add: CAND_eqvt_name CAND_eqvt_coname)apply (drule_tac pi="[(x,c)]" and X="∥ (ty1)∥ " in pt_set_bij2[OF pt_name_inst, OF at_name_inst])apply (perm_simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt)apply (simp)apply (case_tac "ba=aa" )apply (simp)apply (generate_fresh "name" )apply (generate_fresh "coname" )apply (drule_tac a="ca" and z="c" in alpha_name_coname)apply (simp add: fresh_left calc_atm fresh_prod fresh_atm)apply (simp add: fresh_left calc_atm fresh_prod fresh_atm)apply (auto)[1]apply (simp)apply (drule_tac x="[(a,aa)]∙ [(xa,c)]∙ [(a,ca)]∙ [(b,ca)]∙ [(x,c)]∙ z" in spec)apply (drule_tac x="[(a,aa)]∙ [(xa,c)]∙ [(a,ca)]∙ [(b,ca)]∙ [(x,c)]∙ P" in spec)apply (drule mp)apply (rule conjI)apply (auto simp add: calc_atm fresh_prod fresh_atm)[1]apply (rule conjI)apply (auto simp add: fresh_left calc_atm fresh_prod fresh_atm)[1]apply (drule_tac pi="[(x,c)]" and X="∥ (ty2)∥ " in pt_set_bij2[OF pt_name_inst, OF at_name_inst])apply (simp add: CAND_eqvt_name CAND_eqvt_coname)apply (drule_tac pi="[(b,ca)]" and X="∥ (ty2)∥ " in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (simp add: CAND_eqvt_name CAND_eqvt_coname)apply (drule_tac pi="[(a,ca)]" and X="∥ (ty2)∥ " in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (simp add: CAND_eqvt_name CAND_eqvt_coname)apply (drule_tac pi="[(xa,c)]" and X="∥ (ty2)∥ " in pt_set_bij2[OF pt_name_inst, OF at_name_inst])apply (simp add: CAND_eqvt_name CAND_eqvt_coname)apply (drule_tac pi="[(a,aa)]" and X="∥ (ty2)∥ " in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (simp add: CAND_eqvt_name CAND_eqvt_coname)apply (drule_tac pi="[(a,aa)]" and X="∥ (ty1)∥ " in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt)apply (drule_tac pi="[(xa,c)]" and X="∥ (ty1)∥ " in pt_set_bij2[OF pt_name_inst, OF at_name_inst])apply (simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt)apply (drule_tac pi="[(a,ca)]" and X="∥ (ty1)∥ " in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt)apply (drule_tac pi="[(b,ca)]" and X="∥ (ty1)∥ " in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (simp add: CAND_eqvt_name CAND_eqvt_coname)apply (drule_tac pi="[(x,c)]" and X="∥ (ty1)∥ " in pt_set_bij2[OF pt_name_inst, OF at_name_inst])apply (perm_simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt)apply (simp)apply (generate_fresh "name" )apply (generate_fresh "coname" )apply (drule_tac a="ca" and z="c" in alpha_name_coname)apply (simp add: fresh_left calc_atm fresh_prod fresh_atm)apply (simp add: fresh_left calc_atm fresh_prod fresh_atm)apply (auto)[1]apply (simp)apply (drule_tac x="[(a,ba)]∙ [(xa,c)]∙ [(aa,ca)]∙ [(b,ca)]∙ [(x,c)]∙ z" in spec)apply (drule_tac x="[(a,ba)]∙ [(xa,c)]∙ [(aa,ca)]∙ [(b,ca)]∙ [(x,c)]∙ P" in spec)apply (drule mp)apply (rule conjI)apply (auto simp add: calc_atm fresh_prod fresh_atm)[1]apply (rule conjI)apply (auto simp add: fresh_left calc_atm fresh_prod fresh_atm)[1]apply (drule_tac pi="[(x,c)]" and X="∥ (ty2)∥ " in pt_set_bij2[OF pt_name_inst, OF at_name_inst])apply (simp add: CAND_eqvt_name CAND_eqvt_coname)apply (drule_tac pi="[(b,ca)]" and X="∥ (ty2)∥ " in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (simp add: CAND_eqvt_name CAND_eqvt_coname)apply (drule_tac pi="[(aa,ca)]" and X="∥ (ty2)∥ " in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (simp add: CAND_eqvt_name CAND_eqvt_coname)apply (drule_tac pi="[(xa,c)]" and X="∥ (ty2)∥ " in pt_set_bij2[OF pt_name_inst, OF at_name_inst])apply (simp add: CAND_eqvt_name CAND_eqvt_coname)apply (drule_tac pi="[(a,ba)]" and X="∥ (ty2)∥ " in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (simp add: CAND_eqvt_name CAND_eqvt_coname)apply (drule_tac pi="[(a,ba)]" and X="∥ (ty1)∥ " in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt)apply (drule_tac pi="[(xa,c)]" and X="∥ (ty1)∥ " in pt_set_bij2[OF pt_name_inst, OF at_name_inst])apply (simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt)apply (drule_tac pi="[(aa,ca)]" and X="∥ (ty1)∥ " in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt)apply (drule_tac pi="[(b,ca)]" and X="∥ (ty1)∥ " in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (simp add: CAND_eqvt_name CAND_eqvt_coname)apply (drule_tac pi="[(x,c)]" and X="∥ (ty1)∥ " in pt_set_bij2[OF pt_name_inst, OF at_name_inst])apply (perm_simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt)apply (case_tac "a=aa" )apply (simp)apply (generate_fresh "name" )apply (generate_fresh "coname" )apply (drule_tac a="cb" and z="ca" in alpha_name_coname)apply (simp add: fresh_left calc_atm fresh_prod fresh_atm)apply (simp add: fresh_left calc_atm fresh_prod fresh_atm)apply (auto)[1]apply (simp)apply (drule_tac x="[(aa,ba)]∙ [(xa,ca)]∙ [(ba,cb)]∙ [(b,cb)]∙ [(x,ca)]∙ c" in spec)apply (drule_tac x="[(aa,ba)]∙ [(xa,ca)]∙ [(ba,cb)]∙ [(b,cb)]∙ [(x,ca)]∙ Q" in spec)apply (drule mp)apply (rule conjI)apply (auto simp add: calc_atm fresh_prod fresh_atm)[1]apply (rule conjI)apply (auto simp add: fresh_left calc_atm fresh_prod fresh_atm)[1]apply (drule_tac pi="[(x,ca)]" and X="∥ ∥ " in pt_set_bij2[OF pt_name_inst, OF at_name_inst])apply (simp add: CAND_eqvt_name CAND_eqvt_coname)apply (drule_tac pi="[(b,cb)]" and X="∥ ∥ " in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (simp add: CAND_eqvt_name CAND_eqvt_coname)apply (drule_tac pi="[(ba,cb)]" and X="∥ ∥ " in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (simp add: CAND_eqvt_name CAND_eqvt_coname)apply (drule_tac pi="[(xa,ca)]" and X="∥ ∥ " in pt_set_bij2[OF pt_name_inst, OF at_name_inst])apply (simp add: CAND_eqvt_name CAND_eqvt_coname)apply (drule_tac pi="[(aa,ba)]" and X="∥ ∥ " in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (simp add: CAND_eqvt_name CAND_eqvt_coname)apply (drule_tac pi="[(aa,ba)]" and X="∥ ∥ " in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt)apply (drule_tac pi="[(xa,ca)]" and X="∥ ∥ " in pt_set_bij2[OF pt_name_inst, OF at_name_inst])apply (simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt)apply (drule_tac pi="[(ba,cb)]" and X="∥ ∥ " in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt)apply (drule_tac pi="[(b,cb)]" and X="∥ ∥ " in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (simp add: CAND_eqvt_name CAND_eqvt_coname)apply (drule_tac pi="[(x,ca)]" and X="∥ ∥ " in pt_set_bij2[OF pt_name_inst, OF at_name_inst])apply (perm_simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt)apply (simp)apply (case_tac "ba=aa" )apply (simp)apply (generate_fresh "name" )apply (generate_fresh "coname" )apply (drule_tac a="cb" and z="ca" in alpha_name_coname)apply (simp add: fresh_left calc_atm fresh_prod fresh_atm)apply (simp add: fresh_left calc_atm fresh_prod fresh_atm)apply (auto)[1]apply (simp)apply (drule_tac x="[(a,aa)]∙ [(xa,ca)]∙ [(a,cb)]∙ [(b,cb)]∙ [(x,ca)]∙ c" in spec)apply (drule_tac x="[(a,aa)]∙ [(xa,ca)]∙ [(a,cb)]∙ [(b,cb)]∙ [(x,ca)]∙ Q" in spec)apply (drule mp)apply (rule conjI)apply (auto simp add: calc_atm fresh_prod fresh_atm)[1]apply (rule conjI)apply (auto simp add: fresh_left calc_atm fresh_prod fresh_atm)[1]apply (drule_tac pi="[(x,ca)]" and X="∥ ∥ " in pt_set_bij2[OF pt_name_inst, OF at_name_inst])apply (simp add: CAND_eqvt_name CAND_eqvt_coname)apply (drule_tac pi="[(b,cb)]" and X="∥ ∥ " in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (simp add: CAND_eqvt_name CAND_eqvt_coname)apply (drule_tac pi="[(a,cb)]" and X="∥ ∥ " in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (simp add: CAND_eqvt_name CAND_eqvt_coname)apply (drule_tac pi="[(xa,ca)]" and X="∥ ∥ " in pt_set_bij2[OF pt_name_inst, OF at_name_inst])apply (simp add: CAND_eqvt_name CAND_eqvt_coname)apply (drule_tac pi="[(a,aa)]" and X="∥ ∥ " in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (simp add: CAND_eqvt_name CAND_eqvt_coname)apply (drule_tac pi="[(a,aa)]" and X="∥ ∥ " in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt)apply (drule_tac pi="[(xa,ca)]" and X="∥ ∥ " in pt_set_bij2[OF pt_name_inst, OF at_name_inst])apply (simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt)apply (drule_tac pi="[(a,cb)]" and X="∥ ∥ " in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt)apply (drule_tac pi="[(b,cb)]" and X="∥ ∥ " in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (simp add: CAND_eqvt_name CAND_eqvt_coname)apply (drule_tac pi="[(x,ca)]" and X="∥ ∥ " in pt_set_bij2[OF pt_name_inst, OF at_name_inst])apply (perm_simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt)apply (simp)apply (generate_fresh "name" )apply (generate_fresh "coname" )apply (drule_tac a="cb" and z="ca" in alpha_name_coname)apply (simp add: fresh_left calc_atm fresh_prod fresh_atm)apply (simp add: fresh_left calc_atm fresh_prod fresh_atm)apply (auto)[1]apply (simp)apply (drule_tac x="[(a,ba)]∙ [(xa,ca)]∙ [(aa,cb)]∙ [(b,cb)]∙ [(x,ca)]∙ c" in spec)apply (drule_tac x="[(a,ba)]∙ [(xa,ca)]∙ [(aa,cb)]∙ [(b,cb)]∙ [(x,ca)]∙ Q" in spec)apply (drule mp)apply (rule conjI)apply (auto simp add: calc_atm fresh_prod fresh_atm)[1]apply (rule conjI)apply (auto simp add: fresh_left calc_atm fresh_prod fresh_atm)[1]apply (drule_tac pi="[(x,ca)]" and X="∥ ∥ " in pt_set_bij2[OF pt_name_inst, OF at_name_inst])apply (simp add: CAND_eqvt_name CAND_eqvt_coname)apply (drule_tac pi="[(b,cb)]" and X="∥ ∥ " in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (simp add: CAND_eqvt_name CAND_eqvt_coname)apply (drule_tac pi="[(aa,cb)]" and X="∥ ∥ " in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (simp add: CAND_eqvt_name CAND_eqvt_coname)apply (drule_tac pi="[(xa,ca)]" and X="∥ ∥ " in pt_set_bij2[OF pt_name_inst, OF at_name_inst])apply (simp add: CAND_eqvt_name CAND_eqvt_coname)apply (drule_tac pi="[(a,ba)]" and X="∥ ∥ " in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (simp add: CAND_eqvt_name CAND_eqvt_coname)apply (drule_tac pi="[(a,ba)]" and X="∥ ∥ " in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt)apply (drule_tac pi="[(xa,ca)]" and X="∥ ∥ " in pt_set_bij2[OF pt_name_inst, OF at_name_inst])apply (simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt)apply (drule_tac pi="[(aa,cb)]" and X="∥ ∥ " in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt)apply (drule_tac pi="[(b,cb)]" and X="∥ ∥ " in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])apply (simp add: CAND_eqvt_name CAND_eqvt_coname)apply (drule_tac pi="[(x,ca)]" and X="∥ ∥ " in pt_set_bij2[OF pt_name_inst, OF at_name_inst])apply (perm_simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt)done text ‹ Main lemma 1› lemma AXIOMS_imply_SNa:shows ":M ∈ AXIOMSc B ==> SNa M" and "(x):M ∈ AXIOMSn B ==> SNa M" apply -apply (auto simp add: AXIOMSn_def AXIOMSc_def ntrm.inject ctrm.inject alpha)apply (rule Ax_in_SNa)+done lemma BINDING_imply_SNa:shows ":M ∈ BINDINGc B (∥ (B)∥ ) ==> SNa M" and "(x):M ∈ BINDINGn B (∥ ∥ ) ==> SNa M" apply -apply (auto simp add: BINDINGn_def BINDINGc_def ntrm.inject ctrm.inject alpha)apply (drule_tac x="x" in spec)apply (drule_tac x="Ax x a" in spec)apply (drule mp)apply (rule Ax_in_CANDs)apply (drule a_star_preserves_SNa)apply (rule subst_with_ax2)apply (simp add: crename_id)apply (drule_tac x="x" in spec)apply (drule_tac x="Ax x aa" in spec)apply (drule mp)apply (rule Ax_in_CANDs)apply (drule a_star_preserves_SNa)apply (rule subst_with_ax2)apply (simp add: crename_id SNa_eqvt)apply (drule_tac x="a" in spec)apply (drule_tac x="Ax x a" in spec)apply (drule mp)apply (rule Ax_in_CANDs)apply (drule a_star_preserves_SNa)apply (rule subst_with_ax1)apply (simp add: nrename_id)apply (drule_tac x="a" in spec)apply (drule_tac x="Ax xa a" in spec)apply (drule mp)apply (rule Ax_in_CANDs)apply (drule a_star_preserves_SNa)apply (rule subst_with_ax1)apply (simp add: nrename_id SNa_eqvt)done lemma CANDs_imply_SNa:shows ":M ∈ ∥ ∥ ==> SNa M" and "(x):M ∈ ∥ (B)∥ ==> SNa M" proof (induct B arbitrary: a x M rule: ty.induct)case (PR X)case 1 have ":M ∈ ∥ ∥ " by factthen have ":M ∈ NEGc (PR X) (∥ (PR X)∥ )" by simpthen have ":M ∈ AXIOMSc (PR X) ∪ BINDINGc (PR X) (∥ (PR X)∥ )" by simpmoreover assume ":M ∈ AXIOMSc (PR X)" then have "SNa M" by (simp add: AXIOMS_imply_SNa)moreover assume ":M ∈ BINDINGc (PR X) (∥ (PR X)∥ )" then have "SNa M" by (simp add: BINDING_imply_SNa)ultimately show "SNa M" by blast next case 2have "(x):M ∈ (∥ (PR X)∥ )" by factthen have "(x):M ∈ NEGn (PR X) (∥ ∥ )" using NEG_simp by blastthen have "(x):M ∈ AXIOMSn (PR X) ∪ BINDINGn (PR X) (∥ ∥ )" by simpmoreover assume "(x):M ∈ AXIOMSn (PR X)" then have "SNa M" by (simp add: AXIOMS_imply_SNa)moreover assume "(x):M ∈ BINDINGn (PR X) (∥ ∥ )" then have "SNa M" by (simp only: BINDING_imply_SNa)ultimately show "SNa M" by blastnext case (NOT B)have ih1: "∧ :M ∈ ∥ ∥ ==> SNa M" by facthave ih2: "∧ ∈ ∥ (B)∥ ==> SNa M" by factcase 1have ":M ∈ (∥ ∥ )" by factthen have ":M ∈ NEGc (NOT B) (∥ (NOT B)∥ )" by simpthen have ":M ∈ AXIOMSc (NOT B) ∪ BINDINGc (NOT B) (∥ (NOT B)∥ ) ∪ NOTRIGHT (NOT B) (∥ (B)∥ )" by simpmoreover assume ":M ∈ AXIOMSc (NOT B)" then have "SNa M" by (simp add: AXIOMS_imply_SNa)moreover assume ":M ∈ BINDINGc (NOT B) (∥ (NOT B)∥ )" then have "SNa M" by (simp only: BINDING_imply_SNa)moreover assume ":M ∈ NOTRIGHT (NOT B) (∥ (B)∥ )" then obtain x' M' where eq: "M = NotR (x').M' a" and "(x'):M' ∈ (∥ (B)∥ )" using NOTRIGHT_elim by blastthen have "SNa M'" using ih2 by blastthen have "SNa M" using eq by (simp add: NotR_in_SNa)ultimately show "SNa M" by blastnext case 2have "(x):M ∈ (∥ (NOT B)∥ )" by factthen have "(x):M ∈ NEGn (NOT B) (∥ ∥ )" using NEG_simp by blastthen have "(x):M ∈ AXIOMSn (NOT B) ∪ BINDINGn (NOT B) (∥ ∥ ) ∪ NOTLEFT (NOT B) (∥ ∥ )" by (simp only: NEGn.simps)moreover assume "(x):M ∈ AXIOMSn (NOT B)" then have "SNa M" by (simp add: AXIOMS_imply_SNa)moreover assume "(x):M ∈ BINDINGn (NOT B) (∥ ∥ )" then have "SNa M" by (simp only: BINDING_imply_SNa)moreover assume "(x):M ∈ NOTLEFT (NOT B) (∥ ∥ )" then obtain a' M' where eq: "M = NotL .M' x" and ":M' ∈ (∥ ∥ )" using NOTLEFT_elim by blastthen have "SNa M'" using ih1 by blastthen have "SNa M" using eq by (simp add: NotL_in_SNa)ultimately show "SNa M" by blastnext case (AND A B)have ih1: "∧ :M ∈ ∥ ∥ ==> SNa M" by facthave ih2: "∧ ∈ ∥ (A)∥ ==> SNa M" by facthave ih3: "∧ :M ∈ ∥ ∥ ==> SNa M" by facthave ih4: "∧ ∈ ∥ (B)∥ ==> SNa M" by factcase 1have ":M ∈ (∥ ∥ )" by factthen have ":M ∈ NEGc (A AND B) (∥ (A AND B)∥ )" by simpthen have ":M ∈ AXIOMSc (A AND B) ∪ BINDINGc (A AND B) (∥ (A AND B)∥ ) ∪ ANDRIGHT (A AND B) (∥ ∥ ) (∥ ∥ )" by simpmoreover assume ":M ∈ AXIOMSc (A AND B)" then have "SNa M" by (simp add: AXIOMS_imply_SNa)moreover assume ":M ∈ BINDINGc (A AND B) (∥ (A AND B)∥ )" then have "SNa M" by (simp only: BINDING_imply_SNa)moreover assume ":M ∈ ANDRIGHT (A AND B) (∥ ∥ ) (∥ ∥ )" then obtain a' M' b' N' where eq: "M = AndR .M' .N' a" and ":M' ∈ (∥ ∥ )" and ":N' ∈ (∥ ∥ )" by (erule_tac ANDRIGHT_elim, blast)then have "SNa M'" and "SNa N'" using ih1 ih3 by blast+then have "SNa M" using eq by (simp add: AndR_in_SNa)ultimately show "SNa M" by blastnext case 2have "(x):M ∈ (∥ (A AND B)∥ )" by factthen have "(x):M ∈ NEGn (A AND B) (∥ ∥ )" using NEG_simp by blastthen have "(x):M ∈ AXIOMSn (A AND B) ∪ BINDINGn (A AND B) (∥ ∥ ) ∪ ANDLEFT1 (A AND B) (∥ (A)∥ ) ∪ ANDLEFT2 (A AND B) (∥ (B)∥ )" by (simp only: NEGn.simps)moreover assume "(x):M ∈ AXIOMSn (A AND B)" then have "SNa M" by (simp add: AXIOMS_imply_SNa)moreover assume "(x):M ∈ BINDINGn (A AND B) (∥ ∥ )" then have "SNa M" by (simp only: BINDING_imply_SNa)moreover assume "(x):M ∈ ANDLEFT1 (A AND B) (∥ (A)∥ )" then obtain x' M' where eq: "M = AndL1 (x').M' x" and "(x'):M' ∈ (∥ (A)∥ )" using ANDLEFT1_elim by blastthen have "SNa M'" using ih2 by blastthen have "SNa M" using eq by (simp add: AndL1_in_SNa)moreover assume "(x):M ∈ ANDLEFT2 (A AND B) (∥ (B)∥ )" then obtain x' M' where eq: "M = AndL2 (x').M' x" and "(x'):M' ∈ (∥ (B)∥ )" using ANDLEFT2_elim by blastthen have "SNa M'" using ih4 by blastthen have "SNa M" using eq by (simp add: AndL2_in_SNa)ultimately show "SNa M" by blastnext case (OR A B)have ih1: "∧ :M ∈ ∥ ∥ ==> SNa M" by facthave ih2: "∧ ∈ ∥ (A)∥ ==> SNa M" by facthave ih3: "∧ :M ∈ ∥ ∥ ==> SNa M" by facthave ih4: "∧ ∈ ∥ (B)∥ ==> SNa M" by factcase 1have ":M ∈ (∥ ∥ )" by factthen have ":M ∈ NEGc (A OR B) (∥ (A OR B)∥ )" by simpthen have ":M ∈ AXIOMSc (A OR B) ∪ BINDINGc (A OR B) (∥ (A OR B)∥ ) ∪ ORRIGHT1 (A OR B) (∥ ∥ ) ∪ ORRIGHT2 (A OR B) (∥ ∥ )" by simpmoreover assume ":M ∈ AXIOMSc (A OR B)" then have "SNa M" by (simp add: AXIOMS_imply_SNa)moreover assume ":M ∈ BINDINGc (A OR B) (∥ (A OR B)∥ )" then have "SNa M" by (simp only: BINDING_imply_SNa)moreover assume ":M ∈ ORRIGHT1 (A OR B) (∥ ∥ )" then obtain a' M' where eq: "M = OrR1 .M' a" and ":M' ∈ (∥ ∥ )" by (erule_tac ORRIGHT1_elim, blast)then have "SNa M'" using ih1 by blastthen have "SNa M" using eq by (simp add: OrR1_in_SNa)moreover assume ":M ∈ ORRIGHT2 (A OR B) (∥ ∥ )" then obtain a' M' where eq: "M = OrR2 .M' a" and ":M' ∈ (∥ ∥ )" using ORRIGHT2_elim by blastthen have "SNa M'" using ih3 by blastthen have "SNa M" using eq by (simp add: OrR2_in_SNa)ultimately show "SNa M" by blastnext case 2have "(x):M ∈ (∥ (A OR B)∥ )" by factthen have "(x):M ∈ NEGn (A OR B) (∥ ∥ )" using NEG_simp by blastthen have "(x):M ∈ AXIOMSn (A OR B) ∪ BINDINGn (A OR B) (∥ ∥ ) ∪ ORLEFT (A OR B) (∥ (A)∥ ) (∥ (B)∥ )" by (simp only: NEGn.simps)moreover assume "(x):M ∈ AXIOMSn (A OR B)" then have "SNa M" by (simp add: AXIOMS_imply_SNa)moreover assume "(x):M ∈ BINDINGn (A OR B) (∥ ∥ )" then have "SNa M" by (simp only: BINDING_imply_SNa)moreover assume "(x):M ∈ ORLEFT (A OR B) (∥ (A)∥ ) (∥ (B)∥ )" then obtain x' M' y' N' where eq: "M = OrL (x').M' (y').N' x" and "(x'):M' ∈ (∥ (A)∥ )" and "(y'):N' ∈ (∥ (B)∥ )" by (erule_tac ORLEFT_elim, blast)then have "SNa M'" and "SNa N'" using ih2 ih4 by blast+then have "SNa M" using eq by (simp add: OrL_in_SNa)ultimately show "SNa M" by blastnext case (IMP A B)have ih1: "∧ :M ∈ ∥ ∥ ==> SNa M" by facthave ih2: "∧ ∈ ∥ (A)∥ ==> SNa M" by facthave ih3: "∧ :M ∈ ∥ ∥ ==> SNa M" by facthave ih4: "∧ ∈ ∥ (B)∥ ==> SNa M" by factcase 1have ":M ∈ (∥ ∥ )" by factthen have ":M ∈ NEGc (A IMP B) (∥ (A IMP B)∥ )" by simpthen have ":M ∈ AXIOMSc (A IMP B) ∪ BINDINGc (A IMP B) (∥ (A IMP B)∥ ) ∪ IMPRIGHT (A IMP B) (∥ (A)∥ ) (∥ ∥ ) (∥ (B)∥ ) (∥ ∥ )" by simpmoreover assume ":M ∈ AXIOMSc (A IMP B)" then have "SNa M" by (simp add: AXIOMS_imply_SNa)moreover assume ":M ∈ BINDINGc (A IMP B) (∥ (A IMP B)∥ )" then have "SNa M" by (simp only: BINDING_imply_SNa)moreover assume ":M ∈ IMPRIGHT (A IMP B) (∥ (A)∥ ) (∥ ∥ ) (∥ (B)∥ ) (∥ ∥ )" then obtain x' a' M' where eq: "M = ImpR (x')..M' a" and imp: "∀ z P. x'♯ (z,P) ∧ (z):P ∈ ∥ (B)∥ ⟶ (x'):(M'{a':=(z).P}) ∈ ∥ (A)∥ " by (erule_tac IMPRIGHT_elim, blast)obtain z::"name" where fs: "z♯ x'" by (rule_tac exists_fresh, rule fin_supp, blast)have "(z):Ax z a'∈ ∥ (B)∥ " by (simp add: Ax_in_CANDs)with imp fs have "(x'):(M'{a':=(z).Ax z a'}) ∈ ∥ (A)∥ " by (simp add: fresh_prod fresh_atm)then have "SNa (M'{a':=(z).Ax z a'})" using ih2 by blastmoreover have "M'{a':=(z).Ax z a'} ⟶ 🪙 a* M'[a'⊨ c>a']" by (simp add: subst_with_ax2)ultimately have "SNa (M'[a'⊨ c>a'])" by (simp add: a_star_preserves_SNa)then have "SNa M'" by (simp add: crename_id)then have "SNa M" using eq by (simp add: ImpR_in_SNa)ultimately show "SNa M" by blastnext case 2have "(x):M ∈ (∥ (A IMP B)∥ )" by factthen have "(x):M ∈ NEGn (A IMP B) (∥ ∥ )" using NEG_simp by blastthen have "(x):M ∈ AXIOMSn (A IMP B) ∪ BINDINGn (A IMP B) (∥ ∥ ) ∪ IMPLEFT (A IMP B) (∥ ∥ ) (∥ (B)∥ )" by (simp only: NEGn.simps)moreover assume "(x):M ∈ AXIOMSn (A IMP B)" then have "SNa M" by (simp add: AXIOMS_imply_SNa)moreover assume "(x):M ∈ BINDINGn (A IMP B) (∥ ∥ )" then have "SNa M" by (simp only: BINDING_imply_SNa)moreover assume "(x):M ∈ IMPLEFT (A IMP B) (∥ ∥ ) (∥ (B)∥ )" then obtain a' M' y' N' where eq: "M = ImpL .M' (y').N' x" and ":M' ∈ (∥ ∥ )" and "(y'):N' ∈ (∥ (B)∥ )" by (erule_tac IMPLEFT_elim, blast)then have "SNa M'" and "SNa N'" using ih1 ih4 by blast+then have "SNa M" using eq by (simp add: ImpL_in_SNa)ultimately show "SNa M" by blastqed text ‹ Main lemma 2› lemma AXIOMS_preserved:shows ":M ∈ AXIOMSc B ==> M ⟶ 🪙 a* M' ==> :M' ∈ AXIOMSc B" and "(x):M ∈ AXIOMSn B ==> M ⟶ 🪙 a* M' ==> (x):M' ∈ AXIOMSn B" apply (simp_all add: AXIOMSc_def AXIOMSn_def)apply (auto simp add: ntrm.inject ctrm.inject alpha)apply (drule ax_do_not_a_star_reduce)apply (auto)apply (drule ax_do_not_a_star_reduce)apply (auto)apply (drule ax_do_not_a_star_reduce)apply (auto)apply (drule ax_do_not_a_star_reduce)apply (auto)done lemma BINDING_preserved:shows ":M ∈ BINDINGc B (∥ (B)∥ ) ==> M ⟶ 🪙 a* M' ==> :M' ∈ BINDINGc B (∥ (B)∥ )" and "(x):M ∈ BINDINGn B (∥ ∥ ) ==> M ⟶ 🪙 a* M' ==> (x):M' ∈ BINDINGn B (∥ ∥ )" proof -assume red: "M ⟶ 🪙 a* M'" assume asm: ":M ∈ BINDINGc B (∥ (B)∥ )" fix x::"name" and P::"trm" from asm have "((x):P) ∈ (∥ (B)∥ ) ==> SNa (M{a:=(x).P})" by (simp add: BINDINGc_elim)moreover have "M{a:=(x).P} ⟶ 🪙 a* M'{a:=(x).P}" using red by (simp add: a_star_subst2)ultimately have "((x):P) ∈ (∥ (B)∥ ) ==> SNa (M'{a:=(x).P})" by (simp add: a_star_preserves_SNa)then show ":M' ∈ BINDINGc B (∥ (B)∥ )" by (auto simp add: BINDINGc_def)next assume red: "M ⟶ 🪙 a* M'" assume asm: "(x):M ∈ BINDINGn B (∥ ∥ )" fix c::"coname" and P::"trm" from asm have "(:P) ∈ (∥ ∥ ) ==> SNa (M{x:=.P})" by (simp add: BINDINGn_elim)moreover have "M{x:=.P} ⟶ 🪙 a* M'{x:=.P}" using red by (simp add: a_star_subst1)ultimately have "(:P) ∈ (∥ ∥ ) ==> SNa (M'{x:=.P})" by (simp add: a_star_preserves_SNa)then show "(x):M' ∈ BINDINGn B (∥ ∥ )" by (auto simp add: BINDINGn_def)qed lemma CANDs_preserved:shows ":M ∈ ∥ ∥ ==> M ⟶ 🪙 a* M' ==> :M' ∈ ∥ ∥ " and "(x):M ∈ ∥ (B)∥ ==> M ⟶ 🪙 a* M' ==> (x):M' ∈ ∥ (B)∥ " proof (nominal_induct B arbitrary: a x M M' rule: ty.strong_induct) case (PR X)case 1 have asm: "M ⟶ 🪙 a* M'" by facthave ":M ∈ ∥ ∥ " by factthen have ":M ∈ NEGc (PR X) (∥ (PR X)∥ )" by simpthen have ":M ∈ AXIOMSc (PR X) ∪ BINDINGc (PR X) (∥ (PR X)∥ )" by simpmoreover assume ":M ∈ AXIOMSc (PR X)" then have ":M' ∈ AXIOMSc (PR X)" using asm by (simp only: AXIOMS_preserved)moreover assume ":M ∈ BINDINGc (PR X) (∥ (PR X)∥ )" then have ":M' ∈ BINDINGc (PR X) (∥ (PR X)∥ )" using asm by (simp add: BINDING_preserved)ultimately have ":M' ∈ AXIOMSc (PR X) ∪ BINDINGc (PR X) (∥ (PR X)∥ )" by blastthen have ":M' ∈ NEGc (PR X) (∥ (PR X)∥ )" by simpthen show ":M' ∈ (∥ ∥ )" using NEG_simp by blastnext case 2have asm: "M ⟶ 🪙 a* M'" by facthave "(x):M ∈ ∥ (PR X)∥ " by factthen have "(x):M ∈ NEGn (PR X) (∥ ∥ )" using NEG_simp by blastthen have "(x):M ∈ AXIOMSn (PR X) ∪ BINDINGn (PR X) (∥ ∥ )" by simpmoreover assume "(x):M ∈ AXIOMSn (PR X)" then have "(x):M' ∈ AXIOMSn (PR X)" using asm by (simp only: AXIOMS_preserved) moreover assume "(x):M ∈ BINDINGn (PR X) (∥ ∥ )" then have "(x):M' ∈ BINDINGn (PR X) (∥ ∥ )" using asm by (simp only: BINDING_preserved)ultimately have "(x):M' ∈ AXIOMSn (PR X) ∪ BINDINGn (PR X) (∥ ∥ )" by blastthen have "(x):M' ∈ NEGn (PR X) (∥ ∥ )" by simpthen show "(x):M' ∈ (∥ (PR X)∥ )" using NEG_simp by blastnext case (IMP A B)have ih1: "∧ [ :M ∈ ∥ ∥ ; M ⟶ 🪙 a* M'] ==> :M' ∈ ∥ ∥ " by facthave ih2: "∧ [ (x):M ∈ ∥ (A)∥ ; M ⟶ 🪙 a* M'] ==> (x):M' ∈ ∥ (A)∥ " by facthave ih3: "∧ [ :M ∈ ∥ ∥ ; M ⟶ 🪙 a* M'] ==> :M' ∈ ∥ ∥ " by facthave ih4: "∧ [ (x):M ∈ ∥ (B)∥ ; M ⟶ 🪙 a* M'] ==> (x):M' ∈ ∥ (B)∥ " by factcase 1 have asm: "M ⟶ 🪙 a* M'" by facthave ":M ∈ ∥ ∥ " by factthen have ":M ∈ NEGc (A IMP B) (∥ (A IMP B)∥ )" by simpthen have ":M ∈ AXIOMSc (A IMP B) ∪ BINDINGc (A IMP B) (∥ (A IMP B)∥ ) ∪ IMPRIGHT (A IMP B) (∥ (A)∥ ) (∥ ∥ ) (∥ (B)∥ ) (∥ ∥ )" by simpmoreover assume ":M ∈ AXIOMSc (A IMP B)" then have ":M' ∈ AXIOMSc (A IMP B)" using asm by (simp only: AXIOMS_preserved)moreover assume ":M ∈ BINDINGc (A IMP B) (∥ (A IMP B)∥ )" then have ":M' ∈ BINDINGc (A IMP B) (∥ (A IMP B)∥ )" using asm by (simp only: BINDING_preserved)moreover assume ":M ∈ IMPRIGHT (A IMP B) (∥ (A)∥ ) (∥ ∥ ) (∥ (B)∥ ) (∥ ∥ )" then obtain x' a' N' where eq: "M = ImpR (x')..N' a" and fic: "fic (ImpR (x')..N' a) a" and imp1: "∀ z P. x'♯ (z,P) ∧ (z):P ∈ ∥ (B)∥ ⟶ (x'):(N'{a':=(z).P}) ∈ ∥ (A)∥ " and imp2: "∀ c Q. a'♯ (c,Q) ∧ :Q ∈ ∥ ∥ ⟶ :(N'{x':=.Q}) ∈ ∥ ∥ " using IMPRIGHT_elim by blastfrom eq asm obtain N'' where eq': "M' = ImpR (x')..N'' a" and red: "N' ⟶ 🪙 a* N''" using a_star_redu_ImpR_elim by (blast)from imp1 have "∀ z P. x'♯ (z,P) ∧ (z):P ∈ ∥ (B)∥ ⟶ (x'):(N''{a':=(z).P}) ∈ ∥ (A)∥ " using red ih2apply (auto)apply (drule_tac x="z" in spec)apply (drule_tac x="P" in spec)apply (simp)apply (drule_tac a_star_subst2)apply (blast)done moreover from imp2 have "∀ c Q. a'♯ (c,Q) ∧ :Q ∈ ∥ ∥ ⟶ :(N''{x':=.Q}) ∈ ∥ ∥ " using red ih3apply (auto)apply (drule_tac x="c" in spec)apply (drule_tac x="Q" in spec)apply (simp)apply (drule_tac a_star_subst1)apply (blast)done moreover from fic have "fic M' a" using eq asm by (simp add: fic_a_star_reduce)ultimately have ":M' ∈ IMPRIGHT (A IMP B) (∥ (A)∥ ) (∥ ∥ ) (∥ (B)∥ ) (∥ ∥ )" using eq' by autoultimately have ":M' ∈ AXIOMSc (A IMP B) ∪ BINDINGc (A IMP B) (∥ (A IMP B)∥ ) ∪ IMPRIGHT (A IMP B) (∥ (A)∥ ) (∥ ∥ ) (∥ (B)∥ ) (∥ ∥ )" by blastthen have ":M' ∈ NEGc (A IMP B) (∥ (A IMP B)∥ )" by simpthen show ":M' ∈ (∥ ∥ )" using NEG_simp by blastnext case 2have asm: "M ⟶ 🪙 a* M'" by facthave "(x):M ∈ ∥ (A IMP B)∥ " by factthen have "(x):M ∈ NEGn (A IMP B) (∥ ∥ )" using NEG_simp by blastthen have "(x):M ∈ AXIOMSn (A IMP B) ∪ BINDINGn (A IMP B) (∥ ∥ ) ∪ IMPLEFT (A IMP B) (∥ ∥ ) (∥ (B)∥ )" by simpmoreover assume "(x):M ∈ AXIOMSn (A IMP B)" then have "(x):M' ∈ AXIOMSn (A IMP B)" using asm by (simp only: AXIOMS_preserved)moreover assume "(x):M ∈ BINDINGn (A IMP B) (∥ ∥ )" then have "(x):M' ∈ BINDINGn (A IMP B) (∥ ∥ )" using asm by (simp only: BINDING_preserved)moreover assume "(x):M ∈ IMPLEFT (A IMP B) (∥ ∥ ) (∥ (B)∥ )" then obtain a' T' y' N' where eq: "M = ImpL .T' (y').N' x" and fin: "fin (ImpL .T' (y').N' x) x" and imp1: ":T' ∈ ∥ ∥ " and imp2: "(y'):N' ∈ ∥ (B)∥ " by (erule_tac IMPLEFT_elim, blast)from eq asm obtain T'' N'' where eq': "M' = ImpL .T'' (y').N'' x" and red1: "T' ⟶ 🪙 a* T''" and red2: "N' ⟶ 🪙 a* N''" using a_star_redu_ImpL_elim by blastfrom fin have "fin M' x" using eq asm by (simp add: fin_a_star_reduce)moreover from imp1 red1 have ":T'' ∈ ∥ ∥ " using ih1 by simpmoreover from imp2 red2 have "(y'):N'' ∈ ∥ (B)∥ " using ih4 by simpultimately have "(x):M' ∈ IMPLEFT (A IMP B) (∥ ∥ ) (∥ (B)∥ )" using eq' by (simp, blast) ultimately have "(x):M' ∈ AXIOMSn (A IMP B) ∪ BINDINGn (A IMP B) (∥ ∥ ) ∪ IMPLEFT (A IMP B) (∥ ∥ ) (∥ (B)∥ )" by blastthen have "(x):M' ∈ NEGn (A IMP B) (∥ ∥ )" by simpthen show "(x):M' ∈ (∥ (A IMP B)∥ )" using NEG_simp by blastnext case (AND A B)have ih1: "∧ [ :M ∈ ∥ ∥ ; M ⟶ 🪙 a* M'] ==> :M' ∈ ∥ ∥ " by facthave ih2: "∧ [ (x):M ∈ ∥ (A)∥ ; M ⟶ 🪙 a* M'] ==> (x):M' ∈ ∥ (A)∥ " by facthave ih3: "∧ [ :M ∈ ∥ ∥ ; M ⟶ 🪙 a* M'] ==> :M' ∈ ∥ ∥ " by facthave ih4: "∧ [ (x):M ∈ ∥ (B)∥ ; M ⟶ 🪙 a* M'] ==> (x):M' ∈ ∥ (B)∥ " by factcase 1 have asm: "M ⟶ 🪙 a* M'" by facthave ":M ∈ ∥ ∥ " by factthen have ":M ∈ NEGc (A AND B) (∥ (A AND B)∥ )" by simpthen have ":M ∈ AXIOMSc (A AND B) ∪ BINDINGc (A AND B) (∥ (A AND B)∥ ) ∪ ANDRIGHT (A AND B) (∥ ∥ ) (∥ ∥ )" by simpmoreover assume ":M ∈ AXIOMSc (A AND B)" then have ":M' ∈ AXIOMSc (A AND B)" using asm by (simp only: AXIOMS_preserved)moreover assume ":M ∈ BINDINGc (A AND B) (∥ (A AND B)∥ )" then have ":M' ∈ BINDINGc (A AND B) (∥ (A AND B)∥ )" using asm by (simp only: BINDING_preserved)moreover assume ":M ∈ ANDRIGHT (A AND B) (∥ ∥ ) (∥ ∥ )" then obtain a' T' b' N' where eq: "M = AndR .T' .N' a" and fic: "fic (AndR .T' .N' a) a" and imp1: ":T' ∈ ∥ ∥ " and imp2: ":N' ∈ ∥ ∥ " using ANDRIGHT_elim by blastfrom eq asm obtain T'' N'' where eq': "M' = AndR .T'' .N'' a" and red1: "T' ⟶ 🪙 a* T''" and red2: "N' ⟶ 🪙 a* N''" using a_star_redu_AndR_elim by blastfrom fic have "fic M' a" using eq asm by (simp add: fic_a_star_reduce)moreover from imp1 red1 have ":T'' ∈ ∥ ∥ " using ih1 by simpmoreover from imp2 red2 have ":N'' ∈ ∥ ∥ " using ih3 by simpultimately have ":M' ∈ ANDRIGHT (A AND B) (∥ ∥ ) (∥ ∥ )" using eq' by (simp, blast) ultimately have ":M' ∈ AXIOMSc (A AND B) ∪ BINDINGc (A AND B) (∥ (A AND B)∥ ) ∪ ANDRIGHT (A AND B) (∥ ∥ ) (∥ ∥ )" by blastthen have ":M' ∈ NEGc (A AND B) (∥ (A AND B)∥ )" by simpthen show ":M' ∈ (∥ ∥ )" using NEG_simp by blastnext case 2have asm: "M ⟶ 🪙 a* M'" by facthave "(x):M ∈ ∥ (A AND B)∥ " by factthen have "(x):M ∈ NEGn (A AND B) (∥ ∥ )" using NEG_simp by blastthen have "(x):M ∈ AXIOMSn (A AND B) ∪ BINDINGn (A AND B) (∥ ∥ ) ∪ ANDLEFT1 (A AND B) (∥ (A)∥ ) ∪ ANDLEFT2 (A AND B) (∥ (B)∥ )" by simpmoreover assume "(x):M ∈ AXIOMSn (A AND B)" then have "(x):M' ∈ AXIOMSn (A AND B)" using asm by (simp only: AXIOMS_preserved)moreover assume "(x):M ∈ BINDINGn (A AND B) (∥ ∥ )" then have "(x):M' ∈ BINDINGn (A AND B) (∥ ∥ )" using asm by (simp only: BINDING_preserved)moreover assume "(x):M ∈ ANDLEFT1 (A AND B) (∥ (A)∥ )" then obtain y' N' where eq: "M = AndL1 (y').N' x" and fin: "fin (AndL1 (y').N' x) x" and imp: "(y'):N' ∈ ∥ (A)∥ " by (erule_tac ANDLEFT1_elim, blast)from eq asm obtain N'' where eq': "M' = AndL1 (y').N'' x" and red1: "N' ⟶ 🪙 a* N''" using a_star_redu_AndL1_elim by blastfrom fin have "fin M' x" using eq asm by (simp add: fin_a_star_reduce)moreover from imp red1 have "(y'):N'' ∈ ∥ (A)∥ " using ih2 by simpultimately have "(x):M' ∈ ANDLEFT1 (A AND B) (∥ (A)∥ )" using eq' by (simp, blast) moreover assume "(x):M ∈ ANDLEFT2 (A AND B) (∥ (B)∥ )" then obtain y' N' where eq: "M = AndL2 (y').N' x" and fin: "fin (AndL2 (y').N' x) x" and imp: "(y'):N' ∈ ∥ (B)∥ " by (erule_tac ANDLEFT2_elim, blast)from eq asm obtain N'' where eq': "M' = AndL2 (y').N'' x" and red1: "N' ⟶ 🪙 a* N''" using a_star_redu_AndL2_elim by blastfrom fin have "fin M' x" using eq asm by (simp add: fin_a_star_reduce)moreover from imp red1 have "(y'):N'' ∈ ∥ (B)∥ " using ih4 by simpultimately have "(x):M' ∈ ANDLEFT2 (A AND B) (∥ (B)∥ )" using eq' by (simp, blast) ultimately have "(x):M' ∈ AXIOMSn (A AND B) ∪ BINDINGn (A AND B) (∥ ∥ ) ∪ ANDLEFT1 (A AND B) (∥ (A)∥ ) ∪ ANDLEFT2 (A AND B) (∥ (B)∥ )" by blastthen have "(x):M' ∈ NEGn (A AND B) (∥ ∥ )" by simpthen show "(x):M' ∈ (∥ (A AND B)∥ )" using NEG_simp by blastnext case (OR A B)have ih1: "∧ [ :M ∈ ∥ ∥ ; M ⟶ 🪙 a* M'] ==> :M' ∈ ∥ ∥ " by facthave ih2: "∧ [ (x):M ∈ ∥ (A)∥ ; M ⟶ 🪙 a* M'] ==> (x):M' ∈ ∥ (A)∥ " by facthave ih3: "∧ [ :M ∈ ∥ ∥ ; M ⟶ 🪙 a* M'] ==> :M' ∈ ∥ ∥ " by facthave ih4: "∧ [ (x):M ∈ ∥ (B)∥ ; M ⟶ 🪙 a* M'] ==> (x):M' ∈ ∥ (B)∥ " by factcase 1 have asm: "M ⟶ 🪙 a* M'" by facthave ":M ∈ ∥ ∥ " by factthen have ":M ∈ NEGc (A OR B) (∥ (A OR B)∥ )" by simpthen have ":M ∈ AXIOMSc (A OR B) ∪ BINDINGc (A OR B) (∥ (A OR B)∥ ) ∪ ORRIGHT1 (A OR B) (∥ ∥ ) ∪ ORRIGHT2 (A OR B) (∥ ∥ )" by simpmoreover assume ":M ∈ AXIOMSc (A OR B)" then have ":M' ∈ AXIOMSc (A OR B)" using asm by (simp only: AXIOMS_preserved)moreover assume ":M ∈ BINDINGc (A OR B) (∥ (A OR B)∥ )" then have ":M' ∈ BINDINGc (A OR B) (∥ (A OR B)∥ )" using asm by (simp only: BINDING_preserved)moreover assume ":M ∈ ORRIGHT1 (A OR B) (∥ ∥ )" then obtain a' N' where eq: "M = OrR1 .N' a" and fic: "fic (OrR1 .N' a) a" and imp1: ":N' ∈ ∥ ∥ " using ORRIGHT1_elim by blastfrom eq asm obtain N'' where eq': "M' = OrR1 .N'' a" and red1: "N' ⟶ 🪙 a* N''" using a_star_redu_OrR1_elim by blastfrom fic have "fic M' a" using eq asm by (simp add: fic_a_star_reduce)moreover from imp1 red1 have ":N'' ∈ ∥ ∥ " using ih1 by simpultimately have ":M' ∈ ORRIGHT1 (A OR B) (∥ ∥ )" using eq' by (simp, blast) moreover assume ":M ∈ ORRIGHT2 (A OR B) (∥ ∥ )" then obtain a' N' where eq: "M = OrR2 .N' a" and fic: "fic (OrR2 .N' a) a" and imp1: ":N' ∈ ∥ ∥ " using ORRIGHT2_elim by blastfrom eq asm obtain N'' where eq': "M' = OrR2 .N'' a" and red1: "N' ⟶ 🪙 a* N''" using a_star_redu_OrR2_elim by blastfrom fic have "fic M' a" using eq asm by (simp add: fic_a_star_reduce)moreover from imp1 red1 have ":N'' ∈ ∥ ∥ " using ih3 by simpultimately have ":M' ∈ ORRIGHT2 (A OR B) (∥ ∥ )" using eq' by (simp, blast) ultimately have ":M' ∈ AXIOMSc (A OR B) ∪ BINDINGc (A OR B) (∥ (A OR B)∥ ) ∪ ORRIGHT1 (A OR B) (∥ ∥ ) ∪ ORRIGHT2 (A OR B) (∥ ∥ )" by blastthen have ":M' ∈ NEGc (A OR B) (∥ (A OR B)∥ )" by simpthen show ":M' ∈ (∥ ∥ )" using NEG_simp by blastnext case 2have asm: "M ⟶ 🪙 a* M'" by facthave "(x):M ∈ ∥ (A OR B)∥ " by factthen have "(x):M ∈ NEGn (A OR B) (∥ ∥ )" using NEG_simp by blastthen have "(x):M ∈ AXIOMSn (A OR B) ∪ BINDINGn (A OR B) (∥ ∥ ) ∪ ORLEFT (A OR B) (∥ (A)∥ ) (∥ (B)∥ )" by simpmoreover assume "(x):M ∈ AXIOMSn (A OR B)" then have "(x):M' ∈ AXIOMSn (A OR B)" using asm by (simp only: AXIOMS_preserved)moreover assume "(x):M ∈ BINDINGn (A OR B) (∥ ∥ )" then have "(x):M' ∈ BINDINGn (A OR B) (∥ ∥ )" using asm by (simp only: BINDING_preserved)moreover assume "(x):M ∈ ORLEFT (A OR B) (∥ (A)∥ ) (∥ (B)∥ )" then obtain y' T' z' N' where eq: "M = OrL (y').T' (z').N' x" and fin: "fin (OrL (y').T' (z').N' x) x" and imp1: "(y'):T' ∈ ∥ (A)∥ " and imp2: "(z'):N' ∈ ∥ (B)∥ " by (erule_tac ORLEFT_elim, blast)from eq asm obtain T'' N'' where eq': "M' = OrL (y').T'' (z').N'' x" and red1: "T' ⟶ 🪙 a* T''" and red2: "N' ⟶ 🪙 a* N''" using a_star_redu_OrL_elim by blastfrom fin have "fin M' x" using eq asm by (simp add: fin_a_star_reduce)moreover from imp1 red1 have "(y'):T'' ∈ ∥ (A)∥ " using ih2 by simpmoreover from imp2 red2 have "(z'):N'' ∈ ∥ (B)∥ " using ih4 by simpultimately have "(x):M' ∈ ORLEFT (A OR B) (∥ (A)∥ ) (∥ (B)∥ )" using eq' by (simp, blast) ultimately have "(x):M' ∈ AXIOMSn (A OR B) ∪ BINDINGn (A OR B) (∥ ∥ ) ∪ ORLEFT (A OR B) (∥ (A)∥ ) (∥ (B)∥ )" by blastthen have "(x):M' ∈ NEGn (A OR B) (∥ ∥ )" by simpthen show "(x):M' ∈ (∥ (A OR B)∥ )" using NEG_simp by blastnext case (NOT A)have ih1: "∧ [ :M ∈ ∥ ∥ ; M ⟶ 🪙 a* M'] ==> :M' ∈ ∥ ∥ " by facthave ih2: "∧ [ (x):M ∈ ∥ (A)∥ ; M ⟶ 🪙 a* M'] ==> (x):M' ∈ ∥ (A)∥ " by factcase 1 have asm: "M ⟶ 🪙 a* M'" by facthave ":M ∈ ∥ ∥ " by factthen have ":M ∈ NEGc (NOT A) (∥ (NOT A)∥ )" by simpthen have ":M ∈ AXIOMSc (NOT A) ∪ BINDINGc (NOT A) (∥ (NOT A)∥ ) ∪ NOTRIGHT (NOT A) (∥ (A)∥ )" by simpmoreover assume ":M ∈ AXIOMSc (NOT A)" then have ":M' ∈ AXIOMSc (NOT A)" using asm by (simp only: AXIOMS_preserved)moreover assume ":M ∈ BINDINGc (NOT A) (∥ (NOT A)∥ )" then have ":M' ∈ BINDINGc (NOT A) (∥ (NOT A)∥ )" using asm by (simp only: BINDING_preserved)moreover assume ":M ∈ NOTRIGHT (NOT A) (∥ (A)∥ )" then obtain y' N' where eq: "M = NotR (y').N' a" and fic: "fic (NotR (y').N' a) a" and imp: "(y'):N' ∈ ∥ (A)∥ " using NOTRIGHT_elim by blastfrom eq asm obtain N'' where eq': "M' = NotR (y').N'' a" and red: "N' ⟶ 🪙 a* N''" using a_star_redu_NotR_elim by blastfrom fic have "fic M' a" using eq asm by (simp add: fic_a_star_reduce)moreover from imp red have "(y'):N'' ∈ ∥ (A)∥ " using ih2 by simpultimately have ":M' ∈ NOTRIGHT (NOT A) (∥ (A)∥ )" using eq' by (simp, blast) ultimately have ":M' ∈ AXIOMSc (NOT A) ∪ BINDINGc (NOT A) (∥ (NOT A)∥ ) ∪ NOTRIGHT (NOT A) (∥ (A)∥ )" by blastthen have ":M' ∈ NEGc (NOT A) (∥ (NOT A)∥ )" by simpthen show ":M' ∈ (∥ ∥ )" using NEG_simp by blastnext case 2have asm: "M ⟶ 🪙 a* M'" by facthave "(x):M ∈ ∥ (NOT A)∥ " by factthen have "(x):M ∈ NEGn (NOT A) (∥ ∥ )" using NEG_simp by blastthen have "(x):M ∈ AXIOMSn (NOT A) ∪ BINDINGn (NOT A) (∥ ∥ ) ∪ NOTLEFT (NOT A) (∥ ∥ )" by simpmoreover assume "(x):M ∈ AXIOMSn (NOT A)" then have "(x):M' ∈ AXIOMSn (NOT A)" using asm by (simp only: AXIOMS_preserved)moreover assume "(x):M ∈ BINDINGn (NOT A) (∥ ∥ )" then have "(x):M' ∈ BINDINGn (NOT A) (∥ ∥ )" using asm by (simp only: BINDING_preserved)moreover assume "(x):M ∈ NOTLEFT (NOT A) (∥ ∥ )" then obtain a' N' where eq: "M = NotL .N' x" and fin: "fin (NotL .N' x) x" and imp: ":N' ∈ ∥ ∥ " by (erule_tac NOTLEFT_elim, blast)from eq asm obtain N'' where eq': "M' = NotL .N'' x" and red1: "N' ⟶ 🪙 a* N''" using a_star_redu_NotL_elim by blastfrom fin have "fin M' x" using eq asm by (simp add: fin_a_star_reduce)moreover from imp red1 have ":N'' ∈ ∥ ∥ " using ih1 by simpultimately have "(x):M' ∈ NOTLEFT (NOT A) (∥ ∥ )" using eq' by (simp, blast) ultimately have "(x):M' ∈ AXIOMSn (NOT A) ∪ BINDINGn (NOT A) (∥ ∥ ) ∪ NOTLEFT (NOT A) (∥ ∥ )" by blastthen have "(x):M' ∈ NEGn (NOT A) (∥ ∥ )" by simpthen show "(x):M' ∈ (∥ (NOT A)∥ )" using NEG_simp by blastqed lemma CANDs_preserved_single:shows ":M ∈ ∥ ∥ ==> M ⟶ 🪙 a M' ==> :M' ∈ ∥ ∥ " and "(x):M ∈ ∥ (B)∥ ==> M ⟶ 🪙 a M' ==> (x):M' ∈ ∥ (B)∥ " by (auto simp add: a_starI CANDs_preserved)lemma fic_CANDS:assumes a: "¬ fic M a" and b: ":M ∈ ∥ ∥ " shows ":M ∈ AXIOMSc B ∨ :M ∈ BINDINGc B (∥ (B)∥ )" using a bapply (nominal_induct B rule: ty.strong_induct)apply (simp)apply (simp)apply (erule disjE)apply (simp)apply (erule disjE)apply (simp)apply (auto simp add: ctrm.inject)[1]apply (simp add: alpha)apply (erule disjE)apply (simp)apply (auto simp add: calc_atm)[1]apply (drule_tac pi="[(a,aa)]" in fic.eqvt(2))apply (simp add: calc_atm)apply (simp)apply (erule disjE)apply (simp)apply (erule disjE)apply (simp)apply (auto simp add: ctrm.inject)[1]apply (simp add: alpha)apply (erule disjE)apply (simp)apply (erule conjE)+apply (simp)apply (drule_tac pi="[(a,c)]" in fic.eqvt(2))apply (simp add: calc_atm)apply (simp)apply (erule disjE)apply (simp)apply (erule disjE)apply (simp)apply (auto simp add: ctrm.inject)[1]apply (simp add: alpha)apply (erule disjE)apply (simp)apply (erule conjE)+apply (simp)apply (drule_tac pi="[(a,b)]" in fic.eqvt(2))apply (simp add: calc_atm)apply (simp add: alpha)apply (erule disjE)apply (simp)apply (erule conjE)+apply (simp)apply (drule_tac pi="[(a,b)]" in fic.eqvt(2))apply (simp add: calc_atm)apply (simp)apply (erule disjE)apply (simp)apply (erule disjE)apply (simp)apply (auto simp add: ctrm.inject)[1]apply (simp add: alpha)apply (erule disjE)apply (simp)apply (erule conjE)+apply (simp)apply (drule_tac pi="[(a,b)]" in fic.eqvt(2))apply (simp add: calc_atm)done lemma fin_CANDS_aux:assumes a: "¬ fin M x" and b: "(x):M ∈ (NEGn B (∥ ∥ ))" shows "(x):M ∈ AXIOMSn B ∨ (x):M ∈ BINDINGn B (∥ ∥ )" using a bapply (nominal_induct B rule: ty.strong_induct)apply (simp)apply (simp)apply (erule disjE)apply (simp)apply (erule disjE)apply (simp)apply (auto simp add: ntrm.inject)[1]apply (simp add: alpha)apply (erule disjE)apply (simp)apply (auto simp add: calc_atm)[1]apply (drule_tac pi="[(x,xa)]" in fin.eqvt(1))apply (simp add: calc_atm)apply (simp)apply (erule disjE)apply (simp)apply (erule disjE)apply (simp)apply (auto simp add: ntrm.inject)[1]apply (simp add: alpha)apply (erule disjE)apply (simp)apply (erule conjE)+apply (simp)apply (drule_tac pi="[(x,y)]" in fin.eqvt(1))apply (simp add: calc_atm)apply (simp add: alpha)apply (erule disjE)apply (simp)apply (erule conjE)+apply (simp)apply (drule_tac pi="[(x,y)]" in fin.eqvt(1))apply (simp add: calc_atm)apply (simp)apply (erule disjE)apply (simp)apply (erule disjE)apply (simp)apply (auto simp add: ntrm.inject)[1]apply (simp add: alpha)apply (erule disjE)apply (simp)apply (erule conjE)+apply (simp)apply (drule_tac pi="[(x,z)]" in fin.eqvt(1))apply (simp add: calc_atm)apply (simp)apply (erule disjE)apply (simp)apply (erule disjE)apply (simp)apply (auto simp add: ntrm.inject)[1]apply (simp add: alpha)apply (erule disjE)apply (simp)apply (erule conjE)+apply (simp)apply (drule_tac pi="[(x,y)]" in fin.eqvt(1))apply (simp add: calc_atm)done lemma fin_CANDS:assumes a: "¬ fin M x" and b: "(x):M ∈ (∥ (B)∥ )" shows "(x):M ∈ AXIOMSn B ∨ (x):M ∈ BINDINGn B (∥ ∥ )" apply (rule fin_CANDS_aux)apply (rule a)apply (rule NEG_elim)apply (rule b)done lemma BINDING_implies_CAND:shows ":M ∈ BINDINGc B (∥ (B)∥ ) ==> :M ∈ (∥ ∥ )" and "(x):N ∈ BINDINGn B (∥ ∥ ) ==> (x):N ∈ (∥ (B)∥ )" apply -apply (nominal_induct B rule: ty.strong_induct)apply (auto)apply (rule NEG_intro)apply (nominal_induct B rule: ty.strong_induct)apply (auto)done end Messung V0.5 in Prozent C=95 H=91 G=92
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.371Angebot
(Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können 2026-05-03)
¤ *Eine klare Vorstellung vom Zielzustand
2026-05-26
