Theory Class3

theory Class3
  imports Class2
begin

text ‹3rd Main Lemma›

lemma Cut_a_redu_elim:
  assumes a: "Cut <a>.M (x).N a R"
  shows "(M'. R = Cut <a>.M' (x).N  M a M') 
         (N'. R = Cut <a>.M (x).N'  N a N') 
         (Cut <a>.M (x).N c R) 
         (Cut <a>.M (x).N l R)"
  using a
  apply(erule_tac a_redu.cases)
                  apply(simp_all)
   apply(simp_all add: trm.inject)
   apply(rule disjI1)
   apply(auto simp add: alpha)[1]
    apply(rule_tac x="[(a,aa)]M'" in exI)
    apply(perm_simp add: fresh_left calc_atm a_redu.eqvt fresh_a_redu)
   apply(rule_tac x="[(a,aa)]M'" in exI)
   apply(perm_simp add: fresh_left calc_atm a_redu.eqvt fresh_a_redu)
  apply(rule disjI2)
  apply(rule disjI1)
  apply(auto simp add: alpha)[1]
   apply(rule_tac x="[(x,xa)]N'" in exI)
   apply(perm_simp add: fresh_left calc_atm a_redu.eqvt fresh_a_redu)
  apply(rule_tac x="[(x,xa)]N'" in exI)
  apply(perm_simp add: fresh_left calc_atm a_redu.eqvt fresh_a_redu)
  done

lemma Cut_c_redu_elim:
  assumes a: "Cut <a>.M (x).N c R"
  shows "(R = M{a:=(x).N}  ¬fic M a) 
         (R = N{x:=<a>.M}  ¬fin N x)"
  using a
  apply(erule_tac c_redu.cases)
   apply(simp_all)
   apply(simp_all add: trm.inject)
   apply(rule disjI1)
   apply(auto simp add: alpha)[1]
       apply(simp add: subst_rename fresh_atm)
      apply(simp add: subst_rename fresh_atm)
     apply(drule_tac pi="[(a,aa)]" in fic.eqvt(2))
     apply(perm_simp)
    apply(simp add: subst_rename fresh_atm fresh_prod)
   apply(drule_tac pi="[(a,aa)]" in fic.eqvt(2))
   apply(perm_simp)
  apply(rule disjI2)
  apply(auto simp add: alpha)[1]
      apply(simp add: subst_rename fresh_atm)
     apply(drule_tac pi="[(x,xa)]" in fin.eqvt(1))
     apply(perm_simp)
    apply(simp add: subst_rename fresh_atm fresh_prod)
   apply(simp add: subst_rename fresh_atm fresh_prod)
  apply(drule_tac pi="[(x,xa)]" in fin.eqvt(1))
  apply(perm_simp)
  done

lemma not_fic_crename_aux:
  assumes a: "fic M c" "c(a,b)"
  shows "fic (M[a⊢c>b]) c" 
  using a
  apply(nominal_induct M avoiding: c a b rule: trm.strong_induct)
             apply(auto dest!: fic_elims intro!: fic.intros simp add: fresh_prod fresh_atm rename_fresh abs_fresh)
  done

lemma not_fic_crename:
  assumes a: "¬(fic (M[a⊢c>b]) c)" "c(a,b)"
  shows "¬(fic M c)" 
  using a
  apply(auto dest:  not_fic_crename_aux)
  done

lemma not_fin_crename_aux:
  assumes a: "fin M y"
  shows "fin (M[a⊢c>b]) y" 
  using a
  apply(nominal_induct M avoiding: a b rule: trm.strong_induct)
             apply(auto dest!: fin_elims intro!: fin.intros simp add: fresh_prod fresh_atm rename_fresh abs_fresh)
  done

lemma not_fin_crename:
  assumes a: "¬(fin (M[a⊢c>b]) y)" 
  shows "¬(fin M y)" 
  using a
  apply(auto dest:  not_fin_crename_aux)
  done

lemma crename_fresh_interesting1:
  fixes c::"coname"
  assumes a: "c(M[a⊢c>b])" "c(a,b)"
  shows "cM"
  using a
  apply(nominal_induct M avoiding: c a b rule: trm.strong_induct)
             apply(auto split: if_splits simp add: abs_fresh)
  done

lemma crename_fresh_interesting2:
  fixes x::"name"
  assumes a: "x(M[a⊢c>b])" 
  shows "xM"
  using a
  apply(nominal_induct M avoiding: x a b rule: trm.strong_induct)
             apply(auto split: if_splits simp add: abs_fresh abs_supp fin_supp fresh_atm)
  done


lemma fic_crename:
  assumes a: "fic (M[a⊢c>b]) c" "c(a,b)"
  shows "fic M c" 
  using a
  apply(nominal_induct M avoiding: c a b rule: trm.strong_induct)
             apply(auto dest!: fic_elims intro!: fic.intros simp add: fresh_prod fresh_atm rename_fresh abs_fresh
      split: if_splits)
       apply(auto dest: crename_fresh_interesting1 simp add: fresh_prod fresh_atm)
  done

lemma fin_crename:
  assumes a: "fin (M[a⊢c>b]) x"
  shows "fin M x" 
  using a
  apply(nominal_induct M avoiding: x a b rule: trm.strong_induct)
             apply(auto dest!: fin_elims intro!: fin.intros simp add: fresh_prod fresh_atm rename_fresh abs_fresh
      split: if_splits)
        apply(auto dest: crename_fresh_interesting2 simp add: fresh_prod fresh_atm)
  done

lemma crename_Cut:
  assumes a: "R[a⊢c>b] = Cut <c>.M (x).N" "c(a,b,N,R)" "x(M,R)"
  shows "M' N'. R = Cut <c>.M' (x).N'  M'[a⊢c>b] = M  N'[a⊢c>b] = N  cN'  xM'"
  using a
  apply(nominal_induct R avoiding: a b c x M N rule: trm.strong_induct)
             apply(auto split: if_splits)
  apply(simp add: trm.inject)
  apply(auto simp add: alpha)
    apply(rule_tac x="[(name,x)]trm2" in exI)
    apply(perm_simp)
    apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
    apply(drule sym)
    apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst])
    apply(simp add: eqvts calc_atm)
   apply(rule_tac x="[(coname,c)]trm1" in exI)
   apply(perm_simp)
   apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
   apply(drule sym)
   apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst])
   apply(simp add: eqvts calc_atm)
   apply(auto simp add: fresh_atm)[1]
  apply(rule_tac x="[(coname,c)]trm1" in exI)
  apply(perm_simp)
  apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
  apply(rule_tac x="[(name,x)]trm2" in exI)
  apply(perm_simp)
  apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
  apply(drule sym)
  apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst])
  apply(simp add: eqvts calc_atm)
  apply(auto simp add: fresh_atm)[1]
   apply(drule sym)
   apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst])
   apply(simp add: eqvts calc_atm)
  apply(drule sym)
  apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst])
  apply(simp add: eqvts calc_atm)
  done

lemma crename_NotR:
  assumes a: "R[a⊢c>b] = NotR (x).N c" "xR" "c(a,b)"
  shows "N'. (R = NotR (x).N' c)  N'[a⊢c>b] = N" 
  using a
  apply(nominal_induct R avoiding: a b c x N rule: trm.strong_induct)
             apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject)
  apply(rule_tac x="[(name,x)]trm" in exI)
  apply(perm_simp)
  apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
  apply(drule sym)
  apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst])
  apply(simp add: eqvts calc_atm)
  done

