Theory Class2

theory Class2
imports Class1
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
    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 a_star_trans)
    apply(rule a_star_CutL)
    apply(assumption)
    apply(rule a_star_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 a_star_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 ⟶a M'"
  shows "M{c:=(y).P} ⟶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 a_star_trans)
    apply(rule a_star_CutR)
    apply(assumption)
    apply(rule a_star_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 a_star_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 ⟶a* M'"
  shows "M{y:=<c>.P} ⟶a* M'{y:=<c>.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 ⟶a* M'"
  shows "M{c:=(y).P} ⟶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 ‹Candidates and SN›

text ‹SNa›

inductive 
  SNa :: "trm ⇒ bool"
where
  SNaI: "(⋀M'. M ⟶a M' ⟹ SNa M') ⟹ SNa M"

lemma SNa_induct[consumes 1]:
  assumes major: "SNa M"
  assumes hyp: "⋀M'. SNa M' ⟹ (∀M''. M'⟶a M'' ⟶ P M'' ⟹ P M')"
  shows "P M"
  apply (rule major[THEN SNa.induct])
  apply (rule hyp)
  apply (rule SNaI)
  apply (blast)+
  done


lemma double_SNa_aux:
  assumes a_SNa: "SNa a"
  and b_SNa: "SNa b"
  and hyp: "⋀x z.
    (⋀y. x⟶a y ⟹ SNa y) ⟹
    (⋀y. x⟶a y ⟹ P y z) ⟹
    (⋀u. z⟶a u ⟹ SNa u) ⟹
    (⋀u. z⟶a u ⟹ P x u) ⟹ 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⟶ay ⟶ P y z) ∧ (∀u. z⟶a u ⟶ P x u)) ⟶ P x z⟧ ⟹ P a b"
apply(rule_tac double_SNa_aux)
apply(assumption)+
apply(blast)
done

lemma a_preserves_SNa:
  assumes a: "SNa M" "M⟶a M'"
  shows "SNa M'"
using a 
by (erule_tac SNa.cases) (simp)

lemma a_star_preserves_SNa:
  assumes a: "SNa M" and b: "M⟶a* M'"
  shows "SNa M'"
using b 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 <a>.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>.([(a,aa)]∙M'a) x = NotL <aa>.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 <a>.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>.([(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 <a>.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>.([(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).<a>.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>.([(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).<a>.([(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>.([(a,aa)]∙[(x,xa)]∙M'a) b" in subst)
apply(simp add: trm.inject alpha fresh_a_redu abs_fresh abs_perm calc_atm)
apply(simp add: fresh_left calc_atm fresh_a_redu)
apply(simp)
done

lemma AndR_in_SNa:
  assumes a: "SNa M" "SNa N"
  shows "SNa (AndR <a>.M <b>.N c)"
apply(rule_tac a="M" and b="N" in double_SNa)
apply(rule a)+
apply(auto)
apply(rule SNaI)
apply(drule a_redu_AndR_elim)
apply(auto)
done

lemma OrL_in_SNa:
  assumes a: "SNa M" "SNa N"
  shows "SNa (OrL (x).M (y).N z)"
apply(rule_tac a="M" and b="N" in double_SNa)
apply(rule a)+
apply(auto)
apply(rule SNaI)
apply(drule a_redu_OrL_elim)
apply(auto)
done

lemma ImpL_in_SNa:
  assumes a: "SNa M" "SNa N"
  shows "SNa (ImpL <a>.M (y).N z)"
apply(rule_tac a="M" and b="N" in double_SNa)
apply(rule a)+
apply(auto)
apply(rule SNaI)
apply(drule a_redu_ImpL_elim)
apply(auto)
done

lemma SNa_eqvt:
  fixes pi1::"name prm"
  and   pi2::"coname prm"
  shows "SNa M ⟹ SNa (pi1∙M)"
  and   "SNa M ⟹ SNa (pi2∙M)"
apply -
apply(induct rule: SNa.induct)
apply(rule SNaI)
apply(drule_tac pi="(rev pi1)" in a_redu.eqvt(1))
apply(rotate_tac 1)
apply(drule_tac x="(rev pi1)∙M'" in meta_spec)
apply(perm_simp)
apply(induct rule: SNa.induct)
apply(rule SNaI)
apply(drule_tac pi="(rev pi2)" in a_redu.eqvt(2))
apply(rotate_tac 1)
apply(drule_tac x="(rev pi2)∙M'" in meta_spec)
apply(perm_simp)
done

text ‹set operators›

definition AXIOMSn :: "ty ⇒ ntrm set" where
  "AXIOMSn B ≡ { (x):(Ax y b) | x y b. True }"

definition AXIOMSc::"ty ⇒ ctrm set" where
  "AXIOMSc B ≡ { <a>:(Ax y b) | a y b. True }"

definition BINDINGn::"ty ⇒ ctrm set ⇒ ntrm set" where
  "BINDINGn B X ≡ { (x):M | x M. ∀a P. <a>:P∈X ⟶ SNa (M{x:=<a>.P})}"

definition BINDINGc::"ty ⇒ ntrm set ⇒ ctrm set" where
  "BINDINGc B X ≡ { <a>:M | a M. ∀x P. (x):P∈X ⟶ SNa (M{a:=(x).P})}"

lemma BINDINGn_decreasing:
  shows "X⊆Y ⟹ BINDINGn B Y ⊆ BINDINGn B X"
by (simp add: BINDINGn_def) (blast) 

lemma BINDINGc_decreasing:
  shows "X⊆Y ⟹ BINDINGc B Y ⊆ BINDINGc B X"
by (simp add: BINDINGc_def) (blast) 
  
nominal_primrec
  NOTRIGHT :: "ty ⇒ ntrm set ⇒ ctrm set"
where
 "NOTRIGHT (NOT B) X = { <a>:NotR (x).M a | a x M. fic (NotR (x).M a) a ∧ (x):M ∈ X }"
apply(rule TrueI)+
done

lemma NOTRIGHT_eqvt_name:
  fixes pi::"name prm"
  shows "(pi∙(NOTRIGHT (NOT B) X)) = NOTRIGHT (NOT B) (pi∙X)"
apply(auto simp add: perm_set_def)
apply(rule_tac x="pi∙a" in exI) 
apply(rule_tac x="pi∙xb" in exI) 
apply(rule_tac x="pi∙M" in exI)
apply(simp)
apply(rule conjI)
apply(drule_tac pi="pi" in fic.eqvt(1))
apply(simp)
apply(rule_tac x="(xb):M" in exI)
apply(simp)
apply(rule_tac x="(rev pi)∙(<a>:NotR (xa).M a)" in exI)
apply(perm_simp)
apply(rule_tac x="(rev pi)∙a" in exI) 
apply(rule_tac x="(rev pi)∙xa" in exI) 
apply(rule_tac x="(rev pi)∙M" in exI)
apply(simp add: swap_simps)
apply(drule_tac pi="rev pi" in fic.eqvt(1))
apply(simp)
apply(drule sym)
apply(drule pt_bij1[OF pt_name_inst, OF at_name_inst])
apply(simp add: swap_simps)
done

lemma NOTRIGHT_eqvt_coname:
  fixes pi::"coname prm"
  shows "(pi∙(NOTRIGHT (NOT B) X)) = NOTRIGHT (NOT B) (pi∙X)"
apply(auto simp add: perm_set_def)
apply(rule_tac x="pi∙a" in exI) 
apply(rule_tac x="pi∙xb" in exI) 
apply(rule_tac x="pi∙M" in exI)
apply(simp)
apply(rule conjI)
apply(drule_tac pi="pi" in fic.eqvt(2))
apply(simp)
apply(rule_tac x="(xb):M" in exI)
apply(simp)
apply(rule_tac x="<((rev pi)∙a)>:NotR ((rev pi)∙xa).((rev pi)∙M) ((rev pi)∙a)" in exI)
apply(perm_simp)
apply(rule_tac x="(rev pi)∙a" in exI) 
apply(rule_tac x="(rev pi)∙xa" in exI) 
apply(rule_tac x="(rev pi)∙M" in exI)
apply(simp add: swap_simps)
apply(drule_tac pi="rev pi" in fic.eqvt(2))
apply(simp)
apply(drule sym)
apply(drule pt_bij1[OF pt_coname_inst, OF at_coname_inst])
apply(simp add: swap_simps)
done
  
nominal_primrec
  NOTLEFT :: "ty ⇒ ctrm set ⇒ ntrm set"
where
 "NOTLEFT (NOT B) X = { (x):NotL <a>.M x | a x M. fin (NotL <a>.M x) x ∧ <a>:M ∈ X }"
apply(rule TrueI)+
done

