Theory Class2

theory Class2
imports Class1
begin

text ‹Reduction›

lemma fin_not_Cut:
  assumes a: "fin M x"
  shows "¬(∃a M' x N'. M = Cut <a>.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 ⟶⇩c M'" "c♯M" "y♯P"
  shows "M{y:=<c>.P} ⟶⇩c M'{y:=<c>.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:=<c>.P} = M{y:=<c>.P}{a:=(x).(N{y:=<c>.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:=<a>.Ax y a}{y:=<c>.P} = N{y:=<c>.P}{x:=<c>.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 ≠ Ax y a*)
    apply(rule impI)
    apply(subgoal_tac "N{x:=<a>.M}{y:=<c>.P} = N{y:=<c>.P}{x:=<a>.(M{y:=<c>.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 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:=<a>.M}{c:=(y).P} = N{c:=(y).P}{x:=<a>.(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 ≠ 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:=<c>.P} ⟶⇩c M'{y:=<c>.P}"
using a
proof -
  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:=<c>.P} = ([(y',y)]∙M){y':=<c'>.([(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 "… ⟶⇩c ([(y',y)]∙M'){y':=<c'>.([(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:=<c>.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 ⟶⇩c M'" 
  shows "M{c:=(y).P} ⟶⇩c M'{c:=(y).P}"
using a
proof -
  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 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 "… ⟶⇩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' ⟶⇩l M''"
  shows "M ⟶⇩l M''"
using a by simp
  
lemma aux2:
  assumes a: "M ⟶⇩l M'" "M' = M''"
  shows "M ⟶⇩l M''"
using a by simp

lemma aux3:
  assumes a: "M = M'" "M' ⟶⇩a* M''"
  shows "M ⟶⇩a* M''"
using a by simp

lemma aux4:
  assumes a: "M = M'"
  shows "M ⟶⇩a* M'"
using a by blast

lemma l_redu_subst1:
  assumes a: "M ⟶⇩l M'" 
  shows "M{y:=<c>.P} ⟶⇩a* M'{y:=<c>.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 a_star_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 <a>.NotR (u).M a (v).NotL <b>.N v){y:=<c>.P} = 
        (Cut <a>.NotR (u).(M{y:=<c>.P}) a (v).NotL <b>.(N{y:=<c>.P}) v)" using LNot
        by (simp add: subst_fresh abs_fresh fresh_atm)
      also have "… ⟶⇩l (Cut <b>.(N{y:=<c>.P}) (u).(M{y:=<c>.P}))" using LNot
        by (auto intro: l_redu.intros simp add: subst_fresh)
      also have "… = (Cut <b>.N (u).M){y:=<c>.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 <a>.NotR (u).M a (v).NotL <b>.N v){y:=<c>.P} = 
        (Cut <a>.NotR (u).(M{y:=<c>.P}) a (v).NotL <b>.(N{y:=<c>.P}) v)" using LNot
        by (simp add: subst_fresh abs_fresh fresh_atm)
      also have "… ⟶⇩a* (Cut <b>.(N{y:=<c>.P}) (u).(M{y:=<c>.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 <b>.(Cut <c>.P (y).Ax y b) (u).(M{y:=<c>.P}))" using LNot asm
        by simp
      also have "… ⟶⇩a* (Cut <b>.(P[c⊢c>b]) (u).(M{y:=<c>.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 a_star_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 <b>.N (u).M){y:=<c>.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 <a>.NotR (u).M a (v).NotL <b>.N v){y:=<c>.P} ⟶⇩a* (Cut <b>.N (u).M){y:=<c>.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 <b>.AndR <a1>.M1 <a2>.M2 b (z).AndL1 (u).N z){y:=<c>.P} = 
        Cut <b>.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 "… ⟶⇩a* Cut <a1>.(M1{y:=<c>.P}) (u).(N{y:=<c>.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 <a1>.M1 (u).N){y:=<c>.P}" using LAnd1 asm
        by (simp add: subst_fresh abs_fresh fresh_atm)
      finally 
      have "(Cut <b>.AndR <a1>.M1 <a2>.M2 b (z).AndL1 (u).N z){y:=<c>.P} ⟶⇩a* (Cut <a1>.M1 (u).N){y:=<c>.P}"
        by simp
    } 
    moreover
    { assume asm: "M1=Ax y a1"
      have "(Cut <b>.AndR <a1>.M1 <a2>.M2 b (z).AndL1 (u).N z){y:=<c>.P} = 
        Cut <b>.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 "… ⟶⇩a* Cut <a1>.(M1{y:=<c>.P}) (u).(N{y:=<c>.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 <a1>.(Cut <c>.P (y). Ax y a1) (u).(N{y:=<c>.P})" 
        using LAnd1 asm by simp
      also have "… ⟶⇩a* Cut <a1>.P[c⊢c>a1] (u).(N{y:=<c>.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 a_star_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 <a1>.M1 (u).N){y:=<c>.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 <b>.AndR <a1>.M1 <a2>.M2 b (z).AndL1 (u).N z){y:=<c>.P} ⟶⇩a* (Cut <a1>.M1 (u).N){y:=<c>.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 <b>.AndR <a1>.M1 <a2>.M2 b (z).AndL2 (u).N z){y:=<c>.P} = 
        Cut <b>.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 "… ⟶⇩a* Cut <a2>.(M2{y:=<c>.P}) (u).(N{y:=<c>.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 <a2>.M2 (u).N){y:=<c>.P}" using LAnd2 asm
        by (simp add: subst_fresh abs_fresh fresh_atm)
      finally 
      have "(Cut <b>.AndR <a1>.M1 <a2>.M2 b (z).AndL2 (u).N z){y:=<c>.P} ⟶⇩a* (Cut <a2>.M2 (u).N){y:=<c>.P}"
        by simp
    } 
    moreover
    { assume asm: "M2=Ax y a2"
      have "(Cut <b>.AndR <a1>.M1 <a2>.M2 b (z).AndL2 (u).N z){y:=<c>.P} = 
        Cut <b>.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 "… ⟶⇩a* Cut <a2>.(M2{y:=<c>.P}) (u).(N{y:=<c>.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 <a2>.(Cut <c>.P (y). Ax y a2) (u).(N{y:=<c>.P})" 
        using LAnd2 asm by simp
      also have "… ⟶⇩a* Cut <a2>.P[c⊢c>a2] (u).(N{y:=<c>.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 a_star_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 <a2>.M2 (u).N){y:=<c>.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 <b>.AndR <a1>.M1 <a2>.M2 b (z).AndL2 (u).N z){y:=<c>.P} ⟶⇩a* (Cut <a2>.M2 (u).N){y:=<c>.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 <b>.OrR1 <a>.M b (z).OrL (x1).N1 (x2).N2 z){y:=<c>.P} = 
        Cut <b>.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 "… ⟶⇩a* Cut <a>.(M{y:=<c>.P}) (x1).(N1{y:=<c>.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 <a>.M (x1).N1){y:=<c>.P}" using LOr1 asm
        by (simp add: subst_fresh abs_fresh fresh_atm)
      finally 
      have "(Cut <b>.OrR1 <a>.M b (z).OrL (x1).N1 (x2).N2 z){y:=<c>.P} ⟶⇩a* (Cut <a>.M (x1).N1){y:=<c>.P}"
        by simp
    } 
    moreover
    { assume asm: "M=Ax y a"
      have "(Cut <b>.OrR1 <a>.M b (z).OrL (x1).N1 (x2).N2 z){y:=<c>.P} = 
        Cut <b>.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 "… ⟶⇩a* Cut <a>.(M{y:=<c>.P}) (x1).(N1{y:=<c>.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 <a>.(Cut <c>.P (y). Ax y a) (x1).(N1{y:=<c>.P})" 
        using LOr1 asm by simp
      also have "… ⟶⇩a* Cut <a>.P[c⊢c>a] (x1).(N1{y:=<c>.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 a_star_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 <a>.M (x1).N1){y:=<c>.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 <b>.OrR1 <a>.M b (z).OrL (x1).N1 (x2).N2 z){y:=<c>.P} ⟶⇩a* (Cut <a>.M (x1).N1){y:=<c>.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 <b>.OrR2 <a>.M b (z).OrL (x1).N1 (x2).N2 z){y:=<c>.P} = 
        Cut <b>.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 "… ⟶⇩a* Cut <a>.(M{y:=<c>.P}) (x2).(N2{y:=<c>.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 <a>.M (x2).N2){y:=<c>.P}" using LOr2 asm
        by (simp add: subst_fresh abs_fresh fresh_atm)
      finally 
      have "(Cut <b>.OrR2 <a>.M b (z).OrL (x1).N1 (x2).N2 z){y:=<c>.P} ⟶⇩a* (Cut <a>.M (x2).N2){y:=<c>.P}"
        by simp
    } 
    moreover
    { assume asm: "M=Ax y a"
      have "(Cut <b>.OrR2 <a>.M b (z).OrL (x1).N1 (x2).N2 z){y:=<c>.P} = 
        Cut <b>.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 "… ⟶⇩a* Cut <a>.(M{y:=<c>.P}) (x2).(N2{y:=<c>.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 <a>.(Cut <c>.P (y). Ax y a) (x2).(N2{y:=<c>.P})" 
        using LOr2 asm by simp
      also have "… ⟶⇩a* Cut <a>.P[c⊢c>a] (x2).(N2{y:=<c>.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 a_star_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 <a>.M (x2).N2){y:=<c>.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 <b>.OrR2 <a>.M b (z).OrL (x1).N1 (x2).N2 z){y:=<c>.P} ⟶⇩a* (Cut <a>.M (x2).N2){y:=<c>.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 <b>.ImpR (x).<a>.M b (z).ImpL <d>.N (u).Q z){y:=<c>.P} = 
        Cut <b>.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 "… ⟶⇩a* Cut <a>.(Cut <d>.(N{y:=<c>.P})  (x).(M{y:=<c>.P})) (u).(Q{y:=<c>.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 <a>.(Cut <d>.N  (x).M) (u).Q){y:=<c>.P}" using LImp asm
        by (simp add: subst_fresh abs_fresh fresh_atm)
      finally 
      have "(Cut <b>.ImpR (x).<a>.M b (z).ImpL <d>.N (u).Q z){y:=<c>.P} ⟶⇩a* 
                     (Cut <a>.(Cut <d>.N  (x).M) (u).Q){y:=<c>.P}"
        by simp
    } 
    moreover
    { assume asm: "N=Ax y d"
      have "(Cut <b>.ImpR (x).<a>.M b (z).ImpL <d>.N (u).Q z){y:=<c>.P} = 
        Cut <b>.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 "… ⟶⇩a* Cut <a>.(Cut <d>.(N{y:=<c>.P})  (x).(M{y:=<c>.P})) (u).(Q{y:=<c>.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 <a>.(Cut <d>.(Cut <c>.P (y).Ax y d)  (x).(M{y:=<c>.P})) (u).(Q{y:=<c>.P})"
        using LImp asm by simp
      also have "… ⟶⇩a* Cut <a>.(Cut <d>.(P[c⊢c>d]) (x).(M{y:=<c>.P})) (u).(Q{y:=<c>.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 a_star_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 <a>.(Cut <d>.N (x).M) (u).Q){y:=<c>.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 <b>.ImpR (x).<a>.M b (z).ImpL <d>.N (u).Q z){y:=<c>.P} ⟶⇩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 ⟶⇩l M'" 
  shows "M{c:=(y).P} ⟶⇩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 a_star_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 <a>.NotR (u).M a (v).NotL <b>.N v){c:=(y).P} = 
        (Cut <a>.NotR (u).(M{c:=(y).P}) a (v).NotL <b>.(N{c:=(y).P}) v)" using LNot
        by (simp add: subst_fresh abs_fresh fresh_atm)
      also have "… ⟶⇩l (Cut <b>.(N{c:=(y).P}) (u).(M{c:=(y).P}))" using LNot
        by (auto intro: l_redu.intros simp add: subst_fresh)
      also have "… = (Cut <b>.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 <a>.NotR (u).M a (v).NotL <b>.N v){c:=(y).P} = 
        (Cut <a>.NotR (u).(M{c:=(y).P}) a (v).NotL <b>.(N{c:=(y).P}) v)" using LNot
        by (simp add: subst_fresh abs_fresh fresh_atm)
      also have "… ⟶⇩a* (Cut <b>.(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 <b>.(N{c:=(y).P}) (u).(Cut <c>.(Ax u c) (y).P))" using LNot asm
        by simp
      also have "… ⟶⇩a* (Cut <b>.(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 a_star_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 <b>.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 <a>.NotR (u).M a (v).NotL <b>.N v){c:=(y).P} ⟶⇩a* (Cut <b>.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 <b>.AndR <a1>.M1 <a2>.M2 b (z).AndL1 (u).N z){c:=(y).P} = 
        Cut <b>.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 "… ⟶⇩a* Cut <a1>.(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 <a1>.M1 (u).N){c:=(y).P}" using LAnd1 asm
        by (simp add: subst_fresh abs_fresh fresh_atm)
      finally 
      have "(Cut <b>.AndR <a1>.M1 <a2>.M2 b (z).AndL1 (u).N z){c:=(y).P} ⟶⇩a* (Cut <a1>.M1 (u).N){c:=(y).P}"
        by simp
    } 
    moreover
    { assume asm: "N=Ax u c"
      have "(Cut <b>.AndR <a1>.M1 <a2>.M2 b (z).AndL1 (u).N z){c:=(y).P} = 
        Cut <b>.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 "… ⟶⇩a* Cut <a1>.(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 <a1>.(M1{c:=(y).P}) (u).(Cut <c>.(Ax u c) (y).P)" 
        using LAnd1 asm by simp
      also have "… ⟶⇩a* Cut <a1>.(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 a_star_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 <a1>.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 <b>.AndR <a1>.M1 <a2>.M2 b (z).AndL1 (u).N z){c:=(y).P} ⟶⇩a* (Cut <a1>.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 <b>.AndR <a1>.M1 <a2>.M2 b (z).AndL2 (u).N z){c:=(y).P} = 
        Cut <b>.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 "… ⟶⇩a* Cut <a2>.(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 <a2>.M2 (u).N){c:=(y).P}" using LAnd2 asm
        by (simp add: subst_fresh abs_fresh fresh_atm)
      finally 
      have "(Cut <b>.AndR <a1>.M1 <a2>.M2 b (z).AndL2 (u).N z){c:=(y).P} ⟶⇩a* (Cut <a2>.M2 (u).N){c:=(y).P}"
        by simp
    } 
    moreover
    { assume asm: "N=Ax u c"
      have "(Cut <b>.AndR <a1>.M1 <a2>.M2 b (z).AndL2 (u).N z){c:=(y).P} = 
        Cut <b>.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 "… ⟶⇩a* Cut <a2>.(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 <a2>.(M2{c:=(y).P}) (u).(Cut <c>.(Ax u c) (y).P)" 
        using LAnd2 asm by simp
      also have "… ⟶⇩a* Cut <a2>.(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 a_star_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 <a2>.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 <b>.AndR <a1>.M1 <a2>.M2 b (z).AndL2 (u).N z){c:=(y).P} ⟶⇩a* (Cut <a2>.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 <b>.OrR1 <a>.M b (z).OrL (x1).N1 (x2).N2 z){c:=(y).P} = 
        Cut <b>.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 "… ⟶⇩a* Cut <a>.(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 <a>.M (x1).N1){c:=(y).P}" using LOr1 asm
        by (simp add: subst_fresh abs_fresh fresh_atm)
      finally 
      have "(Cut <b>.OrR1 <a>.M b (z).OrL (x1).N1 (x2).N2 z){c:=(y).P} ⟶⇩a* (Cut <a>.M (x1).N1){c:=(y).P}"
        by simp
    } 
    moreover
    { assume asm: "N1=Ax x1 c"
      have "(Cut <b>.OrR1 <a>.M b (z).OrL (x1).N1 (x2).N2 z){c:=(y).P} = 
        Cut <b>.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 "… ⟶⇩a* Cut <a>.(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 <a>.(M{c:=(y).P}) (x1).(Cut <c>.(Ax x1 c) (y).P)" 
        using LOr1 asm by simp
      also have "… ⟶⇩a* Cut <a>.(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 a_star_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 <a>.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 <b>.OrR1 <a>.M b (z).OrL (x1).N1 (x2).N2 z){c:=(y).P} ⟶⇩a* (Cut <a>.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 <b>.OrR2 <a>.M b (z).OrL (x1).N1 (x2).N2 z){c:=(y).P} = 
        Cut <b>.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 "… ⟶⇩a* Cut <a>.(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 <a>.M (x2).N2){c:=(y).P}" using LOr2 asm
        by (simp add: subst_fresh abs_fresh fresh_atm)
      finally 
      have "(Cut <b>.OrR2 <a>.M b (z).OrL (x1).N1 (x2).N2 z){c:=(y).P} ⟶⇩a* (Cut <a>.M (x2).N2){c:=(y).P}"
        by simp
    } 
    moreover
    { assume asm: "N2=Ax x2 c"
      have "(Cut <b>.OrR2 <a>.M b (z).OrL (x1).N1 (x2).N2 z){c:=(y).P} = 
        Cut <b>.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 "… ⟶⇩a* Cut <a>.(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 <a>.(M{c:=(y).P}) (x2).(Cut <c>.(Ax x2 c) (y).P)" 
        using LOr2 asm by simp
      also have "… ⟶⇩a* Cut <a>.(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 a_star_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 <a>.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 <b>.OrR2 <a>.M b (z).OrL (x1).N1 (x2).N2 z){c:=(y).P} ⟶⇩a* (Cut <a>.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 <b>.ImpR (x).<a>.M b (z).ImpL <d>.N (u).Q z){c:=(y).P} = 
        Cut <b>.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 "… ⟶⇩a* Cut <a>.(Cut <d>.(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 <a>.(Cut <d>.N  (x).M) (u).Q){c:=(y).P}" using LImp asm
        by (simp add: subst_fresh abs_fresh fresh_atm)
      finally 
      have "(Cut <b>.ImpR (x).<a>.M b (z).ImpL <d>.N (u).Q z){c:=(y).P} ⟶⇩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 <b>.ImpR (x).<a>.M b (z).ImpL <d>.N (u).Q z){c:=(y).P} = 
        Cut <b>.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 "… ⟶⇩a* Cut <a>.(Cut <d>.(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 <a>.(Cut <d>.(N{c:=(y).P})  (x).(Cut <c>.Ax x c (y).P)) (u).(Q{c:=(y).P})"
        using LImp asm by simp
      also have "… ⟶⇩a* Cut <a>.(Cut <d>.(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 a_star_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 a_star_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 <a>.(Cut <d>.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 <b>.ImpR (x).<a>.M b (z).ImpL <d>.N (u).Q z){c:=(y).P} ⟶⇩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 <b>.ImpR (x).<a>.M b (z).ImpL <d>.N (u).Q z){c:=(y).P} = 
        Cut <b>.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 "… ⟶⇩a* Cut <a>.(Cut <d>.(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 <a>.(Cut <d>.(N{c:=(y).P})  (x).(M{c:=(y).P})) (u).(Cut <c>.Ax u c (y).P)"
        using LImp asm by simp
      also have "… ⟶⇩a* Cut <a>.(Cut <d>.(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 a_star_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 <a>.(Cut <d>.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 <b>.ImpR (x).<a>.M b (z).ImpL <d>.N (u).Q z){c:=(y).P} ⟶⇩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 <b>.ImpR (x).<a>.M b (z).ImpL <d>.N (u).Q z){c:=(y).P} = 
        Cut <b>.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 "… ⟶⇩a* Cut <a>.(Cut <d>.(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 <a>.(Cut <d>.(N{c:=(y).P})  (x).(Cut <c>.Ax x c (y).P)) (u).(Cut <c>.Ax u c (y).P)"
        using LImp asm by simp
      also have "… ⟶⇩a* Cut <a>.(Cut <d>.(N{c:=(y).P})  (x).(Cut <c>.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 a_star_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 <a>.(Cut <d>.(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 a_star_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 <a>.(Cut <d>.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 <b>.ImpR (x).<a>.M b (z).ImpL <d>.N (u).Q z){c:=(y).P} ⟶⇩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 ⟶⇩a M'"
  shows "M{y:=<c>.P} ⟶⇩a* M'{y:=<c>.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