Quelle Class2.thy Sprache: Isabelle

theory Class2
imports Class1
begin

text \<open>Reduction\<close>

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 fresh_atm)
 with a show "\fin M x" by blast
qed

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 blast
qed

lemma c_redu_subst1:
 assumes a: "M \\<^sub>c M'" "c\M" "y\P"
 shows "M{y:=.P} \\<^sub>c M'{y:=.P}"
using a
proof(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 \\<^sub>c M'" "c\P" "y\M"
 shows "M{c:=(y).P} \\<^sub>c M'{c:=(y).P}"
using a
proof(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 \\<^sub>c M'"
 shows "M{y:=.P} \\<^sub>c M'{y:=.P}"
using a
proof -
 obtain y'::"name" where fs1: "y'\<sharp>(M,M',P,P,y)" by (rule exists_fresh(1), rule fin_supp, blast)
 obtain c'::"coname" where fs2: "c'\<sharp>(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 fs2
 apply -
 apply(rule trans)
 apply(rule_tac y="y'" in subst_rename(3))
 apply(simp)
 apply(rule subst_rename(4))
 apply(simp)
 done
 also have "\ \\<^sub>c ([(y',y)]\M'){y':=.([(c',c)]\P)}" using fs1 fs2
 apply -
 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 fs2
 apply -
 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 simp
qed

lemma c_redu_subst2':
 assumes a: "M \\<^sub>c M'"
 shows "M{c:=(y).P} \\<^sub>c M'{c:=(y).P}"
using a
proof -
 obtain y'::"name" where fs1: "y'\<sharp>(M,M',P,P,y)" by (rule exists_fresh(1), rule fin_supp, blast)
 obtain c'::"coname" where fs2: "c'\<sharp>(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 fs2
 apply -
 apply(rule trans)
 apply(rule_tac c="c'" in subst_rename(1))
 apply(simp)
 apply(rule subst_rename(2))
 apply(simp)
 done
 also have "\ \\<^sub>c ([(c',c)]\M'){c':=(y').([(y',y)]\P)}" using fs1 fs2
 apply -
 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 fs2
 apply -
 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 simp
qed

lemma aux1:
 assumes a: "M = M'" "M' \\<^sub>l M''"
 shows "M \\<^sub>l M''"
using a by simp

lemma aux2:
 assumes a: "M \\<^sub>l M'" "M' = M''"
 shows "M \\<^sub>l M''"
using a by simp

lemma aux3:
 assumes a: "M = M'" "M' \\<^sub>a* M''"
 shows "M \\<^sub>a* M''"
using a by simp

lemma aux4:
 assumes a: "M = M'"
 shows "M \\<^sub>a* M'"
using a by blast

lemma l_redu_subst1:
 assumes a: "M \\<^sub>l M'"
 shows "M{y:=.P} \\<^sub>a* M'{y:=.P}"
using a
proof(nominal_induct M M' avoiding: y c P rule: l_redu.strong_induct)
 case LAxR
 then 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 LAxL
 then 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 <a>.NotR (u).(M{y:=<c>.P}) a (v).NotL .(N{y:=<c>.P}) v)" using LNot
 by (simp add: subst_fresh abs_fresh fresh_atm)
 also have "\ \\<^sub>l (Cut .(N{y:=.P}) (u).(M{y:=.P}))" using LNot
 by (auto intro: l_redu.intros simp add: subst_fresh)
 also have "\ = (Cut .N (u).M){y:=.P}" using LNot asm
 by (simp add: subst_fresh abs_fresh fresh_atm)
 finally have ?thesis by auto
 }
 moreover
 { assume asm: "N=Ax y b"
 have "(Cut .NotR (u).M a (v).NotL .N v){y:=.P} =
 (Cut <a>.NotR (u).(M{y:=<c>.P}) a (v).NotL .(N{y:=<c>.P}) v)" using LNot
 by (simp add: subst_fresh abs_fresh fresh_atm)
 also have "\ \\<^sub>a* (Cut .(N{y:=.P}) (u).(M{y:=.P}))" using LNot
 apply -
 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 asm
 by simp
 also have "\ \\<^sub>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 LNot
 apply -
 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 ?thesis
 apply -
 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 asm
 apply -
 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} \\<^sub>a* (Cut .N (u).M){y:=.P}"
 by simp
 }
 ultimately show ?thesis by blast
 qed
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 <a1>.(M1{y:=<c>.P}) <a2>.(M2{y:=<c>.P}) b (z).AndL1 (u).(N{y:=<c>.P}) z"
 using LAnd1 by (simp add: subst_fresh abs_fresh fresh_atm)
 also have "\ \\<^sub>a* Cut .(M1{y:=.P}) (u).(N{y:=.P})"
 using LAnd1
 apply -
 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 asm
 by (simp add: subst_fresh abs_fresh fresh_atm)
 finally
 have "(Cut .AndR .M1 .M2 b (z).AndL1 (u).N z){y:=.P} \\<^sub>a* (Cut .M1 (u).N){y:=.P}"
 by simp
 }
 moreover
 { assume asm: "M1=Ax y a1"
 have "(Cut .AndR .M1 .M2 b (z).AndL1 (u).N z){y:=.P} =
 Cut .AndR <a1>.(M1{y:=<c>.P}) <a2>.(M2{y:=<c>.P}) b (z).AndL1 (u).(N{y:=<c>.P}) z"
 using LAnd1 by (simp add: subst_fresh abs_fresh fresh_atm)
 also have "\ \\<^sub>a* Cut .(M1{y:=.P}) (u).(N{y:=.P})"
 using LAnd1
 apply -
 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 simp
 also have "\ \\<^sub>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 LAnd1
 apply -
 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 ?thesis
 apply -
 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 asm
 apply -
 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} \\<^sub>a* (Cut .M1 (u).N){y:=.P}"
 by simp
 }
 ultimately show ?thesis by blast
 qed
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 <a1>.(M1{y:=<c>.P}) <a2>.(M2{y:=<c>.P}) b (z).AndL2 (u).(N{y:=<c>.P}) z"
 using LAnd2 by (simp add: subst_fresh abs_fresh fresh_atm)
 also have "\ \\<^sub>a* Cut .(M2{y:=.P}) (u).(N{y:=.P})"
 using LAnd2
 apply -
 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 asm
 by (simp add: subst_fresh abs_fresh fresh_atm)
 finally
 have "(Cut .AndR .M1 .M2 b (z).AndL2 (u).N z){y:=.P} \\<^sub>a* (Cut .M2 (u).N){y:=.P}"
 by simp
 }
 moreover
 { assume asm: "M2=Ax y a2"
 have "(Cut .AndR .M1 .M2 b (z).AndL2 (u).N z){y:=.P} =
 Cut .AndR <a1>.(M1{y:=<c>.P}) <a2>.(M2{y:=<c>.P}) b (z).AndL2 (u).(N{y:=<c>.P}) z"
 using LAnd2 by (simp add: subst_fresh abs_fresh fresh_atm)
 also have "\ \\<^sub>a* Cut .(M2{y:=.P}) (u).(N{y:=.P})"
 using LAnd2
 apply -
 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 simp
 also have "\ \\<^sub>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 asm
 apply -
 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 ?thesis
 apply -
 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 asm
 apply -
 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} \\<^sub>a* (Cut .M2 (u).N){y:=.P}"
 by simp
 }
 ultimately show ?thesis by blast
 qed
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 <a>.(M{y:=<c>.P}) b (z).OrL (x1).(N1{y:=<c>.P}) (x2).(N2{y:=<c>.P}) z"
 using LOr1 by (simp add: subst_fresh abs_fresh fresh_atm)
 also have "\ \\<^sub>a* Cut .(M{y:=.P}) (x1).(N1{y:=.P})"
 using LOr1
 apply -
 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 asm
 by (simp add: subst_fresh abs_fresh fresh_atm)
 finally
 have "(Cut .OrR1 .M b (z).OrL (x1).N1 (x2).N2 z){y:=.P} \\<^sub>a* (Cut .M (x1).N1){y:=.P}"
 by simp
 }
 moreover
 { assume asm: "M=Ax y a"
 have "(Cut .OrR1 .M b (z).OrL (x1).N1 (x2).N2 z){y:=.P} =
 Cut .OrR1 <a>.(M{y:=<c>.P}) b (z).OrL (x1).(N1{y:=<c>.P}) (x2).(N2{y:=<c>.P}) z"
 using LOr1 by (simp add: subst_fresh abs_fresh fresh_atm)
 also have "\ \\<^sub>a* Cut .(M{y:=.P}) (x1).(N1{y:=.P})"
 using LOr1
 apply -
 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 simp
 also have "\ \\<^sub>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 LOr1
 apply -
 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 ?thesis
 apply -
 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 asm
 apply -
 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} \\<^sub>a* (Cut .M (x1).N1){y:=.P}"
 by simp
 }
 ultimately show ?thesis by blast
 qed
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 <a>.(M{y:=<c>.P}) b (z).OrL (x1).(N1{y:=<c>.P}) (x2).(N2{y:=<c>.P}) z"
 using LOr2 by (simp add: subst_fresh abs_fresh fresh_atm)
 also have "\ \\<^sub>a* Cut .(M{y:=.P}) (x2).(N2{y:=.P})"
 using LOr2
 apply -
 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 asm
 by (simp add: subst_fresh abs_fresh fresh_atm)
 finally
 have "(Cut .OrR2 .M b (z).OrL (x1).N1 (x2).N2 z){y:=.P} \\<^sub>a* (Cut .M (x2).N2){y:=.P}"
 by simp
 }
 moreover
 { assume asm: "M=Ax y a"
 have "(Cut .OrR2 .M b (z).OrL (x1).N1 (x2).N2 z){y:=.P} =
 Cut .OrR2 <a>.(M{y:=<c>.P}) b (z).OrL (x1).(N1{y:=<c>.P}) (x2).(N2{y:=<c>.P}) z"
 using LOr2 by (simp add: subst_fresh abs_fresh fresh_atm)
 also have "\ \\<^sub>a* Cut .(M{y:=.P}) (x2).(N2{y:=.P})"
 using LOr2
 apply -
 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 simp
 also have "\ \\<^sub>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 LOr2
 apply -
 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 ?thesis
 apply -
 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 asm
 apply -
 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} \\<^sub>a* (Cut .M (x2).N2){y:=.P}"
 by simp
 }
 ultimately show ?thesis by blast
 qed
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).<a>.(M{y:=<c>.P}) b (z).ImpL <d>.(N{y:=<c>.P}) (u).(Q{y:=<c>.P}) z"
 using LImp by (simp add: fresh_prod abs_fresh fresh_atm)
 also have "\ \\<^sub>a* Cut .(Cut .(N{y:=.P}) (x).(M{y:=.P})) (u).(Q{y:=.P})"
 using LImp
 apply -
 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 asm
 by (simp add: subst_fresh abs_fresh fresh_atm)
 finally
 have "(Cut .ImpR (x)..M b (z).ImpL .N (u).Q z){y:=.P} \\<^sub>a*
 (Cut <a>.(Cut <d>.N (x).M) (u).Q){y:=<c>.P}"
 by simp
 }
 moreover
 { assume asm: "N=Ax y d"
 have "(Cut .ImpR (x)..M b (z).ImpL .N (u).Q z){y:=.P} =
 Cut .ImpR (x).<a>.(M{y:=<c>.P}) b (z).ImpL <d>.(N{y:=<c>.P}) (u).(Q{y:=<c>.P}) z"
 using LImp by (simp add: subst_fresh abs_fresh fresh_atm fresh_prod)
 also have "\ \\<^sub>a* Cut .(Cut .(N{y:=.P}) (x).(M{y:=.P})) (u).(Q{y:=.P})"
 using LImp
 apply -
 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 simp
 also have "\ \\<^sub>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 LImp
 apply -
 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 LImp
 apply -
 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 asm
 apply -
 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} \\<^sub>a*
 (Cut <a>.(Cut <d>.N (x).M) (u).Q){y:=<c>.P}"
 by simp
 }
 ultimately show ?thesis by blast
 qed