lemma NOTLEFT_eqvt_name:
  fixes pi::"name prm"
  shows "(pi∙(NOTLEFT (NOT B) X)) = NOTLEFT (NOT B) (pi∙X)"
apply(auto simp add: perm_set_def)
apply(rule_tac x="pi∙a" in exI) 
apply(rule_tac x="pi∙xb" in exI) 
apply(rule_tac x="pi∙M" in exI)
apply(simp)
apply(rule conjI)
apply(drule_tac pi="pi" in fin.eqvt(1))
apply(simp)
apply(rule_tac x="<a>:M" in exI)
apply(simp)
apply(rule_tac x="(((rev pi)∙xa)):NotL <((rev pi)∙a)>.((rev pi)∙M) ((rev pi)∙xa)" in exI)
apply(perm_simp)
apply(rule_tac x="(rev pi)∙a" in exI) 
apply(rule_tac x="(rev pi)∙xa" in exI) 
apply(rule_tac x="(rev pi)∙M" in exI)
apply(simp add: swap_simps)
apply(drule_tac pi="rev pi" in fin.eqvt(1))
apply(simp)
apply(drule sym)
apply(drule pt_bij1[OF pt_name_inst, OF at_name_inst])
apply(simp add: swap_simps)
done

lemma NOTLEFT_eqvt_coname:
  fixes pi::"coname prm"
  shows "(pi∙(NOTLEFT (NOT B) X)) = NOTLEFT (NOT B) (pi∙X)"
apply(auto simp add: perm_set_def)
apply(rule_tac x="pi∙a" in exI) 
apply(rule_tac x="pi∙xb" in exI) 
apply(rule_tac x="pi∙M" in exI)
apply(simp)
apply(rule conjI)
apply(drule_tac pi="pi" in fin.eqvt(2))
apply(simp)
apply(rule_tac x="<a>:M" in exI)
apply(simp)
apply(rule_tac x="(((rev pi)∙xa)):NotL <((rev pi)∙a)>.((rev pi)∙M) ((rev pi)∙xa)" in exI)
apply(perm_simp)
apply(rule_tac x="(rev pi)∙a" in exI) 
apply(rule_tac x="(rev pi)∙xa" in exI) 
apply(rule_tac x="(rev pi)∙M" in exI)
apply(simp add: swap_simps)
apply(drule_tac pi="rev pi" in fin.eqvt(2))
apply(simp)
apply(drule sym)
apply(drule pt_bij1[OF pt_coname_inst, OF at_coname_inst])
apply(simp add: swap_simps)
done
  
nominal_primrec
  ANDRIGHT :: "ty ⇒ ctrm set ⇒ ctrm set ⇒ ctrm set"
where
 "ANDRIGHT (B AND C) X Y = 
            { <c>:AndR <a>.M <b>.N c | c a b M N. fic (AndR <a>.M <b>.N c) c ∧ <a>:M ∈ X ∧ <b>:N ∈ Y }"
apply(rule TrueI)+
done

lemma ANDRIGHT_eqvt_name:
  fixes pi::"name prm"
  shows "(pi∙(ANDRIGHT (A AND B) X Y)) = ANDRIGHT (A AND B) (pi∙X) (pi∙Y)"
apply(auto simp add: perm_set_def)
apply(rule_tac x="pi∙c" in exI)
apply(rule_tac x="pi∙a" in exI)
apply(rule_tac x="pi∙b" in exI)
apply(rule_tac x="pi∙M" in exI)
apply(rule_tac x="pi∙N" in exI)
apply(simp)
apply(rule conjI)
apply(drule_tac pi="pi" in fic.eqvt(1))
apply(simp)
apply(rule conjI)
apply(rule_tac x="<a>:M" in exI)
apply(simp)
apply(rule_tac x="<b>:N" in exI)
apply(simp)
apply(rule_tac x="(rev pi)∙(<c>:AndR <a>.M <b>.N c)" in exI)
apply(perm_simp)
apply(rule_tac x="(rev pi)∙c" in exI)
apply(rule_tac x="(rev pi)∙a" in exI)
apply(rule_tac x="(rev pi)∙b" in exI)
apply(rule_tac x="(rev pi)∙M" in exI)
apply(rule_tac x="(rev pi)∙N" in exI)
apply(simp add: swap_simps)
apply(drule_tac pi="rev pi" in fic.eqvt(1))
apply(simp)
apply(drule sym)
apply(drule sym)
apply(drule pt_bij1[OF pt_name_inst, OF at_name_inst])
apply(drule pt_bij1[OF pt_name_inst, OF at_name_inst])
apply(simp add: swap_simps)
done

lemma ANDRIGHT_eqvt_coname:
  fixes pi::"coname prm"
  shows "(pi∙(ANDRIGHT (A AND B) X Y)) = ANDRIGHT (A AND B) (pi∙X) (pi∙Y)"
apply(auto simp add: perm_set_def)
apply(rule_tac x="pi∙c" in exI)
apply(rule_tac x="pi∙a" in exI)
apply(rule_tac x="pi∙b" in exI)
apply(rule_tac x="pi∙M" in exI)
apply(rule_tac x="pi∙N" in exI)
apply(simp)
apply(rule conjI)
apply(drule_tac pi="pi" in fic.eqvt(2))
apply(simp)
apply(rule conjI)
apply(rule_tac x="<a>:M" in exI)
apply(simp)
apply(rule_tac x="<b>:N" in exI)
apply(simp)
apply(rule_tac x="(rev pi)∙(<c>:AndR <a>.M <b>.N c)" in exI)
apply(perm_simp)
apply(rule_tac x="(rev pi)∙c" in exI)
apply(rule_tac x="(rev pi)∙a" in exI)
apply(rule_tac x="(rev pi)∙b" in exI)
apply(rule_tac x="(rev pi)∙M" in exI)
apply(rule_tac x="(rev pi)∙N" in exI)
apply(simp)
apply(drule_tac pi="rev pi" in fic.eqvt(2))
apply(simp)
apply(drule sym)
apply(drule sym)
apply(drule pt_bij1[OF pt_coname_inst, OF at_coname_inst])
apply(drule pt_bij1[OF pt_coname_inst, OF at_coname_inst])
apply(simp)
done

nominal_primrec
  ANDLEFT1 :: "ty ⇒ ntrm set ⇒ ntrm set"
where
 "ANDLEFT1 (B AND C) X = { (y):AndL1 (x).M y | x y M. fin (AndL1 (x).M y) y ∧ (x):M ∈ X }"
apply(rule TrueI)+
done

lemma ANDLEFT1_eqvt_name:
  fixes pi::"name prm"
  shows "(pi∙(ANDLEFT1 (A AND B) X)) = ANDLEFT1 (A AND B) (pi∙X)"
apply(auto simp add: perm_set_def)
apply(rule_tac x="pi∙xb" in exI) 
apply(rule_tac x="pi∙y" in exI) 
apply(rule_tac x="pi∙M" in exI)
apply(simp)
apply(rule conjI)
apply(drule_tac pi="pi" in fin.eqvt(1))
apply(simp)
apply(rule_tac x="(xb):M" in exI)
apply(simp)
apply(rule_tac x="(rev pi)∙((y):AndL1 (xa).M y)" in exI)
apply(perm_simp)
apply(rule_tac x="(rev pi)∙xa" in exI) 
apply(rule_tac x="(rev pi)∙y" in exI) 
apply(rule_tac x="(rev pi)∙M" in exI)
apply(simp)
apply(drule_tac pi="rev pi" in fin.eqvt(1))
apply(simp)
apply(drule sym)
apply(drule pt_bij1[OF pt_name_inst, OF at_name_inst])
apply(simp)
done

lemma ANDLEFT1_eqvt_coname:
  fixes pi::"coname prm"
  shows "(pi∙(ANDLEFT1 (A AND B) X)) = ANDLEFT1 (A AND B) (pi∙X)"
apply(auto simp add: perm_set_def)
apply(rule_tac x="pi∙xb" in exI) 
apply(rule_tac x="pi∙y" in exI) 
apply(rule_tac x="pi∙M" in exI)
apply(simp)
apply(rule conjI)
apply(drule_tac pi="pi" in fin.eqvt(2))
apply(simp)
apply(rule_tac x="(xb):M" in exI)
apply(simp)
apply(rule_tac x="(rev pi)∙((y):AndL1 (xa).M y)" in exI)
apply(perm_simp)
apply(rule_tac x="(rev pi)∙xa" in exI) 
apply(rule_tac x="(rev pi)∙y" in exI) 
apply(rule_tac x="(rev pi)∙M" in exI)
apply(simp add: swap_simps)
apply(drule_tac pi="rev pi" in fin.eqvt(2))
apply(simp)
apply(drule sym)
apply(drule pt_bij1[OF pt_coname_inst, OF at_coname_inst])
apply(simp add: swap_simps)
done