lemma crename_NotR':
  assumes a: "R[a⊢c>b] = NotR (x).N c" "xR" "ca"
  shows "(N'. (R = NotR (x).N' c)  N'[a⊢c>b] = N)  (N'. (R = NotR (x).N' a)  b=c  N'[a⊢c>b] = N)"
  using a
  apply(nominal_induct R avoiding: a b c x N rule: trm.strong_induct)
             apply(auto split: if_splits simp add: fresh_prod fresh_atm abs_fresh alpha trm.inject)
   apply(rule_tac x="[(name,x)]trm" in exI)
   apply(perm_simp)
   apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
   apply(drule sym)
   apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst])
   apply(simp add: eqvts calc_atm)
  apply(rule_tac x="[(name,x)]trm" in exI)
  apply(perm_simp)
  apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
  apply(drule sym)
  apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst])
  apply(simp add: eqvts calc_atm)
  done

lemma crename_NotR_aux:
  assumes a: "R[a⊢c>b] = NotR (x).N c" 
  shows "(a=c  a=b)  (ac)" 
  using a
  apply(nominal_induct R avoiding: a b c x N rule: trm.strong_induct)
             apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject)
  done

lemma crename_NotL:
  assumes a: "R[a⊢c>b] = NotL <c>.N y" "c(R,a,b)"
  shows "N'. (R = NotL <c>.N' y)  N'[a⊢c>b] = N" 
  using a
  apply(nominal_induct R avoiding: a b c y N rule: trm.strong_induct)
             apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject)
  apply(rule_tac x="[(coname,c)]trm" in exI)
  apply(perm_simp)
  apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
  apply(drule sym)
  apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst])
  apply(simp add: eqvts calc_atm)
  done

lemma crename_AndL1:
  assumes a: "R[a⊢c>b] = AndL1 (x).N y" "xR"
  shows "N'. (R = AndL1 (x).N' y)  N'[a⊢c>b] = N" 
  using a
  apply(nominal_induct R avoiding: a b x y N rule: trm.strong_induct)
             apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject)
  apply(rule_tac x="[(name1,x)]trm" in exI)
  apply(perm_simp)
  apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
  apply(drule sym)
  apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst])
  apply(simp add: eqvts calc_atm)
  done

lemma crename_AndL2:
  assumes a: "R[a⊢c>b] = AndL2 (x).N y" "xR"
  shows "N'. (R = AndL2 (x).N' y)  N'[a⊢c>b] = N" 
  using a
  apply(nominal_induct R avoiding: a b x y N rule: trm.strong_induct)
             apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject)
  apply(rule_tac x="[(name1,x)]trm" in exI)
  apply(perm_simp)
  apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
  apply(drule sym)
  apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst])
  apply(simp add: eqvts calc_atm)
  done

lemma crename_AndR_aux:
  assumes a: "R[a⊢c>b] = AndR <c>.M <d>.N e" 
  shows "(a=e  a=b)  (ae)" 
  using a
  apply(nominal_induct R avoiding: a b c d e M N rule: trm.strong_induct)
             apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject)
  done

lemma crename_AndR:
  assumes a: "R[a⊢c>b] = AndR <c>.M <d>.N e" "c(a,b,d,e,N,R)" "d(a,b,c,e,M,R)" "e(a,b)"
  shows "M' N'. R = AndR <c>.M' <d>.N' e  M'[a⊢c>b] = M  N'[a⊢c>b] = N  cN'  dM'"
  using a
  apply(nominal_induct R avoiding: a b c d e M N rule: trm.strong_induct)
             apply(auto split: if_splits simp add: trm.inject alpha)
        apply(simp add: fresh_atm fresh_prod)
       apply(rule_tac x="[(coname2,d)]trm2" in exI)
       apply(perm_simp)
       apply(auto simp add: abs_fresh fresh_left calc_atm fresh_prod fresh_atm)[1]
      apply(rule_tac x="[(coname1,c)]trm1" in exI)
      apply(perm_simp)
      apply(auto simp add: abs_fresh fresh_left calc_atm fresh_prod fresh_atm)[1]
     apply(rule_tac x="[(coname1,c)]trm1" in exI)
     apply(perm_simp)
     apply(auto simp add: abs_fresh fresh_left calc_atm fresh_prod fresh_atm)[1]
    apply(rule_tac x="[(coname2,d)]trm2" in exI)
    apply(perm_simp)
    apply(auto simp add: abs_fresh fresh_left calc_atm fresh_prod fresh_atm)[1]
   apply(rule_tac x="[(coname1,c)]trm1" in exI)
   apply(perm_simp)
   apply(auto simp add: abs_fresh fresh_left calc_atm fresh_prod fresh_atm)[1]
  apply(rule_tac x="[(coname1,c)]trm1" in exI)
  apply(perm_simp)
  apply(auto simp add: abs_fresh fresh_left calc_atm fresh_prod fresh_atm)[1]
  apply(rule_tac x="[(coname2,d)]trm2" in exI)
  apply(perm_simp)
  apply(auto simp add: abs_fresh fresh_left calc_atm fresh_prod fresh_atm)[1]
   apply(drule sym)
   apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst])
   apply(simp add: eqvts calc_atm)
  apply(drule_tac s="trm2[a⊢c>b]" in  sym)
  apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst])
  apply(simp add: eqvts calc_atm)
  done

lemma crename_AndR':
  assumes a: "R[a⊢c>b] = AndR <c>.M <d>.N e" "c(a,b,d,e,N,R)" "d(a,b,c,e,M,R)" "ea"
  shows "(M' N'. R = AndR <c>.M' <d>.N' e  M'[a⊢c>b] = M  N'[a⊢c>b] = N  cN'  dM') 
         (M' N'. R = AndR <c>.M' <d>.N' a  b=e  M'[a⊢c>b] = M  N'[a⊢c>b] = N  cN'  dM')"
  using a [[simproc del: defined_all]]
  apply(nominal_induct R avoiding: a b c d e M N rule: trm.strong_induct)
             apply(auto split: if_splits simp add: trm.inject alpha)[1]
            apply(auto split: if_splits simp add: trm.inject alpha)[1]
           apply(auto split: if_splits simp add: trm.inject alpha)[1]
          apply(auto split: if_splits simp add: trm.inject alpha)[1]
         apply(simp add: abs_fresh fresh_left calc_atm fresh_prod fresh_atm trm.inject alpha)[1]
         apply(case_tac "coname3=a")
          apply(simp)
          apply(rule_tac x="[(coname1,c)]trm1" in exI)
          apply(perm_simp)
          apply(auto simp add: abs_fresh fresh_left calc_atm fresh_prod fresh_atm)[1]
          apply(rule_tac x="[(coname2,d)]trm2" in exI)
          apply(perm_simp)
          apply(auto simp add: abs_fresh fresh_left calc_atm fresh_prod fresh_atm trm.inject alpha split: if_splits)[1]
           apply(drule sym)
           apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst])
           apply(simp add: eqvts calc_atm)
          apply(drule_tac s="trm2[a⊢c>e]" in  sym)
          apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst])
          apply(simp add: eqvts calc_atm)
         apply(simp)
         apply(rule_tac x="[(coname1,c)]trm1" in exI)
         apply(perm_simp)
         apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
         apply(rule_tac x="[(coname2,d)]trm2" in exI)
         apply(perm_simp)
         apply(auto simp add: abs_fresh fresh_left calc_atm fresh_prod fresh_atm trm.inject alpha split: if_splits)[1]
          apply(drule sym)
          apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst])
          apply(simp add: eqvts calc_atm)
         apply(drule_tac s="trm2[a⊢c>b]" in  sym)
         apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst])
         apply(simp add: eqvts calc_atm)
        apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject)
  done

lemma crename_OrR1_aux:
  assumes a: "R[a⊢c>b] = OrR1 <c>.M e" 
  shows "(a=e  a=b)  (ae)" 
  using a
  apply(nominal_induct R avoiding: a b c e M rule: trm.strong_induct)
             apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject)
  done