qed

lemma l_redu_subst2:
 assumes a: "M \\<^sub>l M'"
 shows "M{c:=(y).P} \\<^sub>a* M'{c:=(y).P}"
using a
proof(nominal_induct M M' avoiding: y c P rule: l_redu.strong_induct)
 case LAxR
 then 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 LAxL
 then 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 <a>.NotR (u).(M{c:=(y).P}) a (v).NotL .(N{c:=(y).P}) v)" using LNot
 by (simp add: subst_fresh abs_fresh fresh_atm)
 also have "\ \\<^sub>l (Cut .(N{c:=(y).P}) (u).(M{c:=(y).P}))" using LNot
 by (auto intro: l_redu.intros simp add: subst_fresh)
 also have "\ = (Cut .N (u).M){c:=(y).P}" using LNot asm
 by (simp add: subst_fresh abs_fresh fresh_atm)
 finally have ?thesis by auto
 }
 moreover
 { assume asm: "M=Ax u c"
 have "(Cut .NotR (u).M a (v).NotL .N v){c:=(y).P} =
 (Cut <a>.NotR (u).(M{c:=(y).P}) a (v).NotL .(N{c:=(y).P}) v)" using LNot
 by (simp add: subst_fresh abs_fresh fresh_atm)
 also have "\ \\<^sub>a* (Cut .(N{c:=(y).P}) (u).(M{c:=(y).P}))" using LNot
 apply -
 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 asm
 by simp
 also have "\ \\<^sub>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 LNot
 apply -
 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 ?thesis
 apply -
 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 asm
 apply -
 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} \\<^sub>a* (Cut .N (u).M){c:=(y).P}"
 by simp
 }
 ultimately show ?thesis by blast
 qed
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 <a1>.(M1{c:=(y).P}) <a2>.(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 "\ \\<^sub>a* Cut .(M1{c:=(y).P}) (u).(N{c:=(y).P})"
 using LAnd1
 apply -
 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 asm
 by (simp add: subst_fresh abs_fresh fresh_atm)
 finally
 have "(Cut .AndR .M1 .M2 b (z).AndL1 (u).N z){c:=(y).P} \\<^sub>a* (Cut .M1 (u).N){c:=(y).P}"
 by simp
 }
 moreover
 { assume asm: "N=Ax u c"
 have "(Cut .AndR .M1 .M2 b (z).AndL1 (u).N z){c:=(y).P} =
 Cut .AndR <a1>.(M1{c:=(y).P}) <a2>.(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 "\ \\<^sub>a* Cut .(M1{c:=(y).P}) (u).(N{c:=(y).P})"
 using LAnd1
 apply -
 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 simp
 also have "\ \\<^sub>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 LAnd1
 apply -
 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 ?thesis
 apply -
 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 asm
 apply -
 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} \\<^sub>a* (Cut .M1 (u).N){c:=(y).P}"
 by simp
 }
 ultimately show ?thesis by blast
 qed
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 <a1>.(M1{c:=(y).P}) <a2>.(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 "\ \\<^sub>a* Cut .(M2{c:=(y).P}) (u).(N{c:=(y).P})"
 using LAnd2
 apply -
 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 asm
 by (simp add: subst_fresh abs_fresh fresh_atm)
 finally
 have "(Cut .AndR .M1 .M2 b (z).AndL2 (u).N z){c:=(y).P} \\<^sub>a* (Cut .M2 (u).N){c:=(y).P}"
 by simp
 }
 moreover
 { assume asm: "N=Ax u c"
 have "(Cut .AndR .M1 .M2 b (z).AndL2 (u).N z){c:=(y).P} =
 Cut .AndR <a1>.(M1{c:=(y).P}) <a2>.(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 "\ \\<^sub>a* Cut .(M2{c:=(y).P}) (u).(N{c:=(y).P})"
 using LAnd2
 apply -
 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 simp
 also have "\ \\<^sub>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 LAnd2
 apply -
 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 ?thesis
 apply -
 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 asm
 apply -
 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} \\<^sub>a* (Cut .M2 (u).N){c:=(y).P}"
 by simp
 }
 ultimately show ?thesis by blast
 qed
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 <a>.(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 "\ \\<^sub>a* Cut .(M{c:=(y).P}) (x1).(N1{c:=(y).P})"
 using LOr1
 apply -
 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 asm
 by (simp add: subst_fresh abs_fresh fresh_atm)
 finally
 have "(Cut .OrR1 .M b (z).OrL (x1).N1 (x2).N2 z){c:=(y).P} \\<^sub>a* (Cut .M (x1).N1){c:=(y).P}"
 by simp
 }
 moreover
 { assume asm: "N1=Ax x1 c"
 have "(Cut .OrR1 .M b (z).OrL (x1).N1 (x2).N2 z){c:=(y).P} =
 Cut .OrR1 <a>.(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 "\ \\<^sub>a* Cut .(M{c:=(y).P}) (x1).(N1{c:=(y).P})"
 using LOr1
 apply -
 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 simp
 also have "\ \\<^sub>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 LOr1
 apply -
 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 ?thesis
 apply -
 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 asm
 apply -
 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} \\<^sub>a* (Cut .M (x1).N1){c:=(y).P}"
 by simp
 }
 ultimately show ?thesis by blast
 qed
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 <a>.(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 "\ \\<^sub>a* Cut .(M{c:=(y).P}) (x2).(N2{c:=(y).P})"
 using LOr2
 apply -
 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 asm
 by (simp add: subst_fresh abs_fresh fresh_atm)
 finally
 have "(Cut .OrR2 .M b (z).OrL (x1).N1 (x2).N2 z){c:=(y).P} \\<^sub>a* (Cut .M (x2).N2){c:=(y).P}"
 by simp
 }
 moreover
 { assume asm: "N2=Ax x2 c"
 have "(Cut .OrR2 .M b (z).OrL (x1).N1 (x2).N2 z){c:=(y).P} =
 Cut .OrR2 <a>.(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 "\ \\<^sub>a* Cut .(M{c:=(y).P}) (x2).(N2{c:=(y).P})"
 using LOr2
 apply -
 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 simp
 also have "\ \\<^sub>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 LOr2
 apply -
 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 ?thesis
 apply -
 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 asm
 apply -
 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} \\<^sub>a* (Cut .M (x2).N2){c:=(y).P}"
 by simp
 }
 ultimately show ?thesis by blast
 qed
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).<a>.(M{c:=(y).P}) b (z).ImpL <d>.(N{c:=(y).P}) (u).(Q{c:=(y).P}) z"
 using LImp by (simp add: fresh_prod abs_fresh fresh_atm)
 also have "\ \\<^sub>a* Cut .(Cut .(N{c:=(y).P}) (x).(M{c:=(y).P})) (u).(Q{c:=(y).P})"
 using LImp
 apply -
 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 asm
 by (simp add: subst_fresh abs_fresh fresh_atm)
 finally
 have "(Cut .ImpR (x)..M b (z).ImpL .N (u).Q z){c:=(y).P} \\<^sub>a*
 (Cut <a>.(Cut <d>.N (x).M) (u).Q){c:=(y).P}"
 by simp
 }
 moreover
 { 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).<a>.(M{c:=(y).P}) b (z).ImpL <d>.(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 "\ \\<^sub>a* Cut .(Cut .(N{c:=(y).P}) (x).(M{c:=(y).P})) (u).(Q{c:=(y).P})"
 using LImp
 apply -
 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 simp
 also have "\ \\<^sub>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 LImp
 apply -
 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 LImp
 apply -
 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 asm
 apply -
 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} \\<^sub>a*
 (Cut <a>.(Cut <d>.N (x).M) (u).Q){c:=(y).P}"
 by simp
 }
 moreover
 { 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).<a>.(M{c:=(y).P}) b (z).ImpL <d>.(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 "\ \\<^sub>a* Cut .(Cut .(N{c:=(y).P}) (x).(M{c:=(y).P})) (u).(Q{c:=(y).P})"
 using LImp
 apply -
 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 simp
 also have "\ \\<^sub>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 LImp
 apply -
 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 LImp
 apply -
 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 asm
 apply -
 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} \\<^sub>a*
 (Cut <a>.(Cut <d>.N (x).M) (u).Q){c:=(y).P}"
 by simp
 }
 moreover
 { 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).<a>.(M{c:=(y).P}) b (z).ImpL <d>.(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 "\ \\<^sub>a* Cut .(Cut .(N{c:=(y).P}) (x).(M{c:=(y).P})) (u).(Q{c:=(y).P})"
 using LImp
 apply -
 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 simp
 also have "\ \\<^sub>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 LImp
 apply -
 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 LImp
 apply -
 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 "\ \\<^sub>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 LImp
 apply -
 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 LImp
 apply -
 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 asm
 apply -
 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} \\<^sub>a*
 (Cut <a>.(Cut <d>.N (x).M) (u).Q){c:=(y).P}"
 by simp
 }
 ultimately show ?thesis by blast
 qed