nominal_primrec
  ANDLEFT2 :: "ty ⇒ ntrm set ⇒ ntrm set"
where
 "ANDLEFT2 (B AND C) X = { (y):AndL2 (x).M y | x y M. fin (AndL2 (x).M y) y ∧ (x):M ∈ X }"
apply(rule TrueI)+
done

lemma ANDLEFT2_eqvt_name:
  fixes pi::"name prm"
  shows "(pi∙(ANDLEFT2 (A AND B) X)) = ANDLEFT2 (A AND B) (pi∙X)"
apply(auto simp add: perm_set_def)
apply(rule_tac x="pi∙xb" in exI) 
apply(rule_tac x="pi∙y" in exI) 
apply(rule_tac x="pi∙M" in exI)
apply(simp)
apply(rule conjI)
apply(drule_tac pi="pi" in fin.eqvt(1))
apply(simp)
apply(rule_tac x="(xb):M" in exI)
apply(simp)
apply(rule_tac x="(rev pi)∙((y):AndL2 (xa).M y)" in exI)
apply(perm_simp)
apply(rule_tac x="(rev pi)∙xa" in exI) 
apply(rule_tac x="(rev pi)∙y" in exI) 
apply(rule_tac x="(rev pi)∙M" in exI)
apply(simp)
apply(drule_tac pi="rev pi" in fin.eqvt(1))
apply(simp)
apply(drule sym)
apply(drule pt_bij1[OF pt_name_inst, OF at_name_inst])
apply(simp)
done

lemma ANDLEFT2_eqvt_coname:
  fixes pi::"coname prm"
  shows "(pi∙(ANDLEFT2 (A AND B) X)) = ANDLEFT2 (A AND B) (pi∙X)"
apply(auto simp add: perm_set_def)
apply(rule_tac x="pi∙xb" in exI) 
apply(rule_tac x="pi∙y" in exI) 
apply(rule_tac x="pi∙M" in exI)
apply(simp)
apply(rule conjI)
apply(drule_tac pi="pi" in fin.eqvt(2))
apply(simp)
apply(rule_tac x="(xb):M" in exI)
apply(simp)
apply(rule_tac x="(rev pi)∙((y):AndL2 (xa).M y)" in exI)
apply(perm_simp)
apply(rule_tac x="(rev pi)∙xa" in exI) 
apply(rule_tac x="(rev pi)∙y" in exI) 
apply(rule_tac x="(rev pi)∙M" in exI)
apply(simp add: swap_simps)
apply(drule_tac pi="rev pi" in fin.eqvt(2))
apply(simp)
apply(drule sym)
apply(drule pt_bij1[OF pt_coname_inst, OF at_coname_inst])
apply(simp add: swap_simps)
done

nominal_primrec
  ORLEFT :: "ty ⇒ ntrm set ⇒ ntrm set ⇒ ntrm set"
where
 "ORLEFT (B OR C) X Y = 
            { (z):OrL (x).M (y).N z | x y z M N. fin (OrL (x).M (y).N z) z ∧ (x):M ∈ X ∧ (y):N ∈ Y }"
apply(rule TrueI)+
done

lemma ORLEFT_eqvt_name:
  fixes pi::"name prm"
  shows "(pi∙(ORLEFT (A OR B) X Y)) = ORLEFT (A OR B) (pi∙X) (pi∙Y)"
apply(auto simp add: perm_set_def)
apply(rule_tac x="pi∙xb" in exI)
apply(rule_tac x="pi∙y" in exI)
apply(rule_tac x="pi∙z" in exI)
apply(rule_tac x="pi∙M" in exI)
apply(rule_tac x="pi∙N" in exI)
apply(simp)
apply(rule conjI)
apply(drule_tac pi="pi" in fin.eqvt(1))
apply(simp)
apply(rule conjI)
apply(rule_tac x="(xb):M" in exI)
apply(simp)
apply(rule_tac x="(y):N" in exI)
apply(simp)
apply(rule_tac x="(rev pi)∙((z):OrL (xa).M (y).N z)" in exI)
apply(perm_simp)
apply(rule_tac x="(rev pi)∙xa" in exI)
apply(rule_tac x="(rev pi)∙y" in exI)
apply(rule_tac x="(rev pi)∙z" in exI)
apply(rule_tac x="(rev pi)∙M" in exI)
apply(rule_tac x="(rev pi)∙N" in exI)
apply(simp)
apply(drule_tac pi="rev pi" in fin.eqvt(1))
apply(simp)
apply(drule sym)
apply(drule sym)
apply(drule pt_bij1[OF pt_name_inst, OF at_name_inst])
apply(drule pt_bij1[OF pt_name_inst, OF at_name_inst])
apply(simp)
done

lemma ORLEFT_eqvt_coname:
  fixes pi::"coname prm"
  shows "(pi∙(ORLEFT (A OR B) X Y)) = ORLEFT (A OR B) (pi∙X) (pi∙Y)"
apply(auto simp add: perm_set_def)
apply(rule_tac x="pi∙xb" in exI)
apply(rule_tac x="pi∙y" in exI)
apply(rule_tac x="pi∙z" in exI)
apply(rule_tac x="pi∙M" in exI)
apply(rule_tac x="pi∙N" in exI)
apply(simp)
apply(rule conjI)
apply(drule_tac pi="pi" in fin.eqvt(2))
apply(simp)
apply(rule conjI)
apply(rule_tac x="(xb):M" in exI)
apply(simp)
apply(rule_tac x="(y):N" in exI)
apply(simp)
apply(rule_tac x="(rev pi)∙((z):OrL (xa).M (y).N z)" in exI)
apply(perm_simp)
apply(rule_tac x="(rev pi)∙xa" in exI)
apply(rule_tac x="(rev pi)∙y" in exI)
apply(rule_tac x="(rev pi)∙z" in exI)
apply(rule_tac x="(rev pi)∙M" in exI)
apply(rule_tac x="(rev pi)∙N" in exI)
apply(simp add: swap_simps)
apply(drule_tac pi="rev pi" in fin.eqvt(2))
apply(simp)
apply(drule sym)
apply(drule sym)
apply(drule pt_bij1[OF pt_coname_inst, OF at_coname_inst])
apply(drule pt_bij1[OF pt_coname_inst, OF at_coname_inst])
apply(simp add: swap_simps)
done

nominal_primrec
  ORRIGHT1 :: "ty ⇒ ctrm set ⇒ ctrm set"
where
 "ORRIGHT1 (B OR C) X = { <b>:OrR1 <a>.M b | a b M. fic (OrR1 <a>.M b) b ∧ <a>:M ∈ X }"
apply(rule TrueI)+
done

lemma ORRIGHT1_eqvt_name:
  fixes pi::"name prm"
  shows "(pi∙(ORRIGHT1 (A OR B) X)) = ORRIGHT1 (A OR B) (pi∙X)"
apply(auto simp add: perm_set_def)
apply(rule_tac x="pi∙a" in exI) 
apply(rule_tac x="pi∙b" in exI) 
apply(rule_tac x="pi∙M" in exI)
apply(simp)
apply(rule conjI)
apply(drule_tac pi="pi" in fic.eqvt(1))
apply(simp)
apply(rule_tac x="<a>:M" in exI)
apply(perm_simp)
apply(rule_tac x="(rev pi)∙(<b>:OrR1 <a>.M b)" in exI)
apply(perm_simp)
apply(rule_tac x="(rev pi)∙a" in exI) 
apply(rule_tac x="(rev pi)∙b" in exI) 
apply(rule_tac x="(rev pi)∙M" in exI)
apply(simp add: swap_simps)
apply(drule_tac pi="rev pi" in fic.eqvt(1))
apply(simp)
apply(drule sym)
apply(drule pt_bij1[OF pt_name_inst, OF at_name_inst])
apply(simp add: swap_simps)
done

lemma ORRIGHT1_eqvt_coname:
  fixes pi::"coname prm"
  shows "(pi∙(ORRIGHT1 (A OR B) X)) = ORRIGHT1 (A OR B) (pi∙X)"
apply(auto simp add: perm_set_def)
apply(rule_tac x="pi∙a" in exI) 
apply(rule_tac x="pi∙b" in exI) 
apply(rule_tac x="pi∙M" in exI)
apply(simp)
apply(rule conjI)
apply(drule_tac pi="pi" in fic.eqvt(2))
apply(simp)
apply(rule_tac x="<a>:M" in exI)
apply(perm_simp)
apply(rule_tac x="(rev pi)∙(<b>:OrR1 <a>.M b)" in exI)
apply(perm_simp)
apply(rule_tac x="(rev pi)∙a" in exI) 
apply(rule_tac x="(rev pi)∙b" in exI) 
apply(rule_tac x="(rev pi)∙M" in exI)
apply(simp)
apply(drule_tac pi="rev pi" in fic.eqvt(2))
apply(simp)
apply(drule sym)
apply(drule pt_bij1[OF pt_coname_inst, OF at_coname_inst])
apply(simp)
done