lemma crename_OrR1:
  assumes a: "R[a⊢c>b] = OrR1 <c>.N d" "c(R,a,b)" "d(a,b)"
  shows "N'. (R = OrR1 <c>.N' d)  N'[a⊢c>b] = N" 
  using a
  apply(nominal_induct R avoiding: a b c d N rule: trm.strong_induct)
             apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject)
  apply(rule_tac x="[(coname1,c)]trm" in exI)
  apply(perm_simp)
  apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
  apply(drule sym)
  apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst])
  apply(simp add: eqvts calc_atm)
  done

lemma crename_OrR1':
  assumes a: "R[a⊢c>b] = OrR1 <c>.N d" "c(R,a,b)" "da"
  shows "(N'. (R = OrR1 <c>.N' d)  N'[a⊢c>b] = N) 
         (N'. (R = OrR1 <c>.N' a)  b=d  N'[a⊢c>b] = N)" 
  using a
  apply(nominal_induct R avoiding: a b c d N rule: trm.strong_induct)
             apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject)
   apply(rule_tac x="[(coname1,c)]trm" in exI)
   apply(perm_simp)
   apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
   apply(drule sym)
   apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst])
   apply(simp add: eqvts calc_atm)
  apply(rule_tac x="[(coname1,c)]trm" in exI)
  apply(perm_simp)
  apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
  apply(drule sym)
  apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst])
  apply(simp add: eqvts calc_atm)
  done

lemma crename_OrR2_aux:
  assumes a: "R[a⊢c>b] = OrR2 <c>.M e" 
  shows "(a=e  a=b)  (ae)" 
  using a
  apply(nominal_induct R avoiding: a b c e M rule: trm.strong_induct)
             apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject)
  done

lemma crename_OrR2:
  assumes a: "R[a⊢c>b] = OrR2 <c>.N d" "c(R,a,b)" "d(a,b)"
  shows "N'. (R = OrR2 <c>.N' d)  N'[a⊢c>b] = N" 
  using a
  apply(nominal_induct R avoiding: a b c d N rule: trm.strong_induct)
             apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject)
  apply(rule_tac x="[(coname1,c)]trm" in exI)
  apply(perm_simp)
  apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
  apply(drule sym)
  apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst])
  apply(simp add: eqvts calc_atm)
  done

lemma crename_OrR2':
  assumes a: "R[a⊢c>b] = OrR2 <c>.N d" "c(R,a,b)" "da"
  shows "(N'. (R = OrR2 <c>.N' d)  N'[a⊢c>b] = N) 
         (N'. (R = OrR2 <c>.N' a)  b=d  N'[a⊢c>b] = N)" 
  using a
  apply(nominal_induct R avoiding: a b c d N rule: trm.strong_induct)
             apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject)
   apply(rule_tac x="[(coname1,c)]trm" in exI)
   apply(perm_simp)
   apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
   apply(drule sym)
   apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst])
   apply(simp add: eqvts calc_atm)
  apply(rule_tac x="[(coname1,c)]trm" in exI)
  apply(perm_simp)
  apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
  apply(drule sym)
  apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst])
  apply(simp add: eqvts calc_atm)
  done

lemma crename_OrL:
  assumes a: "R[a⊢c>b] = OrL (x).M (y).N z" "x(y,z,N,R)" "y(x,z,M,R)"
  shows "M' N'. R = OrL (x).M' (y).N' z  M'[a⊢c>b] = M  N'[a⊢c>b] = N  xN'  yM'"
  using a
  apply(nominal_induct R avoiding: a b x y z M N rule: trm.strong_induct)
             apply(auto split: if_splits simp add: trm.inject alpha)
    apply(rule_tac x="[(name2,y)]trm2" in exI)
    apply(perm_simp)
    apply(auto simp add: abs_fresh fresh_left calc_atm fresh_prod fresh_atm)[1]
   apply(rule_tac x="[(name1,x)]trm1" in exI)
   apply(perm_simp)
   apply(auto simp add: abs_fresh fresh_left calc_atm fresh_prod fresh_atm)[1]
  apply(rule_tac x="[(name1,x)]trm1" in exI)
  apply(perm_simp)
  apply(auto simp add: abs_fresh fresh_left calc_atm fresh_prod fresh_atm)[1]
  apply(rule_tac x="[(name2,y)]trm2" in exI)
  apply(perm_simp)
  apply(auto simp add: abs_fresh fresh_left calc_atm fresh_prod fresh_atm)[1]
   apply(drule sym)
   apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst])
   apply(simp add: eqvts calc_atm)
  apply(drule_tac s="trm2[a⊢c>b]" in  sym)
  apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst])
  apply(simp add: eqvts calc_atm)
  done

lemma crename_ImpL:
  assumes a: "R[a⊢c>b] = ImpL <c>.M (y).N z" "c(a,b,N,R)" "y(z,M,R)"
  shows "M' N'. R = ImpL <c>.M' (y).N' z  M'[a⊢c>b] = M  N'[a⊢c>b] = N  cN'  yM'"
  using a
  apply(nominal_induct R avoiding: a b c y z M N rule: trm.strong_induct)
             apply(auto split: if_splits simp add: trm.inject alpha)
    apply(rule_tac x="[(name1,y)]trm2" in exI)
    apply(perm_simp)
    apply(auto simp add: abs_fresh fresh_left calc_atm fresh_prod fresh_atm)[1]
   apply(rule_tac x="[(coname,c)]trm1" in exI)
   apply(perm_simp)
   apply(auto simp add: abs_fresh fresh_left calc_atm fresh_prod fresh_atm)[1]
  apply(rule_tac x="[(coname,c)]trm1" in exI)
  apply(perm_simp)
  apply(auto simp add: abs_fresh fresh_left calc_atm fresh_prod fresh_atm)[1]
  apply(rule_tac x="[(name1,y)]trm2" in exI)
  apply(perm_simp)
  apply(auto simp add: abs_fresh fresh_left calc_atm fresh_prod fresh_atm)[1]
   apply(drule sym)
   apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst])
   apply(simp add: eqvts calc_atm)
  apply(drule_tac s="trm2[a⊢c>b]" in  sym)
  apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst])
  apply(simp add: eqvts calc_atm)
  done

lemma crename_ImpR_aux:
  assumes a: "R[a⊢c>b] = ImpR (x).<c>.M e" 
  shows "(a=e  a=b)  (ae)" 
  using a
  apply(nominal_induct R avoiding: x a b c e M rule: trm.strong_induct)
             apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject)
  done

lemma crename_ImpR:
  assumes a: "R[a⊢c>b] = ImpR (x).<c>.N d" "c(R,a,b)" "d(a,b)" "xR" 
  shows "N'. (R = ImpR (x).<c>.N' d)  N'[a⊢c>b] = N" 
  using a
  apply(nominal_induct R avoiding: a b x c d N rule: trm.strong_induct)
             apply(auto split: if_splits simp add: fresh_prod fresh_atm abs_perm alpha abs_fresh trm.inject)
   apply(rule_tac x="[(name,x)]trm" in exI)
   apply(perm_simp)
  apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
  apply(rule_tac x="[(name,x)][(coname1, c)]trm" in exI)
  apply(perm_simp)
  apply(simp add: abs_supp fin_supp abs_fresh fresh_left calc_atm fresh_prod)
  apply(drule sym)
  apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst])
  apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst])
  apply(simp add: eqvts calc_atm)
  done

lemma crename_ImpR':
  assumes a: "R[a⊢c>b] = ImpR (x).<c>.N d" "c(R,a,b)" "xR" "da"
  shows "(N'. (R = ImpR (x).<c>.N' d)  N'[a⊢c>b] = N) 
         (N'. (R = ImpR (x).<c>.N' a)  b=d  N'[a⊢c>b] = N)" 
  using a
  apply(nominal_induct R avoiding: x a b c d N rule: trm.strong_induct)
             apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject abs_perm calc_atm)
   apply(rule_tac x="[(name,x)][(coname1,c)]trm" in exI)
   apply(perm_simp)
   apply(simp add: abs_fresh fresh_left calc_atm fresh_prod abs_supp fin_supp)
   apply(drule sym)
   apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst])
   apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst])
   apply(simp add: eqvts calc_atm)
  apply(rule_tac x="[(name,x)][(coname1,c)]trm" in exI)
  apply(perm_simp)
  apply(simp add: abs_fresh fresh_left calc_atm fresh_prod abs_supp fin_supp)
  apply(drule sym)
  apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst])
  apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst])
  apply(simp add: eqvts calc_atm)
  done