qed

lemma a_redu_subst1:
 assumes a: "M \\<^sub>a M'"
 shows "M{y:=.P} \\<^sub>a* M'{y:=.P}"
using a
proof(nominal_induct avoiding: y c P rule: a_redu.strong_induct)
 case al_redu
 then show ?case by (simp only: l_redu_subst1)
next
 case ac_redu
 then 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_NotL
 then 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_NotR
 then show ?case
 apply(auto)
 apply(rule a_star_NotR)
 apply(auto)[1]
 done
next
 case a_AndR_l
 then show ?case
 apply(auto simp add: subst_fresh fresh_a_redu)
 apply(rule a_star_AndR)
 apply(auto)
 done
next
 case a_AndR_r
 then show ?case
 apply(auto simp add: subst_fresh fresh_a_redu)
 apply(rule a_star_AndR)
 apply(auto)
 done
next
 case a_AndL1
 then 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_AndL2
 then 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_OrR1
 then show ?case
 apply(auto simp add: subst_fresh fresh_a_redu)
 apply(rule a_star_OrR1)
 apply(auto)
 done
next
 case a_OrR2
 then show ?case
 apply(auto simp add: subst_fresh fresh_a_redu)
 apply(rule a_star_OrR2)
 apply(auto)
 done
next
 case a_OrL_l
 then 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_r
 then 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_ImpR
 then show ?case
 apply(auto simp add: subst_fresh fresh_a_redu)
 apply(rule a_star_ImpR)
 apply(auto)
 done