nominal_primrec
  ORRIGHT2 :: "ty ⇒ ctrm set ⇒ ctrm set"
where
 "ORRIGHT2 (B OR C) X = { <b>:OrR2 <a>.M b | a b M. fic (OrR2 <a>.M b) b ∧ <a>:M ∈ X }"
apply(rule TrueI)+
done

lemma ORRIGHT2_eqvt_name:
  fixes pi::"name prm"
  shows "(pi∙(ORRIGHT2 (A OR B) X)) = ORRIGHT2 (A OR B) (pi∙X)"
apply(auto simp add: perm_set_def)
apply(rule_tac x="pi∙a" in exI) 
apply(rule_tac x="pi∙b" in exI) 
apply(rule_tac x="pi∙M" in exI)
apply(simp)
apply(rule conjI)
apply(drule_tac pi="pi" in fic.eqvt(1))
apply(simp)
apply(rule_tac x="<a>:M" in exI)
apply(perm_simp)
apply(rule_tac x="(rev pi)∙(<b>:OrR2 <a>.M b)" in exI)
apply(perm_simp)
apply(rule_tac x="(rev pi)∙a" in exI) 
apply(rule_tac x="(rev pi)∙b" in exI) 
apply(rule_tac x="(rev pi)∙M" in exI)
apply(simp add: swap_simps)
apply(drule_tac pi="rev pi" in fic.eqvt(1))
apply(simp)
apply(drule sym)
apply(drule pt_bij1[OF pt_name_inst, OF at_name_inst])
apply(simp add: swap_simps)
done

lemma ORRIGHT2_eqvt_coname:
  fixes pi::"coname prm"
  shows "(pi∙(ORRIGHT2 (A OR B) X)) = ORRIGHT2 (A OR B) (pi∙X)"
apply(auto simp add: perm_set_def)
apply(rule_tac x="pi∙a" in exI) 
apply(rule_tac x="pi∙b" in exI) 
apply(rule_tac x="pi∙M" in exI)
apply(simp)
apply(rule conjI)
apply(drule_tac pi="pi" in fic.eqvt(2))
apply(simp)
apply(rule_tac x="<a>:M" in exI)
apply(perm_simp)
apply(rule_tac x="(rev pi)∙(<b>:OrR2 <a>.M b)" in exI)
apply(perm_simp)
apply(rule_tac x="(rev pi)∙a" in exI) 
apply(rule_tac x="(rev pi)∙b" in exI) 
apply(rule_tac x="(rev pi)∙M" in exI)
apply(simp)
apply(drule_tac pi="rev pi" in fic.eqvt(2))
apply(simp)
apply(drule sym)
apply(drule pt_bij1[OF pt_coname_inst, OF at_coname_inst])
apply(simp)
done

nominal_primrec
  IMPRIGHT :: "ty ⇒ ntrm set ⇒ ctrm set ⇒ ntrm set ⇒ ctrm set ⇒ ctrm set"
where
 "IMPRIGHT (B IMP C) X Y Z U= 
        { <b>:ImpR (x).<a>.M b | x a b M. fic (ImpR (x).<a>.M b) b 
                                        ∧ (∀z P. x♯(z,P) ∧ (z):P ∈ Z ⟶ (x):(M{a:=(z).P}) ∈ X)
                                        ∧ (∀c Q. a♯(c,Q) ∧ <c>:Q ∈ U ⟶ <a>:(M{x:=<c>.Q}) ∈ Y)}"
apply(rule TrueI)+
done

lemma IMPRIGHT_eqvt_name:
  fixes pi::"name prm"
  shows "(pi∙(IMPRIGHT (A IMP B) X Y Z U)) = IMPRIGHT (A IMP B) (pi∙X) (pi∙Y) (pi∙Z) (pi∙U)"
apply(auto simp add: perm_set_def)
apply(rule_tac x="pi∙xb" in exI)
apply(rule_tac x="pi∙a" in exI)
apply(rule_tac x="pi∙b" in exI)
apply(rule_tac x="pi∙M" in exI)
apply(simp)
apply(rule conjI)
apply(drule_tac pi="pi" in fic.eqvt(1))
apply(simp)
apply(rule conjI)
apply(auto)[1]
apply(rule_tac x="(xb):(M{a:=((rev pi)∙z).((rev pi)∙P)})" in exI)
apply(perm_simp add: csubst_eqvt)
apply(drule sym)
apply(drule pt_bij1[OF pt_name_inst, OF at_name_inst])
apply(simp)
apply(simp add: fresh_right)
apply(auto)[1]
apply(rule_tac x="<a>:(M{xb:=<((rev pi)∙c)>.((rev pi)∙Q)})" in exI)
apply(perm_simp add: nsubst_eqvt)
apply(drule sym)
apply(drule pt_bij1[OF pt_name_inst, OF at_name_inst])
apply(simp add: swap_simps fresh_left)
apply(rule_tac x="(rev pi)∙(<b>:ImpR xa.<a>.M b)" in exI)
apply(perm_simp)
apply(rule_tac x="(rev pi)∙xa" in exI)
apply(rule_tac x="(rev pi)∙a" in exI)
apply(rule_tac x="(rev pi)∙b" in exI)
apply(rule_tac x="(rev pi)∙M" in exI)
apply(simp add: swap_simps)
apply(drule_tac pi="rev pi" in fic.eqvt(1))
apply(simp add: swap_simps)
apply(rule conjI)
apply(auto)[1]
apply(drule_tac x="pi∙z" in spec)
apply(drule_tac x="pi∙P" in spec)
apply(drule mp)
apply(simp add: fresh_right)
apply(rule_tac x="(z):P" in exI)
apply(simp)
apply(auto)[1]
apply(drule sym)
apply(drule pt_bij1[OF pt_name_inst, OF at_name_inst])
apply(perm_simp add: csubst_eqvt fresh_right)
apply(auto)[1]
apply(drule_tac x="pi∙c" in spec)
apply(drule_tac x="pi∙Q" in spec)
apply(drule mp)
apply(simp add: swap_simps fresh_left)
apply(rule_tac x="<c>:Q" in exI)
apply(simp add: swap_simps)
apply(auto)[1]
apply(drule sym)
apply(drule pt_bij1[OF pt_name_inst, OF at_name_inst])
apply(perm_simp add: nsubst_eqvt)
done

lemma IMPRIGHT_eqvt_coname:
  fixes pi::"coname prm"
  shows "(pi∙(IMPRIGHT (A IMP B) X Y Z U)) = IMPRIGHT (A IMP B) (pi∙X) (pi∙Y) (pi∙Z) (pi∙U)"
apply(auto simp add: perm_set_def)
apply(rule_tac x="pi∙xb" in exI)
apply(rule_tac x="pi∙a" in exI)
apply(rule_tac x="pi∙b" in exI)
apply(rule_tac x="pi∙M" in exI)
apply(simp)
apply(rule conjI)
apply(drule_tac pi="pi" in fic.eqvt(2))
apply(simp)
apply(rule conjI)
apply(auto)[1]
apply(rule_tac x="(xb):(M{a:=((rev pi)∙z).((rev pi)∙P)})" in exI)
apply(perm_simp add: csubst_eqvt)
apply(drule sym)
apply(drule pt_bij1[OF pt_coname_inst, OF at_coname_inst])
apply(simp add: swap_simps fresh_left)
apply(auto)[1]
apply(rule_tac x="<a>:(M{xb:=<((rev pi)∙c)>.((rev pi)∙Q)})" in exI)
apply(perm_simp add: nsubst_eqvt)
apply(drule sym)
apply(drule pt_bij1[OF pt_coname_inst, OF at_coname_inst])
apply(simp add: fresh_right)
apply(rule_tac x="(rev pi)∙(<b>:ImpR xa.<a>.M b)" in exI)
apply(perm_simp)
apply(rule_tac x="(rev pi)∙xa" in exI)
apply(rule_tac x="(rev pi)∙a" in exI)
apply(rule_tac x="(rev pi)∙b" in exI)
apply(rule_tac x="(rev pi)∙M" in exI)
apply(simp add: swap_simps)
apply(drule_tac pi="rev pi" in fic.eqvt(2))
apply(simp add: swap_simps)
apply(rule conjI)
apply(auto)[1]
apply(drule_tac x="pi∙z" in spec)
apply(drule_tac x="pi∙P" in spec)
apply(simp add: swap_simps fresh_left)
apply(drule mp)
apply(rule_tac x="(z):P" in exI)
apply(simp add: swap_simps)
apply(auto)[1]
apply(drule sym)
apply(drule pt_bij1[OF pt_coname_inst, OF at_coname_inst])
apply(perm_simp add: csubst_eqvt fresh_right)
apply(auto)[1]
apply(drule_tac x="pi∙c" in spec)
apply(drule_tac x="pi∙Q" in spec)
apply(simp add: fresh_right)
apply(drule mp)
apply(rule_tac x="<c>:Q" in exI)
apply(simp)
apply(auto)[1]
apply(drule sym)
apply(drule pt_bij1[OF pt_coname_inst, OF at_coname_inst])
apply(perm_simp add: nsubst_eqvt fresh_right)
done