lemma crename_ax2:
  assumes a: "N[a⊢c>b] = Ax x c"
  shows "d. N = Ax x d"
  using a
  apply(nominal_induct N avoiding: a b rule: trm.strong_induct)
             apply(auto split: if_splits)
  apply(simp add: trm.inject)
  done

lemma crename_interesting1:
  assumes a: "distinct [a,b,c]"
  shows "M[a⊢c>c][c⊢c>b] = M[c⊢c>b][a⊢c>b]"
  using a
  apply(nominal_induct M avoiding: a c b rule: trm.strong_induct)
             apply(auto simp add: rename_fresh simp add: trm.inject alpha)
     apply(blast)
    apply(rotate_tac 12)
    apply(drule_tac x="a" in meta_spec)
    apply(rotate_tac 15)
    apply(drule_tac x="c" in meta_spec)
    apply(rotate_tac 15)
    apply(drule_tac x="b" in meta_spec)
    apply(blast)
   apply(blast)
  apply(blast)
  done

lemma crename_interesting2:
  assumes a: "ac" "ad" "ab" "cd" "bc"
  shows "M[a⊢c>b][c⊢c>d] = M[c⊢c>d][a⊢c>b]"
  using a
  apply(nominal_induct M avoiding: a c b d rule: trm.strong_induct)
             apply(auto simp add: rename_fresh simp add: trm.inject alpha)
  done

lemma crename_interesting3:
  shows "M[a⊢c>c][x⊢n>y] = M[x⊢n>y][a⊢c>c]"
  apply(nominal_induct M avoiding: a c x y rule: trm.strong_induct)
             apply(auto simp add: rename_fresh simp add: trm.inject alpha)
  done