next
 case a_ImpL_r
 then 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_l
 then 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 \\<^sub>a M'"
 shows "M{c:=(y).P} \\<^sub>a* M'{c:=(y).P}"
using a
proof(nominal_induct avoiding: y c P rule: a_redu.strong_induct)
 case al_redu
 then show ?case by (simp only: l_redu_subst2)
next
 case ac_redu
 then 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_NotR
 then 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_NotL
 then show ?case
 apply(auto)
 apply(rule a_star_NotL)
 apply(auto)[1]
 done
next
 case a_AndR_l
 then 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_r
 then 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_AndL1
 then show ?case
 apply(auto simp add: subst_fresh fresh_a_redu)
 apply(rule a_star_AndL1)
 apply(auto)
 done
next
 case a_AndL2
 then show ?case
 apply(auto simp add: subst_fresh fresh_a_redu)
 apply(rule a_star_AndL2)
 apply(auto)
 done
next
 case a_OrR1
 then 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_OrR2
 then 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_l
 then show ?case
 apply(auto simp add: subst_fresh fresh_a_redu)
 apply(rule a_star_OrL)
 apply(auto)
 done
next
 case a_OrL_r
 then show ?case
 apply(auto simp add: subst_fresh fresh_a_redu)
 apply(rule a_star_OrL)
 apply(auto)
 done