nominal_primrec
  IMPLEFT :: "ty ⇒ ctrm set ⇒ ntrm set ⇒ ntrm set"
where
 "IMPLEFT (B IMP C) X Y = 
        { (y):ImpL <a>.M (x).N y | x a y M N. fin (ImpL <a>.M (x).N y) y ∧ <a>:M ∈ X ∧ (x):N ∈ Y }"
apply(rule TrueI)+
done

lemma IMPLEFT_eqvt_name:
  fixes pi::"name prm"
  shows "(pi∙(IMPLEFT (A IMP B) X Y)) = IMPLEFT (A IMP B) (pi∙X) (pi∙Y)"
apply(auto simp add: perm_set_def)
apply(rule_tac x="pi∙xb" in exI) 
apply(rule_tac x="pi∙a" in exI)
apply(rule_tac x="pi∙y" in exI) 
apply(rule_tac x="pi∙M" in exI) 
apply(rule_tac x="pi∙N" in exI)
apply(simp)
apply(rule conjI)
apply(drule_tac pi="pi" in fin.eqvt(1))
apply(simp)
apply(rule conjI)
apply(rule_tac x="<a>:M" in exI)
apply(simp)
apply(rule_tac x="(xb):N" in exI)
apply(simp)
apply(rule_tac x="(rev pi)∙((y):ImpL <a>.M (xa).N y)" in exI)
apply(perm_simp)
apply(rule_tac x="(rev pi)∙xa" in exI) 
apply(rule_tac x="(rev pi)∙a" in exI) 
apply(rule_tac x="(rev pi)∙y" in exI) 
apply(rule_tac x="(rev pi)∙M" in exI)
apply(rule_tac x="(rev pi)∙N" in exI)
apply(simp add: swap_simps)
apply(drule_tac pi="rev pi" in fin.eqvt(1))
apply(simp)
apply(drule sym)
apply(drule sym)
apply(drule pt_bij1[OF pt_name_inst, OF at_name_inst])
apply(drule pt_bij1[OF pt_name_inst, OF at_name_inst])
apply(simp add: swap_simps)
done

lemma IMPLEFT_eqvt_coname:
  fixes pi::"coname prm"
  shows "(pi∙(IMPLEFT (A IMP B) X Y)) = IMPLEFT (A IMP B) (pi∙X) (pi∙Y)"
apply(auto simp add: perm_set_def)
apply(rule_tac x="pi∙xb" in exI) 
apply(rule_tac x="pi∙a" in exI)
apply(rule_tac x="pi∙y" in exI) 
apply(rule_tac x="pi∙M" in exI) 
apply(rule_tac x="pi∙N" in exI)
apply(simp)
apply(rule conjI)
apply(drule_tac pi="pi" in fin.eqvt(2))
apply(simp)
apply(rule conjI)
apply(rule_tac x="<a>:M" in exI)
apply(simp)
apply(rule_tac x="(xb):N" in exI)
apply(simp)
apply(rule_tac x="(rev pi)∙((y):ImpL <a>.M (xa).N y)" in exI)
apply(perm_simp)
apply(rule_tac x="(rev pi)∙xa" in exI) 
apply(rule_tac x="(rev pi)∙a" in exI) 
apply(rule_tac x="(rev pi)∙y" in exI) 
apply(rule_tac x="(rev pi)∙M" in exI)
apply(rule_tac x="(rev pi)∙N" in exI)
apply(simp add: swap_simps)
apply(drule_tac pi="rev pi" in fin.eqvt(2))
apply(simp)
apply(drule sym)
apply(drule sym)
apply(drule pt_bij1[OF pt_coname_inst, OF at_coname_inst])
apply(drule pt_bij1[OF pt_coname_inst, OF at_coname_inst])
apply(simp add: swap_simps)
done

lemma sum_cases:
 shows "(∃y. x=Inl y) ∨ (∃y. x=Inr y)"
apply(rule_tac s="x" in sumE)
apply(auto)
done

function
  NEGc::"ty ⇒ ntrm set ⇒ ctrm set"
and
  NEGn::"ty ⇒ ctrm set ⇒ ntrm set"
where
  "NEGc (PR A)    X = AXIOMSc (PR A) ∪ BINDINGc (PR A) X"  
| "NEGc (NOT C)   X = AXIOMSc (NOT C) ∪ BINDINGc (NOT C) X 
                         ∪ NOTRIGHT (NOT C) (lfp (NEGn C ∘ NEGc C))"  
| "NEGc (C AND D) X = AXIOMSc (C AND D) ∪ BINDINGc (C AND D) X 
                     ∪ ANDRIGHT (C AND D) (NEGc C (lfp (NEGn C ∘ NEGc C))) (NEGc D (lfp (NEGn D ∘ NEGc D)))"
| "NEGc (C OR D)  X = AXIOMSc (C OR D) ∪ BINDINGc (C OR D) X  
                         ∪ ORRIGHT1 (C OR D) (NEGc C (lfp (NEGn C ∘ NEGc C))) 
                         ∪ ORRIGHT2 (C OR D) (NEGc D (lfp (NEGn D ∘ NEGc D)))"
| "NEGc (C IMP D) X = AXIOMSc (C IMP D) ∪ BINDINGc (C IMP D) X 
    ∪ IMPRIGHT (C IMP D) (lfp (NEGn C ∘ NEGc C)) (NEGc D (lfp (NEGn D ∘ NEGc D))) 
                          (lfp (NEGn D ∘ NEGc D)) (NEGc C (lfp (NEGn C ∘ NEGc C)))"
| "NEGn (PR A)    X = AXIOMSn (PR A) ∪ BINDINGn (PR A) X"   
| "NEGn (NOT C)   X = AXIOMSn (NOT C) ∪ BINDINGn (NOT C) X 
                         ∪ NOTLEFT (NOT C) (NEGc C (lfp (NEGn C ∘ NEGc C)))"  
| "NEGn (C AND D) X = AXIOMSn (C AND D) ∪ BINDINGn (C AND D) X 
                         ∪ ANDLEFT1 (C AND D) (lfp (NEGn C ∘ NEGc C)) 
                         ∪ ANDLEFT2 (C AND D) (lfp (NEGn D ∘ NEGc D))"
| "NEGn (C OR D)  X = AXIOMSn (C OR D) ∪ BINDINGn (C OR D) X 
                         ∪ ORLEFT (C OR D) (lfp (NEGn C ∘ NEGc C)) (lfp (NEGn D ∘ NEGc D))"
| "NEGn (C IMP D) X = AXIOMSn (C IMP D) ∪ BINDINGn (C IMP D) X 
                         ∪ IMPLEFT (C IMP D) (NEGc C (lfp (NEGn C ∘ NEGc C))) (lfp (NEGn D ∘ NEGc D))"
using ty_cases sum_cases 
apply(auto simp add: ty.inject)
apply(drule_tac x="x" in meta_spec)
apply(fastforce simp add: ty.inject)
done

termination
apply(relation "measure (case_sum (size∘fst) (size∘fst))")
apply(simp_all)
done

text ‹Candidates›

lemma test1:
  shows "x∈(X∪Y) = (x∈X ∨ x∈Y)"
by blast

lemma test2:
  shows "x∈(X∩Y) = (x∈X ∧ x∈Y)"
by blast

lemma big_inter_eqvt:
  fixes pi1::"name prm"
  and   X::"('a::pt_name) set set"
  and   pi2::"coname prm"
  and   Y::"('b::pt_coname) set set"
  shows "(pi1∙(⋂X)) = ⋂(pi1∙X)"
  and   "(pi2∙(⋂Y)) = ⋂(pi2∙Y)"