lemma crename_credu:
  assumes a: "(M[a⊢c>b]) c M'"
  shows "M0. M0[a⊢c>b]=M'  M c M0"
  using a
  apply(nominal_induct M"M[a⊢c>b]" M' avoiding: M a b rule: c_redu.strong_induct)
   apply(drule sym)
   apply(drule crename_Cut)
     apply(simp)
    apply(simp)
   apply(auto)
   apply(rule_tac x="M'{a:=(x).N'}" in exI)
   apply(rule conjI)
    apply(simp add: fresh_atm abs_fresh subst_comm fresh_prod)
   apply(rule c_redu.intros)
     apply(auto dest: not_fic_crename)[1]
    apply(simp add: abs_fresh)
   apply(simp add: abs_fresh)
  apply(drule sym)
  apply(drule crename_Cut)
    apply(simp)
   apply(simp)
  apply(auto)
  apply(rule_tac x="N'{x:=<a>.M'}" in exI)
  apply(rule conjI)
   apply(simp add: fresh_atm abs_fresh subst_comm fresh_prod)
  apply(rule c_redu.intros)
    apply(auto dest: not_fin_crename)[1]
   apply(simp add: abs_fresh)
  apply(simp add: abs_fresh)
  done

lemma crename_lredu:
  assumes a: "(M[a⊢c>b]) l M'"
  shows "M0. M0[a⊢c>b]=M'  M l M0"
  using a
  apply(nominal_induct M"M[a⊢c>b]" M' avoiding: M a b rule: l_redu.strong_induct)
         apply(drule sym)
         apply(drule crename_Cut)
           apply(simp add: fresh_prod fresh_atm)
          apply(simp)
         apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1]
         apply(case_tac "aa=ba")
          apply(simp add: crename_id)
          apply(rule l_redu.intros)
            apply(simp)
           apply(simp add: fresh_atm)
          apply(assumption)
         apply(frule crename_ax2)
         apply(auto)[1]
         apply(case_tac "d=aa")
          apply(simp add: trm.inject)
          apply(rule_tac x="M'[a⊢c>aa]" in exI)
          apply(rule conjI)
           apply(rule crename_interesting1)
           apply(simp)
          apply(rule l_redu.intros)
            apply(simp)
           apply(simp add: fresh_atm)
          apply(auto dest: fic_crename simp add: fresh_prod fresh_atm)[1]
         apply(simp add: trm.inject)
         apply(rule_tac x="M'[a⊢c>b]" in exI)
         apply(rule conjI)
          apply(rule crename_interesting2)
              apply(simp)
             apply(simp)
            apply(simp)
           apply(simp)
          apply(simp)
         apply(rule l_redu.intros)
           apply(simp)
          apply(simp add: fresh_atm)
         apply(auto dest: fic_crename simp add: fresh_prod fresh_atm)[1]
        apply(drule sym)
        apply(drule crename_Cut)
          apply(simp add: fresh_prod fresh_atm)
         apply(simp add: fresh_prod fresh_atm)
        apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1]
        apply(case_tac "aa=b")
         apply(simp add: crename_id)
         apply(rule l_redu.intros)
           apply(simp)
          apply(simp add: fresh_atm)
         apply(assumption)
        apply(frule crename_ax2)
        apply(auto)[1]
        apply(case_tac "d=aa")
         apply(simp add: trm.inject)
        apply(simp add: trm.inject)
        apply(rule_tac x="N'[x⊢n>y]" in exI)
        apply(rule conjI)
         apply(rule sym)
         apply(rule crename_interesting3)
        apply(rule l_redu.intros)
          apply(simp)
         apply(simp add: fresh_atm)
        apply(auto dest: fin_crename simp add: fresh_prod fresh_atm)[1]
    (* LNot *)
       apply(drule sym)
       apply(drule crename_Cut)
         apply(simp add: fresh_prod abs_fresh fresh_atm)
        apply(simp add: fresh_prod abs_fresh fresh_atm)
       apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1]
       apply(drule crename_NotR)
         apply(simp add: fresh_prod abs_fresh fresh_atm)
        apply(simp add: fresh_prod abs_fresh fresh_atm)
       apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1]
       apply(drule crename_NotL)
        apply(simp add: fresh_prod abs_fresh fresh_atm)
       apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1]
       apply(rule_tac x="Cut <b>.N'b (x).N'a" in exI)
       apply(simp add: fresh_atm)[1]
       apply(rule l_redu.intros)
            apply(auto simp add: fresh_prod intro: crename_fresh_interesting2)[1]
           apply(auto simp add: fresh_atm fresh_prod intro: crename_fresh_interesting2)[1]
          apply(auto simp add: fresh_atm fresh_prod intro: crename_fresh_interesting1)[1]
         apply(auto simp add: fresh_atm fresh_prod intro: crename_fresh_interesting1)[1]
        apply(simp add: fresh_atm)
       apply(simp add: fresh_atm)
    (* LAnd1 *)
      apply(auto dest: fin_crename simp add: fresh_prod fresh_atm)[1]
      apply(drule sym)
      apply(drule crename_Cut)
        apply(simp add: fresh_prod abs_fresh fresh_atm)
       apply(simp add: fresh_prod abs_fresh fresh_atm)
      apply(auto)[1]
      apply(drule crename_AndR)
         apply(simp add: fresh_prod abs_fresh fresh_atm)
        apply(simp add: fresh_prod abs_fresh fresh_atm)
       apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1]
      apply(drule crename_AndL1)
       apply(simp add: fresh_prod abs_fresh fresh_atm)
      apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1]
      apply(rule_tac x="Cut <a1>.M'a (x).N'a" in exI)
      apply(simp add: fresh_atm)[1]
      apply(rule l_redu.intros)
           apply(auto simp add: fresh_atm abs_fresh fresh_prod intro: crename_fresh_interesting1)[1]
          apply(auto simp add: abs_fresh fresh_atm fresh_prod intro: crename_fresh_interesting2)[1]
         apply(auto simp add: fresh_atm fresh_prod intro: crename_fresh_interesting1)[1]
        apply(auto simp add: fresh_atm fresh_prod intro: crename_fresh_interesting1)[1]
       apply(simp add: fresh_atm)
      apply(simp add: fresh_atm)
    (* LAnd2 *)
     apply(auto dest: fin_crename simp add: fresh_prod fresh_atm)[1]
     apply(drule sym)
     apply(drule crename_Cut)
       apply(simp add: fresh_prod abs_fresh fresh_atm)
      apply(simp add: fresh_prod abs_fresh fresh_atm)
     apply(auto)[1]
     apply(drule crename_AndR)
        apply(simp add: fresh_prod abs_fresh fresh_atm)
       apply(simp add: fresh_prod abs_fresh fresh_atm)
      apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1]
     apply(drule crename_AndL2)
      apply(simp add: fresh_prod abs_fresh fresh_atm)
     apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1]
     apply(rule_tac x="Cut <a2>.N'b (x).N'a" in exI)
     apply(simp add: fresh_atm)[1]
     apply(rule l_redu.intros)
          apply(auto simp add: fresh_atm abs_fresh fresh_prod intro: crename_fresh_interesting1)[1]
         apply(auto simp add: abs_fresh fresh_atm fresh_prod intro: crename_fresh_interesting2)[1]
        apply(auto simp add: fresh_atm fresh_prod intro: crename_fresh_interesting1)[1]
       apply(auto simp add: fresh_atm fresh_prod intro: crename_fresh_interesting1)[1]
      apply(simp add: fresh_atm)
     apply(simp add: fresh_atm)
    (* LOr1 *)
    apply(auto dest: fin_crename simp add: fresh_prod fresh_atm)[1]
    apply(drule sym)
    apply(drule crename_Cut)
      apply(simp add: fresh_prod abs_fresh fresh_atm)
     apply(simp add: fresh_prod abs_fresh fresh_atm)
    apply(auto)[1]
    apply(drule crename_OrL)
      apply(simp add: fresh_prod abs_fresh fresh_atm)
     apply(simp add: fresh_prod abs_fresh fresh_atm)
    apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1]
    apply(drule crename_OrR1)
      apply(simp add: fresh_prod abs_fresh fresh_atm)
     apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1]
    apply(auto)
    apply(rule_tac x="Cut <a>.N' (x1).M'a" in exI)
    apply(rule conjI)
     apply(simp add: abs_fresh fresh_atm)[1]
    apply(rule l_redu.intros)
         apply(auto simp add: fresh_atm abs_fresh fresh_prod intro: crename_fresh_interesting1)[1]
        apply(auto simp add: abs_fresh fresh_atm fresh_prod intro: crename_fresh_interesting2)[1]
       apply(auto simp add: abs_fresh fresh_atm fresh_prod intro: crename_fresh_interesting1)[1]
      apply(auto simp add: abs_fresh fresh_atm fresh_prod intro: crename_fresh_interesting1)[1]
     apply(simp add: fresh_atm)
    apply(simp add: fresh_atm)
    (* LOr2 *)
   apply(auto dest: fin_crename simp add: fresh_prod fresh_atm)[1]
   apply(drule sym)
   apply(drule crename_Cut)
     apply(simp add: fresh_prod abs_fresh fresh_atm)
    apply(simp add: fresh_prod abs_fresh fresh_atm)
   apply(auto)[1]
   apply(drule crename_OrL)
     apply(simp add: fresh_prod abs_fresh fresh_atm)
    apply(simp add: fresh_prod abs_fresh fresh_atm)
   apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1]
   apply(drule crename_OrR2)
     apply(simp add: fresh_prod abs_fresh fresh_atm)
    apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1]
   apply(auto)
   apply(rule_tac x="Cut <a>.N' (x2).N'a" in exI)
   apply(rule conjI)
    apply(simp add: abs_fresh fresh_atm)[1]
   apply(rule l_redu.intros)
        apply(auto simp add: fresh_atm abs_fresh fresh_prod intro: crename_fresh_interesting1)[1]
       apply(auto simp add: abs_fresh fresh_atm fresh_prod intro: crename_fresh_interesting2)[1]
      apply(auto simp add: abs_fresh fresh_atm fresh_prod intro: crename_fresh_interesting1)[1]
     apply(auto simp add: abs_fresh fresh_atm fresh_prod intro: crename_fresh_interesting1)[1]
    apply(simp add: fresh_atm)
   apply(simp add: fresh_atm)
    (* ImpL *)
  apply(auto dest: fin_crename simp add: fresh_prod fresh_atm)[1]
  apply(drule sym)
  apply(drule crename_Cut)
    apply(simp add: fresh_prod abs_fresh fresh_atm)
   apply(simp add: fresh_prod abs_fresh fresh_atm abs_supp fin_supp)
  apply(auto)[1]
  apply(drule crename_ImpL)
    apply(simp add: fresh_prod abs_fresh fresh_atm)
   apply(simp add: fresh_prod abs_fresh fresh_atm)
  apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1]
  apply(drule crename_ImpR)
     apply(simp add: fresh_prod abs_fresh fresh_atm)
    apply(simp add: fresh_prod abs_fresh fresh_atm)
   apply(simp)
  apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1]
  apply(rule_tac x="Cut <a>.(Cut <c>.M'a (x).N') (y).N'a" in exI)
  apply(rule conjI)
   apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
  apply(rule l_redu.intros)
       apply(auto simp add: fresh_atm abs_fresh abs_supp fin_supp fresh_prod intro: crename_fresh_interesting2)[1]
      apply(auto simp add: abs_fresh fresh_atm abs_supp fin_supp fresh_prod intro: crename_fresh_interesting1)[1]
     apply(auto simp add: abs_fresh fresh_atm abs_supp fin_supp fresh_prod intro: crename_fresh_interesting2)[1]
    apply(auto simp add: abs_fresh fresh_atm abs_supp fin_supp fresh_prod intro: crename_fresh_interesting1)[1]
   apply(auto simp add: abs_fresh fresh_atm abs_supp fin_supp fresh_prod intro: crename_fresh_interesting1)[1]
  apply(auto simp add: abs_fresh fresh_atm abs_supp fin_supp fresh_prod intro: crename_fresh_interesting1)[1]
  done

