Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Isabelle/HOL/Nominal/Examples/   (Isabelle Prover Version 2025-1©)  Datei vom 16.11.2025 mit Größe 236 kB image not shown  

SSL Class2.thy

  Sprache: Isabelle
 

theory Class2
imports Class1
begin

text Reduction

lemma fin_not_Cut:
  assumes a: "fin M x"
  shows "¬(a M' x N'. M = Cut <a>.M' (x).N')"
using a
by (induct) (auto)

lemma fresh_not_fin:
  assumes a: "xM"
  shows "¬fin M x"
proof -
  have "fin M x ==> xM ==> 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: "aM"
  shows "¬fic M a"
proof -
  have "fic M a ==> aM ==> 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'" "cM" "yP"
  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 \<noteq> 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'" "cP" "yM"
  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 \<noteq> Ax y a*)
    apply(rule impI)
    apply(subgoal_tac "M{a:=(x).N}{c:=(y).P} = M{c:=(y).P}{a:=(x).(N{c:=(y).P})}")
    apply(simp)
    apply(rule c_redu.left)
    apply(rule not_fic_subst2)
    apply(simp)
    apply(simp add: subst_fresh)
    apply(simp add: subst_fresh)
    apply(simp add: abs_fresh fresh_atm)
    apply(rule subst_subst4)
    apply(simp add: fresh_prod fresh_atm)
    apply(simp add: fresh_prod fresh_atm)
    apply(simp add: fresh_prod fresh_atm)
    apply(simp add: fresh_prod fresh_atm)
    apply(simp)
    done
qed