apply(auto simp add: perm_set_def)
apply(rule_tac x="(rev pi1)∙x" in exI)
apply(perm_simp)
apply(rule ballI)
apply(drule_tac x="pi1∙xa" in spec)
apply(auto)
apply(drule_tac x="xa" in spec)
apply(auto)[1]
apply(rule_tac x="(rev pi1)∙xb" in exI)
apply(perm_simp)
apply(simp add: pt_set_bij1[OF pt_name_inst, OF at_name_inst])
apply(simp add: pt_set_bij[OF pt_name_inst, OF at_name_inst])
apply(simp add: pt_set_bij1[OF pt_name_inst, OF at_name_inst])
apply(rule_tac x="(rev pi2)∙x" in exI)
apply(perm_simp)
apply(rule ballI)
apply(drule_tac x="pi2∙xa" in spec)
apply(auto)
apply(drule_tac x="xa" in spec)
apply(auto)[1]
apply(rule_tac x="(rev pi2)∙xb" in exI)
apply(perm_simp)
apply(simp add: pt_set_bij1[OF pt_coname_inst, OF at_coname_inst])
apply(simp add: pt_set_bij[OF pt_coname_inst, OF at_coname_inst])
apply(simp add: pt_set_bij1[OF pt_coname_inst, OF at_coname_inst])
done

lemma lfp_eqvt:
  fixes pi1::"name prm"
  and   f::"'a set ⇒ ('a::pt_name) set"
  and   pi2::"coname prm"
  and   g::"'b set ⇒ ('b::pt_coname) set"
  shows "pi1∙(lfp f) = lfp (pi1∙f)"
  and   "pi2∙(lfp g) = lfp (pi2∙g)"
apply(simp add: lfp_def)
apply(simp add: big_inter_eqvt)
apply(simp add: pt_Collect_eqvt[OF pt_name_inst, OF at_name_inst])
apply(subgoal_tac "{u. (pi1∙f) u ⊆ u} = {u. ((rev pi1)∙((pi1∙f) u)) ⊆ ((rev pi1)∙u)}")
apply(perm_simp)
apply(rule Collect_cong)
apply(rule iffI)
apply(rule subseteq_eqvt(1)[THEN iffD1])
apply(simp add: perm_bool)
apply(drule subseteq_eqvt(1)[THEN iffD2])
apply(simp add: perm_bool)
apply(simp add: lfp_def)
apply(simp add: big_inter_eqvt)
apply(simp add: pt_Collect_eqvt[OF pt_coname_inst, OF at_coname_inst])
apply(subgoal_tac "{u. (pi2∙g) u ⊆ u} = {u. ((rev pi2)∙((pi2∙g) u)) ⊆ ((rev pi2)∙u)}")
apply(perm_simp)
apply(rule Collect_cong)
apply(rule iffI)
apply(rule subseteq_eqvt(2)[THEN iffD1])
apply(simp add: perm_bool)
apply(drule subseteq_eqvt(2)[THEN iffD2])
apply(simp add: perm_bool)
done

abbreviation
  CANDn::"ty ⇒ ntrm set"  ("∥'(_')∥" [60] 60) 
where
  "∥(B)∥ ≡ lfp (NEGn B ∘ NEGc B)" 

abbreviation
  CANDc::"ty ⇒ ctrm set"  ("∥<_>∥" [60] 60)
where
  "∥<B>∥ ≡ NEGc B (∥(B)∥)"

lemma NEGn_decreasing:
  shows "X⊆Y ⟹ NEGn B Y ⊆ NEGn B X"
by (nominal_induct B rule: ty.strong_induct)
   (auto dest: BINDINGn_decreasing)

lemma NEGc_decreasing:
  shows "X⊆Y ⟹ NEGc B Y ⊆ NEGc B X"
by (nominal_induct B rule: ty.strong_induct)
   (auto dest: BINDINGc_decreasing)

lemma mono_NEGn_NEGc:
  shows "mono (NEGn B ∘ NEGc B)"
  and   "mono (NEGc B ∘ NEGn B)"
proof -
  have "∀X Y. X⊆Y ⟶ NEGn B (NEGc B X) ⊆ NEGn B (NEGc B Y)"
  proof (intro strip)
    fix X::"ntrm set" and Y::"ntrm set"
    assume "X⊆Y"
    then have "NEGc B Y ⊆ NEGc B X" by (simp add: NEGc_decreasing)
    then show "NEGn B (NEGc B X) ⊆ NEGn B (NEGc B Y)" by (simp add: NEGn_decreasing)
  qed
  then show "mono (NEGn B ∘ NEGc B)" by (simp add: mono_def)
next
  have "∀X Y. X⊆Y ⟶ NEGc B (NEGn B X) ⊆ NEGc B (NEGn B Y)"
  proof (intro strip)
    fix X::"ctrm set" and Y::"ctrm set"
    assume "X⊆Y"
    then have "NEGn B Y ⊆ NEGn B X" by (simp add: NEGn_decreasing)
    then show "NEGc B (NEGn B X) ⊆ NEGc B (NEGn B Y)" by (simp add: NEGc_decreasing)
  qed
  then show "mono (NEGc B ∘ NEGn B)" by (simp add: mono_def)
qed

lemma NEG_simp:
  shows "∥<B>∥ = NEGc B (∥(B)∥)"
  and   "∥(B)∥ = NEGn B (∥<B>∥)"
proof -
  show "∥<B>∥ = NEGc B (∥(B)∥)" by simp
next
  have "∥(B)∥ ≡ lfp (NEGn B ∘ NEGc B)" by simp
  then have "∥(B)∥ = (NEGn B ∘ NEGc B) (∥(B)∥)" using mono_NEGn_NEGc def_lfp_unfold by blast
  then show "∥(B)∥ = NEGn B (∥<B>∥)" by simp
qed

lemma NEG_elim:
  shows "M ∈ ∥<B>∥ ⟹ M ∈ NEGc B (∥(B)∥)"
  and   "N ∈ ∥(B)∥ ⟹ N ∈ NEGn B (∥<B>∥)"
using NEG_simp by (blast)+

lemma NEG_intro:
  shows "M ∈ NEGc B (∥(B)∥) ⟹ M ∈ ∥<B>∥"
  and   "N ∈ NEGn B (∥<B>∥) ⟹ N ∈ ∥(B)∥"
using NEG_simp by (blast)+

lemma NEGc_simps:
  shows "NEGc (PR A) (∥(PR A)∥) = AXIOMSc (PR A) ∪ BINDINGc (PR A) (∥(PR A)∥)"  
  and   "NEGc (NOT C) (∥(NOT C)∥) = AXIOMSc (NOT C) ∪ BINDINGc (NOT C) (∥(NOT C)∥) 
                                        ∪ (NOTRIGHT (NOT C) (∥(C)∥))"  
  and   "NEGc (C AND D) (∥(C AND D)∥) = AXIOMSc (C AND D) ∪ BINDINGc (C AND D) (∥(C AND D)∥) 
                                        ∪ (ANDRIGHT (C AND D) (∥<C>∥) (∥<D>∥))"
  and   "NEGc (C OR D) (∥(C OR D)∥) = AXIOMSc (C OR D) ∪ BINDINGc (C OR D)  (∥(C OR D)∥)
                                        ∪ (ORRIGHT1 (C OR D) (∥<C>∥)) ∪ (ORRIGHT2 (C OR D) (∥<D>∥))"
  and   "NEGc (C IMP D) (∥(C IMP D)∥) = AXIOMSc (C IMP D) ∪ BINDINGc (C IMP D) (∥(C IMP D)∥) 
          ∪ (IMPRIGHT (C IMP D) (∥(C)∥) (∥<D>∥) (∥(D)∥) (∥<C>∥))"
by (simp_all only: NEGc.simps)

lemma AXIOMS_in_CANDs:
  shows "AXIOMSn B ⊆ (∥(B)∥)"
  and   "AXIOMSc B ⊆ (∥<B>∥)"
proof -
  have "AXIOMSn B ⊆ NEGn B (∥<B>∥)"
    by (nominal_induct B rule: ty.strong_induct) (auto)
  then show "AXIOMSn B ⊆ ∥(B)∥" using NEG_simp by blast
next
  have "AXIOMSc B ⊆ NEGc B (∥(B)∥)"
    by (nominal_induct B rule: ty.strong_induct) (auto)
  then show "AXIOMSc B ⊆ ∥<B>∥" using NEG_simp by blast
qed

lemma Ax_in_CANDs:
  shows "(y):Ax x a ∈ ∥(B)∥"
  and   "<b>:Ax x a ∈ ∥<B>∥"
proof -
  have "(y):Ax x a ∈ AXIOMSn B" by (auto simp add: AXIOMSn_def)
  also have "AXIOMSn B ⊆ ∥(B)∥" by (rule AXIOMS_in_CANDs)
  finally show "(y):Ax x a ∈ ∥(B)∥" by simp