lemma crename_aredu:
  assumes a: "(M[a⊢c>b]) a M'" "ab"
  shows "M0. M0[a⊢c>b]=M'  M a M0"
  using a
  apply(nominal_induct "M[a⊢c>b]" M' avoiding: M a b rule: a_redu.strong_induct)
                  apply(drule  crename_lredu)
                  apply(blast)
                 apply(drule  crename_credu)
                 apply(blast)
    (* Cut *)
                apply(drule sym)
                apply(drule crename_Cut)
                  apply(simp)
                 apply(simp)
                apply(auto)[1]
                apply(drule_tac x="M'a" in meta_spec)
                apply(drule_tac x="aa" in meta_spec)
                apply(drule_tac x="b" in meta_spec)
                apply(auto)[1]
                apply(rule_tac x="Cut <a>.M0 (x).N'" in exI)
                apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
                apply(rule conjI)
                 apply(rule trans)
                  apply(rule crename.simps)
                   apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
                  apply(drule crename_fresh_interesting2)
                  apply(simp add: fresh_a_redu)
                 apply(simp)
                apply(auto)[1]
               apply(drule sym)
               apply(drule crename_Cut)
                 apply(simp)
                apply(simp)
               apply(auto)[1]
               apply(drule_tac x="N'a" in meta_spec)
               apply(drule_tac x="aa" in meta_spec)
               apply(drule_tac x="b" in meta_spec)
               apply(auto)[1]
               apply(rule_tac x="Cut <a>.M' (x).M0" in exI)
               apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
               apply(rule conjI)
                apply(rule trans)
                 apply(rule crename.simps)
                  apply(simp add: abs_fresh abs_supp fin_supp fresh_atm fresh_prod)[1]
                  apply(drule crename_fresh_interesting1)
                   apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
                  apply(simp add: fresh_a_redu)
                 apply(simp)
                apply(simp)
               apply(auto)[1]
    (* NotL *)
              apply(drule sym)
              apply(drule crename_NotL)
               apply(simp)
              apply(auto)[1]
              apply(drule_tac x="N'" in meta_spec)
              apply(drule_tac x="aa" in meta_spec)
              apply(drule_tac x="b" in meta_spec)
              apply(auto)[1]
              apply(rule_tac x="NotL <a>.M0 x" in exI)
              apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
              apply(auto)[1]
    (* NotR *)
             apply(drule sym)
             apply(frule crename_NotR_aux)
             apply(erule disjE)
              apply(auto)[1]
             apply(drule crename_NotR')
               apply(simp)
              apply(simp add: fresh_atm)
             apply(erule disjE)
              apply(auto)[1]
              apply(drule_tac x="N'" in meta_spec)
              apply(drule_tac x="aa" in meta_spec)
              apply(drule_tac x="b" in meta_spec)
              apply(auto)[1]
              apply(rule_tac x="NotR (x).M0 a" in exI)
              apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
              apply(auto)[1]
             apply(auto)[1]
             apply(drule_tac x="N'" in meta_spec)
             apply(drule_tac x="aa" in meta_spec)
             apply(drule_tac x="a" in meta_spec)
             apply(auto)[1]
             apply(rule_tac x="NotR (x).M0 aa" in exI)
             apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
             apply(auto)[1]
    (* AndR *)
            apply(drule sym)
            apply(frule crename_AndR_aux)
            apply(erule disjE)
             apply(auto)[1]
            apply(drule crename_AndR')
               apply(simp add: fresh_prod fresh_atm)
              apply(simp add: fresh_atm)
             apply(simp add: fresh_atm)
            apply(erule disjE)
             apply(auto)[1]
             apply(drule_tac x="M'a" in meta_spec)
             apply(drule_tac x="aa" in meta_spec)
             apply(drule_tac x="ba" in meta_spec)
             apply(auto)[1]
             apply(rule_tac x="AndR <a>.M0 <b>.N' c" in exI)
             apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
             apply(auto)[1]
             apply(rule trans)
              apply(rule crename.simps)
                apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
               apply(simp add: fresh_prod abs_fresh abs_supp fin_supp fresh_atm)[1]
               apply(auto intro: fresh_a_redu)[1]
              apply(simp add: fresh_prod abs_fresh abs_supp fin_supp fresh_atm)[1]
             apply(simp add: fresh_prod abs_fresh abs_supp fin_supp fresh_atm)[1]
            apply(auto)[1]
            apply(drule_tac x="M'a" in meta_spec)
            apply(drule_tac x="aa" in meta_spec)
            apply(drule_tac x="c" in meta_spec)
            apply(auto)[1]
            apply(rule_tac x="AndR <a>.M0 <b>.N' aa" in exI)
            apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
            apply(auto)[1]
            apply(rule trans)
             apply(rule crename.simps)
               apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
              apply(simp add: fresh_prod abs_fresh abs_supp fin_supp fresh_atm)[1]
              apply(auto intro: fresh_a_redu)[1]
             apply(simp add: fresh_prod abs_fresh abs_supp fin_supp fresh_atm)[1]
            apply(simp add: fresh_prod abs_fresh abs_supp fin_supp fresh_atm)[1]
           apply(drule sym)
           apply(frule crename_AndR_aux)
           apply(erule disjE)
            apply(auto)[1]
           apply(drule crename_AndR')
              apply(simp add: fresh_prod fresh_atm)
             apply(simp add: fresh_atm)
            apply(simp add: fresh_atm)
           apply(erule disjE)
            apply(auto)[1]
            apply(drule_tac x="N'a" in meta_spec)
            apply(drule_tac x="aa" in meta_spec)
            apply(drule_tac x="ba" in meta_spec)
            apply(auto)[1]
            apply(rule_tac x="AndR <a>.M' <b>.M0 c" in exI)
            apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
            apply(auto)[1]
            apply(rule trans)
             apply(rule crename.simps)
               apply(simp add: abs_fresh abs_supp fin_supp fresh_atm fresh_prod)[1]
               apply(auto intro: fresh_a_redu)[1]
              apply(simp add: fresh_prod abs_fresh abs_supp fin_supp fresh_atm)[1]
             apply(simp add: fresh_prod abs_fresh abs_supp fin_supp fresh_atm)[1]
            apply(simp add: fresh_prod abs_fresh abs_supp fin_supp fresh_atm)[1]
           apply(auto)[1]
           apply(drule_tac x="N'a" in meta_spec)
           apply(drule_tac x="aa" in meta_spec)
           apply(drule_tac x="c" in meta_spec)
           apply(auto)[1]
           apply(rule_tac x="AndR <a>.M' <b>.M0 aa" in exI)
           apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
           apply(auto)[1]
           apply(rule trans)
            apply(rule crename.simps)
              apply(simp add: abs_fresh abs_supp fin_supp fresh_atm fresh_prod)[1]
              apply(auto intro: fresh_a_redu)[1]
             apply(simp add: fresh_prod abs_fresh abs_supp fin_supp fresh_atm)[1]
            apply(simp add: fresh_prod abs_fresh abs_supp fin_supp fresh_atm)[1]
           apply(simp)
    (* AndL1 *)
          apply(drule sym)
          apply(drule crename_AndL1)
           apply(simp)
          apply(auto)[1]
          apply(drule_tac x="N'" in meta_spec)
          apply(drule_tac x="a" in meta_spec)
          apply(drule_tac x="b" in meta_spec)
          apply(auto)[1]
          apply(rule_tac x="AndL1 (x).M0 y" in exI)
          apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
          apply(auto)[1]
    (* AndL2 *)
         apply(drule sym)
         apply(drule crename_AndL2)
          apply(simp)
         apply(auto)[1]
         apply(drule_tac x="N'" in meta_spec)
         apply(drule_tac x="a" in meta_spec)
         apply(drule_tac x="b" in meta_spec)
         apply(auto)[1]
         apply(rule_tac x="AndL2 (x).M0 y" in exI)
         apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
         apply(auto)[1]
    (* OrL *)
        apply(drule sym)
        apply(drule crename_OrL)
          apply(simp)
          apply(auto simp add: fresh_atm fresh_prod)[1]
         apply(auto simp add: fresh_atm fresh_prod)[1]
        apply(auto)[1]
        apply(drule_tac x="M'a" in meta_spec)
        apply(drule_tac x="a" in meta_spec)
        apply(drule_tac x="b" in meta_spec)
        apply(auto)[1]
        apply(rule_tac x="OrL (x).M0 (y).N' z" in exI)
        apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
        apply(auto)[1]
        apply(rule trans)
         apply(rule crename.simps)
           apply(simp add: abs_fresh abs_supp fin_supp fresh_atm fresh_prod)[1]
          apply(simp add: fresh_prod abs_fresh abs_supp fin_supp fresh_atm)[1]
          apply(auto intro: fresh_a_redu)[1]
         apply(simp add: fresh_prod abs_fresh abs_supp fin_supp fresh_atm)[1]
        apply(simp)
       apply(drule sym)
       apply(drule crename_OrL)
         apply(simp)
         apply(auto simp add: fresh_atm fresh_prod)[1]
        apply(auto simp add: fresh_atm fresh_prod)[1]
       apply(auto)[1]
       apply(drule_tac x="N'a" in meta_spec)
       apply(drule_tac x="a" in meta_spec)
       apply(drule_tac x="b" in meta_spec)
       apply(auto)[1]
       apply(rule_tac x="OrL (x).M' (y).M0 z" in exI)
       apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
       apply(auto)[1]
       apply(rule trans)
        apply(rule crename.simps)
          apply(simp add: abs_fresh abs_supp fin_supp fresh_atm fresh_prod)[1]
          apply(auto intro: fresh_a_redu)[1]
         apply(simp add: fresh_prod abs_fresh abs_supp fin_supp fresh_atm)[1]
        apply(simp)
       apply(simp)
    (* OrR1 *)
      apply(drule sym)
      apply(frule crename_OrR1_aux)
      apply(erule disjE)
       apply(auto)[1]
      apply(drule crename_OrR1')
        apply(simp)
       apply(simp add: fresh_atm)
      apply(erule disjE)
       apply(auto)[1]
       apply(drule_tac x="N'" in meta_spec)
       apply(drule_tac x="aa" in meta_spec)
       apply(drule_tac x="ba" in meta_spec)
       apply(auto)[1]
       apply(rule_tac x="OrR1 <a>.M0 b" in exI)
       apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
       apply(auto)[1]
      apply(auto)[1]
      apply(drule_tac x="N'" in meta_spec)
      apply(drule_tac x="aa" in meta_spec)
      apply(drule_tac x="b" in meta_spec)
      apply(auto)[1]
      apply(rule_tac x="OrR1 <a>.M0 aa" in exI)
      apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
      apply(auto)[1]
    (* OrR2 *)
     apply(drule sym)
     apply(frule crename_OrR2_aux)
     apply(erule disjE)
      apply(auto)[1]
     apply(drule crename_OrR2')
       apply(simp)
      apply(simp add: fresh_atm)
     apply(erule disjE)
      apply(auto)[1]
      apply(drule_tac x="N'" in meta_spec)
      apply(drule_tac x="aa" in meta_spec)
      apply(drule_tac x="ba" in meta_spec)
      apply(auto)[1]
      apply(rule_tac x="OrR2 <a>.M0 b" in exI)
      apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
      apply(auto)[1]
     apply(auto)[1]
     apply(drule_tac x="N'" in meta_spec)
     apply(drule_tac x="aa" in meta_spec)
     apply(drule_tac x="b" in meta_spec)
     apply(auto)[1]
     apply(rule_tac x="OrR2 <a>.M0 aa" in exI)
     apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
     apply(auto)[1]
    (* ImpL *)
    apply(drule sym)
    apply(drule crename_ImpL)
      apply(simp)
     apply(simp)
    apply(auto)[1]
    apply(drule_tac x="M'a" in meta_spec)
    apply(drule_tac x="aa" in meta_spec)
    apply(drule_tac x="b" in meta_spec)
    apply(auto)[1]
    apply(rule_tac x="ImpL <a>.M0 (x).N' y" in exI)
    apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
    apply(auto)[1]
    apply(rule trans)
     apply(rule crename.simps)
      apply(simp add: abs_fresh abs_supp fin_supp fresh_atm fresh_prod)[1]
     apply(simp add: fresh_prod abs_fresh abs_supp fin_supp fresh_atm)[1]
     apply(auto intro: fresh_a_redu)[1]
    apply(simp add: fresh_prod abs_fresh abs_supp fin_supp fresh_atm)[1]
   apply(drule sym)
   apply(drule crename_ImpL)
     apply(simp)
    apply(simp)
   apply(auto)[1]
   apply(drule_tac x="N'a" in meta_spec)
   apply(drule_tac x="aa" in meta_spec)
   apply(drule_tac x="b" in meta_spec)
   apply(auto)[1]
   apply(rule_tac x="ImpL <a>.M' (x).M0 y" in exI)
   apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
   apply(auto)[1]
   apply(rule trans)
    apply(rule crename.simps)
     apply(simp add: abs_fresh abs_supp fin_supp fresh_atm fresh_prod)[1]
     apply(auto intro: fresh_a_redu)[1]
    apply(simp add: fresh_prod abs_fresh abs_supp fin_supp fresh_atm)[1]
   apply(simp)
    (* ImpR *)
  apply(drule sym)
  apply(frule crename_ImpR_aux)
  apply(erule disjE)
   apply(auto)[1]
  apply(drule crename_ImpR')
     apply(simp)
    apply(simp add: fresh_atm)
   apply(simp add: fresh_atm)
  apply(erule disjE)
   apply(auto)[1]
   apply(drule_tac x="N'" in meta_spec)
   apply(drule_tac x="aa" in meta_spec)
   apply(drule_tac x="ba" in meta_spec)
   apply(auto)[1]
   apply(rule_tac x="ImpR (x).<a>.M0 b" in exI)
   apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
   apply(auto)[1]
  apply(auto)[1]
  apply(drule_tac x="N'" in meta_spec)
  apply(drule_tac x="aa" in meta_spec)
  apply(drule_tac x="b" in meta_spec)
  apply(auto)[1]
  apply(rule_tac x="ImpR (x).<a>.M0 aa" in exI)
  apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
  apply(auto)[1]
  done

lemma SNa_preserved_renaming1:
  assumes a: "SNa M"
  shows "SNa (M[a⊢c>b])"
  using a
  apply(induct rule: SNa_induct)
  apply(case_tac "a=b")
   apply(simp add: crename_id)
  apply(rule SNaI)
  apply(drule crename_aredu)
   apply(blast)+
  done

lemma nrename_interesting1:
  assumes a: "distinct [x,y,z]"
  shows "M[x⊢n>z][z⊢n>y] = M[z⊢n>y][x⊢n>y]"
  using a
  apply(nominal_induct M avoiding: x y z rule: trm.strong_induct)
             apply(auto simp add: rename_fresh simp add: trm.inject alpha)
     apply(blast)
    apply(blast)
   apply(rotate_tac 12)
   apply(drule_tac x="x" in meta_spec)
   apply(rotate_tac 15)
   apply(drule_tac x="y" in meta_spec)
   apply(rotate_tac 15)
   apply(drule_tac x="z" in meta_spec)
   apply(blast)
  apply(rotate_tac 11)
  apply(drule_tac x="x" in meta_spec)
  apply(rotate_tac 14)
  apply(drule_tac x="y" in meta_spec)
  apply(rotate_tac 14)
  apply(drule_tac x="z" in meta_spec)
  apply(blast)
  done

lemma nrename_interesting2:
  assumes a: "xz" "xu" "xy" "zu" "yz"
  shows "M[x⊢n>y][z⊢n>u] = M[z⊢n>u][x⊢n>y]"
  using a
  apply(nominal_induct M avoiding: x y z u rule: trm.strong_induct)
             apply(auto simp add: rename_fresh simp add: trm.inject alpha)
  done

lemma not_fic_nrename_aux:
  assumes a: "fic M c" 
  shows "fic (M[x⊢n>y]) c" 
  using a
  apply(nominal_induct M avoiding: c x y rule: trm.strong_induct)
             apply(auto dest!: fic_elims intro!: fic.intros simp add: fresh_prod fresh_atm rename_fresh abs_fresh)
  done

lemma not_fic_nrename:
  assumes a: "¬(fic (M[x⊢n>y]) c)" 
  shows "¬(fic M c)" 
  using a
  apply(auto dest:  not_fic_nrename_aux)
  done

lemma fin_nrename:
  assumes a: "fin M z" "z(x,y)"
  shows "fin (M[x⊢n>y]) z" 
  using a
  apply(nominal_induct M avoiding: x y z rule: trm.strong_induct)
             apply(auto dest!: fin_elims intro!: fin.intros simp add: fresh_prod fresh_atm rename_fresh abs_fresh
      split: if_splits)
  done

lemma nrename_fresh_interesting1:
  fixes z::"name"
  assumes a: "z(M[x⊢n>y])" "z(x,y)"
  shows "zM"
  using a
  apply(nominal_induct M avoiding: x y z rule: trm.strong_induct)
             apply(auto split: if_splits simp add: abs_fresh abs_supp fin_supp)
  done

lemma nrename_fresh_interesting2:
  fixes c::"coname"
  assumes a: "c(M[x⊢n>y])" 
  shows "cM"
  using a
  apply(nominal_induct M avoiding: x y c rule: trm.strong_induct)
             apply(auto split: if_splits simp add: abs_fresh abs_supp fin_supp fresh_atm)
  done

lemma fin_nrename2:
  assumes a: "fin (M[x⊢n>y]) z" "z(x,y)"
  shows "fin M z" 
  using a
  apply(nominal_induct M avoiding: x y z rule: trm.strong_induct)
             apply(auto dest!: fin_elims intro!: fin.intros simp add: fresh_prod fresh_atm rename_fresh abs_fresh
      split: if_splits)
        apply(auto dest: nrename_fresh_interesting1 simp add: fresh_atm fresh_prod)
  done

lemma nrename_Cut:
  assumes a: "R[x⊢n>y] = Cut <c>.M (z).N" "c(N,R)" "z(x,y,M,R)"
  shows "M' N'. R = Cut <c>.M' (z).N'  M'[x⊢n>y] = M  N'[x⊢n>y] = N  cN'  zM'"
  using a
  apply(nominal_induct R avoiding: c y x z M N rule: trm.strong_induct)
             apply(auto split: if_splits)
  apply(simp add: trm.inject)
  apply(auto simp add: alpha fresh_atm)
  apply(rule_tac x="[(coname,c)]trm1" in exI)
  apply(perm_simp)
  apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
  apply(rule_tac x="[(name,z)]trm2" in exI)
  apply(perm_simp)
  apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
  apply(rule conjI)
   apply(drule sym)
   apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst])
   apply(simp add: eqvts calc_atm)
  apply(auto simp add: fresh_atm)[1]
  apply(drule sym)
  apply(drule sym)
  apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst])
  apply(simp add: eqvts calc_atm)
  done

lemma nrename_NotR:
  assumes a: "R[x⊢n>y] = NotR (z).N c" "z(R,x,y)" 
  shows "N'. (R = NotR (z).N' c)  N'[x⊢n>y] = N" 
  using a
  apply(nominal_induct R avoiding: x y c z N rule: trm.strong_induct)
             apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject)
  apply(rule_tac x="[(name,z)]trm" in exI)
  apply(perm_simp)
  apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
  apply(drule sym)
  apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst])
  apply(simp add: eqvts calc_atm)
  done