next
 case a_ImpR
 then 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_l
 then show ?case
 apply(auto simp add: subst_fresh fresh_a_redu)
 apply(rule a_star_ImpL)
 apply(auto)
 done
next
 case a_ImpL_r
 then 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 \\<^sub>a* M'"
 shows "M{y:=.P} \\<^sub>a* M'{y:=.P}"
using a
apply(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 \\<^sub>a* M'"
 shows "M{c:=(y).P} \\<^sub>a* M'{c:=(y).P}"
using a
apply(induct)
apply(blast)
apply(drule_tac y="y" and c="c" and P="P" in a_redu_subst2)
apply(auto)
done

text \<open>Candidates and SN\<close>

text \<open>SNa\<close>

inductive
 SNa :: "trm \ bool"
where
 SNaI: "(\M'. M \\<^sub>a M' \ SNa M') \ SNa M"

lemma SNa_induct[consumes 1]:
 assumes major: "SNa M"
 assumes hyp: "\M'. SNa M' \ (\M''. M'\\<^sub>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: "\x z.
 (\<And>y. x\<longrightarrow>\<^sub>a y \<Longrightarrow> SNa y) \<Longrightarrow>
 (\<And>y. x\<longrightarrow>\<^sub>a y \<Longrightarrow> P y z) \<Longrightarrow>
 (\<And>u. z\<longrightarrow>\<^sub>a u \<Longrightarrow> SNa u) \<Longrightarrow>
 (\<And>u. z\<longrightarrow>\<^sub>a u \<Longrightarrow> P x u) \<Longrightarrow> P x z"
 shows "P a b"
proof -
 from a_SNa
 have r: "\b. SNa b \ P a b"
 proof (induct a rule: SNa.induct)
 case (SNaI x)
 note SNa' = this
 have "SNa b" by fact
 thus ?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\\<^sub>ay \ P y z) \ (\u. z\\<^sub>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\\<^sub>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\\<^sub>a* M'"
 shows "SNa M'"
using b a
by (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 a
apply(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 a
apply(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 a
apply(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 a
apply(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 a
apply(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 a
apply(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 a
apply(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:
--> --------------------

--> maximum size reached

--> --------------------

quality100%

¤ Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.0.48Bemerkung: (vorverarbeitet) ¤

*Bot Zugriff

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.