next
  have "<b>:Ax x a ∈ AXIOMSc B" by (auto simp add: AXIOMSc_def)
  also have "AXIOMSc B ⊆ ∥<B>∥" by (rule AXIOMS_in_CANDs)
  finally show "<b>:Ax x a ∈ ∥<B>∥" by simp
qed

lemma AXIOMS_eqvt_aux_name:
  fixes pi::"name prm"
  shows "M ∈ AXIOMSn B ⟹ (pi∙M) ∈ AXIOMSn B" 
  and   "N ∈ AXIOMSc B ⟹ (pi∙N) ∈ AXIOMSc B"
apply(auto simp add: AXIOMSn_def AXIOMSc_def)
apply(rule_tac x="pi∙x" in exI)
apply(rule_tac x="pi∙y" in exI)
apply(rule_tac x="pi∙b" in exI)
apply(simp)
apply(rule_tac x="pi∙a" in exI)
apply(rule_tac x="pi∙y" in exI)
apply(rule_tac x="pi∙b" in exI)
apply(simp)
done

lemma AXIOMS_eqvt_aux_coname:
  fixes pi::"coname prm"
  shows "M ∈ AXIOMSn B ⟹ (pi∙M) ∈ AXIOMSn B" 
  and   "N ∈ AXIOMSc B ⟹ (pi∙N) ∈ AXIOMSc B"
apply(auto simp add: AXIOMSn_def AXIOMSc_def)
apply(rule_tac x="pi∙x" in exI)
apply(rule_tac x="pi∙y" in exI)
apply(rule_tac x="pi∙b" in exI)
apply(simp)
apply(rule_tac x="pi∙a" in exI)
apply(rule_tac x="pi∙y" in exI)
apply(rule_tac x="pi∙b" in exI)
apply(simp)
done

lemma AXIOMS_eqvt_name:
  fixes pi::"name prm"
  shows "(pi∙AXIOMSn B) = AXIOMSn B" 
  and   "(pi∙AXIOMSc B) = AXIOMSc B"
apply(auto)
apply(simp add: pt_set_bij1a[OF pt_name_inst, OF at_name_inst])
apply(drule_tac pi="pi" in AXIOMS_eqvt_aux_name(1))
apply(perm_simp)
apply(drule_tac pi="rev pi" in AXIOMS_eqvt_aux_name(1))
apply(simp add: pt_set_bij1[OF pt_name_inst, OF at_name_inst])
apply(simp add: pt_set_bij1a[OF pt_name_inst, OF at_name_inst])
apply(drule_tac pi="pi" in AXIOMS_eqvt_aux_name(2))
apply(perm_simp)
apply(drule_tac pi="rev pi" in AXIOMS_eqvt_aux_name(2))
apply(simp add: pt_set_bij1[OF pt_name_inst, OF at_name_inst])
done

lemma AXIOMS_eqvt_coname:
  fixes pi::"coname prm"
  shows "(pi∙AXIOMSn B) = AXIOMSn B" 
  and   "(pi∙AXIOMSc B) = AXIOMSc B"
apply(auto)
apply(simp add: pt_set_bij1a[OF pt_coname_inst, OF at_coname_inst])
apply(drule_tac pi="pi" in AXIOMS_eqvt_aux_coname(1))
apply(perm_simp)
apply(drule_tac pi="rev pi" in AXIOMS_eqvt_aux_coname(1))
apply(simp add: pt_set_bij1[OF pt_coname_inst, OF at_coname_inst])
apply(simp add: pt_set_bij1a[OF pt_coname_inst, OF at_coname_inst])
apply(drule_tac pi="pi" in AXIOMS_eqvt_aux_coname(2))
apply(perm_simp)
apply(drule_tac pi="rev pi" in AXIOMS_eqvt_aux_coname(2))
apply(simp add: pt_set_bij1[OF pt_coname_inst, OF at_coname_inst])
done

lemma BINDING_eqvt_name:
  fixes pi::"name prm"
  shows "(pi∙(BINDINGn B X)) = BINDINGn B (pi∙X)" 
  and   "(pi∙(BINDINGc B Y)) = BINDINGc B (pi∙Y)" 
apply(auto simp add: BINDINGn_def BINDINGc_def perm_set_def)
apply(rule_tac x="pi∙xb" in exI)
apply(rule_tac x="pi∙M" in exI)
apply(simp)
apply(auto)[1]
apply(drule_tac x="(rev pi)∙a" in spec)
apply(drule_tac x="(rev pi)∙P" in spec)
apply(drule mp)
apply(drule sym)
apply(drule pt_bij1[OF pt_name_inst, OF at_name_inst])
apply(simp)
apply(drule_tac ?pi1.0="pi" in SNa_eqvt(1))
apply(perm_simp add: nsubst_eqvt)
apply(rule_tac x="(rev pi∙xa):(rev pi∙M)" in exI)
apply(perm_simp)
apply(rule_tac x="rev pi∙xa" in exI)
apply(rule_tac x="rev pi∙M" in exI)
apply(simp)
apply(auto)[1]
apply(drule_tac x="pi∙a" in spec)
apply(drule_tac x="pi∙P" in spec)
apply(drule mp)
apply(force)
apply(drule_tac ?pi1.0="rev pi" in SNa_eqvt(1))
apply(perm_simp add: nsubst_eqvt)
apply(rule_tac x="pi∙a" in exI)
apply(rule_tac x="pi∙M" in exI)
apply(simp)
apply(auto)[1]
apply(drule_tac x="(rev pi)∙x" in spec)
apply(drule_tac x="(rev pi)∙P" in spec)
apply(drule mp)
apply(drule sym)
apply(drule pt_bij1[OF pt_name_inst, OF at_name_inst])
apply(simp)
apply(drule_tac ?pi1.0="pi" in SNa_eqvt(1))
apply(perm_simp add: csubst_eqvt)
apply(rule_tac x="<(rev pi∙a)>:(rev pi∙M)" in exI)
apply(perm_simp)
apply(rule_tac x="rev pi∙a" in exI)
apply(rule_tac x="rev pi∙M" in exI)
apply(simp add: swap_simps)
apply(auto)[1]
apply(drule_tac x="pi∙x" in spec)
apply(drule_tac x="pi∙P" in spec)
apply(drule mp)
apply(force)
apply(drule_tac ?pi1.0="rev pi" in SNa_eqvt(1))
apply(perm_simp add: csubst_eqvt)
done

lemma BINDING_eqvt_coname:
  fixes pi::"coname prm"
  shows "(pi∙(BINDINGn B X)) = BINDINGn B (pi∙X)" 
  and   "(pi∙(BINDINGc B Y)) = BINDINGc B (pi∙Y)" 
apply(auto simp add: BINDINGn_def BINDINGc_def perm_set_def)
apply(rule_tac x="pi∙xb" in exI)
apply(rule_tac x="pi∙M" in exI)
apply(simp)
apply(auto)[1]
apply(drule_tac x="(rev pi)∙a" in spec)
apply(drule_tac x="(rev pi)∙P" in spec)
apply(drule mp)
apply(drule sym)
apply(drule pt_bij1[OF pt_coname_inst, OF at_coname_inst])
apply(simp)
apply(drule_tac ?pi2.0="pi" in SNa_eqvt(2))
apply(perm_simp add: nsubst_eqvt)
apply(rule_tac x="(rev pi∙xa):(rev pi∙M)" in exI)
apply(perm_simp)
apply(rule_tac x="rev pi∙xa" in exI)
apply(rule_tac x="rev pi∙M" in exI)
apply(simp add: swap_simps)
apply(auto)[1]
apply(drule_tac x="pi∙a" in spec)
apply(drule_tac x="pi∙P" in spec)
apply(drule mp)
apply(force)
apply(drule_tac ?pi2.0="rev pi" in SNa_eqvt(2))
apply(perm_simp add: nsubst_eqvt)
apply(rule_tac x="pi∙a" in exI)
apply(rule_tac x="pi∙M" in exI)
apply(simp)
apply(auto)[1]
apply(drule_tac x="(rev pi)∙x" in spec)
apply(drule_tac x="(rev pi)∙P" in spec)
apply(drule mp)
apply(drule sym)
apply(drule pt_bij1[OF pt_coname_inst, OF at_coname_inst])
apply(simp)
apply(drule_tac ?pi2.0="pi" in SNa_eqvt(2))
apply(perm_simp add: csubst_eqvt)
apply(rule_tac x="<(rev pi∙a)>:(rev pi∙M)" in exI)
apply(perm_simp)
apply(rule_tac x="rev pi∙a" in exI)
apply(rule_tac x="rev pi∙M" in exI)
apply(simp)
apply(auto)[1]
apply(drule_tac x="pi∙x" in spec)
apply(drule_tac x="pi∙P" in spec)
apply(drule mp)
apply(force)
apply(drule_tac ?pi2.0="rev pi" in SNa_eqvt(2))
apply(perm_simp add: csubst_eqvt)
done