lemma nrename_NotL:
  assumes a: "R[x⊢n>y] = NotL <c>.N z" "cR" "z(x,y)"
  shows "N'. (R = NotL <c>.N' z)  N'[x⊢n>y] = N" 
  using a
  apply(nominal_induct R avoiding: x y c z N rule: trm.strong_induct)
             apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject)
  apply(rule_tac x="[(coname,c)]trm" in exI)
  apply(perm_simp)
  apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
  apply(drule sym)
  apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst])
  apply(simp add: eqvts calc_atm)
  done

lemma nrename_NotL':
  assumes a: "R[x⊢n>y] = NotL <c>.N u" "cR" "xy" 
  shows "(N'. (R = NotL <c>.N' u)  N'[x⊢n>y] = N)  (N'. (R = NotL <c>.N' x)  y=u  N'[x⊢n>y] = N)"
  using a
  apply(nominal_induct R avoiding: y u c x N rule: trm.strong_induct)
             apply(auto split: if_splits simp add: fresh_prod fresh_atm abs_fresh alpha trm.inject)
   apply(rule_tac x="[(coname,c)]trm" in exI)
   apply(perm_simp)
   apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
   apply(drule sym)
   apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst])
   apply(simp add: eqvts calc_atm)
  apply(rule_tac x="[(coname,c)]trm" in exI)
  apply(perm_simp)
  apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
  apply(drule sym)
  apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst])
  apply(simp add: eqvts calc_atm)
  done