lemma c_redu_subst1':
  assumes a: "M c M'" 
  shows "M{y:=<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 rtranclp_trans)
    apply(rule a_starI)
    apply(rule al_redu)
    apply(rule l_redu.intros)
    apply(simp add: subst_fresh)
    apply(simp add: fresh_atm)
    apply(rule fic_subst2)
    apply(simp_all)
    apply(rule aux4)
    apply(rule subst_comm')
    apply(simp_all)
    done
next
  case LAxL
  then show ?case
    apply -
    apply(rule aux3)
    apply(rule better_Cut_substn)
    apply(simp add: abs_fresh)
    apply(simp)
    apply(simp add: trm.inject fresh_atm)
    apply(auto)
    apply(rule aux4)
    apply(rule sym)
    apply(rule fin_substn_nrename)
    apply(simp_all)
    apply(rule a_starI)
    apply(rule al_redu)
    apply(rule aux2)
    apply(rule l_redu.intros)
    apply(simp add: subst_fresh)
    apply(simp add: fresh_atm)
    apply(rule fin_subst1)
    apply(simp_all)
    apply(rule subst_comm')
    apply(simp_all)
    done
next
  case (LNot v M N u a b)
  then show ?case
  proof -
    { assume asm: "NAx 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[cc>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 rtranclp_trans)
          apply(rule a_starI)
          apply(rule ac_redu)
          apply(rule better_left)
          apply(simp)
          apply(simp add: subst_with_ax2)
          done
      qed
      also have " = (Cut <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: "M1Ax 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[cc>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 rtranclp_trans)
          apply(rule a_starI)
          apply(rule ac_redu)
          apply(rule better_left)
          apply(simp)
          apply(simp add: subst_with_ax2)
          done
      qed
      also have " = (Cut <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: "M2Ax 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[cc>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 rtranclp_trans)
          apply(rule a_starI)
          apply(rule ac_redu)
          apply(rule better_left)
          apply(simp)
          apply(simp add: subst_with_ax2)
          done
      qed
      also have " = (Cut <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: "MAx 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[cc>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 rtranclp_trans)
          apply(rule a_starI)
          apply(rule ac_redu)
          apply(rule better_left)
          apply(simp)
          apply(simp add: subst_with_ax2)
          done
      qed
      also have " = (Cut <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: "MAx 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[cc>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 rtranclp_trans)
          apply(rule a_starI)
          apply(rule ac_redu)
          apply(rule better_left)
          apply(simp)
          apply(simp add: subst_with_ax2)
          done
      qed
      also have " = (Cut <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: "NAx 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[cc>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 rtranclp_trans)
          apply(rule a_starI)
          apply(rule ac_redu)
          apply(rule better_left)
          apply(simp)
          apply(simp add: subst_with_ax2)
          done
      qed
      also have " = (Cut <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 rtranclp_trans)
    apply(rule a_starI)
    apply(rule al_redu)
    apply(rule l_redu.intros)
    apply(simp add: subst_fresh)
    apply(simp add: fresh_atm)
    apply(rule fin_subst2)
    apply(simp_all)
    apply(rule aux4)
    apply(rule subst_comm')
    apply(simp_all)
    done
next
  case (LNot v M N u a b)
  then show ?case
  proof -
    { assume asm: "MAx 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[yn>u]))" 
      proof (cases "fin P y")
        case True 
        assume "fin P y"
        then show ?thesis using LNot
          apply -
          apply(rule a_starI)
          apply(rule better_CutR_intro)
          apply(rule al_redu)
          apply(rule better_LAxL_intro)
          apply(simp)
          done
      next
        case False 
        assume "¬fin P y" 
        then show ?thesis
          apply -
          apply(rule a_star_CutR)
          apply(rule rtranclp_trans)
          apply(rule a_starI)
          apply(rule ac_redu)
          apply(rule better_right)
          apply(simp)
          apply(simp add: subst_with_ax1)
          done
      qed
      also have " = (Cut <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: "NAx 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[yn>u])"
      proof (cases "fin P y")
        case True 
        assume "fin P y"
        then show ?thesis using LAnd1
          apply -
          apply(rule a_starI)
          apply(rule better_CutR_intro)
          apply(rule al_redu)
          apply(rule better_LAxL_intro)
          apply(simp)
          done
      next
        case False 
        assume "¬fin P y" 
        then show ?thesis
          apply -
          apply(rule a_star_CutR)
          apply(rule rtranclp_trans)
          apply(rule a_starI)
          apply(rule ac_redu)
          apply(rule better_right)
          apply(simp)
          apply(simp add: subst_with_ax1)
          done
      qed
      also have " = (Cut <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: "NAx 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[yn>u])"
      proof (cases "fin P y")
        case True 
        assume "fin P y"
        then show ?thesis using LAnd2
          apply -
          apply(rule a_starI)
          apply(rule better_CutR_intro)
          apply(rule al_redu)
          apply(rule better_LAxL_intro)
          apply(simp)
          done
      next
        case False 
        assume "¬fin P y" 
        then show ?thesis
          apply -
          apply(rule a_star_CutR)
          apply(rule rtranclp_trans)
          apply(rule a_starI)
          apply(rule ac_redu)
          apply(rule better_right)
          apply(simp)
          apply(simp add: subst_with_ax1)
          done
      qed
      also have " = (Cut <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: "N1Ax 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[yn>x1])"
      proof (cases "fin P y")
        case True 
        assume "fin P y"
        then show ?thesis using LOr1
          apply -
          apply(rule a_starI)
          apply(rule better_CutR_intro)
          apply(rule al_redu)
          apply(rule better_LAxL_intro)
          apply(simp)
          done
      next
        case False 
        assume "¬fin P y" 
        then show ?thesis
          apply -
          apply(rule a_star_CutR)
          apply(rule rtranclp_trans)
          apply(rule a_starI)
          apply(rule ac_redu)
          apply(rule better_right)
          apply(simp)
          apply(simp add: subst_with_ax1)
          done
      qed
      also have " = (Cut <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: "N2Ax 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[yn>x2])"
      proof (cases "fin P y")
        case True 
        assume "fin P y"
        then show ?thesis using LOr2
          apply -
          apply(rule a_starI)
          apply(rule better_CutR_intro)
          apply(rule al_redu)
          apply(rule better_LAxL_intro)
          apply(simp)
          done
      next
        case False 
        assume "¬fin P y" 
        then show ?thesis
          apply -
          apply(rule a_star_CutR)
          apply(rule rtranclp_trans)
          apply(rule a_starI)
          apply(rule ac_redu)
          apply(rule better_right)
          apply(simp)
          apply(simp add: subst_with_ax1)
          done
      qed
      also have " = (Cut <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: "MAx x c QAx 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 QAx 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[yn>x])) (u).(Q{c:=(y).P})"
      proof (cases "fin P y")
        case True 
        assume "fin P y"
        then show ?thesis using LImp
          apply -
          apply(rule a_star_CutL)
          apply(rule a_star_CutR)
          apply(rule rtranclp_trans)
          apply(rule a_starI)
          apply(rule al_redu)
          apply(rule better_LAxL_intro)
          apply(simp)
          apply(simp)
          done
      next
        case False 
        assume "¬fin P y" 
        then show ?thesis using LImp
          apply -
          apply(rule a_star_CutL)
          apply(rule a_star_CutR)
          apply(rule rtranclp_trans)
          apply(rule a_starI)
          apply(rule ac_redu)
          apply(rule better_right)
          apply(simp)
          apply(simp add: subst_with_ax1)
          done
      qed
      also have " = (Cut <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: "MAx 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[yn>u])"
      proof (cases "fin P y")
        case True 
        assume "fin P y"
        then show ?thesis using LImp
          apply -
          apply(rule a_star_CutR)
          apply(rule a_starI)
          apply(rule al_redu)
          apply(rule better_LAxL_intro)
          apply(simp)
          done
      next
        case False 
        assume "¬fin P y" 
        then show ?thesis using LImp
          apply -
          apply(rule a_star_CutR)
          apply(rule rtranclp_trans)
          apply(rule a_starI)
          apply(rule ac_redu)
          apply(rule better_right)
          apply(simp)
          apply(simp add: subst_with_ax1)
          done
      qed
      also have " = (Cut <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[yn>u])"
      proof (cases "fin P y")
        case True 
        assume "fin P y"
        then show ?thesis using LImp
          apply -
          apply(rule a_star_CutR)
          apply(rule a_starI)
          apply(rule al_redu)
          apply(rule better_LAxL_intro)
          apply(simp)
          done
      next
        case False 
        assume "¬fin P y" 
        then show ?thesis using LImp
          apply -
          apply(rule a_star_CutR)
          apply(rule rtranclp_trans)
          apply(rule a_starI)
          apply(rule ac_redu)
          apply(rule better_right)
          apply(simp)
          apply(simp add: subst_with_ax1)
          done
      qed
      also have " a* Cut <a>.(Cut <d>.(N{c:=(y).P}) (x).(P[yn>x])) (u).(P[yn>u])"
      proof (cases "fin P y")
        case True 
        assume "fin P y"
        then show ?thesis using LImp
          apply -
          apply(rule a_star_CutL)
          apply(rule a_star_CutR)
          apply(rule a_starI)
          apply(rule al_redu)
          apply(rule better_LAxL_intro)
          apply(simp)
          done
      next
        case False 
        assume "¬fin P y" 
        then show ?thesis using LImp
          apply -
          apply(rule a_star_CutL)
          apply(rule a_star_CutR)
          apply(rule rtranclp_trans)
          apply(rule a_starI)
          apply(rule ac_redu)
          apply(rule better_right)
          apply(simp)
          apply(simp add: subst_with_ax1)
          done
      qed
      also have " = (Cut <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 rtranclp_trans)
    apply(rule a_star_CutL)
    apply(assumption)
    apply(rule rtranclp_trans)
    apply(rule_tac M'="P[cc>a]" in a_star_CutL)
    apply(case_tac "fic P c")
    apply(rule a_starI)
    apply(rule al_redu)
    apply(rule better_LAxR_intro)
    apply(simp)
    apply(rule rtranclp_trans)
    apply(rule a_starI)
    apply(rule ac_redu)
    apply(rule better_left)
    apply(simp)
    apply(rule subst_with_ax2)
    apply(rule aux4)
    apply(simp add: trm.inject)
    apply(simp add: alpha fresh_atm)
    apply(simp add: crename_swap)
    apply(rule impI)
    apply(rule a_star_CutL)
    apply(auto)
    done
next
  case (a_Cut_r a N x M M' y c P)
  then show ?case
    apply(auto simp add: subst_fresh fresh_a_redu)
    apply(rule a_star_CutR)
    apply(auto)[1]
    apply(rule a_star_CutR)
    apply(auto)[1]
    done
next
  case a_NotL
  then show ?case 
    apply(auto)
    apply(generate_fresh "name")
    apply(fresh_fun_simp)
    apply(fresh_fun_simp)
    apply(simp add: subst_fresh)
    apply(rule a_star_CutR)
    apply(rule a_star_NotL)
    apply(auto)[1]
    apply(rule a_star_NotL)
    apply(auto)[1]
    done
next
  case a_NotR
  then show ?case 
    apply(auto)
    apply(rule a_star_NotR)
    apply(auto)[1]
    done
next
  case a_AndR_l
  then show ?case
    apply(auto simp add: subst_fresh fresh_a_redu)
    apply(rule a_star_AndR)
    apply(auto)
    done
next
  case a_AndR_r
  then show ?case
    apply(auto simp add: subst_fresh fresh_a_redu)
    apply(rule a_star_AndR)
    apply(auto)
    done
next
  case a_AndL1
  then show ?case 
    apply(auto)
    apply(generate_fresh "name")
    apply(fresh_fun_simp)
    apply(fresh_fun_simp)
    apply(simp add: subst_fresh)
    apply(rule a_star_CutR)
    apply(rule a_star_AndL1)
    apply(auto)[1]
    apply(rule a_star_AndL1)
    apply(auto)[1]
    done
next
  case a_AndL2
  then show ?case 
    apply(auto)
    apply(generate_fresh "name")
    apply(fresh_fun_simp)
    apply(fresh_fun_simp)
    apply(simp add: subst_fresh)
    apply(rule a_star_CutR)
    apply(rule a_star_AndL2)
    apply(auto)[1]
    apply(rule a_star_AndL2)
    apply(auto)[1]
    done
next
  case a_OrR1
  then show ?case
    apply(auto simp add: subst_fresh fresh_a_redu)
    apply(rule a_star_OrR1)
    apply(auto)
    done
next
  case a_OrR2
  then show ?case
    apply(auto simp add: subst_fresh fresh_a_redu)
    apply(rule a_star_OrR2)
    apply(auto)
    done
next
  case a_OrL_l
  then show ?case 
    apply(auto simp add: subst_fresh fresh_a_redu)
    apply(generate_fresh "name")
    apply(fresh_fun_simp)
    apply(fresh_fun_simp)
    apply(simp add: subst_fresh)
    apply(rule a_star_CutR)
    apply(rule a_star_OrL)
    apply(auto)
    apply(rule a_star_OrL)
    apply(auto)
    done
next
  case a_OrL_r
  then show ?case 
    apply(auto simp add: subst_fresh fresh_a_redu)
    apply(generate_fresh "name")
    apply(fresh_fun_simp)
    apply(fresh_fun_simp)
    apply(simp add: subst_fresh)
    apply(rule a_star_CutR)
    apply(rule a_star_OrL)
    apply(auto)
    apply(rule a_star_OrL)
    apply(auto)
    done
next
  case a_ImpR
  then show ?case
    apply(auto simp add: subst_fresh fresh_a_redu)
    apply(rule a_star_ImpR)
    apply(auto)
    done
next
  case a_ImpL_r
  then show ?case 
    apply(auto simp add: subst_fresh fresh_a_redu)
    apply(generate_fresh "name")
    apply(fresh_fun_simp)
    apply(fresh_fun_simp)
    apply(simp add: subst_fresh)
    apply(rule a_star_CutR)
    apply(rule a_star_ImpL)
    apply(auto)
    apply(rule a_star_ImpL)
    apply(auto)
    done
next
  case a_ImpL_l
  then show ?case 
    apply(auto simp add: subst_fresh fresh_a_redu)
    apply(generate_fresh "name")
    apply(fresh_fun_simp)
    apply(fresh_fun_simp)
    apply(simp add: subst_fresh)
    apply(rule a_star_CutR)
    apply(rule a_star_ImpL)
    apply(auto)
    apply(rule a_star_ImpL)
    apply(auto)
    done
qed

lemma a_redu_subst2:
  assumes a: "M 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 rtranclp_trans)
    apply(rule a_star_CutR)
    apply(assumption)
    apply(rule rtranclp_trans)
    apply(rule_tac N'="P[yn>x]" in a_star_CutR)
    apply(case_tac "fin P y")
    apply(rule a_starI)
    apply(rule al_redu)
    apply(rule better_LAxL_intro)
    apply(simp)
    apply(rule rtranclp_trans)
    apply(rule a_starI)
    apply(rule ac_redu)
    apply(rule better_right)
    apply(simp)
    apply(rule subst_with_ax1)
    apply(rule aux4)
    apply(simp add: trm.inject)
    apply(simp add: alpha fresh_atm)
    apply(simp add: nrename_swap)
    apply(rule impI)
    apply(rule a_star_CutR)
    apply(auto)
    done
next
  case (a_Cut_l a N x M M' y c P)
  then show ?case
    apply(auto simp add: subst_fresh fresh_a_redu)
    apply(rule a_star_CutL)
    apply(auto)[1]
    apply(rule a_star_CutL)
    apply(auto)[1]
    done
next
  case a_NotR
  then show ?case 
    apply(auto)
    apply(generate_fresh "coname")
    apply(fresh_fun_simp)
    apply(fresh_fun_simp)
    apply(simp add: subst_fresh)
    apply(rule a_star_CutL)
    apply(rule a_star_NotR)
    apply(auto)[1]
    apply(rule a_star_NotR)
    apply(auto)[1]
    done
next
  case a_NotL
  then show ?case 
    apply(auto)
    apply(rule a_star_NotL)
    apply(auto)[1]
    done
next
  case a_AndR_l
  then show ?case
    apply(auto simp add: subst_fresh fresh_a_redu)
    apply(generate_fresh "coname")
    apply(fresh_fun_simp)
    apply(fresh_fun_simp)
    apply(simp add: subst_fresh)
    apply(rule a_star_CutL)
    apply(rule a_star_AndR)
    apply(auto)
    apply(rule a_star_AndR)
    apply(auto)
    done
next
  case a_AndR_r
  then show ?case
    apply(auto simp add: subst_fresh fresh_a_redu)
    apply(generate_fresh "coname")
    apply(fresh_fun_simp)
    apply(fresh_fun_simp)
    apply(simp add: subst_fresh)
    apply(rule a_star_CutL)
    apply(rule a_star_AndR)
    apply(auto)
    apply(rule a_star_AndR)
    apply(auto)
    done
next
  case a_AndL1
  then show ?case
    apply(auto simp add: subst_fresh fresh_a_redu)
    apply(rule a_star_AndL1)
    apply(auto)
    done
next
  case a_AndL2
  then show ?case
    apply(auto simp add: subst_fresh fresh_a_redu)
    apply(rule a_star_AndL2)
    apply(auto)
    done
next
  case a_OrR1
  then show ?case 
    apply(auto)
    apply(generate_fresh "coname")
    apply(fresh_fun_simp)
    apply(fresh_fun_simp)
    apply(simp add: subst_fresh)
    apply(rule a_star_CutL)
    apply(rule a_star_OrR1)
    apply(auto)[1]
    apply(rule a_star_OrR1)
    apply(auto)[1]
    done
next
  case a_OrR2
  then show ?case 
    apply(auto)
    apply(generate_fresh "coname")
    apply(fresh_fun_simp)
    apply(fresh_fun_simp)
    apply(simp add: subst_fresh)
    apply(rule a_star_CutL)
    apply(rule a_star_OrR2)
    apply(auto)[1]
    apply(rule a_star_OrR2)
    apply(auto)[1]
    done
next
  case a_OrL_l
  then show ?case
    apply(auto simp add: subst_fresh fresh_a_redu)
    apply(rule a_star_OrL)
    apply(auto)
    done
next
  case a_OrL_r
  then show ?case
    apply(auto simp add: subst_fresh fresh_a_redu)
    apply(rule a_star_OrL)
    apply(auto)
    done
next
  case a_ImpR
  then show ?case 
    apply(auto simp add: subst_fresh fresh_a_redu)
    apply(generate_fresh "coname")
    apply(fresh_fun_simp)
    apply(fresh_fun_simp)
    apply(simp add: subst_fresh)
    apply(rule a_star_CutL)
    apply(rule a_star_ImpR)
    apply(auto)
    apply(rule a_star_ImpR)
    apply(auto)
    done
next
  case a_ImpL_l
  then show ?case
    apply(auto simp add: subst_fresh fresh_a_redu)
    apply(rule a_star_ImpL)
    apply(auto)
    done
next
  case a_ImpL_r
  then show ?case
    apply(auto simp add: subst_fresh fresh_a_redu)
    apply(rule a_star_ImpL)
    apply(auto)
    done
qed

lemma a_star_subst1:
  assumes a: "M 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. xa y ==> SNa y) ==>
    (y. xa y ==> P y z) ==>
    (u. za u ==> SNa u) ==>
    (u. za 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. xay P y z) (u. za 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" "Ma M'"
  shows "SNa M'"
using a 
by (erule_tac SNa.cases) (simp)

lemma a_star_preserves_SNa:
  assumes a: "SNa M" and b: "Ma* 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 (pi1M)"
  and   "SNa M ==> SNa (pi2M)"
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>:PX SNa (M{x:=<a>.P})}"

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

lemma BINDINGn_decreasing:
  shows "XY ==> BINDINGn B Y BINDINGn B X"
by (simp add: BINDINGn_def) (blast) 

lemma BINDINGc_decreasing:
  shows "XY ==> 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) (piX)"
apply(auto simp add: perm_set_def)
apply(rule_tac x="pia" in exI) 
apply(rule_tac x="pixb" in exI) 
apply(rule_tac x="piM" 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) (piX)"
apply(auto simp add: perm_set_def)
apply(rule_tac x="pia" in exI) 
apply(rule_tac x="pixb" in exI) 
apply(rule_tac x="piM" 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) (piX)"
apply(auto simp add: perm_set_def)
apply(rule_tac x="pia" in exI) 
apply(rule_tac x="pixb" in exI) 
apply(rule_tac x="piM" 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) (piX)"
apply(auto simp add: perm_set_def)
apply(rule_tac x="pia" in exI) 
apply(rule_tac x="pixb" in exI) 
apply(rule_tac x="piM" 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) (piX) (piY)"
apply(auto simp add: perm_set_def)
apply(rule_tac x="pic" in exI)
apply(rule_tac x="pia" in exI)
apply(rule_tac x="pib" in exI)
apply(rule_tac x="piM" in exI)
apply(rule_tac x="piN" 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) (piX) (piY)"
apply(auto simp add: perm_set_def)
apply(rule_tac x="pic" in exI)
apply(rule_tac x="pia" in exI)
apply(rule_tac x="pib" in exI)
apply(rule_tac x="piM" in exI)
apply(rule_tac x="piN" 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) (piX)"
apply(auto simp add: perm_set_def)
apply(rule_tac x="pixb" in exI) 
apply(rule_tac x="piy" in exI) 
apply(rule_tac x="piM" 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) (piX)"
apply(auto simp add: perm_set_def)
apply(rule_tac x="pixb" in exI) 
apply(rule_tac x="piy" in exI) 
apply(rule_tac x="piM" 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) (piX)"
apply(auto simp add: perm_set_def)
apply(rule_tac x="pixb" in exI) 
apply(rule_tac x="piy" in exI) 
apply(rule_tac x="piM" 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) (piX)"
apply(auto simp add: perm_set_def)
apply(rule_tac x="pixb" in exI) 
apply(rule_tac x="piy" in exI) 
apply(rule_tac x="piM" 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) (piX) (piY)"
apply(auto simp add: perm_set_def)
apply(rule_tac x="pixb" in exI)
apply(rule_tac x="piy" in exI)
apply(rule_tac x="piz" in exI)
apply(rule_tac x="piM" in exI)
apply(rule_tac x="piN" 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) (piX) (piY)"
apply(auto simp add: perm_set_def)
apply(rule_tac x="pixb" in exI)
apply(rule_tac x="piy" in exI)
apply(rule_tac x="piz" in exI)
apply(rule_tac x="piM" in exI)
apply(rule_tac x="piN" 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) (piX)"
apply(auto simp add: perm_set_def)
apply(rule_tac x="pia" in exI) 
apply(rule_tac x="pib" in exI) 
apply(rule_tac x="piM" 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) (piX)"
apply(auto simp add: perm_set_def)
apply(rule_tac x="pia" in exI) 
apply(rule_tac x="pib" in exI) 
apply(rule_tac x="piM" 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) (piX)"
apply(auto simp add: perm_set_def)
apply(rule_tac x="pia" in exI) 
apply(rule_tac x="pib" in exI) 
apply(rule_tac x="piM" 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) (piX)"
apply(auto simp add: perm_set_def)
apply(rule_tac x="pia" in exI) 
apply(rule_tac x="pib" in exI) 
apply(rule_tac x="piM" 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) (piX) (piY) (piZ) (piU)"
apply(auto simp add: perm_set_def)
apply(rule_tac x="pixb" in exI)
apply(rule_tac x="pia" in exI)
apply(rule_tac x="pib" in exI)
apply(rule_tac x="piM" 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="piz" in spec)
apply(drule_tac x="piP" 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="pic" in spec)
apply(drule_tac x="piQ" 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) (piX) (piY) (piZ) (piU)"
apply(auto simp add: perm_set_def)
apply(rule_tac x="pixb" in exI)
apply(rule_tac x="pia" in exI)
apply(rule_tac x="pib" in exI)
apply(rule_tac x="piM" 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="piz" in spec)
apply(drule_tac x="piP" 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="pic" in spec)
apply(drule_tac x="piQ" 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) (piX) (piY)"
apply(auto simp add: perm_set_def)
apply(rule_tac x="pixb" in exI) 
apply(rule_tac x="pia" in exI)
apply(rule_tac x="piy" in exI) 
apply(rule_tac x="piM" in exI) 
apply(rule_tac x="piN" 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) (piX) (piY)"
apply(auto simp add: perm_set_def)
apply(rule_tac x="pixb" in exI) 
apply(rule_tac x="pia" in exI)
apply(rule_tac x="piy" in exI) 
apply(rule_tac x="piM" in exI) 
apply(rule_tac x="piN" 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 (sizefst) (sizefst))")
apply(simp_all)
done

text Candidates

lemma test1:
  shows "x(XY) = (xX xY)"
by blast

lemma test2:
  shows "x(XY) = (xX xY)"
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)) = (pi1X)"
  and   "(pi2(Y)) = (pi2Y)"
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="pi1xa" 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="pi2xa" 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 (pi1f)"
  and   "pi2(lfp g) = lfp (pi2g)"
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. (pi1f) u u} = {u. ((rev pi1)((pi1f) 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. (pi2g) u u} = {u. ((rev pi2)((pi2g) 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"  ('(_') [6060
where
  "(B) lfp (NEGn B NEGc B)" 

abbreviation
  CANDc::"ty ctrm set"  (🚫 [6060)
where
  "<B> NEGc B ((B))"

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

lemma NEGc_decreasing:
  shows "XY ==> 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. XY NEGn B (NEGc B X) NEGn B (NEGc B Y)"
  proof (intro strip)
    fix X::"ntrm set" and Y::"ntrm set"
    assume "XY"
    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. XY NEGc B (NEGn B X) NEGc B (NEGn B Y)"
  proof (intro strip)
    fix X::"ctrm set" and Y::"ctrm set"
    assume "XY"
    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 ==> (piM) AXIOMSn B" 
  and   "N AXIOMSc B ==> (piN) AXIOMSc B"
apply(auto simp add: AXIOMSn_def AXIOMSc_def)
apply(rule_tac x="pix" in exI)
apply(rule_tac x="piy" in exI)
apply(rule_tac x="pib" in exI)
apply(simp)
apply(rule_tac x="pia" in exI)
apply(rule_tac x="piy" in exI)
apply(rule_tac x="pib" in exI)
apply(simp)
done

lemma AXIOMS_eqvt_aux_coname:
  fixes pi::"coname prm"
  shows "M AXIOMSn B ==> (piM) AXIOMSn B" 
  and   "N AXIOMSc B ==> (piN) AXIOMSc B"
apply(auto simp add: AXIOMSn_def AXIOMSc_def)
apply(rule_tac x="pix" in exI)
apply(rule_tac x="piy" in exI)
apply(rule_tac x="pib" in exI)
apply(simp)
apply(rule_tac x="pia" in exI)
apply(rule_tac x="piy" in exI)
apply(rule_tac x="pib" in exI)
apply(simp)
done

lemma AXIOMS_eqvt_name:
  fixes pi::"name prm"
  shows "(piAXIOMSn B) = AXIOMSn B" 
  and   "(piAXIOMSc 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 "(piAXIOMSn B) = AXIOMSn B" 
  and   "(piAXIOMSc 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 (piX)" 
  and   "(pi(BINDINGc B Y)) = BINDINGc B (piY)" 
apply(auto simp add: BINDINGn_def BINDINGc_def perm_set_def)
apply(rule_tac x="pixb" in exI)
apply(rule_tac x="piM" 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 pixa):(rev piM)" in exI)
apply(perm_simp)
apply(rule_tac x="rev pixa" in exI)
apply(rule_tac x="rev piM" in exI)
apply(simp)
apply(auto)[1]
apply(drule_tac x="pia" in spec)
apply(drule_tac x="piP" 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="pia" in exI)
apply(rule_tac x="piM" 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 pia)>:(rev piM)" in exI)
apply(perm_simp)
apply(rule_tac x="rev pia" in exI)
apply(rule_tac x="rev piM" in exI)
apply(simp add: swap_simps)
apply(auto)[1]
apply(drule_tac x="pix" in spec)
apply(drule_tac x="piP" 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 (piX)" 
  and   "(pi(BINDINGc B Y)) = BINDINGc B (piY)" 
apply(auto simp add: BINDINGn_def BINDINGc_def perm_set_def)
apply(rule_tac x="pixb" in exI)
apply(rule_tac x="piM" 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 pixa):(rev piM)" in exI)
apply(perm_simp)
apply(rule_tac x="rev pixa" in exI)
apply(rule_tac x="rev piM" in exI)
apply(simp add: swap_simps)
apply(auto)[1]
apply(drule_tac x="pia" in spec)
apply(drule_tac x="piP" 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="pia" in exI)
apply(rule_tac x="piM" 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 pia)>:(rev piM)" in exI)
apply(perm_simp)
apply(rule_tac x="rev pia" in exI)
apply(rule_tac x="rev piM" in exI)
apply(simp)
apply(auto)[1]
apply(drule_tac x="pix" in spec)
apply(drule_tac x="piP" 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)
    apply(simp only: comp_def)
    apply(simp only: perm_fun_def)
    apply(simp only: NEGc.simps NEGn.simps)
    apply(simp only: union_eqvt AXIOMS_eqvt_coname BINDING_eqvt_coname ANDRIGHT_eqvt_coname 
                     ANDLEFT2_eqvt_coname ANDLEFT1_eqvt_coname)
    apply(perm_simp add: ih1 ih2 ih3 ih4)
    done
  { case 1 show ?case by (rule g)
  next 
    case 2 show ?case
      by (simp only: NEGc_simps union_eqvt AXIOMS_eqvt_coname BINDING_eqvt_coname 
                     ANDRIGHT_eqvt_coname ANDLEFT1_eqvt_coname ANDLEFT2_eqvt_coname 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_coname BINDING_eqvt_coname ORRIGHT1_eqvt_coname 
                     ORRIGHT2_eqvt_coname ORLEFT_eqvt_coname)
    apply(perm_simp add: ih1 ih2 ih3 ih4)
    done
  { case 1 show ?case by (rule g)
  next 
    case 2 show ?case
      by (simp only: NEGc_simps union_eqvt AXIOMS_eqvt_coname BINDING_eqvt_coname 
                     ORRIGHT1_eqvt_coname ORRIGHT2_eqvt_coname ORLEFT_eqvt_coname 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_coname BINDING_eqvt_coname IMPRIGHT_eqvt_coname 
         IMPLEFT_eqvt_coname)
    apply(perm_simp add: ih1 ih2 ih3 ih4)
    done
  { case 1 show ?case by (rule g)
  next 
    case 2 show ?case
      by (simp only: NEGc_simps union_eqvt AXIOMS_eqvt_coname BINDING_eqvt_coname 
                     IMPRIGHT_eqvt_coname IMPLEFT_eqvt_coname ih1 ih2 ih3 ih4 g)
  }
qed

text Elimination rules for the set-operators

lemma BINDINGc_elim:
  assumes a: "<a>:M BINDINGc B ((B))"
  shows "x P. ((x):P)((B)) SNa (M{a:=(x).P})"
using a
apply(auto simp add: BINDINGc_def)
apply(auto simp add: ctrm.inject alpha)
apply(drule_tac x="[(a,aa)]x" in spec)
apply(drule_tac x="[(a,aa)]P" in spec)
apply(drule mp)
apply(drule_tac pi="[(a,aa)]" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(simp add: CAND_eqvt_coname)
apply(drule_tac ?pi2.0="[(a,aa)]" in SNa_eqvt(2))
apply(perm_simp add: csubst_eqvt)
done

lemma BINDINGn_elim:
  assumes a: "(x):M BINDINGn B (<B>)"
  shows "c P. (<c>:P)(<B>) SNa (M{x:=<c>.P})"
using a
apply(auto simp add: BINDINGn_def)
apply(auto simp add: ntrm.inject alpha)
apply(drule_tac x="[(x,xa)]c" in spec)
apply(drule_tac x="[(x,xa)]P" in spec)
apply(drule mp)
apply(drule_tac pi="[(x,xa)]" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(simp add: CAND_eqvt_name)
apply(drule_tac ?pi1.0="[(x,xa)]" in SNa_eqvt(1))
apply(perm_simp add: nsubst_eqvt)
done

lemma NOTRIGHT_elim:
  assumes a: "<a>:M NOTRIGHT (NOT B) ((B))"
  obtains x' M' where "M = NotR (x').M' a" and "fic (NotR (x').M' a) a" and "(x'):M' ((B))"
using a
apply(auto simp add: ctrm.inject alpha abs_fresh calc_atm)
apply(drule_tac x="x" in meta_spec)
apply(drule_tac x="[(a,aa)]Ma" in meta_spec)
apply(simp)
apply(drule meta_mp)
apply(drule_tac pi="[(a,aa)]" in fic.eqvt(2))
apply(simp add: calc_atm)
apply(drule meta_mp)
apply(drule_tac pi="[(a,aa)]" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(simp add: calc_atm CAND_eqvt_coname)
apply(simp)
done

lemma NOTLEFT_elim:
  assumes a: "(x):M NOTLEFT (NOT B) (<B>)"
  obtains a' M' where "M = NotL <a'>.M' x" and "fin (NotL <a'>.M' x) x" and "<a'>:M' (<B>)"
using a
apply(auto simp add: ntrm.inject alpha abs_fresh calc_atm)
apply(drule_tac x="a" in meta_spec)
apply(drule_tac x="[(x,xa)]Ma" in meta_spec)
apply(simp)
apply(drule meta_mp)
apply(drule_tac pi="[(x,xa)]" in fin.eqvt(1))
apply(simp add: calc_atm)
apply(drule meta_mp)
apply(drule_tac pi="[(x,xa)]" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(simp add: calc_atm CAND_eqvt_name)
apply(simp)
done

lemma ANDRIGHT_elim:
  assumes a: "<a>:M ANDRIGHT (B AND C) (<B>) (<C>)"
  obtains d' M' e' N' where "M = AndR <d'>.M' <e'>.N' a" and "fic (AndR <d'>.M' <e'>.N' a) a" 
                      and "<d'>:M' (<B>)" and "<e'>:N' (<C>)"
using a
apply(auto simp add: ctrm.inject alpha abs_fresh calc_atm fresh_atm)
apply(drule_tac x="c" in meta_spec)
apply(drule_tac x="[(a,c)]Ma" in meta_spec)
apply(drule_tac x="c" in meta_spec)
apply(drule_tac x="[(a,c)]N" in meta_spec)
apply(simp)
apply(drule meta_mp)
apply(drule_tac pi="[(a,c)]" in fic.eqvt(2))
apply(simp add: calc_atm)
apply(drule meta_mp)
apply(drule_tac pi="[(a,c)]" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(simp add: calc_atm CAND_eqvt_coname)
apply(drule meta_mp)
apply(drule_tac pi="[(a,c)]" and x="<a>:N" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(simp add: calc_atm CAND_eqvt_coname)
apply(simp)
apply(case_tac "a=b")
apply(simp)
apply(drule_tac x="c" in meta_spec)
apply(drule_tac x="[(b,c)]Ma" in meta_spec)
apply(drule_tac x="c" in meta_spec)
apply(drule_tac x="[(b,c)]N" in meta_spec)
apply(simp)
apply(drule meta_mp)
apply(drule_tac pi="[(b,c)]" in fic.eqvt(2))
apply(simp add: calc_atm)
apply(drule meta_mp)
apply(drule_tac pi="[(b,c)]" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(simp add: calc_atm CAND_eqvt_coname)
apply(drule meta_mp)
apply(drule_tac pi="[(b,c)]" and x="<b>:N" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(simp add: calc_atm CAND_eqvt_coname)
apply(simp)
apply(simp)
apply(case_tac "c=b")
apply(simp)
apply(drule_tac x="b" in meta_spec)
apply(drule_tac x="[(a,b)]Ma" in meta_spec)
apply(drule_tac x="a" in meta_spec)
apply(drule_tac x="[(a,b)]N" in meta_spec)
apply(simp)
apply(drule meta_mp)
apply(drule_tac pi="[(a,b)]" in fic.eqvt(2))
apply(simp add: calc_atm)
apply(drule meta_mp)
apply(drule_tac pi="[(a,b)]" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(simp add: calc_atm CAND_eqvt_coname)
apply(drule meta_mp)
apply(drule_tac pi="[(a,b)]" and x="<b>:N" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(simp add: calc_atm CAND_eqvt_coname)
apply(simp)
apply(simp)
apply(drule_tac x="c" in meta_spec)
apply(drule_tac x="[(a,c)]Ma" in meta_spec)
apply(drule_tac x="b" in meta_spec)
apply(drule_tac x="[(a,c)]N" in meta_spec)
apply(simp)
apply(drule meta_mp)
apply(drule_tac pi="[(a,c)]" in fic.eqvt(2))
apply(simp add: calc_atm)
apply(drule meta_mp)
apply(drule_tac pi="[(a,c)]" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(simp add: calc_atm CAND_eqvt_coname)
apply(drule meta_mp)
apply(drule_tac pi="[(a,c)]" and x="<b>:N" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(simp add: calc_atm CAND_eqvt_coname)
apply(simp)
apply(case_tac "a=aa")
apply(simp)
apply(drule_tac x="c" in meta_spec)
apply(drule_tac x="[(aa,c)]Ma" in meta_spec)
apply(drule_tac x="c" in meta_spec)
apply(drule_tac x="[(aa,c)]N" in meta_spec)
apply(simp)
apply(drule meta_mp)
apply(drule_tac pi="[(aa,c)]" in fic.eqvt(2))
apply(simp add: calc_atm)
apply(drule meta_mp)
apply(drule_tac pi="[(aa,c)]" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(simp add: calc_atm CAND_eqvt_coname)
apply(drule meta_mp)
apply(drule_tac pi="[(aa,c)]" and x="<aa>:N" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(simp add: calc_atm CAND_eqvt_coname)
apply(simp)
apply(simp)
apply(case_tac "c=aa")
apply(simp)
apply(drule_tac x="a" in meta_spec)
apply(drule_tac x="[(a,aa)]Ma" in meta_spec)
apply(drule_tac x="aa" in meta_spec)
apply(drule_tac x="[(a,aa)]N" in meta_spec)
apply(simp)
apply(drule meta_mp)
apply(drule_tac pi="[(a,aa)]" in fic.eqvt(2))
apply(simp add: calc_atm)
apply(drule meta_mp)
apply(drule_tac pi="[(a,aa)]" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(simp add: calc_atm CAND_eqvt_coname)
apply(drule meta_mp)
apply(drule_tac pi="[(a,aa)]" and x="<a>:N" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(simp add: calc_atm CAND_eqvt_coname)
apply(simp)
apply(simp)
apply(drule_tac x="aa" in meta_spec)
apply(drule_tac x="[(a,c)]Ma" in meta_spec)
apply(drule_tac x="c" in meta_spec)
apply(drule_tac x="[(a,c)]N" in meta_spec)
apply(simp)
apply(drule meta_mp)
apply(drule_tac pi="[(a,c)]" in fic.eqvt(2))
apply(simp add: calc_atm)
apply(drule meta_mp)
apply(drule_tac pi="[(a,c)]" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(simp add: calc_atm CAND_eqvt_coname)
apply(drule meta_mp)
apply(drule_tac pi="[(a,c)]" and x="<a>:N" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(simp add: calc_atm CAND_eqvt_coname)
apply(simp)
apply(case_tac "a=aa")
apply(simp)
apply(case_tac "aa=b")
apply(simp)
apply(drule_tac x="c" in meta_spec)
apply(drule_tac x="[(b,c)]Ma" in meta_spec)
apply(drule_tac x="c" in meta_spec)
apply(drule_tac x="[(b,c)]N" in meta_spec)
apply(simp)
apply(drule meta_mp)
apply(drule_tac pi="[(b,c)]" in fic.eqvt(2))
apply(simp add: calc_atm)
apply(drule meta_mp)
apply(drule_tac pi="[(b,c)]" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(simp add: calc_atm CAND_eqvt_coname)
apply(drule meta_mp)
apply(drule_tac pi="[(b,c)]" and x="<b>:N" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(simp add: calc_atm CAND_eqvt_coname)
apply(simp)
apply(simp)
apply(case_tac "c=b")
apply(simp)
apply(drule_tac x="b" in meta_spec)
apply(drule_tac x="[(aa,b)]Ma" in meta_spec)
apply(drule_tac x="aa" in meta_spec)
apply(drule_tac x="[(aa,b)]N" in meta_spec)
apply(simp)
apply(drule meta_mp)
apply(drule_tac pi="[(aa,b)]" in fic.eqvt(2))
apply(simp add: calc_atm)
apply(drule meta_mp)
apply(drule_tac pi="[(aa,b)]" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(simp add: calc_atm CAND_eqvt_coname)
apply(drule meta_mp)
apply(drule_tac pi="[(aa,b)]" and x="<b>:N" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(simp add: calc_atm CAND_eqvt_coname)
apply(simp)
apply(simp)
apply(drule_tac x="c" in meta_spec)
apply(drule_tac x="[(aa,c)]Ma" in meta_spec)
apply(drule_tac x="b" in meta_spec)
apply(drule_tac x="[(aa,c)]N" in meta_spec)
apply(simp)
apply(drule meta_mp)
apply(drule_tac pi="[(aa,c)]" in fic.eqvt(2))
apply(simp add: calc_atm)
apply(drule meta_mp)
apply(drule_tac pi="[(aa,c)]" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(simp add: calc_atm CAND_eqvt_coname)
apply(drule meta_mp)
apply(drule_tac pi="[(aa,c)]" and x="<b>:N" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(simp add: calc_atm CAND_eqvt_coname)
apply(simp)
apply(simp)
apply(case_tac "c=aa")
apply(simp)
apply(case_tac "a=b")
apply(simp)
apply(drule_tac x="b" in meta_spec)
apply(drule_tac x="[(b,aa)]Ma" in meta_spec)
apply(drule_tac x="aa" in meta_spec)
apply(drule_tac x="[(b,aa)]N" in meta_spec)
apply(simp)
apply(drule meta_mp)
apply(drule_tac pi="[(b,aa)]" in fic.eqvt(2))
apply(simp add: calc_atm)
apply(drule meta_mp)
apply(drule_tac pi="[(b,aa)]" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(simp add: calc_atm CAND_eqvt_coname)
apply(drule meta_mp)
apply(drule_tac pi="[(b,aa)]" and x="<b>:N" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(simp add: calc_atm CAND_eqvt_coname)
apply(simp)
apply(simp)
apply(case_tac "aa=b")
apply(simp)
apply(drule_tac x="a" in meta_spec)
apply(drule_tac x="[(a,b)]Ma" in meta_spec)
apply(drule_tac x="a" in meta_spec)
apply(drule_tac x="[(a,b)]N" in meta_spec)
apply(simp)
apply(drule meta_mp)
apply(drule_tac pi="[(a,b)]" in fic.eqvt(2))
apply(simp add: calc_atm)
apply(drule meta_mp)
apply(drule_tac pi="[(a,b)]" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(simp add: calc_atm CAND_eqvt_coname)
apply(drule meta_mp)
apply(drule_tac pi="[(a,b)]" and x="<b>:N" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(simp add: calc_atm CAND_eqvt_coname)
apply(simp)
apply(simp)
apply(drule_tac x="a" in meta_spec)
apply(drule_tac x="[(a,aa)]Ma" in meta_spec)
apply(drule_tac x="b" in meta_spec)
apply(drule_tac x="[(a,aa)]N" in meta_spec)
apply(simp)
apply(drule meta_mp)
apply(drule_tac pi="[(a,aa)]" in fic.eqvt(2))
apply(simp add: calc_atm)
apply(drule meta_mp)
apply(drule_tac pi="[(a,aa)]" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(simp add: calc_atm CAND_eqvt_coname)
apply(drule meta_mp)
apply(drule_tac pi="[(a,aa)]" and x="<b>:N" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(simp add: calc_atm CAND_eqvt_coname)
apply(simp)
apply(simp)
apply(case_tac "a=b")
apply(simp)
apply(drule_tac x="aa" in meta_spec)
apply(drule_tac x="[(b,c)]Ma" in meta_spec)
apply(drule_tac x="c" in meta_spec)
apply(drule_tac x="[(b,c)]N" in meta_spec)
apply(simp)
apply(drule meta_mp)
apply(drule_tac pi="[(b,c)]" in fic.eqvt(2))
apply(simp add: calc_atm)
apply(drule meta_mp)
apply(drule_tac pi="[(b,c)]" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(simp add: calc_atm CAND_eqvt_coname)
apply(drule meta_mp)
apply(drule_tac pi="[(b,c)]" and x="<b>:N" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(simp add: calc_atm CAND_eqvt_coname)
apply(simp)
apply(simp)
apply(case_tac "c=b")
apply(simp)
apply(drule_tac x="aa" in meta_spec)
apply(drule_tac x="[(a,b)]Ma" in meta_spec)
apply(drule_tac x="a" in meta_spec)
apply(drule_tac x="[(a,b)]N" in meta_spec)
apply(simp)
apply(drule meta_mp)
apply(drule_tac pi="[(a,b)]" in fic.eqvt(2))
apply(simp add: calc_atm)
apply(drule meta_mp)
apply(drule_tac pi="[(a,b)]" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(simp add: calc_atm CAND_eqvt_coname)
apply(drule meta_mp)
apply(drule_tac pi="[(a,b)]" and x="<b>:N" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(simp add: calc_atm CAND_eqvt_coname)
apply(simp)
apply(simp)
apply(drule_tac x="aa" in meta_spec)
apply(drule_tac x="[(a,c)]Ma" in meta_spec)
apply(drule_tac x="b" in meta_spec)
apply(drule_tac x="[(a,c)]N" in meta_spec)
apply(simp)
apply(drule meta_mp)
apply(drule_tac pi="[(a,c)]" in fic.eqvt(2))
apply(simp add: calc_atm)
apply(drule meta_mp)
apply(drule_tac pi="[(a,c)]" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(simp add: calc_atm CAND_eqvt_coname)
apply(drule meta_mp)
apply(drule_tac pi="[(a,c)]" and x="<b>:N" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(simp add: calc_atm CAND_eqvt_coname)
apply(simp)
done 

lemma ANDLEFT1_elim:
  assumes a: "(x):M ANDLEFT1 (B AND C) ((B))"
  obtains x' M' where "M = AndL1 (x').M' x" and "fin (AndL1 (x').M' x) x" and "(x'):M' ((B))"
using a [[ hypsubst_thin = true ]]
apply(auto simp add: ntrm.inject alpha abs_fresh calc_atm)
apply(drule_tac x="y" in meta_spec)
apply(drule_tac x="[(x,y)]M" in meta_spec)
apply(simp)
apply(drule meta_mp)
apply(drule_tac pi="[(x,y)]" in fin.eqvt(1))
apply(simp add: calc_atm)
apply(drule meta_mp)
apply(drule_tac pi="[(x,y)]" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(simp add: calc_atm CAND_eqvt_name)
apply(simp)
apply(case_tac "x=xa")
apply(simp)
apply(drule_tac x="y" in meta_spec)
apply(drule_tac x="[(xa,y)]M" in meta_spec)
apply(simp)
apply(drule meta_mp)
apply(drule_tac pi="[(xa,y)]" in fin.eqvt(1))
apply(simp add: calc_atm)
apply(drule meta_mp)
apply(drule_tac pi="[(xa,y)]" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(simp add: calc_atm CAND_eqvt_name)
apply(simp)
apply(simp)
apply(case_tac "y=xa")
apply(simp)
apply(drule_tac x="x" in meta_spec)
apply(drule_tac x="[(x,xa)]M" in meta_spec)
apply(simp)
apply(drule meta_mp)
apply(drule_tac pi="[(x,xa)]" in fin.eqvt(1))
apply(simp add: calc_atm)
apply(drule meta_mp)
apply(drule_tac pi="[(x,xa)]" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(simp add: calc_atm CAND_eqvt_name)
apply(simp)
apply(simp)
apply(drule_tac x="xa" in meta_spec)
apply(drule_tac x="[(x,y)]M" in meta_spec)
apply(simp)
apply(drule meta_mp)
apply(drule_tac pi="[(x,y)]" in fin.eqvt(1))
apply(simp add: calc_atm)
apply(drule meta_mp)
apply(drule_tac pi="[(x,y)]" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(simp add: calc_atm CAND_eqvt_name)
apply(simp)
done

lemma ANDLEFT2_elim:
  assumes a: "(x):M ANDLEFT2 (B AND C) ((C))"
  obtains x' M' where "M = AndL2 (x').M' x" and "fin (AndL2 (x').M' x) x" and "(x'):M' ((C))"
using a [[ hypsubst_thin = true ]]
apply(auto simp add: ntrm.inject alpha abs_fresh calc_atm)
apply(drule_tac x="y" in meta_spec)
apply(drule_tac x="[(x,y)]M" in meta_spec)
apply(simp)
apply(drule meta_mp)
apply(drule_tac pi="[(x,y)]" in fin.eqvt(1))
apply(simp add: calc_atm)
apply(drule meta_mp)
apply(drule_tac pi="[(x,y)]" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(simp add: calc_atm CAND_eqvt_name)
apply(simp)
apply(case_tac "x=xa")
apply(simp)
apply(drule_tac x="y" in meta_spec)
apply(drule_tac x="[(xa,y)]M" in meta_spec)
apply(simp)
apply(drule meta_mp)
apply(drule_tac pi="[(xa,y)]" in fin.eqvt(1))
apply(simp add: calc_atm)
apply(drule meta_mp)
apply(drule_tac pi="[(xa,y)]" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(simp add: calc_atm CAND_eqvt_name)
apply(simp)
apply(simp)
apply(case_tac "y=xa")
apply(simp)
apply(drule_tac x="x" in meta_spec)
apply(drule_tac x="[(x,xa)]M" in meta_spec)
apply(simp)
apply(drule meta_mp)
apply(drule_tac pi="[(x,xa)]" in fin.eqvt(1))
apply(simp add: calc_atm)
apply(drule meta_mp)
apply(drule_tac pi="[(x,xa)]" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(simp add: calc_atm CAND_eqvt_name)
apply(simp)
apply(simp)
apply(drule_tac x="xa" in meta_spec)
apply(drule_tac x="[(x,y)]M" in meta_spec)
apply(simp)
apply(drule meta_mp)
apply(drule_tac pi="[(x,y)]" in fin.eqvt(1))
apply(simp add: calc_atm)
apply(drule meta_mp)
apply(drule_tac pi="[(x,y)]" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(simp add: calc_atm CAND_eqvt_name)
apply(simp)
done

lemma ORRIGHT1_elim:
  assumes a: "<a>:M ORRIGHT1 (B OR C) (<B>)"
  obtains a' M' where "M = OrR1 <a'>.M' a" and "fic (OrR1 <a'>.M' a) a" and "<a'>:M' (<B>)"
using a
apply(auto simp add: ctrm.inject alpha abs_fresh calc_atm)
apply(drule_tac x="b" in meta_spec)
apply(drule_tac x="[(a,b)]Ma" in meta_spec)
apply(simp)
apply(drule meta_mp)
apply(drule_tac pi="[(a,b)]" in fic.eqvt(2))
apply(simp add: calc_atm)
apply(drule meta_mp)
apply(drule_tac pi="[(a,b)]" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(simp add: calc_atm CAND_eqvt_coname)
apply(simp)
apply(case_tac "a=aa")
apply(simp)
apply(drule_tac x="b" in meta_spec)
apply(drule_tac x="[(aa,b)]Ma" in meta_spec)
apply(simp)
apply(drule meta_mp)
apply(drule_tac pi="[(aa,b)]" in fic.eqvt(2))
apply(simp add: calc_atm)
apply(drule meta_mp)
apply(drule_tac pi="[(aa,b)]" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(simp add: calc_atm CAND_eqvt_coname)
apply(simp)
apply(simp)
apply(case_tac "b=aa")
apply(simp)
apply(drule_tac x="a" in meta_spec)
apply(drule_tac x="[(a,aa)]Ma" in meta_spec)
apply(simp)
apply(drule meta_mp)
apply(drule_tac pi="[(a,aa)]" in fic.eqvt(2))
apply(simp add: calc_atm)
apply(drule meta_mp)
apply(drule_tac pi="[(a,aa)]" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(simp add: calc_atm CAND_eqvt_coname)
apply(simp)
apply(simp)
apply(drule_tac x="aa" in meta_spec)
apply(drule_tac x="[(a,b)]Ma" in meta_spec)
apply(simp)
apply(drule meta_mp)
apply(drule_tac pi="[(a,b)]" in fic.eqvt(2))
apply(simp add: calc_atm)
apply(drule meta_mp)
apply(drule_tac pi="[(a,b)]" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(simp add: calc_atm CAND_eqvt_coname)
apply(simp)
done

lemma ORRIGHT2_elim:
  assumes a: "<a>:M ORRIGHT2 (B OR C) (<C>)"
  obtains a' M' where "M = OrR2 <a'>.M' a" and "fic (OrR2 <a'>.M' a) a" and "<a'>:M' (<C>)"
using a
apply(auto simp add: ctrm.inject alpha abs_fresh calc_atm)
apply(drule_tac x="b" in meta_spec)
apply(drule_tac x="[(a,b)]Ma" in meta_spec)
apply(simp)
apply(drule meta_mp)
apply(drule_tac pi="[(a,b)]" in fic.eqvt(2))
apply(simp add: calc_atm)
apply(drule meta_mp)
apply(drule_tac pi="[(a,b)]" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(simp add: calc_atm CAND_eqvt_coname)
apply(simp)
apply(case_tac "a=aa")
apply(simp)
apply(drule_tac x="b" in meta_spec)
apply(drule_tac x="[(aa,b)]Ma" in meta_spec)
apply(simp)
apply(drule meta_mp)
apply(drule_tac pi="[(aa,b)]" in fic.eqvt(2))
apply(simp add: calc_atm)
apply(drule meta_mp)
apply(drule_tac pi="[(aa,b)]" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(simp add: calc_atm CAND_eqvt_coname)
apply(simp)
apply(simp)
apply(case_tac "b=aa")
apply(simp)
apply(drule_tac x="a" in meta_spec)
apply(drule_tac x="[(a,aa)]Ma" in meta_spec)
apply(simp)
apply(drule meta_mp)
apply(drule_tac pi="[(a,aa)]" in fic.eqvt(2))
apply(simp add: calc_atm)
apply(drule meta_mp)
apply(drule_tac pi="[(a,aa)]" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(simp add: calc_atm CAND_eqvt_coname)
apply(simp)
apply(simp)
apply(drule_tac x="aa" in meta_spec)
apply(drule_tac x="[(a,b)]Ma" in meta_spec)
apply(simp)
apply(drule meta_mp)
apply(drule_tac pi="[(a,b)]" in fic.eqvt(2))
apply(simp add: calc_atm)
apply(drule meta_mp)
apply(drule_tac pi="[(a,b)]" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(simp add: calc_atm CAND_eqvt_coname)
apply(simp)
done

lemma ORLEFT_elim:
  assumes a: "(x):M ORLEFT (B OR C) ((B)) ((C))"
  obtains y' M' z' N' where "M = OrL (y').M' (z').N' x" and "fin (OrL (y').M' (z').N' x) x" 
                      and "(y'):M' ((B))" and "(z'):N' ((C))"
using a
apply(auto simp add: ntrm.inject alpha abs_fresh calc_atm fresh_atm)
apply(drule_tac x="z" in meta_spec)
apply(drule_tac x="[(x,z)]Ma" in meta_spec)
apply(drule_tac x="z" in meta_spec)
apply(drule_tac x="[(x,z)]N" in meta_spec)
apply(simp)
apply(drule meta_mp)
apply(drule_tac pi="[(x,z)]" in fin.eqvt(1))
apply(simp add: calc_atm)
apply(drule meta_mp)
apply(drule_tac pi="[(x,z)]" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(simp add: calc_atm CAND_eqvt_name)
apply(drule meta_mp)
apply(drule_tac pi="[(x,z)]" and x="(x):N" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(simp add: calc_atm CAND_eqvt_name)
apply(simp)
apply(case_tac "x=y")
apply(simp)
apply(drule_tac x="z" in meta_spec)
apply(drule_tac x="[(y,z)]Ma" in meta_spec)
apply(drule_tac x="z" in meta_spec)
apply(drule_tac x="[(y,z)]N" in meta_spec)
apply(simp)
apply(drule meta_mp)
apply(drule_tac pi="[(y,z)]" in fin.eqvt(1))
apply(simp add: calc_atm)
apply(drule meta_mp)
apply(drule_tac pi="[(y,z)]" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(simp add: calc_atm CAND_eqvt_name)
apply(drule meta_mp)
apply(drule_tac pi="[(y,z)]" and x="(y):N" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(simp add: calc_atm CAND_eqvt_name)
apply(simp)
apply(simp)
apply(case_tac "z=y")
apply(simp)
apply(drule_tac x="y" in meta_spec)
apply(drule_tac x="[(x,y)]Ma" in meta_spec)
apply(drule_tac x="x" in meta_spec)
apply(drule_tac x="[(x,y)]N" in meta_spec)
apply(simp)
apply(drule meta_mp)
apply(drule_tac pi="[(x,y)]" in fin.eqvt(1))
apply(simp add: calc_atm)
apply(drule meta_mp)
apply(drule_tac pi="[(x,y)]" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(simp add: calc_atm CAND_eqvt_name)
apply(drule meta_mp)
apply(drule_tac pi="[(x,y)]" and x="(y):N" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(simp add: calc_atm CAND_eqvt_name)
apply(simp)
apply(simp)
apply(drule_tac x="z" in meta_spec)
apply(drule_tac x="[(x,z)]Ma" in meta_spec)
apply(drule_tac x="y" in meta_spec)
apply(drule_tac x="[(x,z)]N" in meta_spec)
apply(simp)
apply(drule meta_mp)
apply(drule_tac pi="[(x,z)]" in fin.eqvt(1))
apply(simp add: calc_atm)
apply(drule meta_mp)
apply(drule_tac pi="[(x,z)]" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(simp add: calc_atm CAND_eqvt_name)
apply(drule meta_mp)
apply(drule_tac pi="[(x,z)]" and x="(y):N" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(simp add: calc_atm CAND_eqvt_name)
apply(simp)
apply(case_tac "x=xa")
apply(simp)
apply(drule_tac x="z" in meta_spec)
apply(drule_tac x="[(xa,z)]Ma" in meta_spec)
apply(drule_tac x="z" in meta_spec)
apply(drule_tac x="[(xa,z)]N" in meta_spec)
apply(simp)
apply(drule meta_mp)
apply(drule_tac pi="[(xa,z)]" in fin.eqvt(1))
apply(simp add: calc_atm)
apply(drule meta_mp)
apply(drule_tac pi="[(xa,z)]" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(simp add: calc_atm CAND_eqvt_name)
apply(drule meta_mp)
apply(drule_tac pi="[(xa,z)]" and x="(xa):N" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(simp add: calc_atm CAND_eqvt_name)
apply(simp)
apply(simp)
apply(case_tac "z=xa")
apply(simp)
apply(drule_tac x="x" in meta_spec)
apply(drule_tac x="[(x,xa)]Ma" in meta_spec)
apply(drule_tac x="xa" in meta_spec)
apply(drule_tac x="[(x,xa)]N" in meta_spec)
apply(simp)
apply(drule meta_mp)
apply(drule_tac pi="[(x,xa)]" in fin.eqvt(1))
apply(simp add: calc_atm)
apply(drule meta_mp)
apply(drule_tac pi="[(x,xa)]" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(simp add: calc_atm CAND_eqvt_name)
apply(drule meta_mp)
apply(drule_tac pi="[(x,xa)]" and x="(x):N" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(simp add: calc_atm CAND_eqvt_name)
apply(simp)
apply(simp)
apply(drule_tac x="xa" in meta_spec)
apply(drule_tac x="[(x,z)]Ma" in meta_spec)
apply(drule_tac x="z" in meta_spec)
apply(drule_tac x="[(x,z)]N" in meta_spec)
apply(simp)
apply(drule meta_mp)
apply(drule_tac pi="[(x,z)]" in fin.eqvt(1))
apply(simp add: calc_atm)
apply(drule meta_mp)
apply(drule_tac pi="[(x,z)]" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(simp add: calc_atm CAND_eqvt_name)
apply(drule meta_mp)
apply(drule_tac pi="[(x,z)]" and x="(x):N" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(simp add: calc_atm CAND_eqvt_name)
apply(simp)
apply(case_tac "x=xa")
apply(simp)
apply(case_tac "xa=y")
apply(simp)
apply(drule_tac x="z" in meta_spec)
apply(drule_tac x="[(y,z)]Ma" in meta_spec)
apply(drule_tac x="z" in meta_spec)
apply(drule_tac x="[(y,z)]N" in meta_spec)
apply(simp)
apply(drule meta_mp)
apply(drule_tac pi="[(y,z)]" in fin.eqvt(1))
apply(simp add: calc_atm)
apply(drule meta_mp)
apply(drule_tac pi="[(y,z)]" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(simp add: calc_atm CAND_eqvt_name)
apply(drule meta_mp)
apply(drule_tac pi="[(y,z)]" and x="(y):N" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(simp add: calc_atm CAND_eqvt_name)
apply(simp)
apply(simp)
apply(case_tac "z=y")
apply(simp)
apply(drule_tac x="y" in meta_spec)
apply(drule_tac x="[(xa,y)]Ma" in meta_spec)
apply(drule_tac x="xa" in meta_spec)
apply(drule_tac x="[(xa,y)]N" in meta_spec)
apply(simp)
apply(drule meta_mp)
apply(drule_tac pi="[(xa,y)]" in fin.eqvt(1))
apply(simp add: calc_atm)
apply(drule meta_mp)
apply(drule_tac pi="[(xa,y)]" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(simp add: calc_atm CAND_eqvt_name)
apply(drule meta_mp)
apply(drule_tac pi="[(xa,y)]" and x="(y):N" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(simp add: calc_atm CAND_eqvt_name)
apply(simp)
apply(simp)
apply(drule_tac x="z" in meta_spec)
apply(drule_tac x="[(xa,z)]Ma" in meta_spec)
apply(drule_tac x="y" in meta_spec)
apply(drule_tac x="[(xa,z)]N" in meta_spec)
apply(simp)
apply(drule meta_mp)
apply(drule_tac pi="[(xa,z)]" in fin.eqvt(1))
apply(simp add: calc_atm)
apply(drule meta_mp)
apply(drule_tac pi="[(xa,z)]" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(simp add: calc_atm CAND_eqvt_name)
apply(drule meta_mp)
apply(drule_tac pi="[(xa,z)]" and x="(y):N" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(simp add: calc_atm CAND_eqvt_name)
apply(simp)
apply(simp)
apply(case_tac "z=xa")
apply(simp)
apply(case_tac "x=y")
apply(simp)
apply(drule_tac x="y" in meta_spec)
apply(drule_tac x="[(y,xa)]Ma" in meta_spec)
apply(drule_tac x="xa" in meta_spec)
apply(drule_tac x="[(y,xa)]N" in meta_spec)
apply(simp)
apply(drule meta_mp)
apply(drule_tac pi="[(y,xa)]" in fin.eqvt(1))
apply(simp add: calc_atm)
apply(drule meta_mp)
apply(drule_tac pi="[(y,xa)]" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(simp add: calc_atm CAND_eqvt_name)
apply(drule meta_mp)
apply(drule_tac pi="[(y,xa)]" and x="(y):N" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(simp add: calc_atm CAND_eqvt_name)
apply(simp)
apply(simp)
apply(case_tac "xa=y")
apply(simp)
apply(drule_tac x="x" in meta_spec)
apply(drule_tac x="[(x,y)]Ma" in meta_spec)
apply(drule_tac x="x" in meta_spec)
apply(drule_tac x="[(x,y)]N" in meta_spec)
apply(simp)
apply(drule meta_mp)
apply(drule_tac pi="[(x,y)]" in fin.eqvt(1))
apply(simp add: calc_atm)
apply(drule meta_mp)
apply(drule_tac pi="[(x,y)]" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(simp add: calc_atm CAND_eqvt_name)
apply(drule meta_mp)
apply(drule_tac pi="[(x,y)]" and x="(y):N" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(simp add: calc_atm CAND_eqvt_name)
apply(simp)
apply(simp)
apply(drule_tac x="x" in meta_spec)
apply(drule_tac x="[(x,xa)]Ma" in meta_spec)
apply(drule_tac x="y" in meta_spec)
apply(drule_tac x="[(x,xa)]N" in meta_spec)
apply(simp)
apply(drule meta_mp)
apply(drule_tac pi="[(x,xa)]" in fin.eqvt(1))
apply(simp add: calc_atm)
apply(drule meta_mp)
apply(drule_tac pi="[(x,xa)]" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(simp add: calc_atm CAND_eqvt_name)
apply(drule meta_mp)
apply(drule_tac pi="[(x,xa)]" and x="(y):N" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(simp add: calc_atm CAND_eqvt_name)
apply(simp)
apply(simp)
apply(case_tac "x=y")
apply(simp)
apply(drule_tac x="xa" in meta_spec)
apply(drule_tac x="[(y,z)]Ma" in meta_spec)
apply(drule_tac x="z" in meta_spec)
apply(drule_tac x="[(y,z)]N" in meta_spec)
apply(simp)
apply(drule meta_mp)
apply(drule_tac pi="[(y,z)]" in fin.eqvt(1))
apply(simp add: calc_atm)
apply(drule meta_mp)
apply(drule_tac pi="[(y,z)]" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(simp add: calc_atm CAND_eqvt_name)
apply(drule meta_mp)
apply(drule_tac pi="[(y,z)]" and x="(y):N" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(simp add: calc_atm CAND_eqvt_name)
apply(simp)
apply(simp)
apply(case_tac "z=y")
apply(simp)
apply(drule_tac x="xa" in meta_spec)
apply(drule_tac x="[(x,y)]Ma" in meta_spec)
apply(drule_tac x="x" in meta_spec)
apply(drule_tac x="[(x,y)]N" in meta_spec)
apply(simp)
apply(drule meta_mp)
apply(drule_tac pi="[(x,y)]" in fin.eqvt(1))
apply(simp add: calc_atm)
apply(drule meta_mp)
apply(drule_tac pi="[(x,y)]" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(simp add: calc_atm CAND_eqvt_name)
apply(drule meta_mp)
apply(drule_tac pi="[(x,y)]" and x="(y):N" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(simp add: calc_atm CAND_eqvt_name)
apply(simp)
apply(simp)
apply(drule_tac x="xa" in meta_spec)
apply(drule_tac x="[(x,z)]Ma" in meta_spec)
apply(drule_tac x="y" in meta_spec)
apply(drule_tac x="[(x,z)]N" in meta_spec)
apply(simp)
apply(drule meta_mp)
apply(drule_tac pi="[(x,z)]" in fin.eqvt(1))
apply(simp add: calc_atm)
apply(drule meta_mp)
apply(drule_tac pi="[(x,z)]" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(simp add: calc_atm CAND_eqvt_name)
apply(drule meta_mp)
apply(drule_tac pi="[(x,z)]" and x="(y):N" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(simp add: calc_atm CAND_eqvt_name)
apply(simp)
done

lemma IMPRIGHT_elim:
  assumes a: "<a>:M IMPRIGHT (B IMP C) ((B)) (<C>) ((C)) (<B>)"
  obtains x' a' M' where "M = ImpR (x').<a'>.M' a" and "fic (ImpR (x').<a'>.M' a) a" 
                   and "z P. x'(z,P) (z):P (C) (x'):(M'{a':=(z).P}) (B)" 
                   and "c Q. a'(c,Q) <c>:Q <B> <a'>:(M'{x':=<c>.Q}) <C>"
using a
apply(auto simp add: ctrm.inject alpha abs_fresh calc_atm)
apply(drule_tac x="x" in meta_spec)
apply(drule_tac x="b" in meta_spec)
apply(drule_tac x="[(a,b)]Ma" in meta_spec)
apply(simp)
apply(drule_tac pi="[(a,b)]" in fic.eqvt(2))
apply(simp add: calc_atm)
apply(drule meta_mp)
apply(auto)[1]
apply(drule_tac pi="[(a,b)]" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(simp add: calc_atm CAND_eqvt_coname)
apply(drule_tac x="z" in spec)
apply(drule_tac x="[(a,b)]P" in spec)
apply(simp add: fresh_prod fresh_left calc_atm)
apply(drule_tac pi="[(a,b)]" and x="(x):Ma{a:=(z).([(a,b)]P)}" 
                                     in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(perm_simp add: calc_atm csubst_eqvt CAND_eqvt_coname)
apply(drule meta_mp)
apply(auto)[1]
apply(drule_tac pi="[(a,b)]" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(simp add:  CAND_eqvt_coname)
apply(rotate_tac 2)
apply(drule_tac x="[(a,b)]c" in spec)
apply(drule_tac x="[(a,b)]Q" in spec)
apply(simp add: fresh_prod fresh_left)
apply(drule mp)
apply(simp add: calc_atm)
apply(drule_tac pi="[(a,b)]" and x="<a>:Ma{x:=<([(a,b)]c)>.([(a,b)]Q)}" 
                                        in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(perm_simp add: nsubst_eqvt CAND_eqvt_coname)
apply(simp add: calc_atm)
apply(case_tac "a=aa")
apply(simp)
apply(drule_tac x="x" in meta_spec)
apply(drule_tac x="b" in meta_spec)
apply(drule_tac x="[(aa,b)]Ma" in meta_spec)
apply(simp)
apply(drule meta_mp)
apply(drule_tac pi="[(aa,b)]" in fic.eqvt(2))
apply(simp add: calc_atm)
apply(drule meta_mp)
apply(auto)[1]
apply(drule_tac pi="[(a,b)]" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(simp add: calc_atm CAND_eqvt_coname)
apply(drule_tac x="z" in spec)
apply(drule_tac x="[(a,b)]P" in spec)
apply(simp add: fresh_prod fresh_left calc_atm)
apply(drule_tac pi="[(a,b)]" and x="(x):Ma{a:=(z).([(a,b)]P)}" 
                                     in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(perm_simp add: calc_atm csubst_eqvt  CAND_eqvt_coname)
apply(drule meta_mp)
apply(auto)[1]
apply(drule_tac pi="[(a,b)]" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(simp add: CAND_eqvt_coname)
apply(drule_tac x="[(a,b)]c" in spec)
apply(drule_tac x="[(a,b)]Q" in spec)
apply(simp)
apply(simp add: fresh_prod fresh_left)
apply(drule mp)
apply(simp add: calc_atm)
apply(drule_tac pi="[(a,b)]" and x="<a>:Ma{x:=<([(a,b)]c)>.([(a,b)]Q)}" 
                                      in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(perm_simp add: nsubst_eqvt CAND_eqvt_coname)
apply(simp add: calc_atm)
apply(simp)
apply(case_tac "b=aa")
apply(simp)
apply(drule_tac x="x" in meta_spec)
apply(drule_tac x="a" in meta_spec)
apply(drule_tac x="[(a,aa)]Ma" in meta_spec)
apply(simp)
apply(drule meta_mp)
apply(drule_tac pi="[(a,aa)]" in fic.eqvt(2))
apply(simp add: calc_atm)
apply(drule meta_mp)
apply(auto)[1]
apply(drule_tac pi="[(a,aa)]" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(simp add: calc_atm CAND_eqvt_coname)
apply(drule_tac x="z" in spec)
apply(drule_tac x="[(a,aa)]P" in spec)
apply(simp add: fresh_prod fresh_left calc_atm)
apply(drule_tac pi="[(a,aa)]" and x="(x):Ma{aa:=(z).([(a,aa)]P)}" 
                                    in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(perm_simp add: calc_atm csubst_eqvt  CAND_eqvt_coname)
apply(drule meta_mp)
apply(auto)[1]
apply(drule_tac pi="[(a,aa)]" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(simp add:  CAND_eqvt_coname)
apply(drule_tac x="[(a,aa)]c" in spec)
apply(drule_tac x="[(a,aa)]Q" in spec)
apply(simp)
apply(simp add: fresh_prod fresh_left)
apply(drule mp)
apply(simp add: calc_atm)
apply(drule_tac pi="[(a,aa)]" and x="<aa>:Ma{x:=<([(a,aa)]c)>.([(a,aa)]Q)}" 
                                    in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(perm_simp add: nsubst_eqvt  CAND_eqvt_coname)
apply(simp add: calc_atm)
apply(simp)
apply(drule_tac x="x" in meta_spec)
apply(drule_tac x="aa" in meta_spec)
apply(drule_tac x="[(a,b)]Ma" in meta_spec)
apply(simp)
apply(drule meta_mp)
apply(drule_tac pi="[(a,b)]" in fic.eqvt(2))
apply(simp add: calc_atm)
apply(drule meta_mp)
apply(auto)[1]
apply(drule_tac pi="[(a,b)]" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(simp add: calc_atm  CAND_eqvt_coname)
apply(drule_tac x="z" in spec)
apply(drule_tac x="[(a,b)]P" in spec)
apply(simp add: fresh_prod fresh_left calc_atm)
apply(drule_tac pi="[(a,b)]" and x="(x):Ma{aa:=(z).([(a,b)]P)}" 
                                          in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(perm_simp add: calc_atm csubst_eqvt  CAND_eqvt_coname)
apply(drule meta_mp)
apply(auto)[1]
apply(drule_tac pi="[(a,b)]" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(simp add:  CAND_eqvt_coname)
apply(drule_tac x="[(a,b)]c" in spec)
apply(drule_tac x="[(a,b)]Q" in spec)
apply(simp add: fresh_prod fresh_left)
apply(drule mp)
apply(simp add: calc_atm)
apply(drule_tac pi="[(a,b)]" and x="<aa>:Ma{x:=<([(a,b)]c)>.([(a,b)]Q)}" 
                                        in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(perm_simp add: nsubst_eqvt  CAND_eqvt_coname)
apply(simp add: calc_atm)
done

lemma IMPLEFT_elim:
  assumes a: "(x):M IMPLEFT (B IMP C) (<B>) ((C))"
  obtains x' a' M' N' where "M = ImpL <a'>.M' (x').N' x" and "fin (ImpL <a'>.M' (x').N' x) x" 
                   and "<a'>:M' <B>" and "(x'):N' (C)"
using a
apply(auto simp add: ntrm.inject alpha abs_fresh calc_atm)
apply(drule_tac x="a" in meta_spec)
apply(drule_tac x="[(x,y)]Ma" in meta_spec)
apply(drule_tac x="y" in meta_spec)
apply(drule_tac x="[(x,y)]N" in meta_spec)
apply(simp)
apply(drule meta_mp)
apply(drule_tac pi="[(x,y)]" in fin.eqvt(1))
apply(simp add: calc_atm)
apply(drule meta_mp)
apply(drule_tac pi="[(x,y)]" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(simp add: calc_atm CAND_eqvt_name)
apply(drule meta_mp)
apply(drule_tac pi="[(x,y)]" and x="(x):N" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(perm_simp add: calc_atm  CAND_eqvt_name)
apply(simp)
apply(case_tac "x=xa")
apply(simp)
apply(drule_tac x="a" in meta_spec)
apply(drule_tac x="[(xa,y)]Ma" in meta_spec)
apply(drule_tac x="y" in meta_spec)
apply(drule_tac x="[(xa,y)]N" in meta_spec)
apply(simp)
apply(drule meta_mp)
apply(drule_tac pi="[(xa,y)]" in fin.eqvt(1))
apply(simp add: calc_atm)
apply(drule meta_mp)
apply(drule_tac pi="[(xa,y)]" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(simp add: calc_atm CAND_eqvt_name)
apply(drule meta_mp)
apply(drule_tac pi="[(xa,y)]" and x="(xa):N" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(simp add: calc_atm CAND_eqvt_name)
apply(simp)
apply(simp)
apply(case_tac "y=xa")
apply(simp)
apply(drule_tac x="a" in meta_spec)
apply(drule_tac x="[(x,xa)]Ma" in meta_spec)
apply(drule_tac x="x" in meta_spec)
apply(drule_tac x="[(x,xa)]N" in meta_spec)
apply(simp)
apply(drule meta_mp)
apply(drule_tac pi="[(x,xa)]" in fin.eqvt(1))
apply(simp add: calc_atm)
apply(drule meta_mp)
apply(drule_tac pi="[(x,xa)]" and x="<a>:Ma" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(simp add: calc_atm  CAND_eqvt_name)
apply(drule meta_mp)
apply(drule_tac pi="[(x,xa)]" and x="(xa):N" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(simp add: calc_atm CAND_eqvt_name)
apply(simp)
apply(simp)
apply(drule_tac x="a" in meta_spec)
apply(drule_tac x="[(x,y)]Ma" in meta_spec)
apply(drule_tac x="xa" in meta_spec)
apply(drule_tac x="[(x,y)]N" in meta_spec)
apply(simp)
apply(drule meta_mp)
apply(drule_tac pi="[(x,y)]" in fin.eqvt(1))
apply(simp add: calc_atm)
apply(drule meta_mp)
apply(drule_tac pi="[(x,y)]" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(simp add: calc_atm CAND_eqvt_name)
apply(drule meta_mp)
apply(drule_tac pi="[(x,y)]" and x="(xa):N" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(simp add: calc_atm CAND_eqvt_name)
apply(simp)
done

lemma CANDs_alpha:
  shows "<a>:M (<B>) ==> [a].M = [b].N ==> <b>:N (<B>)"
  and   "(x):M ((B)) ==> [x].M = [y].N ==> (y):N ((B))"
apply(auto simp add: alpha)
apply(drule_tac pi="[(a,b)]" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(perm_simp add: CAND_eqvt_coname calc_atm)
apply(drule_tac pi="[(x,y)]" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(perm_simp add: CAND_eqvt_name calc_atm)
done

lemma CAND_NotR_elim:
  assumes a: "<a>:NotR (x).M a (<B>)" "<a>:NotR (x).M a BINDINGc B ((B))"
  shows "B'. B = NOT B' (x):M ((B'))" 
using a
apply(nominal_induct B rule: ty.strong_induct)
apply(simp_all add: ty.inject AXIOMSc_def ctrm.inject alpha)
apply(auto intro: CANDs_alpha simp add: trm.inject calc_atm abs_fresh fresh_atm)
apply(drule_tac pi="[(a,aa)]" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(auto simp add: CAND_eqvt_coname calc_atm intro: CANDs_alpha)
done

lemma CAND_NotL_elim_aux:
  assumes a: "(x):NotL <a>.M x NEGn B (<B>)" "(x):NotL <a>.M x BINDINGn B (<B>)"
  shows "B'. B = NOT B' <a>:M (<B'>)" 
using a
apply(nominal_induct B rule: ty.strong_induct)
apply(simp_all add: ty.inject AXIOMSn_def ntrm.inject alpha)
apply(auto intro: CANDs_alpha simp add: trm.inject calc_atm abs_fresh fresh_atm)
apply(drule_tac pi="[(x,xa)]" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(auto simp add: CAND_eqvt_name calc_atm intro: CANDs_alpha)
done

lemmas CAND_NotL_elim = CAND_NotL_elim_aux[OF NEG_elim(2)]

lemma CAND_AndR_elim:
  assumes a: "<a>:AndR <b>.M <c>.N a (<B>)" "<a>:AndR <b>.M <c>.N a BINDINGc B ((B))"
  shows "B1 B2. B = B1 AND B2 <b>:M (<B1>) <c>:N (<B2>)" 
using a
apply(nominal_induct B rule: ty.strong_induct)
apply(simp_all add: ty.inject AXIOMSc_def ctrm.inject alpha)
apply(auto intro: CANDs_alpha simp add: trm.inject calc_atm abs_fresh fresh_atm)
apply(drule_tac pi="[(a,ca)]" and x="<a>:Ma" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(simp add: CAND_eqvt_coname calc_atm)
apply(auto intro: CANDs_alpha)[1]
apply(drule_tac pi="[(a,ca)]" and x="<a>:Na" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(simp add: CAND_eqvt_coname calc_atm)
apply(auto intro: CANDs_alpha)[1]
apply(drule_tac pi="[(a,ca)]" and x="<a>:Ma" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(simp add: CAND_eqvt_coname calc_atm)
apply(auto intro: CANDs_alpha)[1]
apply(case_tac "a=ba")
apply(simp)
apply(drule_tac pi="[(ba,ca)]" and x="<ba>:Na" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(simp add: CAND_eqvt_coname calc_atm)
apply(auto intro: CANDs_alpha)[1]
apply(simp)
apply(case_tac "ca=ba")
apply(simp)
apply(drule_tac pi="[(a,ba)]" and x="<ba>:Na" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(simp add: CAND_eqvt_coname calc_atm)
apply(auto intro: CANDs_alpha)[1]
apply(simp)
apply(drule_tac pi="[(a,ca)]" and x="<ba>:Na" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(simp add: CAND_eqvt_coname calc_atm)
apply(auto intro: CANDs_alpha)[1]
apply(case_tac "a=aa")
apply(simp)
apply(drule_tac pi="[(aa,ca)]" and x="<aa>:Ma" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(simp add: CAND_eqvt_coname calc_atm)
apply(auto intro: CANDs_alpha)[1]
apply(simp)
apply(case_tac "ca=aa")
apply(simp)
apply(drule_tac pi="[(a,aa)]" and x="<aa>:Ma" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(simp add: CAND_eqvt_coname calc_atm)
apply(auto intro: CANDs_alpha)[1]
apply(simp)
apply(drule_tac pi="[(a,ca)]" and x="<aa>:Ma" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(simp add: CAND_eqvt_coname calc_atm)
apply(auto intro: CANDs_alpha)[1]
apply(drule_tac pi="[(a,ca)]" and x="<a>:Na" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(simp add: CAND_eqvt_coname calc_atm)
apply(auto intro: CANDs_alpha)[1]
apply(case_tac "a=aa")
apply(simp)
apply(drule_tac pi="[(aa,ca)]" and x="<aa>:Ma" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(simp add: CAND_eqvt_coname calc_atm)
apply(auto intro: CANDs_alpha)[1]
apply(simp)
apply(case_tac "ca=aa")
apply(simp)
apply(drule_tac pi="[(a,aa)]" and x="<aa>:Ma" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(simp add: CAND_eqvt_coname calc_atm)
apply(auto intro: CANDs_alpha)[1]
apply(simp)
apply(drule_tac pi="[(a,ca)]" and x="<aa>:Ma" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(simp add: CAND_eqvt_coname calc_atm)
apply(auto intro: CANDs_alpha)[1]
apply(case_tac "a=ba")
apply(simp)
apply(drule_tac pi="[(ba,ca)]" and x="<ba>:Na" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(simp add: CAND_eqvt_coname calc_atm)
apply(auto intro: CANDs_alpha)[1]
apply(simp)
apply(case_tac "ca=ba")
apply(simp)
apply(drule_tac pi="[(a,ba)]" and x="<ba>:Na" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(simp add: CAND_eqvt_coname calc_atm)
apply(auto intro: CANDs_alpha)[1]
apply(simp)
apply(drule_tac pi="[(a,ca)]" and x="<ba>:Na" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(simp add: CAND_eqvt_coname calc_atm)
apply(auto intro: CANDs_alpha)[1]
done

lemma CAND_OrR1_elim:
  assumes a: "<a>:OrR1 <b>.M a (<B>)" "<a>:OrR1 <b>.M a BINDINGc B ((B))"
  shows "B1 B2. B = B1 OR B2 <b>:M (<B1>)" 
using a
apply(nominal_induct B rule: ty.strong_induct)
apply(simp_all add: ty.inject AXIOMSc_def ctrm.inject alpha)
apply(auto intro: CANDs_alpha simp add: trm.inject calc_atm abs_fresh fresh_atm)
apply(drule_tac pi="[(a,ba)]" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(auto simp add: CAND_eqvt_coname calc_atm intro: CANDs_alpha)
apply(case_tac "a=aa")
apply(simp)
apply(drule_tac pi="[(aa,ba)]" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(auto simp add: CAND_eqvt_coname calc_atm intro: CANDs_alpha)
apply(case_tac "ba=aa")
apply(simp)
apply(drule_tac pi="[(a,aa)]" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(auto simp add: CAND_eqvt_coname calc_atm intro: CANDs_alpha)
apply(drule_tac pi="[(a,ba)]" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(auto simp add: CAND_eqvt_coname calc_atm intro: CANDs_alpha)
done

lemma CAND_OrR2_elim:
  assumes a: "<a>:OrR2 <b>.M a (<B>)" "<a>:OrR2 <b>.M a BINDINGc B ((B))"
  shows "B1 B2. B = B1 OR B2 <b>:M (<B2>)" 
using a
apply(nominal_induct B rule: ty.strong_induct)
apply(simp_all add: ty.inject AXIOMSc_def ctrm.inject alpha)
apply(auto intro: CANDs_alpha simp add: trm.inject calc_atm abs_fresh fresh_atm)
apply(drule_tac pi="[(a,ba)]" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(auto simp add: CAND_eqvt_coname calc_atm intro: CANDs_alpha)
apply(case_tac "a=aa")
apply(simp)
apply(drule_tac pi="[(aa,ba)]" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(auto simp add: CAND_eqvt_coname calc_atm intro: CANDs_alpha)
apply(case_tac "ba=aa")
apply(simp)
apply(drule_tac pi="[(a,aa)]" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(auto simp add: CAND_eqvt_coname calc_atm intro: CANDs_alpha)
apply(drule_tac pi="[(a,ba)]" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(auto simp add: CAND_eqvt_coname calc_atm intro: CANDs_alpha)
done

lemma CAND_OrL_elim_aux:
  assumes a: "(x):(OrL (y).M (z).N x) NEGn B (<B>)" "(x):(OrL (y).M (z).N x) BINDINGn B (<B>)"
  shows "B1 B2. B = B1 OR B2 (y):M ((B1)) (z):N ((B2))" 
using a
apply(nominal_induct B rule: ty.strong_induct)
apply(simp_all add: ty.inject AXIOMSn_def ntrm.inject alpha)
apply(auto intro: CANDs_alpha simp add: trm.inject calc_atm abs_fresh fresh_atm)
apply(drule_tac pi="[(x,za)]" and x="(x):Ma" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(simp add: CAND_eqvt_name calc_atm)
apply(auto intro: CANDs_alpha)[1]
apply(drule_tac pi="[(x,za)]" and x="(x):Na" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(simp add: CAND_eqvt_name calc_atm)
apply(auto intro: CANDs_alpha)[1]
apply(drule_tac pi="[(x,za)]" and x="(x):Ma" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(simp add: CAND_eqvt_name calc_atm)
apply(auto intro: CANDs_alpha)[1]
apply(case_tac "x=ya")
apply(simp)
apply(drule_tac pi="[(ya,za)]" and x="(ya):Na" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(simp add: CAND_eqvt_name calc_atm)
apply(auto intro: CANDs_alpha)[1]
apply(simp)
apply(case_tac "za=ya")
apply(simp)
apply(drule_tac pi="[(x,ya)]" and x="(ya):Na" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(simp add: CAND_eqvt_name calc_atm)
apply(auto intro: CANDs_alpha)[1]
apply(simp)
apply(drule_tac pi="[(x,za)]" and x="(ya):Na" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(simp add: CAND_eqvt_name calc_atm)
apply(auto intro: CANDs_alpha)[1]
apply(case_tac "x=xa")
apply(simp)
apply(drule_tac pi="[(xa,za)]" and x="(xa):Ma" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(simp add: CAND_eqvt_name calc_atm)
apply(auto intro: CANDs_alpha)[1]
apply(simp)
apply(case_tac "za=xa")
apply(simp)
apply(drule_tac pi="[(x,xa)]" and x="(xa):Ma" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(simp add: CAND_eqvt_name calc_atm)
apply(auto intro: CANDs_alpha)[1]
apply(simp)
apply(drule_tac pi="[(x,za)]" and x="(xa):Ma" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(simp add: CAND_eqvt_name calc_atm)
apply(auto intro: CANDs_alpha)[1]
apply(drule_tac pi="[(x,za)]" and x="(x):Na" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(simp add: CAND_eqvt_name calc_atm)
apply(auto intro: CANDs_alpha)[1]
apply(case_tac "x=xa")
apply(simp)
apply(drule_tac pi="[(xa,za)]" and x="(xa):Ma" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(simp add: CAND_eqvt_name calc_atm)
apply(auto intro: CANDs_alpha)[1]
apply(simp)
apply(case_tac "za=xa")
apply(simp)
apply(drule_tac pi="[(x,xa)]" and x="(xa):Ma" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(simp add: CAND_eqvt_name calc_atm)
apply(auto intro: CANDs_alpha)[1]
apply(simp)
apply(drule_tac pi="[(x,za)]" and x="(xa):Ma" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(simp add: CAND_eqvt_name calc_atm)
apply(auto intro: CANDs_alpha)[1]
apply(case_tac "x=ya")
apply(simp)
apply(drule_tac pi="[(ya,za)]" and x="(ya):Na" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(simp add: CAND_eqvt_name calc_atm)
apply(auto intro: CANDs_alpha)[1]
apply(simp)
apply(case_tac "za=ya")
apply(simp)
apply(drule_tac pi="[(x,ya)]" and x="(ya):Na" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(simp add: CAND_eqvt_name calc_atm)
apply(auto intro: CANDs_alpha)[1]
apply(simp)
apply(drule_tac pi="[(x,za)]" and x="(ya):Na" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(simp add: CAND_eqvt_name calc_atm)
apply(auto intro: CANDs_alpha)[1]
done

lemmas CAND_OrL_elim = CAND_OrL_elim_aux[OF NEG_elim(2)]

lemma CAND_AndL1_elim_aux:
  assumes a: "(x):(AndL1 (y).M x) NEGn B (<B>)" "(x):(AndL1 (y).M x) BINDINGn B (<B>)"
  shows "B1 B2. B = B1 AND B2 (y):M ((B1))" 
using a
apply(nominal_induct B rule: ty.strong_induct)
apply(simp_all add: ty.inject AXIOMSn_def ntrm.inject alpha)
apply(auto intro: CANDs_alpha simp add: trm.inject calc_atm abs_fresh fresh_atm)
apply(drule_tac pi="[(x,ya)]" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(auto simp add: CAND_eqvt_name calc_atm intro: CANDs_alpha)
apply(case_tac "x=xa")
apply(simp)
apply(drule_tac pi="[(xa,ya)]" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(auto simp add: CAND_eqvt_name calc_atm intro: CANDs_alpha)
apply(case_tac "ya=xa")
apply(simp)
apply(drule_tac pi="[(x,xa)]" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(auto simp add: CAND_eqvt_name calc_atm intro: CANDs_alpha)
apply(drule_tac pi="[(x,ya)]" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(auto simp add: CAND_eqvt_name calc_atm intro: CANDs_alpha)
done

lemmas CAND_AndL1_elim = CAND_AndL1_elim_aux[OF NEG_elim(2)]

lemma CAND_AndL2_elim_aux:
  assumes a: "(x):(AndL2 (y).M x) NEGn B (<B>)" "(x):(AndL2 (y).M x) BINDINGn B (<B>)"
  shows "B1 B2. B = B1 AND B2 (y):M ((B2))" 
using a
apply(nominal_induct B rule: ty.strong_induct)
apply(simp_all add: ty.inject AXIOMSn_def ntrm.inject alpha)
apply(auto intro: CANDs_alpha simp add: trm.inject calc_atm abs_fresh fresh_atm)
apply(drule_tac pi="[(x,ya)]" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(auto simp add: CAND_eqvt_name calc_atm intro: CANDs_alpha)
apply(case_tac "x=xa")
apply(simp)
apply(drule_tac pi="[(xa,ya)]" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(auto simp add: CAND_eqvt_name calc_atm intro: CANDs_alpha)
apply(case_tac "ya=xa")
apply(simp)
apply(drule_tac pi="[(x,xa)]" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(auto simp add: CAND_eqvt_name calc_atm intro: CANDs_alpha)
apply(drule_tac pi="[(x,ya)]" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(auto simp add: CAND_eqvt_name calc_atm intro: CANDs_alpha)
done

lemmas CAND_AndL2_elim = CAND_AndL2_elim_aux[OF NEG_elim(2)]

lemma CAND_ImpL_elim_aux:
  assumes a: "(x):(ImpL <a>.M (z).N x) NEGn B (<B>)" "(x):(ImpL <a>.M (z).N x) BINDINGn B (<B>)"
  shows "B1 B2. B = B1 IMP B2 <a>:M (<B1>) (z):N ((B2))" 
using a
apply(nominal_induct B rule: ty.strong_induct)
apply(simp_all add: ty.inject AXIOMSn_def ntrm.inject alpha)
apply(auto intro: CANDs_alpha simp add: trm.inject calc_atm abs_fresh fresh_atm)
apply(drule_tac pi="[(x,y)]" and x="<aa>:Ma" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(simp add: CAND_eqvt_name calc_atm)
apply(auto intro: CANDs_alpha)[1]
apply(drule_tac pi="[(x,y)]" and x="(x):Na" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(simp add: CAND_eqvt_name calc_atm)
apply(auto intro: CANDs_alpha)[1]
apply(drule_tac pi="[(x,y)]" and x="<aa>:Ma" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(simp add: CAND_eqvt_name calc_atm)
apply(auto intro: CANDs_alpha)[1]
apply(case_tac "x=xa")
apply(simp)
apply(drule_tac pi="[(xa,y)]" and x="(xa):Na" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(simp add: CAND_eqvt_name calc_atm)
apply(auto intro: CANDs_alpha)[1]
apply(simp)
apply(case_tac "y=xa")
apply(simp)
apply(drule_tac pi="[(x,xa)]" and x="(xa):Na" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(simp add: CAND_eqvt_name calc_atm)
apply(auto intro: CANDs_alpha)[1]
apply(simp)
apply(drule_tac pi="[(x,y)]" and x="(xa):Na" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(simp add: CAND_eqvt_name calc_atm)
apply(auto intro: CANDs_alpha)[1]
done

lemmas CAND_ImpL_elim = CAND_ImpL_elim_aux[OF NEG_elim(2)]

lemma CAND_ImpR_elim:
  assumes a: "<a>:ImpR (x).<b>.M a (<B>)" "<a>:ImpR (x).<b>.M a BINDINGc B ((B))"
  shows "B1 B2. B = B1 IMP B2
                 (z P. x(z,P) (z):P (B2) (x):(M{b:=(z).P}) (B1))
                 (c Q. b(c,Q) <c>:Q <B1> <b>:(M{x:=<c>.Q}) <B2>)" 
using a
apply(nominal_induct B rule: ty.strong_induct)
apply(simp_all add: ty.inject AXIOMSc_def ctrm.inject alpha)
apply(auto intro: CANDs_alpha simp add: trm.inject calc_atm abs_fresh fresh_atm fresh_prod fresh_bij)
apply(generate_fresh "name"
apply(generate_fresh "coname")
apply(drule_tac a="ca" and z="c" in alpha_name_coname)
apply(simp) 
apply(simp) 
apply(simp) 
apply(drule_tac x="[(xa,c)][(aa,ca)][(b,ca)][(x,c)]z" in spec)
apply(drule_tac x="[(xa,c)][(aa,ca)][(b,ca)][(x,c)]P" in spec)
apply(drule mp)
apply(rule conjI)
apply(auto simp add: calc_atm fresh_prod fresh_atm)[1]
apply(rule conjI)
apply(auto simp add: fresh_left calc_atm fresh_prod fresh_atm)[1]
apply(drule_tac pi="[(x,c)]" and X="(ty2)" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(simp add: CAND_eqvt_name CAND_eqvt_coname)
apply(drule_tac pi="[(b,ca)]" and X="(ty2)" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(simp add: CAND_eqvt_name CAND_eqvt_coname)
apply(drule_tac pi="[(aa,ca)]" and X="(ty2)" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(simp add: CAND_eqvt_name CAND_eqvt_coname)
apply(drule_tac pi="[(xa,c)]" and X="(ty2)" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(simp add: CAND_eqvt_name CAND_eqvt_coname)
apply(drule_tac pi="[(xa,c)]" and X="(ty1)" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt)
apply(drule_tac pi="[(aa,ca)]" and X="(ty1)" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt)
apply(drule_tac pi="[(b,ca)]" and X="(ty1)" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(simp add: CAND_eqvt_name CAND_eqvt_coname)
apply(drule_tac pi="[(x,c)]" and X="(ty1)" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(perm_simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt)
apply(generate_fresh "name")
apply(generate_fresh "coname")
apply(drule_tac a="cb" and z="ca" in alpha_name_coname)
apply(simp)
apply(simp)
apply(simp)
apply(drule_tac x="[(xa,ca)][(aa,cb)][(b,cb)][(x,ca)]c" in spec)
apply(drule_tac x="[(xa,ca)][(aa,cb)][(b,cb)][(x,ca)]Q" in spec)
apply(drule mp)
apply(rule conjI)
apply(auto simp add: calc_atm fresh_prod fresh_atm)[1]
apply(rule conjI)
apply(auto simp add: fresh_left calc_atm fresh_prod fresh_atm)[1]
apply(drule_tac pi="[(x,ca)]" and X="<ty1>" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(simp add: CAND_eqvt_name CAND_eqvt_coname)
apply(drule_tac pi="[(b,cb)]" and X="<ty1>" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(simp add: CAND_eqvt_name CAND_eqvt_coname)
apply(drule_tac pi="[(aa,cb)]" and X="<ty1>" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(simp add: CAND_eqvt_name CAND_eqvt_coname)
apply(drule_tac pi="[(xa,ca)]" and X="<ty1>" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(simp add: CAND_eqvt_name CAND_eqvt_coname)
apply(drule_tac pi="[(xa,ca)]" and X="<ty2>" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt)
apply(drule_tac pi="[(aa,cb)]" and X="<ty2>" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt)
apply(drule_tac pi="[(b,cb)]" and X="<ty2>" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(simp add: CAND_eqvt_name CAND_eqvt_coname)
apply(drule_tac pi="[(x,ca)]" and X="<ty2>" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(perm_simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt)
apply(generate_fresh "name")
apply(generate_fresh "coname")
apply(drule_tac a="ca" and z="c" in alpha_name_coname)
apply(simp add: fresh_left calc_atm fresh_prod fresh_atm)
apply(simp add: fresh_left calc_atm fresh_prod fresh_atm)
apply(auto)[1]
apply(simp)
apply(drule_tac x="[(a,ba)][(xa,c)][(ba,ca)][(b,ca)][(x,c)]z" in spec)
apply(drule_tac x="[(a,ba)][(xa,c)][(ba,ca)][(b,ca)][(x,c)]P" in spec)
apply(drule mp)
apply(rule conjI)
apply(auto simp add: calc_atm fresh_prod fresh_atm)[1]
apply(rule conjI)
apply(auto simp add: fresh_left calc_atm fresh_prod fresh_atm)[1]
apply(drule_tac pi="[(x,c)]" and X="(ty2)" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(simp add: CAND_eqvt_name CAND_eqvt_coname)
apply(drule_tac pi="[(b,ca)]" and X="(ty2)" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(simp add: CAND_eqvt_name CAND_eqvt_coname)
apply(drule_tac pi="[(ba,ca)]" and X="(ty2)" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(simp add: CAND_eqvt_name CAND_eqvt_coname)
apply(drule_tac pi="[(xa,c)]" and X="(ty2)" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(simp add: CAND_eqvt_name CAND_eqvt_coname)
apply(drule_tac pi="[(a,ba)]" and X="(ty2)" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(simp add: CAND_eqvt_name CAND_eqvt_coname)
apply(drule_tac pi="[(a,ba)]" and X="(ty1)" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt)
apply(drule_tac pi="[(xa,c)]" and X="(ty1)" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt)
apply(drule_tac pi="[(ba,ca)]" and X="(ty1)" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt)
apply(drule_tac pi="[(b,ca)]" and X="(ty1)" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(simp add: CAND_eqvt_name CAND_eqvt_coname)
apply(drule_tac pi="[(x,c)]" and X="(ty1)" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(perm_simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt)
apply(generate_fresh "name")
apply(generate_fresh "coname")
apply(drule_tac a="cb" and z="ca" in alpha_name_coname)
apply(simp add: fresh_left calc_atm fresh_prod fresh_atm)
apply(simp add: fresh_left calc_atm fresh_prod fresh_atm)
apply(auto)[1]
apply(simp)
apply(drule_tac x="[(a,ba)][(xa,ca)][(ba,cb)][(b,cb)][(x,ca)]c" in spec)
apply(drule_tac x="[(a,ba)][(xa,ca)][(ba,cb)][(b,cb)][(x,ca)]Q" in spec)
apply(drule mp)
apply(rule conjI)
apply(auto simp add: calc_atm fresh_prod fresh_atm)[1]
apply(rule conjI)
apply(auto simp add: fresh_left calc_atm fresh_prod fresh_atm)[1]
apply(drule_tac pi="[(x,ca)]" and X="<ty1>" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(simp add: CAND_eqvt_name CAND_eqvt_coname)
apply(drule_tac pi="[(b,cb)]" and X="<ty1>" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(simp add: CAND_eqvt_name CAND_eqvt_coname)
apply(drule_tac pi="[(ba,cb)]" and X="<ty1>" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(simp add: CAND_eqvt_name CAND_eqvt_coname)
apply(drule_tac pi="[(xa,ca)]" and X="<ty1>" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(simp add: CAND_eqvt_name CAND_eqvt_coname)
apply(drule_tac pi="[(a,ba)]" and X="<ty1>" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(simp add: CAND_eqvt_name CAND_eqvt_coname)
apply(drule_tac pi="[(a,ba)]" and X="<ty2>" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt)
apply(drule_tac pi="[(xa,ca)]" and X="<ty2>" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt)
apply(drule_tac pi="[(ba,cb)]" and X="<ty2>" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt)
apply(drule_tac pi="[(b,cb)]" and X="<ty2>" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(simp add: CAND_eqvt_name CAND_eqvt_coname)
apply(drule_tac pi="[(x,ca)]" and X="<ty2>" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(perm_simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt)
apply(case_tac "a=aa")
apply(simp)
apply(generate_fresh "name")
apply(generate_fresh "coname")
apply(drule_tac a="ca" and z="c" in alpha_name_coname)
apply(simp add: fresh_left calc_atm fresh_prod fresh_atm)
apply(simp add: fresh_left calc_atm fresh_prod fresh_atm)
apply(auto)[1]
apply(simp)
apply(drule_tac x="[(aa,ba)][(xa,c)][(ba,ca)][(b,ca)][(x,c)]z" in spec)
apply(drule_tac x="[(aa,ba)][(xa,c)][(ba,ca)][(b,ca)][(x,c)]P" in spec)
apply(drule mp)
apply(rule conjI)
apply(auto simp add: calc_atm fresh_prod fresh_atm)[1]
apply(rule conjI)
apply(auto simp add: fresh_left calc_atm fresh_prod fresh_atm)[1]
apply(drule_tac pi="[(x,c)]" and X="(ty2)" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(simp add: CAND_eqvt_name CAND_eqvt_coname)
apply(drule_tac pi="[(b,ca)]" and X="(ty2)" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(simp add: CAND_eqvt_name CAND_eqvt_coname)
apply(drule_tac pi="[(ba,ca)]" and X="(ty2)" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(simp add: CAND_eqvt_name CAND_eqvt_coname)
apply(drule_tac pi="[(xa,c)]" and X="(ty2)" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(simp add: CAND_eqvt_name CAND_eqvt_coname)
apply(drule_tac pi="[(aa,ba)]" and X="(ty2)" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(simp add: CAND_eqvt_name CAND_eqvt_coname)
apply(drule_tac pi="[(aa,ba)]" and X="(ty1)" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt)
apply(drule_tac pi="[(xa,c)]" and X="(ty1)" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt)
apply(drule_tac pi="[(ba,ca)]" and X="(ty1)" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt)
apply(drule_tac pi="[(b,ca)]" and X="(ty1)" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(simp add: CAND_eqvt_name CAND_eqvt_coname)
apply(drule_tac pi="[(x,c)]" and X="(ty1)" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(perm_simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt)
apply(simp)
apply(case_tac "ba=aa")
apply(simp)
apply(generate_fresh "name")
apply(generate_fresh "coname")
apply(drule_tac a="ca" and z="c" in alpha_name_coname)
apply(simp add: fresh_left calc_atm fresh_prod fresh_atm)
apply(simp add: fresh_left calc_atm fresh_prod fresh_atm)
apply(auto)[1]
apply(simp)
apply(drule_tac x="[(a,aa)][(xa,c)][(a,ca)][(b,ca)][(x,c)]z" in spec)
apply(drule_tac x="[(a,aa)][(xa,c)][(a,ca)][(b,ca)][(x,c)]P" in spec)
apply(drule mp)
apply(rule conjI)
apply(auto simp add: calc_atm fresh_prod fresh_atm)[1]
apply(rule conjI)
apply(auto simp add: fresh_left calc_atm fresh_prod fresh_atm)[1]
apply(drule_tac pi="[(x,c)]" and X="(ty2)" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(simp add: CAND_eqvt_name CAND_eqvt_coname)
apply(drule_tac pi="[(b,ca)]" and X="(ty2)" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(simp add: CAND_eqvt_name CAND_eqvt_coname)
apply(drule_tac pi="[(a,ca)]" and X="(ty2)" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(simp add: CAND_eqvt_name CAND_eqvt_coname)
apply(drule_tac pi="[(xa,c)]" and X="(ty2)" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(simp add: CAND_eqvt_name CAND_eqvt_coname)
apply(drule_tac pi="[(a,aa)]" and X="(ty2)" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(simp add: CAND_eqvt_name CAND_eqvt_coname)
apply(drule_tac pi="[(a,aa)]" and X="(ty1)" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt)
apply(drule_tac pi="[(xa,c)]" and X="(ty1)" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt)
apply(drule_tac pi="[(a,ca)]" and X="(ty1)" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt)
apply(drule_tac pi="[(b,ca)]" and X="(ty1)" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(simp add: CAND_eqvt_name CAND_eqvt_coname)
apply(drule_tac pi="[(x,c)]" and X="(ty1)" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(perm_simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt)
apply(simp)
apply(generate_fresh "name")
apply(generate_fresh "coname")
apply(drule_tac a="ca" and z="c" in alpha_name_coname)
apply(simp add: fresh_left calc_atm fresh_prod fresh_atm)
apply(simp add: fresh_left calc_atm fresh_prod fresh_atm)
apply(auto)[1]
apply(simp)
apply(drule_tac x="[(a,ba)][(xa,c)][(aa,ca)][(b,ca)][(x,c)]z" in spec)
apply(drule_tac x="[(a,ba)][(xa,c)][(aa,ca)][(b,ca)][(x,c)]P" in spec)
apply(drule mp)
apply(rule conjI)
apply(auto simp add: calc_atm fresh_prod fresh_atm)[1]
apply(rule conjI)
apply(auto simp add: fresh_left calc_atm fresh_prod fresh_atm)[1]
apply(drule_tac pi="[(x,c)]" and X="(ty2)" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(simp add: CAND_eqvt_name CAND_eqvt_coname)
apply(drule_tac pi="[(b,ca)]" and X="(ty2)" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(simp add: CAND_eqvt_name CAND_eqvt_coname)
apply(drule_tac pi="[(aa,ca)]" and X="(ty2)" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(simp add: CAND_eqvt_name CAND_eqvt_coname)
apply(drule_tac pi="[(xa,c)]" and X="(ty2)" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(simp add: CAND_eqvt_name CAND_eqvt_coname)
apply(drule_tac pi="[(a,ba)]" and X="(ty2)" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(simp add: CAND_eqvt_name CAND_eqvt_coname)
apply(drule_tac pi="[(a,ba)]" and X="(ty1)" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt)
apply(drule_tac pi="[(xa,c)]" and X="(ty1)" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt)
apply(drule_tac pi="[(aa,ca)]" and X="(ty1)" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt)
apply(drule_tac pi="[(b,ca)]" and X="(ty1)" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(simp add: CAND_eqvt_name CAND_eqvt_coname)
apply(drule_tac pi="[(x,c)]" and X="(ty1)" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(perm_simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt)
apply(case_tac "a=aa")
apply(simp)
apply(generate_fresh "name")
apply(generate_fresh "coname")
apply(drule_tac a="cb" and z="ca" in alpha_name_coname)
apply(simp add: fresh_left calc_atm fresh_prod fresh_atm)
apply(simp add: fresh_left calc_atm fresh_prod fresh_atm)
apply(auto)[1]
apply(simp)
apply(drule_tac x="[(aa,ba)][(xa,ca)][(ba,cb)][(b,cb)][(x,ca)]c" in spec)
apply(drule_tac x="[(aa,ba)][(xa,ca)][(ba,cb)][(b,cb)][(x,ca)]Q" in spec)
apply(drule mp)
apply(rule conjI)
apply(auto simp add: calc_atm fresh_prod fresh_atm)[1]
apply(rule conjI)
apply(auto simp add: fresh_left calc_atm fresh_prod fresh_atm)[1]
apply(drule_tac pi="[(x,ca)]" and X="<ty1>" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(simp add: CAND_eqvt_name CAND_eqvt_coname)
apply(drule_tac pi="[(b,cb)]" and X="<ty1>" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(simp add: CAND_eqvt_name CAND_eqvt_coname)
apply(drule_tac pi="[(ba,cb)]" and X="<ty1>" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(simp add: CAND_eqvt_name CAND_eqvt_coname)
apply(drule_tac pi="[(xa,ca)]" and X="<ty1>" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(simp add: CAND_eqvt_name CAND_eqvt_coname)
apply(drule_tac pi="[(aa,ba)]" and X="<ty1>" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(simp add: CAND_eqvt_name CAND_eqvt_coname)
apply(drule_tac pi="[(aa,ba)]" and X="<ty2>" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt)
apply(drule_tac pi="[(xa,ca)]" and X="<ty2>" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt)
apply(drule_tac pi="[(ba,cb)]" and X="<ty2>" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt)
apply(drule_tac pi="[(b,cb)]" and X="<ty2>" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(simp add: CAND_eqvt_name CAND_eqvt_coname)
apply(drule_tac pi="[(x,ca)]" and X="<ty2>" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(perm_simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt)
apply(simp)
apply(case_tac "ba=aa")
apply(simp)
apply(generate_fresh "name")
apply(generate_fresh "coname")
apply(drule_tac a="cb" and z="ca" in alpha_name_coname)
apply(simp add: fresh_left calc_atm fresh_prod fresh_atm)
apply(simp add: fresh_left calc_atm fresh_prod fresh_atm)
apply(auto)[1]
apply(simp)
apply(drule_tac x="[(a,aa)][(xa,ca)][(a,cb)][(b,cb)][(x,ca)]c" in spec)
apply(drule_tac x="[(a,aa)][(xa,ca)][(a,cb)][(b,cb)][(x,ca)]Q" in spec)
apply(drule mp)
apply(rule conjI)
apply(auto simp add: calc_atm fresh_prod fresh_atm)[1]
apply(rule conjI)
apply(auto simp add: fresh_left calc_atm fresh_prod fresh_atm)[1]
apply(drule_tac pi="[(x,ca)]" and X="<ty1>" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(simp add: CAND_eqvt_name CAND_eqvt_coname)
apply(drule_tac pi="[(b,cb)]" and X="<ty1>" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(simp add: CAND_eqvt_name CAND_eqvt_coname)
apply(drule_tac pi="[(a,cb)]" and X="<ty1>" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(simp add: CAND_eqvt_name CAND_eqvt_coname)
apply(drule_tac pi="[(xa,ca)]" and X="<ty1>" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(simp add: CAND_eqvt_name CAND_eqvt_coname)
apply(drule_tac pi="[(a,aa)]" and X="<ty1>" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(simp add: CAND_eqvt_name CAND_eqvt_coname)
apply(drule_tac pi="[(a,aa)]" and X="<ty2>" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt)
apply(drule_tac pi="[(xa,ca)]" and X="<ty2>" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt)
apply(drule_tac pi="[(a,cb)]" and X="<ty2>" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt)
apply(drule_tac pi="[(b,cb)]" and X="<ty2>" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(simp add: CAND_eqvt_name CAND_eqvt_coname)
apply(drule_tac pi="[(x,ca)]" and X="<ty2>" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(perm_simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt)
apply(simp)
apply(generate_fresh "name")
apply(generate_fresh "coname")
apply(drule_tac a="cb" and z="ca" in alpha_name_coname)
apply(simp add: fresh_left calc_atm fresh_prod fresh_atm)
apply(simp add: fresh_left calc_atm fresh_prod fresh_atm)
apply(auto)[1]
apply(simp)
apply(drule_tac x="[(a,ba)][(xa,ca)][(aa,cb)][(b,cb)][(x,ca)]c" in spec)
apply(drule_tac x="[(a,ba)][(xa,ca)][(aa,cb)][(b,cb)][(x,ca)]Q" in spec)
apply(drule mp)
apply(rule conjI)
apply(auto simp add: calc_atm fresh_prod fresh_atm)[1]
apply(rule conjI)
apply(auto simp add: fresh_left calc_atm fresh_prod fresh_atm)[1]
apply(drule_tac pi="[(x,ca)]" and X="<ty1>" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(simp add: CAND_eqvt_name CAND_eqvt_coname)
apply(drule_tac pi="[(b,cb)]" and X="<ty1>" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(simp add: CAND_eqvt_name CAND_eqvt_coname)
apply(drule_tac pi="[(aa,cb)]" and X="<ty1>" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(simp add: CAND_eqvt_name CAND_eqvt_coname)
apply(drule_tac pi="[(xa,ca)]" and X="<ty1>" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(simp add: CAND_eqvt_name CAND_eqvt_coname)
apply(drule_tac pi="[(a,ba)]" and X="<ty1>" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(simp add: CAND_eqvt_name CAND_eqvt_coname)
apply(drule_tac pi="[(a,ba)]" and X="<ty2>" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt)
apply(drule_tac pi="[(xa,ca)]" and X="<ty2>" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt)
apply(drule_tac pi="[(aa,cb)]" and X="<ty2>" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt)
apply(drule_tac pi="[(b,cb)]" and X="<ty2>" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(simp add: CAND_eqvt_name CAND_eqvt_coname)
apply(drule_tac pi="[(x,ca)]" and X="<ty2>" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(perm_simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt)
done

text Main lemma 1

lemma AXIOMS_imply_SNa:
  shows "<a>:M AXIOMSc B ==> SNa M"
  and   "(x):M AXIOMSn B ==> SNa M"
apply -
apply(auto simp add: AXIOMSn_def AXIOMSc_def ntrm.inject ctrm.inject alpha)
apply(rule Ax_in_SNa)+
done

lemma BINDING_imply_SNa:
  shows "<a>:M BINDINGc B ((B)) ==> SNa M"
  and   "(x):M BINDINGn B (<B>) ==> SNa M"
apply -
apply(auto simp add: BINDINGn_def BINDINGc_def ntrm.inject ctrm.inject alpha)
apply(drule_tac x="x" in spec)
apply(drule_tac x="Ax x a" in spec)
apply(drule mp)
apply(rule Ax_in_CANDs)
apply(drule a_star_preserves_SNa)
apply(rule subst_with_ax2)
apply(simp add: crename_id)
apply(drule_tac x="x" in spec)
apply(drule_tac x="Ax x aa" in spec)
apply(drule mp)
apply(rule Ax_in_CANDs)
apply(drule a_star_preserves_SNa)
apply(rule subst_with_ax2)
apply(simp add: crename_id SNa_eqvt)
apply(drule_tac x="a" in spec)
apply(drule_tac x="Ax x a" in spec)
apply(drule mp)
apply(rule Ax_in_CANDs)
apply(drule a_star_preserves_SNa)
apply(rule subst_with_ax1)
apply(simp add: nrename_id)
apply(drule_tac x="a" in spec)
apply(drule_tac x="Ax xa a" in spec)
apply(drule mp)
apply(rule Ax_in_CANDs)
apply(drule a_star_preserves_SNa)
apply(rule subst_with_ax1)
apply(simp add: nrename_id SNa_eqvt)
done

lemma CANDs_imply_SNa:
  shows "<a>:M <B> ==> SNa M"
  and   "(x):M (B) ==> SNa M"
proof(induct B arbitrary: a x M rule: ty.induct)
  case (PR X)
  { case 1 
    have "<a>:M <PR X>" by fact
    then have "<a>:M NEGc (PR X) ((PR X))" by simp
    then have "<a>:M AXIOMSc (PR X) BINDINGc (PR X) ((PR X))" by simp
    moreover
    { assume "<a>:M AXIOMSc (PR X)"
      then have "SNa M" by (simp add: AXIOMS_imply_SNa)
    }
    moreover
    { assume "<a>:M BINDINGc (PR X) ((PR X))"
      then have "SNa M" by (simp add: BINDING_imply_SNa)
    }
    ultimately show "SNa M" by blast 
  next
    case 2
    have "(x):M ((PR X))" by fact
    then have "(x):M NEGn (PR X) (<PR X>)" using NEG_simp by blast
    then have "(x):M AXIOMSn (PR X) BINDINGn (PR X) (<PR X>)" by simp
    moreover
    { assume "(x):M AXIOMSn (PR X)"
      then have "SNa M" by (simp add: AXIOMS_imply_SNa)
    }
    moreover
    { assume "(x):M BINDINGn (PR X) (<PR X>)"
      then have "SNa M" by (simp only: BINDING_imply_SNa)
    }
    ultimately show "SNa M" by blast
  }
next
  case (NOT B)
  have ih1: "a M. <a>:M <B> ==> SNa M" by fact
  have ih2: "x M. (x):M (B) ==> SNa M" by fact
  { case 1
    have "<a>:M (<NOT B>)" by fact
    then have "<a>:M NEGc (NOT B) ((NOT B))" by simp
    then have "<a>:M AXIOMSc (NOT B) BINDINGc (NOT B) ((NOT B)) NOTRIGHT (NOT B) ((B))" by simp
     moreover
    { assume "<a>:M AXIOMSc (NOT B)"
      then have "SNa M" by (simp add: AXIOMS_imply_SNa)
    }
    moreover
    { assume "<a>:M BINDINGc (NOT B) ((NOT B))"
      then have "SNa M" by (simp only: BINDING_imply_SNa)
    }
     moreover
    { assume "<a>:M NOTRIGHT (NOT B) ((B))"
      then obtain x' M' where eq: "M = NotR (x').M' a" and "(x'):M' ((B))"
        using NOTRIGHT_elim by blast
      then have "SNa M'" using ih2 by blast
      then have "SNa M" using eq by (simp add: NotR_in_SNa)
    }
    ultimately show "SNa M" by blast
  next
    case 2
    have "(x):M ((NOT B))" by fact
    then have "(x):M NEGn (NOT B) (<NOT B>)" using NEG_simp by blast
    then have "(x):M AXIOMSn (NOT B) BINDINGn (NOT B) (<NOT B>) NOTLEFT (NOT B) (<B>)" 
      by (simp only: NEGn.simps)
     moreover
    { assume "(x):M AXIOMSn (NOT B)"
      then have "SNa M" by (simp add: AXIOMS_imply_SNa)
    }
    moreover
    { assume "(x):M BINDINGn (NOT B) (<NOT B>)"
      then have "SNa M" by (simp only: BINDING_imply_SNa)
    }
     moreover
    { assume "(x):M NOTLEFT (NOT B) (<B>)"
      then obtain a' M' where eq: "M = NotL <a'>.M' x" and "<a'>:M' (<B>)"
        using NOTLEFT_elim by blast
      then have "SNa M'" using ih1 by blast
      then have "SNa M" using eq by (simp add: NotL_in_SNa)
    }
    ultimately show "SNa M" by blast
  }
next
  case (AND A B)
  have ih1: "a M. <a>:M <A> ==> SNa M" by fact
  have ih2: "x M. (x):M (A) ==> SNa M" by fact
  have ih3: "a M. <a>:M <B> ==> SNa M" by fact
  have ih4: "x M. (x):M (B) ==> SNa M" by fact
  { case 1
    have "<a>:M (<A AND B>)" by fact
    then have "<a>:M NEGc (A AND B) ((A AND B))" by simp
    then have "<a>:M AXIOMSc (A AND B) BINDINGc (A AND B) ((A AND B))
                                   ANDRIGHT (A AND B) (<A>) (<B>)" by simp
     moreover
    { assume "<a>:M AXIOMSc (A AND B)"
      then have "SNa M" by (simp add: AXIOMS_imply_SNa)
    }
    moreover
    { assume "<a>:M BINDINGc (A AND B) ((A AND B))"
      then have "SNa M" by (simp only: BINDING_imply_SNa)
    }
     moreover
    { assume "<a>:M ANDRIGHT (A AND B) (<A>) (<B>)"
      then obtain a' M' b' N' where eq: "M = AndR <a'>.M' <b'>.N' a" 
                                and "<a'>:M' (<A>)" and "<b'>:N' (<B>)"
        by (erule_tac ANDRIGHT_elim, blast)
      then have "SNa M'" and "SNa N'" using ih1 ih3 by blast+
      then have "SNa M" using eq by (simp add: AndR_in_SNa)
    }
    ultimately show "SNa M" by blast
  next
    case 2
    have "(x):M ((A AND B))" by fact
    then have "(x):M NEGn (A AND B) (<A AND B>)" using NEG_simp by blast
    then have "(x):M AXIOMSn (A AND B) BINDINGn (A AND B) (<A AND B>)
                        ANDLEFT1 (A AND B) ((A)) ANDLEFT2 (A AND B) ((B))" 
      by (simp only: NEGn.simps)
     moreover
    { assume "(x):M AXIOMSn (A AND B)"
      then have "SNa M" by (simp add: AXIOMS_imply_SNa)
    }
    moreover
    { assume "(x):M BINDINGn (A AND B) (<A AND B>)"
      then have "SNa M" by (simp only: BINDING_imply_SNa)
    }
     moreover
    { assume "(x):M ANDLEFT1 (A AND B) ((A))"
      then obtain x' M' where eq: "M = AndL1 (x').M' x" and "(x'):M' ((A))"
        using ANDLEFT1_elim by blast
      then have "SNa M'" using ih2 by blast
      then have "SNa M" using eq by (simp add: AndL1_in_SNa)
    }
    moreover
    { assume "(x):M ANDLEFT2 (A AND B) ((B))"
      then obtain x' M' where eq: "M = AndL2 (x').M' x" and "(x'):M' ((B))"
        using ANDLEFT2_elim by blast
      then have "SNa M'" using ih4 by blast
      then have "SNa M" using eq by (simp add: AndL2_in_SNa)
    }
    ultimately show "SNa M" by blast
  }
next
  case (OR A B)
  have ih1: "a M. <a>:M <A> ==> SNa M" by fact
  have ih2: "x M. (x):M (A) ==> SNa M" by fact
  have ih3: "a M. <a>:M <B> ==> SNa M" by fact
  have ih4: "x M. (x):M (B) ==> SNa M" by fact
  { case 1
    have "<a>:M (<A OR B>)" by fact
    then have "<a>:M NEGc (A OR B) ((A OR B))" by simp
    then have "<a>:M AXIOMSc (A OR B) BINDINGc (A OR B) ((A OR B))
                                   ORRIGHT1 (A OR B) (<A>) ORRIGHT2 (A OR B) (<B>)" by simp
     moreover
    { assume "<a>:M AXIOMSc (A OR B)"
      then have "SNa M" by (simp add: AXIOMS_imply_SNa)
    }
    moreover
    { assume "<a>:M BINDINGc (A OR B) ((A OR B))"
      then have "SNa M" by (simp only: BINDING_imply_SNa)
    }
     moreover
    { assume "<a>:M ORRIGHT1 (A OR B) (<A>)"
      then obtain a' M' where eq: "M = OrR1 <a'>.M' a" 
                                and "<a'>:M' (<A>)" 
        by (erule_tac ORRIGHT1_elim, blast)
      then have "SNa M'" using ih1 by blast
      then have "SNa M" using eq by (simp add: OrR1_in_SNa)
    }
     moreover
    { assume "<a>:M ORRIGHT2 (A OR B) (<B>)"
      then obtain a' M' where eq: "M = OrR2 <a'>.M' a" and "<a'>:M' (<B>)" 
        using ORRIGHT2_elim by blast
      then have "SNa M'" using ih3 by blast
      then have "SNa M" using eq by (simp add: OrR2_in_SNa)
    }
    ultimately show "SNa M" by blast
  next
    case 2
    have "(x):M ((A OR B))" by fact
    then have "(x):M NEGn (A OR B) (<A OR B>)" using NEG_simp by blast
    then have "(x):M AXIOMSn (A OR B) BINDINGn (A OR B) (<A OR B>)
                        ORLEFT (A OR B) ((A)) ((B))" 
      by (simp only: NEGn.simps)
     moreover
    { assume "(x):M AXIOMSn (A OR B)"
      then have "SNa M" by (simp add: AXIOMS_imply_SNa)
    }
    moreover
    { assume "(x):M BINDINGn (A OR B) (<A OR B>)"
      then have "SNa M" by (simp only: BINDING_imply_SNa)
    }
     moreover
    { assume "(x):M ORLEFT (A OR B) ((A)) ((B))"
      then obtain x' M' y' N' where eq: "M = OrL (x').M' (y').N' x" 
                                and "(x'):M' ((A))" and  "(y'):N' ((B))"
        by (erule_tac ORLEFT_elim, blast)
      then have "SNa M'" and "SNa N'" using ih2 ih4 by blast+
      then have "SNa M" using eq by (simp add: OrL_in_SNa)
    }
    ultimately show "SNa M" by blast
  }
next 
  case (IMP A B)
  have ih1: "a M. <a>:M <A> ==> SNa M" by fact
  have ih2: "x M. (x):M (A) ==> SNa M" by fact
  have ih3: "a M. <a>:M <B> ==> SNa M" by fact
  have ih4: "x M. (x):M (B) ==> SNa M" by fact
  { case 1
    have "<a>:M (<A IMP B>)" by fact
    then have "<a>:M NEGc (A IMP B) ((A IMP B))" by simp
    then have "<a>:M AXIOMSc (A IMP B) BINDINGc (A IMP B) ((A IMP B))
                                   IMPRIGHT (A IMP B) ((A)) (<B>) ((B)) (<A>)" by simp
     moreover
    { assume "<a>:M AXIOMSc (A IMP B)"
      then have "SNa M" by (simp add: AXIOMS_imply_SNa)
    }
    moreover
    { assume "<a>:M BINDINGc (A IMP B) ((A IMP B))"
      then have "SNa M" by (simp only: BINDING_imply_SNa)
    }
     moreover
    { assume "<a>:M IMPRIGHT (A IMP B) ((A)) (<B>) ((B)) (<A>)"
      then obtain x' a' M' where eq: "M = ImpR (x').<a'>.M' a" 
                           and imp: "z P. x'(z,P) (z):P (B) (x'):(M'{a':=(z).P}) (A)"    
        by (erule_tac IMPRIGHT_elim, blast)
      obtain z::"name" where fs: "zx'" by (rule_tac exists_fresh, rule fin_supp, blast)
      have "(z):Ax z a' (B)" by (simp add: Ax_in_CANDs)
      with imp fs have "(x'):(M'{a':=(z).Ax z a'}) (A)" by (simp add: fresh_prod fresh_atm)
      then have "SNa (M'{a':=(z).Ax z a'})" using ih2 by blast
      moreover 
      have "M'{a':=(z).Ax z a'} a* M'[a'c>a']" by (simp add: subst_with_ax2)
      ultimately have "SNa (M'[a'c>a'])" by (simp add: a_star_preserves_SNa)
      then have "SNa M'" by (simp add: crename_id)
      then have "SNa M" using eq by (simp add: ImpR_in_SNa)
    }
    ultimately show "SNa M" by blast
  next
    case 2
    have "(x):M ((A IMP B))" by fact
    then have "(x):M NEGn (A IMP B) (<A IMP B>)" using NEG_simp by blast
    then have "(x):M AXIOMSn (A IMP B) BINDINGn (A IMP B) (<A IMP B>)
                        IMPLEFT (A IMP B) (<A>) ((B))" 
      by (simp only: NEGn.simps)
     moreover
    { assume "(x):M AXIOMSn (A IMP B)"
      then have "SNa M" by (simp add: AXIOMS_imply_SNa)
    }
    moreover
    { assume "(x):M BINDINGn (A IMP B) (<A IMP B>)"
      then have "SNa M" by (simp only: BINDING_imply_SNa)
    }
     moreover
    { assume "(x):M IMPLEFT (A IMP B) (<A>) ((B))"
      then obtain a' M' y' N' where eq: "M = ImpL <a'>.M' (y').N' x" 
                                and "<a'>:M' (<A>)" and  "(y'):N' ((B))"
        by (erule_tac IMPLEFT_elim, blast)
      then have "SNa M'" and "SNa N'" using ih1 ih4 by blast+
      then have "SNa M" using eq by (simp add: ImpL_in_SNa)
    }
    ultimately show "SNa M" by blast
  }
qed 

text Main lemma 2

lemma AXIOMS_preserved:
  shows "<a>:M AXIOMSc B ==> M a* M' ==> <a>:M' AXIOMSc B"
  and   "(x):M AXIOMSn B ==> M a* M' ==> (x):M' AXIOMSn B"
  apply(simp_all add: AXIOMSc_def AXIOMSn_def)
  apply(auto simp add: ntrm.inject ctrm.inject alpha)
  apply(drule ax_do_not_a_star_reduce)
  apply(auto)
  apply(drule ax_do_not_a_star_reduce)
  apply(auto)
  apply(drule ax_do_not_a_star_reduce)
  apply(auto)
  apply(drule ax_do_not_a_star_reduce)
  apply(auto)
  done  

lemma BINDING_preserved:
  shows "<a>:M BINDINGc B ((B)) ==> M a* M' ==> <a>:M' BINDINGc B ((B))"
  and   "(x):M BINDINGn B (<B>) ==> M a* M' ==> (x):M' BINDINGn B (<B>)"
proof -
  assume red: "M a* M'"
  assume asm: "<a>:M BINDINGc B ((B))"
  {
    fix x::"name" and  P::"trm"
    from asm have "((x):P) ((B)) ==> SNa (M{a:=(x).P})" by (simp add: BINDINGc_elim)
    moreover
    have "M{a:=(x).P} a* M'{a:=(x).P}" using red by (simp add: a_star_subst2)
    ultimately 
    have "((x):P) ((B)) ==> SNa (M'{a:=(x).P})" by (simp add: a_star_preserves_SNa)
  }
  then show "<a>:M' BINDINGc B ((B))" by (auto simp add: BINDINGc_def)
next
  assume red: "M a* M'"
  assume asm: "(x):M BINDINGn B (<B>)"
  {
    fix c::"coname" and  P::"trm"
    from asm have "(<c>:P) (<B>) ==> SNa (M{x:=<c>.P})" by (simp add: BINDINGn_elim)
    moreover
    have "M{x:=<c>.P} a* M'{x:=<c>.P}" using red by (simp add: a_star_subst1)
    ultimately 
    have "(<c>:P) (<B>) ==> SNa (M'{x:=<c>.P})" by (simp add: a_star_preserves_SNa)
  }
  then show "(x):M' BINDINGn B (<B>)" by (auto simp add: BINDINGn_def)
qed
    
lemma CANDs_preserved:
  shows "<a>:M <B> ==> M a* M' ==> <a>:M' <B>"
  and   "(x):M (B) ==> M a* M' ==> (x):M' (B)" 
proof(nominal_induct B arbitrary: a x M M' rule: ty.strong_induct) 
  case (PR X)
  { case 1 
    have asm: "M a* M'" by fact
    have "<a>:M <PR X>" by fact
    then have "<a>:M NEGc (PR X) ((PR X))" by simp
    then have "<a>:M AXIOMSc (PR X) BINDINGc (PR X) ((PR X))" by simp
    moreover
    { assume "<a>:M AXIOMSc (PR X)"
      then have "<a>:M' AXIOMSc (PR X)" using asm by (simp only: AXIOMS_preserved)
    }
    moreover
    { assume "<a>:M BINDINGc (PR X) ((PR X))"
      then have "<a>:M' BINDINGc (PR X) ((PR X))" using asm by (simp add: BINDING_preserved)
    }
    ultimately have "<a>:M' AXIOMSc (PR X) BINDINGc (PR X) ((PR X))" by blast
    then have "<a>:M' NEGc (PR X) ((PR X))" by simp
    then show "<a>:M' (<PR X>)" using NEG_simp by blast
  next
    case 2
    have asm: "M a* M'" by fact
    have "(x):M (PR X)" by fact
    then have "(x):M NEGn (PR X) (<PR X>)" using NEG_simp by blast
    then have "(x):M AXIOMSn (PR X) BINDINGn (PR X) (<PR X>)" by simp
    moreover
    { assume "(x):M AXIOMSn (PR X)"
      then have "(x):M' AXIOMSn (PR X)" using asm by (simp only: AXIOMS_preserved) 
    }
    moreover
    { assume "(x):M BINDINGn (PR X) (<PR X>)"
      then have "(x):M' BINDINGn (PR X) (<PR X>)" using asm by (simp only: BINDING_preserved)
    }
    ultimately have "(x):M' AXIOMSn (PR X) BINDINGn (PR X) (<PR X>)" by blast
    then have "(x):M' NEGn (PR X) (<PR X>)" by simp
    then show "(x):M' ((PR X))" using NEG_simp by blast
  }
next
  case (IMP A B)
  have ih1: "a M M'. [<a>:M <A>; M a* M'] ==> <a>:M' <A>" by fact
  have ih2: "x M M'. [(x):M (A); M a* M'] ==> (x):M' (A)" by fact
  have ih3: "a M M'. [<a>:M <B>; M a* M'] ==> <a>:M' <B>" by fact
  have ih4: "x M M'. [(x):M (B); M a* M'] ==> (x):M' (B)" by fact
  { case 1 
    have asm: "M a* M'" by fact
    have "<a>:M <A IMP B>" by fact
    then have "<a>:M NEGc (A IMP B) ((A IMP B))" by simp
    then have "<a>:M AXIOMSc (A IMP B) BINDINGc (A IMP B) ((A IMP B))
                             IMPRIGHT (A IMP B) ((A)) (<B>) ((B)) (<A>)" by simp
    moreover
    { assume "<a>:M AXIOMSc (A IMP B)"
      then have "<a>:M' AXIOMSc (A IMP B)" using asm by (simp only: AXIOMS_preserved)
    }
    moreover
    { assume "<a>:M BINDINGc (A IMP B) ((A IMP B))"
      then have "<a>:M' BINDINGc (A IMP B) ((A IMP B))" using asm by (simp only: BINDING_preserved)
    }
    moreover
    { assume "<a>:M IMPRIGHT (A IMP B) ((A)) (<B>) ((B)) (<A>)"
      then obtain x' a' N' where eq: "M = ImpR (x').<a'>.N' a" and fic: "fic (ImpR (x').<a'>.N' a) a"
                           and imp1: "z P. x'(z,P) (z):P (B) (x'):(N'{a':=(z).P}) (A)" 
                           and imp2: "c Q. a'(c,Q) <c>:Q <A> <a'>:(N'{x':=<c>.Q}) <B>"
        using IMPRIGHT_elim by blast
      from eq asm obtain N'' where eq': "M' = ImpR (x').<a'>.N'' a" and red: "N' a* N''" 
        using a_star_redu_ImpR_elim by (blast)
      from imp1 have "z P. x'(z,P) (z):P (B) (x'):(N''{a':=(z).P}) (A)" using red ih2
        apply(auto)
        apply(drule_tac x="z" in spec)
        apply(drule_tac x="P" in spec)
        apply(simp)
        apply(drule_tac a_star_subst2)
        apply(blast)
        done
      moreover
      from imp2 have "c Q. a'(c,Q) <c>:Q <A> <a'>:(N''{x':=<c>.Q}) <B>" using red ih3
        apply(auto)
        apply(drule_tac x="c" in spec)
        apply(drule_tac x="Q" in spec)
        apply(simp)
        apply(drule_tac a_star_subst1)
        apply(blast)
        done
      moreover
      from fic have "fic M' a" using eq asm by (simp add: fic_a_star_reduce)
      ultimately have "<a>:M' IMPRIGHT (A IMP B) ((A)) (<B>) ((B)) (<A>)" using eq' by auto
    }
    ultimately have "<a>:M' AXIOMSc (A IMP B) BINDINGc (A IMP B) ((A IMP B))
                                             IMPRIGHT (A IMP B) ((A)) (<B>) ((B)) (<A>)" by blast
    then have "<a>:M' NEGc (A IMP B) ((A IMP B))" by simp
    then show "<a>:M' (<A IMP B>)" using NEG_simp by blast
  next
    case 2
    have asm: "M a* M'" by fact
    have "(x):M (A IMP B)" by fact
    then have "(x):M NEGn (A IMP B) (<A IMP B>)" using NEG_simp by blast
    then have "(x):M AXIOMSn (A IMP B) BINDINGn (A IMP B) (<A IMP B>)
                                               IMPLEFT (A IMP B) (<A>) ((B))" by simp
    moreover
    { assume "(x):M AXIOMSn (A IMP B)"
      then have "(x):M' AXIOMSn (A IMP B)" using asm by (simp only: AXIOMS_preserved)
    }
    moreover
    { assume "(x):M BINDINGn (A IMP B) (<A IMP B>)"
      then have "(x):M' BINDINGn (A IMP B) (<A IMP B>)" using asm by (simp only: BINDING_preserved)
    }
    moreover
    { assume "(x):M IMPLEFT (A IMP B) (<A>) ((B))"
      then obtain a' T' y' N' where eq: "M = ImpL <a'>.T' (y').N' x" 
                             and fin: "fin (ImpL <a'>.T' (y').N' x) x"
                             and imp1: "<a'>:T' <A>" and imp2: "(y'):N' (B)"
        by (erule_tac IMPLEFT_elim, blast)
      from eq asm obtain T'' N'' where eq': "M' = ImpL <a'>.T'' (y').N'' x" 
                                 and red1: "T' a* T''"  and red2: "N' a* N''"
        using a_star_redu_ImpL_elim by blast
      from fin have "fin M' x" using eq asm by (simp add: fin_a_star_reduce)
      moreover
      from imp1 red1 have "<a'>:T'' <A>" using ih1 by simp
      moreover
      from imp2 red2 have "(y'):N'' (B)" using ih4 by simp
      ultimately have "(x):M' IMPLEFT (A IMP B) (<A>) ((B))" using eq' by (simp, blast) 
    }
    ultimately have "(x):M' AXIOMSn (A IMP B) BINDINGn (A IMP B) (<A IMP B>)
                                               IMPLEFT (A IMP B) (<A>) ((B))" by blast
    then have "(x):M' NEGn (A IMP B) (<A IMP B>)" by simp
    then show "(x):M' ((A IMP B))" using NEG_simp by blast
  }
next
  case (AND A B)
  have ih1: "a M M'. [<a>:M <A>; M a* M'] ==> <a>:M' <A>" by fact
  have ih2: "x M M'. [(x):M (A); M a* M'] ==> (x):M' (A)" by fact
  have ih3: "a M M'. [<a>:M <B>; M a* M'] ==> <a>:M' <B>" by fact
  have ih4: "x M M'. [(x):M (B); M a* M'] ==> (x):M' (B)" by fact
  { case 1 
    have asm: "M a* M'" by fact
    have "<a>:M <A AND B>" by fact
    then have "<a>:M NEGc (A AND B) ((A AND B))" by simp
    then have "<a>:M AXIOMSc (A AND B) BINDINGc (A AND B) ((A AND B))
                                               ANDRIGHT (A AND B) (<A>) (<B>)" by simp
    moreover
    { assume "<a>:M AXIOMSc (A AND B)"
      then have "<a>:M' AXIOMSc (A AND B)" using asm by (simp only: AXIOMS_preserved)
    }
    moreover
    { assume "<a>:M BINDINGc (A AND B) ((A AND B))"
      then have "<a>:M' BINDINGc (A AND B) ((A AND B))" using asm by (simp only: BINDING_preserved)
    }
    moreover
    { assume "<a>:M ANDRIGHT (A AND B) (<A>) (<B>)"
      then obtain a' T' b' N' where eq: "M = AndR <a'>.T' <b'>.N' a" 
                              and fic: "fic (AndR <a'>.T' <b'>.N' a) a"
                           and imp1: "<a'>:T' <A>" and imp2: "<b'>:N' <B>"
        using ANDRIGHT_elim by blast
      from eq asm obtain T'' N'' where eq': "M' = AndR <a'>.T'' <b'>.N'' a" 
                          and red1: "T' a* T''" and red2: "N' a* N''" 
        using a_star_redu_AndR_elim by blast
      from fic have "fic M' a" using eq asm by (simp add: fic_a_star_reduce)
      moreover
      from imp1 red1 have "<a'>:T'' <A>" using ih1 by simp
      moreover
      from imp2 red2 have "<b'>:N'' <B>" using ih3 by simp
      ultimately have "<a>:M' ANDRIGHT (A AND B) (<A>) (<B>)" using eq' by (simp, blast) 
    }
    ultimately have "<a>:M' AXIOMSc (A AND B) BINDINGc (A AND B) ((A AND B))
                                               ANDRIGHT (A AND B) (<A>) (<B>)" by blast
    then have "<a>:M' NEGc (A AND B) ((A AND B))" by simp
    then show "<a>:M' (<A AND B>)" using NEG_simp by blast
  next
    case 2
    have asm: "M a* M'" by fact
    have "(x):M (A AND B)" by fact
    then have "(x):M NEGn (A AND B) (<A AND B>)" using NEG_simp by blast
    then have "(x):M AXIOMSn (A AND B) BINDINGn (A AND B) (<A AND B>)
                                      ANDLEFT1 (A AND B) ((A)) ANDLEFT2 (A AND B) ((B))" by simp
    moreover
    { assume "(x):M AXIOMSn (A AND B)"
      then have "(x):M' AXIOMSn (A AND B)" using asm by (simp only: AXIOMS_preserved)
    }
    moreover
    { assume "(x):M BINDINGn (A AND B) (<A AND B>)"
      then have "(x):M' BINDINGn (A AND B) (<A AND B>)" using asm by (simp only: BINDING_preserved)
    }
    moreover
    { assume "(x):M ANDLEFT1 (A AND B) ((A))"
      then obtain y' N' where eq: "M = AndL1 (y').N' x" 
                             and fin: "fin (AndL1 (y').N' x) x" and imp: "(y'):N' (A)"
        by (erule_tac ANDLEFT1_elim, blast)
      from eq asm obtain N'' where eq': "M' = AndL1 (y').N'' x" and red1: "N' a* N''"
        using a_star_redu_AndL1_elim by blast
      from fin have "fin M' x" using eq asm by (simp add: fin_a_star_reduce)
      moreover
      from imp red1 have "(y'):N'' (A)" using ih2 by simp
      ultimately have "(x):M' ANDLEFT1 (A AND B) ((A))" using eq' by (simp, blast) 
    }
     moreover
    { assume "(x):M ANDLEFT2 (A AND B) ((B))"
      then obtain y' N' where eq: "M = AndL2 (y').N' x" 
                             and fin: "fin (AndL2 (y').N' x) x" and imp: "(y'):N' (B)"
        by (erule_tac ANDLEFT2_elim, blast)
      from eq asm obtain N'' where eq': "M' = AndL2 (y').N'' x" and red1: "N' a* N''"
        using a_star_redu_AndL2_elim by blast
      from fin have "fin M' x" using eq asm by (simp add: fin_a_star_reduce)
      moreover
      from imp red1 have "(y'):N'' (B)" using ih4 by simp
      ultimately have "(x):M' ANDLEFT2 (A AND B) ((B))" using eq' by (simp, blast) 
    }
    ultimately have "(x):M' AXIOMSn (A AND B) BINDINGn (A AND B) (<A AND B>)
                                ANDLEFT1 (A AND B) ((A)) ANDLEFT2 (A AND B) ((B))" by blast
    then have "(x):M' NEGn (A AND B) (<A AND B>)" by simp
    then show "(x):M' ((A AND B))" using NEG_simp by blast
  }
next    
 case (OR A B)
  have ih1: "a M M'. [<a>:M <A>; M a* M'] ==> <a>:M' <A>" by fact
  have ih2: "x M M'. [(x):M (A); M a* M'] ==> (x):M' (A)" by fact
  have ih3: "a M M'. [<a>:M <B>; M a* M'] ==> <a>:M' <B>" by fact
  have ih4: "x M M'. [(x):M (B); M a* M'] ==> (x):M' (B)" by fact
  { case 1 
    have asm: "M a* M'" by fact
    have "<a>:M <A OR B>" by fact
    then have "<a>:M NEGc (A OR B) ((A OR B))" by simp
    then have "<a>:M AXIOMSc (A OR B) BINDINGc (A OR B) ((A OR B))
                           ORRIGHT1 (A OR B) (<A>) ORRIGHT2 (A OR B) (<B>)" by simp
    moreover
    { assume "<a>:M AXIOMSc (A OR B)"
      then have "<a>:M' AXIOMSc (A OR B)" using asm by (simp only: AXIOMS_preserved)
    }
    moreover
    { assume "<a>:M BINDINGc (A OR B) ((A OR B))"
      then have "<a>:M' BINDINGc (A OR B) ((A OR B))" using asm by (simp only: BINDING_preserved)
    }
    moreover
    { assume "<a>:M ORRIGHT1 (A OR B) (<A>)"
      then obtain a' N' where eq: "M = OrR1 <a'>.N' a" 
                              and fic: "fic (OrR1 <a'>.N' a) a" and imp1: "<a'>:N' <A>"
        using ORRIGHT1_elim by blast
      from eq asm obtain N'' where eq': "M' = OrR1 <a'>.N'' a" and red1: "N' a* N''" 
        using a_star_redu_OrR1_elim by blast
      from fic have "fic M' a" using eq asm by (simp add: fic_a_star_reduce)
      moreover
      from imp1 red1 have "<a'>:N'' <A>" using ih1 by simp
      ultimately have "<a>:M' ORRIGHT1 (A OR B) (<A>)" using eq' by (simp, blast) 
    }
    moreover
    { assume "<a>:M ORRIGHT2 (A OR B) (<B>)"
      then obtain a' N' where eq: "M = OrR2 <a'>.N' a" 
                              and fic: "fic (OrR2 <a'>.N' a) a" and imp1: "<a'>:N' <B>"
        using ORRIGHT2_elim by blast
      from eq asm obtain N'' where eq': "M' = OrR2 <a'>.N'' a" and red1: "N' a* N''" 
        using a_star_redu_OrR2_elim by blast
      from fic have "fic M' a" using eq asm by (simp add: fic_a_star_reduce)
      moreover
      from imp1 red1 have "<a'>:N'' <B>" using ih3 by simp
      ultimately have "<a>:M' ORRIGHT2 (A OR B) (<B>)" using eq' by (simp, blast) 
    }
    ultimately have "<a>:M' AXIOMSc (A OR B) BINDINGc (A OR B) ((A OR B))
                                 ORRIGHT1 (A OR B) (<A>) ORRIGHT2 (A OR B) (<B>)" by blast
    then have "<a>:M' NEGc (A OR B) ((A OR B))" by simp
    then show "<a>:M' (<A OR B>)" using NEG_simp by blast
  next
    case 2
    have asm: "M a* M'" by fact
    have "(x):M (A OR B)" by fact
    then have "(x):M NEGn (A OR B) (<A OR B>)" using NEG_simp by blast
    then have "(x):M AXIOMSn (A OR B) BINDINGn (A OR B) (<A OR B>)
                                      ORLEFT (A OR B) ((A)) ((B))" by simp
    moreover
    { assume "(x):M AXIOMSn (A OR B)"
      then have "(x):M' AXIOMSn (A OR B)" using asm by (simp only: AXIOMS_preserved)
    }
    moreover
    { assume "(x):M BINDINGn (A OR B) (<A OR B>)"
      then have "(x):M' BINDINGn (A OR B) (<A OR B>)" using asm by (simp only: BINDING_preserved)
    }
    moreover
    { assume "(x):M ORLEFT (A OR B) ((A)) ((B))"
      then obtain y' T' z' N' where eq: "M = OrL (y').T' (z').N' x" 
                             and fin: "fin (OrL (y').T' (z').N' x) x" 
                             and imp1: "(y'):T' (A)" and imp2: "(z'):N' (B)"
        by (erule_tac ORLEFT_elim, blast)
      from eq asm obtain T'' N'' where eq': "M' = OrL (y').T'' (z').N'' x" 
                and red1: "T' a* T''" and red2: "N' a* N''"
        using a_star_redu_OrL_elim by blast
      from fin have "fin M' x" using eq asm by (simp add: fin_a_star_reduce)
      moreover
      from imp1 red1 have "(y'):T'' (A)" using ih2 by simp
      moreover
      from imp2 red2 have "(z'):N'' (B)" using ih4 by simp
      ultimately have "(x):M' ORLEFT (A OR B) ((A)) ((B))" using eq' by (simp, blast) 
    }
    ultimately have "(x):M' AXIOMSn (A OR B) BINDINGn (A OR B) (<A OR B>)
                                ORLEFT (A OR B) ((A)) ((B))" by blast
    then have "(x):M' NEGn (A OR B) (<A OR B>)" by simp
    then show "(x):M' ((A OR B))" using NEG_simp by blast
  }
next
  case (NOT A)
  have ih1: "a M M'. [<a>:M <A>; M a* M'] ==> <a>:M' <A>" by fact
  have ih2: "x M M'. [(x):M (A); M a* M'] ==> (x):M' (A)" by fact
  { case 1 
    have asm: "M a* M'" by fact
    have "<a>:M <NOT A>" by fact
    then have "<a>:M NEGc (NOT A) ((NOT A))" by simp
    then have "<a>:M AXIOMSc (NOT A) BINDINGc (NOT A) ((NOT A))
                                               NOTRIGHT (NOT A) ((A))" by simp
    moreover
    { assume "<a>:M AXIOMSc (NOT A)"
      then have "<a>:M' AXIOMSc (NOT A)" using asm by (simp only: AXIOMS_preserved)
    }
    moreover
    { assume "<a>:M BINDINGc (NOT A) ((NOT A))"
      then have "<a>:M' BINDINGc (NOT A) ((NOT A))" using asm by (simp only: BINDING_preserved)
    }
    moreover
    { assume "<a>:M NOTRIGHT (NOT A) ((A))"
      then obtain y' N' where eq: "M = NotR (y').N' a" 
                              and fic: "fic (NotR (y').N' a) a" and imp: "(y'):N' (A)"
        using NOTRIGHT_elim by blast
      from eq asm obtain N'' where eq': "M' = NotR (y').N'' a" and red: "N' a* N''" 
        using a_star_redu_NotR_elim by blast
      from fic have "fic M' a" using eq asm by (simp add: fic_a_star_reduce)
      moreover
      from imp red have "(y'):N'' (A)" using ih2 by simp
      ultimately have "<a>:M' NOTRIGHT (NOT A) ((A))" using eq' by (simp, blast) 
    }
    ultimately have "<a>:M' AXIOMSc (NOT A) BINDINGc (NOT A) ((NOT A))
                                               NOTRIGHT (NOT A) ((A))" by blast
    then have "<a>:M' NEGc (NOT A) ((NOT A))" by simp
    then show "<a>:M' (<NOT A>)" using NEG_simp by blast
  next
    case 2
    have asm: "M a* M'" by fact
    have "(x):M (NOT A)" by fact
    then have "(x):M NEGn (NOT A) (<NOT A>)" using NEG_simp by blast
    then have "(x):M AXIOMSn (NOT A) BINDINGn (NOT A) (<NOT A>)
                                      NOTLEFT (NOT A) (<A>)" by simp
    moreover
    { assume "(x):M AXIOMSn (NOT A)"
      then have "(x):M' AXIOMSn (NOT A)" using asm by (simp only: AXIOMS_preserved)
    }
    moreover
    { assume "(x):M BINDINGn (NOT A) (<NOT A>)"
      then have "(x):M' BINDINGn (NOT A) (<NOT A>)" using asm by (simp only: BINDING_preserved)
    }
    moreover
    { assume "(x):M NOTLEFT (NOT A) (<A>)"
      then obtain a' N' where eq: "M = NotL <a'>.N' x" 
                             and fin: "fin (NotL <a'>.N' x) x" and imp: "<a'>:N' <A>"
        by (erule_tac NOTLEFT_elim, blast)
      from eq asm obtain N'' where eq': "M' = NotL <a'>.N'' x" and red1: "N' a* N''"
        using a_star_redu_NotL_elim by blast
      from fin have "fin M' x" using eq asm by (simp add: fin_a_star_reduce)
      moreover
      from imp red1 have "<a'>:N'' <A>" using ih1 by simp
      ultimately have "(x):M' NOTLEFT (NOT A) (<A>)" using eq' by (simp, blast) 
    }
    ultimately have "(x):M' AXIOMSn (NOT A) BINDINGn (NOT A) (<NOT A>)
                                NOTLEFT (NOT A) (<A>)" by blast
    then have "(x):M' NEGn (NOT A) (<NOT A>)" by simp
    then show "(x):M' ((NOT A))" using NEG_simp by blast
  }
qed

lemma CANDs_preserved_single:
  shows "<a>:M <B> ==> M a M' ==> <a>:M' <B>"
  and   "(x):M (B) ==> M a M' ==> (x):M' (B)"
by (auto simp add: a_starI CANDs_preserved)

lemma fic_CANDS:
  assumes a: "¬fic M a"
  and     b: "<a>:M <B>"
  shows "<a>:M AXIOMSc B <a>:M BINDINGc B ((B))"
using a b
apply(nominal_induct B rule: ty.strong_induct)
apply(simp)
apply(simp)
apply(erule disjE)
apply(simp)
apply(erule disjE)
apply(simp)
apply(auto simp add: ctrm.inject)[1]
apply(simp add: alpha)
apply(erule disjE)
apply(simp)
apply(auto simp add: calc_atm)[1]
apply(drule_tac pi="[(a,aa)]" in fic.eqvt(2))
apply(simp add: calc_atm)
apply(simp)
apply(erule disjE)
apply(simp)
apply(erule disjE)
apply(simp)
apply(auto simp add: ctrm.inject)[1]
apply(simp add: alpha)
apply(erule disjE)
apply(simp)
apply(erule conjE)+
apply(simp)
apply(drule_tac pi="[(a,c)]" in fic.eqvt(2))
apply(simp add: calc_atm)
apply(simp)
apply(erule disjE)
apply(simp)
apply(erule disjE)
apply(simp)
apply(auto simp add: ctrm.inject)[1]
apply(simp add: alpha)
apply(erule disjE)
apply(simp)
apply(erule conjE)+
apply(simp)
apply(drule_tac pi="[(a,b)]" in fic.eqvt(2))
apply(simp add: calc_atm)
apply(simp add: alpha)
apply(erule disjE)
apply(simp)
apply(erule conjE)+
apply(simp)
apply(drule_tac pi="[(a,b)]" in fic.eqvt(2))
apply(simp add: calc_atm)
apply(simp)
apply(erule disjE)
apply(simp)
apply(erule disjE)
apply(simp)
apply(auto simp add: ctrm.inject)[1]
apply(simp add: alpha)
apply(erule disjE)
apply(simp)
apply(erule conjE)+
apply(simp)
apply(drule_tac pi="[(a,b)]" in fic.eqvt(2))
apply(simp add: calc_atm)
done

lemma fin_CANDS_aux:
  assumes a: "¬fin M x"
  and     b: "(x):M (NEGn B (<B>))"
  shows "(x):M AXIOMSn B (x):M BINDINGn B (<B>)"
using a b
apply(nominal_induct B rule: ty.strong_induct)
apply(simp)
apply(simp)
apply(erule disjE)
apply(simp)
apply(erule disjE)
apply(simp)
apply(auto simp add: ntrm.inject)[1]
apply(simp add: alpha)
apply(erule disjE)
apply(simp)
apply(auto simp add: calc_atm)[1]
apply(drule_tac pi="[(x,xa)]" in fin.eqvt(1))
apply(simp add: calc_atm)
apply(simp)
apply(erule disjE)
apply(simp)
apply(erule disjE)
apply(simp)
apply(auto simp add: ntrm.inject)[1]
apply(simp add: alpha)
apply(erule disjE)
apply(simp)
apply(erule conjE)+
apply(simp)
apply(drule_tac pi="[(x,y)]" in fin.eqvt(1))
apply(simp add: calc_atm)
apply(simp add: alpha)
apply(erule disjE)
apply(simp)
apply(erule conjE)+
apply(simp)
apply(drule_tac pi="[(x,y)]" in fin.eqvt(1))
apply(simp add: calc_atm)
apply(simp)
apply(erule disjE)
apply(simp)
apply(erule disjE)
apply(simp)
apply(auto simp add: ntrm.inject)[1]
apply(simp add: alpha)
apply(erule disjE)
apply(simp)
apply(erule conjE)+
apply(simp)
apply(drule_tac pi="[(x,z)]" in fin.eqvt(1))
apply(simp add: calc_atm)
apply(simp)
apply(erule disjE)
apply(simp)
apply(erule disjE)
apply(simp)
apply(auto simp add: ntrm.inject)[1]
apply(simp add: alpha)
apply(erule disjE)
apply(simp)
apply(erule conjE)+
apply(simp)
apply(drule_tac pi="[(x,y)]" in fin.eqvt(1))
apply(simp add: calc_atm)
done

lemma fin_CANDS:
  assumes a: "¬fin M x"
  and     b: "(x):M ((B))"
  shows "(x):M AXIOMSn B (x):M BINDINGn B (<B>)"
apply(rule fin_CANDS_aux)
apply(rule a)
apply(rule NEG_elim)
apply(rule b)
done

lemma BINDING_implies_CAND:
  shows "<c>:M BINDINGc B ((B)) ==> <c>:M (<B>)"
  and   "(x):N BINDINGn B (<B>) ==> (x):N ((B))"
apply -
apply(nominal_induct B rule: ty.strong_induct)
apply(auto)
apply(rule NEG_intro)
apply(nominal_induct B rule: ty.strong_induct)
apply(auto)
done

end

Messung V0.5 in Prozent
C=100 H=100 G=100

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

*Bot Zugriff






Versionsinformation zu Columbo

Bemerkung:

PVS Prover

Isabelle Prover

NIST Cobol Testsuite

Cephes Mathematical Library

Vienna Development Method

Anfrage:

Dauer der Verarbeitung:

Sekunden

sprechenden Kalenders