lemma CAND_eqvt_name:
  fixes pi::"name prm"
  shows   "(pi∙(∥(B)∥)) = (∥(B)∥)"
  and     "(pi∙(∥<B>∥)) = (∥<B>∥)"
proof (nominal_induct B rule: ty.strong_induct)
  case (PR X)
  { case 1 show ?case 
      apply -
      apply(simp add: lfp_eqvt)
      apply(simp add: perm_fun_def)
      apply(simp add: union_eqvt AXIOMS_eqvt_name BINDING_eqvt_name)
      apply(perm_simp)
    done
  next
    case 2 show ?case
      apply -
      apply(simp only: NEGc_simps)
      apply(simp add: union_eqvt AXIOMS_eqvt_name BINDING_eqvt_name)
      apply(simp add: lfp_eqvt)
      apply(simp add: comp_def)
      apply(simp add: perm_fun_def)
      apply(simp add: union_eqvt AXIOMS_eqvt_name BINDING_eqvt_name)
      apply(perm_simp)
      done
  }
next
  case (NOT B)
  have ih1: "pi∙(∥(B)∥) = (∥(B)∥)" by fact
  have ih2: "pi∙(∥<B>∥) = (∥<B>∥)" by fact
  have g: "pi∙(∥(NOT B)∥) = (∥(NOT B)∥)"
    apply -
    apply(simp only: lfp_eqvt)
    apply(simp only: comp_def)
    apply(simp only: perm_fun_def)
    apply(simp only: NEGc.simps NEGn.simps)
    apply(simp only: union_eqvt AXIOMS_eqvt_name BINDING_eqvt_name NOTRIGHT_eqvt_name NOTLEFT_eqvt_name)
    apply(perm_simp add: ih1 ih2)
    done
  { case 1 show ?case by (rule g)
  next 
    case 2 show ?case
      by (simp only: NEGc_simps union_eqvt AXIOMS_eqvt_name BINDING_eqvt_name NOTRIGHT_eqvt_name ih1 ih2 g)
  }
next
  case (AND A B)
  have ih1: "pi∙(∥(A)∥) = (∥(A)∥)" by fact
  have ih2: "pi∙(∥<A>∥) = (∥<A>∥)" by fact
  have ih3: "pi∙(∥(B)∥) = (∥(B)∥)" by fact
  have ih4: "pi∙(∥<B>∥) = (∥<B>∥)" by fact
  have g: "pi∙(∥(A AND B)∥) = (∥(A AND B)∥)"
    apply -
    apply(simp only: lfp_eqvt)
    apply(simp only: comp_def)
    apply(simp only: perm_fun_def)
    apply(simp only: NEGc.simps NEGn.simps)
    apply(simp only: union_eqvt AXIOMS_eqvt_name BINDING_eqvt_name ANDRIGHT_eqvt_name 
                     ANDLEFT2_eqvt_name ANDLEFT1_eqvt_name)
    apply(perm_simp add: ih1 ih2 ih3 ih4)
    done
  { case 1 show ?case by (rule g)
  next 
    case 2 show ?case
      by (simp only: NEGc_simps union_eqvt AXIOMS_eqvt_name BINDING_eqvt_name 
                     ANDRIGHT_eqvt_name ANDLEFT1_eqvt_name ANDLEFT2_eqvt_name ih1 ih2 ih3 ih4 g)
  }
next
  case (OR A B)
  have ih1: "pi∙(∥(A)∥) = (∥(A)∥)" by fact
  have ih2: "pi∙(∥<A>∥) = (∥<A>∥)" by fact
  have ih3: "pi∙(∥(B)∥) = (∥(B)∥)" by fact
  have ih4: "pi∙(∥<B>∥) = (∥<B>∥)" by fact
  have g: "pi∙(∥(A OR B)∥) = (∥(A OR B)∥)"
    apply -
    apply(simp only: lfp_eqvt)
    apply(simp only: comp_def)
    apply(simp only: perm_fun_def)
    apply(simp only: NEGc.simps NEGn.simps)
    apply(simp only: union_eqvt AXIOMS_eqvt_name BINDING_eqvt_name ORRIGHT1_eqvt_name 
                     ORRIGHT2_eqvt_name ORLEFT_eqvt_name)
    apply(perm_simp add: ih1 ih2 ih3 ih4)
    done
  { case 1 show ?case by (rule g)
  next 
    case 2 show ?case
      by (simp only: NEGc_simps union_eqvt AXIOMS_eqvt_name BINDING_eqvt_name 
                     ORRIGHT1_eqvt_name ORRIGHT2_eqvt_name ORLEFT_eqvt_name ih1 ih2 ih3 ih4 g)
  }
next
  case (IMP A B)
  have ih1: "pi∙(∥(A)∥) = (∥(A)∥)" by fact
  have ih2: "pi∙(∥<A>∥) = (∥<A>∥)" by fact
  have ih3: "pi∙(∥(B)∥) = (∥(B)∥)" by fact
  have ih4: "pi∙(∥<B>∥) = (∥<B>∥)" by fact
  have g: "pi∙(∥(A IMP B)∥) = (∥(A IMP B)∥)"
    apply -
    apply(simp only: lfp_eqvt)
    apply(simp only: comp_def)
    apply(simp only: perm_fun_def)
    apply(simp only: NEGc.simps NEGn.simps)
    apply(simp only: union_eqvt AXIOMS_eqvt_name BINDING_eqvt_name IMPRIGHT_eqvt_name IMPLEFT_eqvt_name)
    apply(perm_simp add: ih1 ih2 ih3 ih4)
    done
  { case 1 show ?case by (rule g)
  next 
    case 2 show ?case
      by (simp only: NEGc_simps union_eqvt AXIOMS_eqvt_name BINDING_eqvt_name 
                     IMPRIGHT_eqvt_name IMPLEFT_eqvt_name ih1 ih2 ih3 ih4 g)
  }
qed

lemma CAND_eqvt_coname:
  fixes pi::"coname prm"
  shows   "(pi∙(∥(B)∥)) = (∥(B)∥)"
  and     "(pi∙(∥<B>∥)) = (∥<B>∥)"
proof (nominal_induct B rule: ty.strong_induct)
  case (PR X)
  { case 1 show ?case 
      apply -
      apply(simp add: lfp_eqvt)
      apply(simp add: perm_fun_def)
      apply(simp add: union_eqvt AXIOMS_eqvt_coname BINDING_eqvt_coname)
      apply(perm_simp)
    done
  next
    case 2 show ?case
      apply -
      apply(simp only: NEGc_simps)
      apply(simp add: union_eqvt AXIOMS_eqvt_coname BINDING_eqvt_coname)
      apply(simp add: lfp_eqvt)
      apply(simp add: comp_def)
      apply(simp add: perm_fun_def)
      apply(simp add: union_eqvt AXIOMS_eqvt_coname BINDING_eqvt_coname)
      apply(perm_simp)
      done
  }
next
  case (NOT B)
  have ih1: "pi∙(∥(B)∥) = (∥(B)∥)" by fact
  have ih2: "pi∙(∥<B>∥) = (∥<B>∥)" by fact
  have g: "pi∙(∥(NOT B)∥) = (∥(NOT B)∥)"
    apply -
    apply(simp only: lfp_eqvt)
    apply(simp only: comp_def)
    apply(simp only: perm_fun_def)
    apply(simp only: NEGc.simps NEGn.simps)
    apply(simp only: union_eqvt AXIOMS_eqvt_coname BINDING_eqvt_coname 
            NOTRIGHT_eqvt_coname NOTLEFT_eqvt_coname)
    apply(perm_simp add: ih1 ih2)
    done
  { case 1 show ?case by (rule g)
  next 
    case 2 show ?case
      by (simp only: NEGc_simps union_eqvt AXIOMS_eqvt_coname BINDING_eqvt_coname 
              NOTRIGHT_eqvt_coname ih1 ih2 g)
  }
next
  case (AND A B)
  have ih1: "pi∙(∥(A)∥) = (∥(A)∥)" by fact
  have ih2: "pi∙(∥<A>∥) = (∥<A>∥)" by fact
  have ih3: "pi∙(∥(B)∥) = (∥(B)∥)" by fact
  have ih4: "pi∙(∥<B>∥) = (∥<B>∥)" by fact
  have g: "pi∙(∥(A AND B)∥) = (∥(A AND B)∥)"
    apply -
    apply(simp only: lfp_eqvt)