lemma nrename_NotL_aux:
  assumes a: "R[x⊢n>y] = NotL <c>.N u" 
  shows "(x=u  x=y)  (xu)" 
  using a
  apply(nominal_induct R avoiding: y u c x N rule: trm.strong_induct)
             apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject)
  done

lemma nrename_AndL1:
  assumes a: "R[x⊢n>y] = AndL1 (z).N u" "z(R,x,y)" "u(x,y)"
  shows "N'. (R = AndL1 (z).N' u)  N'[x⊢n>y] = N" 
  using a
  apply(nominal_induct R avoiding: z u x y N rule: trm.strong_induct)
             apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject)
  apply(rule_tac x="[(name1,z)]trm" in exI)
  apply(perm_simp)
  apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
  apply(drule sym)
  apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst])
  apply(simp add: eqvts calc_atm)
  done

lemma nrename_AndL1':
  assumes a: "R[x⊢n>y] = AndL1 (v).N u" "v(R,u,x,y)" "xy" 
  shows "(N'. (R = AndL1 (v).N' u)  N'[x⊢n>y] = N)  (N'. (R = AndL1 (v).N' x)  y=u  N'[x⊢n>y] = N)"
  using a
  apply(nominal_induct R avoiding: y u v x N rule: trm.strong_induct)
             apply(auto split: if_splits simp add: fresh_prod fresh_atm abs_fresh alpha trm.inject)
   apply(rule_tac x="[(name1,v)]trm" in exI)
   apply(perm_simp)
   apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
   apply(drule sym)
   apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst])
   apply(simp add: eqvts calc_atm)
  apply(rule_tac x="[(name1,v)]trm" in exI)
  apply(perm_simp)
  apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
  apply(drule sym)
  apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst])
  apply(simp add: eqvts calc_atm)
  done

lemma nrename_AndL1_aux:
  assumes a: "R[x⊢n>y] = AndL1 (v).N u" 
  shows "(x=u  x=y)  (xu)" 
  using a
  apply(nominal_induct R avoiding: y u v x N rule: trm.strong_induct)
             apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject)
  done

lemma nrename_AndL2:
  assumes a: "R[x⊢n>y] = AndL2 (z).N u" "z(R,x,y)" "u(x,y)"
  shows "N'. (R = AndL2 (z).N' u)  N'[x⊢n>y] = N" 
  using a
  apply(nominal_induct R avoiding: z u x y N rule: trm.strong_induct)
             apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject)
  apply(rule_tac x="[(name1,z)]trm" in exI)
  apply(perm_simp)
  apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
  apply(drule sym)
  apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst])
  apply(simp add: eqvts calc_atm)
  done

lemma nrename_AndL2':
  assumes a: "R[x⊢n>y] = AndL2 (v).N u" "v(R,u,x,y)" "xy" 
  shows "(N'. (R = AndL2 (v).N' u)  N'[x⊢n>y] = N)  (N'. (R = AndL2 (v).N' x)  y=u  N'[x⊢n>y] = N)"
  using a
  apply(nominal_induct R avoiding: y u v x N rule: trm.strong_induct)
             apply(auto split: if_splits simp add: fresh_prod fresh_atm abs_fresh alpha trm.inject)
   apply(rule_tac x="[(name1,v)]trm" in exI)
   apply(perm_simp)
   apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
   apply(drule sym)
   apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst])
   apply(simp add: eqvts calc_atm)
  apply(rule_tac x="[(name1,v)]trm" in exI)
  apply(perm_simp)
  apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
  apply(drule sym)
  apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst])
  apply(simp add: eqvts calc_atm)
  done

lemma nrename_AndL2_aux:
  assumes a: "R[x⊢n>y] = AndL2 (v).N u" 
  shows "(x=u  x=y)  (xu)" 
  using a
  apply(nominal_induct R avoiding: y u v x N rule: trm.strong_induct)
             apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject)
  done

lemma nrename_AndR:
  assumes a: "R[x⊢n>y] = AndR <c>.M <d>.N e" "c(d,e,