# Theory Class3

theory Class3
imports Class2
```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(rule disjI1)
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(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(rule disjI1)
apply(drule_tac pi="[(a,aa)]" in fic.eqvt(2))
apply(perm_simp)
apply(drule_tac pi="[(a,aa)]" in fic.eqvt(2))
apply(perm_simp)
apply(rule disjI2)
apply(drule_tac pi="[(x,xa)]" in fin.eqvt(1))
apply(perm_simp)
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 "c♯M"
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 "x♯M"
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 ∧ c♯N' ∧ x♯M'"
using a
apply(nominal_induct R avoiding: a b c x M N rule: trm.strong_induct)
apply(auto split: if_splits)
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(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(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(drule sym)
apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst])
apply(drule sym)
apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst])
done

lemma crename_NotR:
assumes a: "R[a⊢c>b] = NotR (x).N c" "x♯R" "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])
done

lemma crename_NotR':
assumes a: "R[a⊢c>b] = NotR (x).N c" "x♯R" "c♯a"
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(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])
done

lemma crename_NotR_aux:
assumes a: "R[a⊢c>b] = NotR (x).N c"
shows "(a=c ∧ a=b) ∨ (a≠c)"
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])
done

lemma crename_AndL1:
assumes a: "R[a⊢c>b] = AndL1 (x).N y" "x♯R"
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])
done

lemma crename_AndL2:
assumes a: "R[a⊢c>b] = AndL2 (x).N y" "x♯R"
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])
done

lemma crename_AndR_aux:
assumes a: "R[a⊢c>b] = AndR <c>.M <d>.N e"
shows "(a=e ∧ a=b) ∨ (a≠e)"
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 ∧ c♯N' ∧ d♯M'"
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(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(drule_tac s="trm2[a⊢c>b]" in  sym)
apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst])
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"
shows "(∃M' N'. R = AndR <c>.M' <d>.N' e ∧ M'[a⊢c>b] = M ∧ N'[a⊢c>b] = N ∧ c♯N' ∧ d♯M') ∨
(∃M' N'. R = AndR <c>.M' <d>.N' a ∧ b=e ∧ M'[a⊢c>b] = M ∧ N'[a⊢c>b] = N ∧ c♯N' ∧ d♯M')"
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)[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(drule_tac s="trm2[a⊢c>e]" in  sym)
apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst])
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(drule_tac s="trm2[a⊢c>b]" in  sym)
apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst])
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) ∨ (a≠e)"
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])
done

lemma crename_OrR1':
assumes a: "R[a⊢c>b] = OrR1 <c>.N d" "c♯(R,a,b)" "d♯a"
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(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])
done

lemma crename_OrR2_aux:
assumes a: "R[a⊢c>b] = OrR2 <c>.M e"
shows "(a=e ∧ a=b) ∨ (a≠e)"
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])
done

lemma crename_OrR2':
assumes a: "R[a⊢c>b] = OrR2 <c>.N d" "c♯(R,a,b)" "d♯a"
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(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])
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 ∧ x♯N' ∧ y♯M'"
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(drule_tac s="trm2[a⊢c>b]" in  sym)
apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst])
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 ∧ c♯N' ∧ y♯M'"
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(drule_tac s="trm2[a⊢c>b]" in  sym)
apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst])
done

lemma crename_ImpR_aux:
assumes a: "R[a⊢c>b] = ImpR (x).<c>.M e"
shows "(a=e ∧ a=b) ∨ (a≠e)"
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)" "x♯R"
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])
done

lemma crename_ImpR':
assumes a: "R[a⊢c>b] = ImpR (x).<c>.N d" "c♯(R,a,b)" "x♯R" "d♯a"
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(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])
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)
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(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: "a≠c" "a≠d" "a≠b" "c≠d" "b≠c"
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)
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)
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(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]
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)
apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1]
apply(case_tac "aa=ba")
apply(rule l_redu.intros)
apply(simp)
apply(assumption)
apply(frule crename_ax2)
apply(auto)[1]
apply(case_tac "d=aa")
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(auto dest: fic_crename simp add: fresh_prod fresh_atm)[1]
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(auto dest: fic_crename simp add: fresh_prod fresh_atm)[1]
apply(drule sym)
apply(drule crename_Cut)
apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1]
apply(case_tac "aa=b")
apply(rule l_redu.intros)
apply(simp)
apply(assumption)
apply(frule crename_ax2)
apply(auto)[1]
apply(case_tac "d=aa")
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(auto dest: fin_crename simp add: fresh_prod fresh_atm)[1]
(* LNot *)
apply(drule sym)
apply(drule crename_Cut)
apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1]
apply(drule crename_NotR)
apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1]
apply(drule crename_NotL)
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(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]
(* LAnd1 *)
apply(auto dest: fin_crename simp add: fresh_prod fresh_atm)[1]
apply(drule sym)
apply(drule crename_Cut)
apply(auto)[1]
apply(drule crename_AndR)
apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1]
apply(drule crename_AndL1)
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(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]
(* LAnd2 *)
apply(auto dest: fin_crename simp add: fresh_prod fresh_atm)[1]
apply(drule sym)
apply(drule crename_Cut)
apply(auto)[1]
apply(drule crename_AndR)
apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1]
apply(drule crename_AndL2)
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(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]
(* LOr1 *)
apply(auto dest: fin_crename simp add: fresh_prod fresh_atm)[1]
apply(drule sym)
apply(drule crename_Cut)
apply(auto)[1]
apply(drule crename_OrL)
apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1]
apply(drule crename_OrR1)
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(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]
(* LOr2 *)
apply(auto dest: fin_crename simp add: fresh_prod fresh_atm)[1]
apply(drule sym)
apply(drule crename_Cut)
apply(auto)[1]
apply(drule crename_OrL)
apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1]
apply(drule crename_OrR2)
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(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]
(* 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 abs_supp fin_supp)
apply(auto)[1]
apply(drule crename_ImpL)
apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1]
apply(drule crename_ImpR)
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'" "a≠b"
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)
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)
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(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(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(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)[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)[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(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(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(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(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(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: "x≠z" "x≠u" "x≠y" "z≠u" "y≠z"
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)
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 "z♯M"
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 "c♯M"
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 ∧ c♯N' ∧ z♯M'"
using a
apply(nominal_induct R avoiding: c y x z M N rule: trm.strong_induct)
apply(auto split: if_splits)
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(drule sym)
apply(drule sym)
apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst])
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])
done

lemma nrename_NotL:
assumes a: "R[x⊢n>y] = NotL <c>.N z" "c♯R" "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])
done

lemma nrename_NotL':
assumes a: "R[x⊢n>y] = NotL <c>.N u" "c♯R" "x≠y"
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(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])
done

lemma nrename_NotL_aux:
assumes a: "R[x⊢n>y] = NotL <c>.N u"
shows "(x=u ∧ x=y) ∨ (x≠u)"
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])
done

lemma nrename_AndL1':
assumes a: "R[x⊢n>y] = AndL1 (v).N u" "v♯(R,u,x,y)" "x≠y"
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(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])
done

lemma nrename_AndL1_aux:
assumes a: "R[x⊢n>y] = AndL1 (v).N u"
shows "(x=u ∧ x=y) ∨ (x≠u)"
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])
done

lemma nrename_AndL2':
assumes a: "R[x⊢n>y] = AndL2 (v).N u" "v♯(R,u,x,y)" "x≠y"
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(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])
done

lemma nrename_AndL2_aux:
assumes a: "R[x⊢n>y] = AndL2 (v).N u"
shows "(x=u ∧ x=y) ∨ (x≠u)"
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,N,R)" "d♯(c,e,M,R)"
shows "∃M' N'. R = AndR <c>.M' <d>.N' e ∧ M'[x⊢n>y] = M ∧ N'[x⊢n>y] = N ∧ c♯N' ∧ d♯M'"
using a
apply(nominal_induct R avoiding: x y c d e M N rule: trm.strong_induct)
apply(auto split: if_splits simp add: trm.inject alpha)
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(drule_tac s="trm2[x⊢n>y]" in  sym)
apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst])
done

lemma nrename_OrR1:
assumes a: "R[x⊢n>y] = OrR1 <c>.N d" "c♯(R,d)"
shows "∃N'. (R = OrR1 <c>.N' d) ∧ N'[x⊢n>y] = N"
using a
apply(nominal_induct R avoiding: x y 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])
done

lemma nrename_OrR2:
assumes a: "R[x⊢n>y] = OrR2 <c>.N d" "c♯(R,d)"
shows "∃N'. (R = OrR2 <c>.N' d) ∧ N'[x⊢n>y] = N"
using a
apply(nominal_induct R avoiding: x y 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])
done

lemma nrename_OrL:
assumes a: "R[u⊢n>v] = OrL (x).M (y).N z" "x♯(y,z,u,v,N,R)" "y♯(x,z,u,v,M,R)" "z♯(u,v)"
shows "∃M' N'. R = OrL (x).M' (y).N' z ∧ M'[u⊢n>v] = M ∧ N'[u⊢n>v] = N ∧ x♯N' ∧ y♯M'"
using a
apply(nominal_induct R avoiding: u v x y z M N rule: trm.strong_induct)
apply(auto split: if_splits simp add: trm.inject alpha fresh_prod fresh_atm)
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(drule_tac s="trm2[u⊢n>v]" in  sym)
apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst])
done

lemma nrename_OrL':
assumes a: "R[x⊢n>y] = OrL (v).M (w).N u" "v♯(R,N,u,x,y)" "w♯(R,M,u,x,y)" "x≠y"
shows "(∃M' N'. (R = OrL (v).M' (w).N' u) ∧ M'[x⊢n>y] = M ∧ N'[x⊢n>y] = N) ∨
(∃M' N'. (R = OrL (v).M' (w).N' x) ∧ y=u ∧ M'[x⊢n>y] = M ∧ N'[x⊢n>y] = N)"
using a
apply(nominal_induct R avoiding: y x u v w M 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)]∙trm1" in exI)
apply(perm_simp)
apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
apply(rule_tac x="[(name2,w)]∙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_name_inst,OF at_name_inst])
apply(drule_tac s="trm2[x⊢n>u]" in sym)
apply(drule_tac pt_bij1[OF pt_name_inst,OF at_name_inst])
apply(rule_tac x="[(name1,v)]∙trm1" in exI)
apply(perm_simp)
apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
apply(rule_tac x="[(name2,w)]∙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_name_inst,OF at_name_inst])
apply(drule_tac s="trm2[x⊢n>y]" in sym)
apply(drule_tac pt_bij1[OF pt_name_inst,OF at_name_inst])
done

lemma nrename_OrL_aux:
assumes a: "R[x⊢n>y] = OrL (v).M (w).N u"
shows "(x=u ∧ x=y) ∨ (x≠u)"
using a
apply(nominal_induct R avoiding: y x w u v M N rule: trm.strong_induct)
apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject)
done

lemma nrename_ImpL:
assumes a: "R[x⊢n>y] = ImpL <c>.M (u).N z" "c♯(N,R)" "u♯(y,x,z,M,R)" "z♯(x,y)"
shows "∃M' N'. R = ImpL <c>.M' (u).N' z ∧ M'[x⊢n>y] = M ∧ N'[x⊢n>y] = N ∧ c♯N' ∧ u♯M'"
using a
apply(nominal_induct R avoiding: u x c y z M N rule: trm.strong_induct)
apply(auto split: if_splits simp add: trm.inject alpha fresh_prod fresh_atm)
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,u)]∙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(drule_tac s="trm2[x⊢n>y]" in  sym)
apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst])
apply(simp add: eqvts calc_atm fresh_prod fresh_atm)
done

lemma nrename_ImpL':
assumes a: "R[x⊢n>y] = ImpL <c>.M (w).N u" "c♯(R,N)" "w♯(R,M,u,x,y)" "x≠y"
shows "(∃M' N'. (R = ImpL <c>.M' (w).N' u) ∧ M'[x⊢n>y] = M ∧ N'[x⊢n>y] = N) ∨
(∃M' N'. (R = ImpL <c>.M' (w).N' x) ∧ y=u ∧ M'[x⊢n>y] = M ∧ N'[x⊢n>y] = N)"
using a
apply(nominal_induct R avoiding: y x u c w M 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)]∙trm1" in exI)
apply(perm_simp)
apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
apply(rule_tac x="[(name1,w)]∙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(drule_tac s="trm2[x⊢n>u]" in sym)
apply(drule_tac pt_bij1[OF pt_name_inst,OF at_name_inst])
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="[(name1,w)]∙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(drule_tac s="trm2[x⊢n>y]" in sym)
apply(drule_tac pt_bij1[OF pt_name_inst,OF at_name_inst])
done

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

lemma nrename_ImpR:
assumes a: "R[u⊢n>v] = ImpR (x).<c>.N d" "c♯(R,d)" "x♯(R,u,v)"
shows "∃N'. (R = ImpR (x).<c>.N' d) ∧ N'[u⊢n>v] = N"
using a
apply(nominal_induct R avoiding: u v 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])
done

lemma nrename_credu:
assumes a: "(M[x⊢n>y]) ⟶⇩c M'"
shows "∃M0. M0[x⊢n>y]=M' ∧ M ⟶⇩c M0"
using a
apply(nominal_induct M≡"M[x⊢n>y]" M' avoiding: M x y rule: c_redu.strong_induct)
apply(drule sym)
apply(drule nrename_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_nrename)[1]
apply(drule sym)
apply(drule nrename_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)
apply(drule_tac x="xa" and y="y" in fin_nrename)
done

lemma nrename_ax2:
assumes a: "N[x⊢n>y] = Ax z c"
shows "∃z. N = Ax z c"
using a
apply(nominal_induct N avoiding: x y rule: trm.strong_induct)
apply(auto split: if_splits)
done

lemma fic_nrename:
assumes a: "fic (M[x⊢n>y]) c"
shows "fic M 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
split: if_splits)
apply(auto dest: nrename_fresh_interesting2 simp add: fresh_prod fresh_atm)
done

lemma nrename_lredu:
assumes a: "(M[x⊢n>y]) ⟶⇩l M'"
shows "∃M0. M0[x⊢n>y]=M' ∧ M ⟶⇩l M0"
using a
apply(nominal_induct M≡"M[x⊢n>y]" M' avoiding: M x y rule: l_redu.strong_induct)
apply(drule sym)
apply(drule nrename_Cut)
apply(simp)
apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1]
apply(case_tac "xa=y")
apply(rule l_redu.intros)
apply(simp)
apply(assumption)
apply(frule nrename_ax2)
apply(auto)[1]
apply(case_tac "z=xa")
apply(simp)
apply(rule_tac x="M'[a⊢c>b]" in exI)
apply(rule conjI)
apply(rule crename_interesting3)
apply(rule l_redu.intros)
apply(simp)
apply(auto dest: fic_nrename simp add: fresh_prod fresh_atm)[1]
apply(drule sym)
apply(drule nrename_Cut)
apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1]
apply(case_tac "xa=ya")
apply(rule l_redu.intros)
apply(simp)
apply(assumption)
apply(frule nrename_ax2)
apply(auto)[1]
apply(case_tac "z=xa")
apply(rule_tac x="N'[x⊢n>xa]" in exI)
apply(rule conjI)
apply(rule nrename_interesting1)
apply(auto)[1]
apply(rule l_redu.intros)
apply(simp)
apply(auto dest: fin_nrename2 simp add: fresh_prod fresh_atm)[1]
apply(rule_tac x="N'[x⊢n>y]" in exI)
apply(rule conjI)
apply(rule nrename_interesting2)
apply(simp_all)
apply(rule l_redu.intros)
apply(simp)
apply(auto dest: fin_nrename2 simp add: fresh_prod fresh_atm)[1]
(* LNot *)
apply(drule sym)
apply(drule nrename_Cut)
apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1]
apply(drule nrename_NotR)
apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1]
apply(drule nrename_NotL)
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(rule l_redu.intros)
apply(auto simp add: fresh_prod fresh_atm intro: nrename_fresh_interesting1)[1]
apply(auto simp add: fresh_atm fresh_prod intro: nrename_fresh_interesting1)[1]
apply(auto simp add: fresh_atm fresh_prod intro: nrename_fresh_interesting2)[1]
apply(auto simp add: fresh_atm fresh_prod intro: nrename_fresh_interesting2)[1]
(* LAnd1 *)
apply(auto dest: fin_crename simp add: fresh_prod fresh_atm)[1]
apply(drule sym)
apply(drule nrename_Cut)
apply(auto)[1]
apply(drule nrename_AndR)
apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1]
apply(drule nrename_AndL1)
apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1]
apply(rule_tac x="Cut <a1>.M'a (x).N'b" in exI)
apply(rule l_redu.intros)
apply(auto simp add: fresh_atm abs_fresh fresh_prod intro: nrename_fresh_interesting2)[1]
apply(auto simp add: abs_fresh fresh_atm fresh_prod intro: nrename_fresh_interesting1)[1]
apply(auto simp add: fresh_atm fresh_prod intro: nrename_fresh_interesting1)[1]
apply(auto simp add: fresh_atm fresh_prod intro: nrename_fresh_interesting1)[1]
apply(auto simp add: fresh_atm fresh_prod intro: nrename_fresh_interesting1)[1]
(* LAnd2 *)
apply(auto dest: fin_crename simp add: fresh_prod fresh_atm)[1]
apply(drule sym)
apply(drule nrename_Cut)
apply(auto)[1]
apply(drule nrename_AndR)
apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1]
apply(drule nrename_AndL2)
apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1]
apply(rule_tac x="Cut <a2>.N'a (x).N'b" in exI)
apply(rule l_redu.intros)
apply(auto simp add: fresh_atm abs_fresh fresh_prod intro: nrename_fresh_interesting2)[1]
apply(auto simp add: abs_fresh fresh_atm fresh_prod intro: nrename_fresh_interesting1)[1]
apply(auto simp add: fresh_atm fresh_prod intro: nrename_fresh_interesting1)[1]
apply(auto simp add: fresh_atm fresh_prod intro: nrename_fresh_interesting1)[1]
apply(auto simp add: fresh_atm fresh_prod intro: nrename_fresh_interesting1)[1]
(* LOr1 *)
apply(auto dest: fin_crename simp add: fresh_prod fresh_atm)[1]
apply(drule sym)
apply(drule nrename_Cut)
apply(auto)[1]
apply(drule nrename_OrL)
apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1]
apply(drule nrename_OrR1)
apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1]
apply(rule_tac x="Cut <a>.N' (x1).M'a" in exI)
apply(rule conjI)
apply(rule l_redu.intros)
apply(auto simp add: fresh_atm abs_fresh fresh_prod intro: nrename_fresh_interesting2)[1]
apply(auto simp add: abs_fresh fresh_atm fresh_prod intro: nrename_fresh_interesting1)[1]
apply(auto simp add: abs_fresh fresh_atm fresh_prod intro: nrename_fresh_interesting1)[1]
apply(auto simp add: abs_fresh fresh_atm fresh_prod intro: nrename_fresh_interesting1)[1]
(* LOr2 *)
apply(auto dest: fin_crename simp add: fresh_prod fresh_atm)[1]
apply(drule sym)
apply(drule nrename_Cut)
apply(auto)[1]
apply(drule nrename_OrL)
apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1]
apply(drule nrename_OrR2)
apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1]
apply(rule_tac x="Cut <a>.N' (x2).N'a" in exI)
apply(rule conjI)
apply(rule l_redu.intros)
apply(auto simp add: fresh_atm abs_fresh fresh_prod intro: nrename_fresh_interesting2)[1]
apply(auto simp add: abs_fresh fresh_atm fresh_prod intro: nrename_fresh_interesting1)[1]
apply(auto simp add: abs_fresh fresh_atm fresh_prod intro: nrename_fresh_interesting1)[1]
apply(auto simp add: abs_fresh fresh_atm fresh_prod intro: nrename_fresh_interesting1)[1]
(* ImpL *)
apply(auto dest: fin_crename simp add: fresh_prod fresh_atm)[1]
apply(drule sym)
apply(drule nrename_Cut)
apply(simp add: fresh_prod abs_fresh fresh_atm abs_supp fin_supp)
apply(auto)[1]
apply(drule nrename_ImpL)
apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1]
apply(drule nrename_ImpR)
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: nrename_fresh_interesting1)[1]
apply(auto simp add: abs_fresh fresh_atm abs_supp fin_supp fresh_prod intro: nrename_fresh_interesting2)[1]
apply(auto simp add: abs_fresh fresh_atm abs_supp fin_supp fresh_prod intro: nrename_fresh_interesting1)[1]
apply(auto simp add: abs_fresh fresh_atm abs_supp fin_supp fresh_prod intro: nrename_fresh_interesting2)[1]
apply(auto simp add: abs_fresh fresh_atm abs_supp fin_supp fresh_prod intro: nrename_fresh_interesting2)[1]
apply(auto simp add: abs_fresh fresh_atm abs_supp fin_supp fresh_prod intro: nrename_fresh_interesting2)[1]
done

lemma nrename_aredu:
assumes a: "(M[x⊢n>y]) ⟶⇩a M'" "x≠y"
shows "∃M0. M0[x⊢n>y]=M' ∧ M ⟶⇩a M0"
using a
apply(nominal_induct "M[x⊢n>y]" M' avoiding: M x y rule: a_redu.strong_induct)
apply(drule  nrename_lredu)
apply(blast)
apply(drule  nrename_credu)
apply(blast)
(* Cut *)
apply(drule sym)
apply(drule nrename_Cut)
apply(simp)
apply(simp)
apply(auto)[1]
apply(drule_tac x="M'a" in meta_spec)
apply(drule_tac x="xa" in meta_spec)
apply(drule_tac x="y" 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 nrename.simps)
apply(drule nrename_fresh_interesting2)
apply(simp add: fresh_prod abs_fresh abs_supp fin_supp fresh_atm)[1]
apply(drule nrename_fresh_interesting1)
apply(simp)
apply(auto)[1]
apply(drule sym)
apply(drule nrename_Cut)
apply(simp)
apply(simp)
apply(auto)[1]
apply(drule_tac x="N'a" in meta_spec)
apply(drule_tac x="xa" in meta_spec)
apply(drule_tac x="y" 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 nrename.simps)
apply(simp add: abs_fresh abs_supp fin_supp fresh_atm fresh_prod)[1]
apply(simp)
apply(auto)[1]
(* NotL *)
apply(drule sym)
apply(frule nrename_NotL_aux)
apply(erule disjE)
apply(auto)[1]
apply(drule nrename_NotL')
apply(simp)
apply(erule disjE)
apply(auto)[1]
apply(drule_tac x="N'" in meta_spec)
apply(drule_tac x="xa" in meta_spec)
apply(drule_tac x="y" 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]
apply(auto)[1]
apply(drule_tac x="N'" in meta_spec)
apply(drule_tac x="xa" in meta_spec)
apply(drule_tac x="x" in meta_spec)
apply(auto)[1]
apply(rule_tac x="NotL <a>.M0 xa" in exI)
apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
apply(auto)[1]
(* NotR *)
apply(drule sym)
apply(drule nrename_NotR)
apply(simp)
apply(auto)[1]
apply(drule_tac x="N'" in meta_spec)
apply(drule_tac x="xa" in meta_spec)
apply(drule_tac x="y" 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]
(* AndR *)
apply(drule sym)
apply(drule nrename_AndR)
apply(simp)
apply(auto)[1]
apply(drule_tac x="M'a" in meta_spec)
apply(drule_tac x="x" in meta_spec)
apply(drule_tac x="y" 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 nrename.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 nrename_AndR)
apply(simp)
apply(auto)[1]
apply(drule_tac x="N'a" in meta_spec)
apply(drule_tac x="x" in meta_spec)
apply(drule_tac x="y" 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 nrename.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)
(* AndL1 *)
apply(drule sym)
apply(frule nrename_AndL1_aux)
apply(erule disjE)
apply(auto)[1]
apply(drule nrename_AndL1')
apply(simp)
apply(erule disjE)
apply(auto)[1]
apply(drule_tac x="N'" in meta_spec)
apply(drule_tac x="xa" in meta_spec)
apply(drule_tac x="ya" 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]
apply(auto)[1]
apply(drule_tac x="N'" in meta_spec)
apply(drule_tac x="xa" in meta_spec)
apply(drule_tac x="y" in meta_spec)
apply(auto)[1]
apply(rule_tac x="AndL1 (x).M0 xa" in exI)
apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
apply(auto)[1]
(* AndL2 *)
apply(drule sym)
apply(frule nrename_AndL2_aux)
apply(erule disjE)
apply(auto)[1]
apply(drule nrename_AndL2')
apply(simp)
apply(erule disjE)
apply(auto)[1]
apply(drule_tac x="N'" in meta_spec)
apply(drule_tac x="xa" in meta_spec)
apply(drule_tac x="ya" 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]
apply(auto)[1]
apply(drule_tac x="N'" in meta_spec)
apply(drule_tac x="xa" in meta_spec)
apply(drule_tac x="y" in meta_spec)
apply(auto)[1]
apply(rule_tac x="AndL2 (x).M0 xa" in exI)
apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
apply(auto)[1]
(* OrL *)
apply(drule sym)
apply(frule nrename_OrL_aux)
apply(erule disjE)
apply(auto)[1]
apply(drule nrename_OrL')
apply(erule disjE)
apply(auto)[1]
apply(drule_tac x="M'a" in meta_spec)
apply(drule_tac x="xa" in meta_spec)
apply(drule_tac x="ya" 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 nrename.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="xa" in meta_spec)
apply(drule_tac x="z" in meta_spec)
apply(auto)[1]
apply(rule_tac x="OrL (x).M0 (y).N' xa" in exI)
apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
apply(auto)[1]
apply(rule trans)
apply(rule nrename.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 nrename_OrL_aux)
apply(erule disjE)
apply(auto)[1]
apply(drule nrename_OrL')
apply(erule disjE)
apply(auto)[1]
apply(drule_tac x="N'a" in meta_spec)
apply(drule_tac x="xa" in meta_spec)
apply(drule_tac x="ya" 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 nrename.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="xa" in meta_spec)
apply(drule_tac x="z" in meta_spec)
apply(auto)[1]
apply(rule_tac x="OrL (x).M' (y).M0 xa" in exI)
apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
apply(auto)[1]
apply(rule trans)
apply(rule nrename.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 add: fresh_prod abs_fresh abs_supp fin_supp fresh_atm)[1]
(* OrR1 *)
apply(drule sym)
apply(drule nrename_OrR1)
apply(simp)
apply(auto)[1]
apply(drule_tac x="N'" in meta_spec)
apply(drule_tac x="x" in meta_spec)
apply(drule_tac x="y" 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]
(* OrR2 *)
apply(drule sym)
apply(drule nrename_OrR2)
apply(simp)
apply(auto)[1]
apply(drule_tac x="N'" in meta_spec)
apply(drule_tac x="x" in meta_spec)
apply(drule_tac x="y" 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]
(* ImpL *)
apply(drule sym)
apply(frule nrename_ImpL_aux)
apply(erule disjE)
apply(auto)[1]
apply(drule nrename_ImpL')
apply(erule disjE)
apply(auto)[1]
apply(drule_tac x="M'a" in meta_spec)
apply(drule_tac x="xa" in meta_spec)
apply(drule_tac x="ya" 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 nrename.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(auto)[1]
apply(drule_tac x="M'a" in meta_spec)
apply(drule_tac x="xa" in meta_spec)
apply(drule_tac x="y" in meta_spec)
apply(auto)[1]
apply(rule_tac x="ImpL <a>.M0 (x).N' xa" in exI)
apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
apply(auto)[1]
apply(rule trans)
apply(rule nrename.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(drule sym)
apply(frule nrename_ImpL_aux)
apply(erule disjE)
apply(auto)[1]
apply(drule nrename_ImpL')
apply(erule disjE)
apply(auto)[1]
apply(drule_tac x="N'a" in meta_spec)
apply(drule_tac x="xa" in meta_spec)
apply(drule_tac x="ya" 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 nrename.simps)
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="N'a" in meta_spec)
apply(drule_tac x="xa" in meta_spec)
apply(drule_tac x="y" in meta_spec)
apply(auto)[1]
apply(rule_tac x="ImpL <a>.M' (x).M0 xa" in exI)
apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
apply(auto)[1]
apply(rule trans)
apply(rule nrename.simps)
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]
(* ImpR *)
apply(drule sym)
apply(drule nrename_ImpR)
apply(simp)
apply(simp)
apply(auto)[1]
apply(drule_tac x="N'" in meta_spec)
apply(drule_tac x="xa" in meta_spec)
apply(drule_tac x="y" 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]
done

lemma SNa_preserved_renaming2:
assumes a: "SNa N"
shows "SNa (N[x⊢n>y])"
using a
apply(induct rule: SNa_induct)
apply(case_tac "x=y")
apply(rule SNaI)
apply(drule nrename_aredu)
apply(blast)+
done

text ‹helper-stuff to set up the induction›

abbreviation
SNa_set :: "trm set"
where
"SNa_set ≡ {M. SNa M}"

abbreviation
A_Redu_set :: "(trm×trm) set"
where
"A_Redu_set ≡ {(N,M)| M N. M ⟶⇩a N}"

lemma SNa_elim:
assumes a: "SNa M"
shows "(∀M. (∀N. M ⟶⇩a N ⟶ P N)⟶ P M) ⟶ P M"
using a
by (induct rule: SNa.induct) (blast)

lemma wf_SNa_restricted:
shows "wf (A_Redu_set ∩ (UNIV × SNa_set))"
apply(unfold wf_def)
apply(intro strip)
apply(case_tac "SNa x")
apply(simp (no_asm_use))
apply(drule_tac P="P" in SNa_elim)
apply(erule mp)
apply(blast)
(* other case *)
apply(drule_tac x="x" in spec)
apply(erule mp)
apply(fast)
done

definition SNa_Redu :: "(trm × trm) set" where
"SNa_Redu ≡ A_Redu_set ∩ (UNIV × SNa_set)"

lemma wf_SNa_Redu:
shows "wf SNa_Redu"
apply(unfold SNa_Redu_def)
apply(rule wf_SNa_restricted)
done

lemma wf_measure_triple:
shows "wf ((measure size) <*lex*> SNa_Redu <*lex*> SNa_Redu)"
by (auto intro: wf_SNa_Redu)

lemma my_wf_induct_triple:
assumes a: " wf(r1 <*lex*> r2 <*lex*> r3)"
and     b: "⋀x. ⟦⋀y. ((fst y,fst (snd y),snd (snd y)),(fst x,fst (snd x), snd (snd x)))
∈ (r1 <*lex*> r2 <*lex*> r3) ⟶ P y⟧ ⟹ P x"
shows "P x"
using a
apply(induct x rule: wf_induct_rule)
apply(rule b)
apply(simp)
done

lemma my_wf_induct_triple':
assumes a: " wf(r1 <*lex*> r2 <*lex*> r3)"
and    b: "⋀x1 x2 x3. ⟦⋀y1 y2 y3. ((y1,y2,y3),(x1,x2,x3)) ∈ (r1 <*lex*> r2 <*lex*> r3) ⟶ P (y1,y2,y3)⟧
⟹ P (x1,x2,x3)"
shows "P (x1,x2,x3)"
apply(rule_tac my_wf_induct_triple[OF a])
apply(case_tac x rule: prod.exhaust)
apply(simp)
apply(rename_tac p a b)
apply(case_tac b)
apply(simp)
apply(rule b)
apply(blast)
done

lemma my_wf_induct_triple'':
assumes a: " wf(r1 <*lex*> r2 <*lex*> r3)"
and     b: "⋀x1 x2 x3. ⟦⋀y1 y2 y3. ((y1,y2,y3),(x1,x2,x3)) ∈ (r1 <*lex*> r2 <*lex*> r3) ⟶ P y1 y2 y3⟧
⟹ P x1 x2 x3"
shows "P x1 x2 x3"
apply(rule_tac my_wf_induct_triple'[where P="λ(x1,x2,x3). P x1 x2 x3", simplified])
apply(rule a)
apply(rule b)
apply(auto)
done

lemma excluded_m:
assumes a: "<a>:M ∈ (∥<B>∥)" "(x):N ∈ (∥(B)∥)"
shows "(<a>:M ∈ BINDINGc B (∥(B)∥) ∨ (x):N ∈ BINDINGn B (∥<B>∥))
∨¬(<a>:M ∈ BINDINGc B (∥(B)∥) ∨ (x):N ∈ BINDINGn B (∥<B>∥))"
by (blast)

lemma tricky_subst:
assumes a1: "b♯(c,N)"
and     a2: "z♯(x,P)"
and     a3: "M≠Ax z b"
shows "(Cut <c>.N (z).M){b:=(x).P} = Cut <c>.N (z).(M{b:=(x).P})"
using a1 a2 a3
apply -
apply(generate_fresh "coname")
apply(subgoal_tac "Cut <c>.N (z).M = Cut <ca>.([(ca,c)]∙N) (z).M")
apply(simp)
apply(rule trans)
apply(rule better_Cut_substc)
apply(simp)
apply(simp)
apply(subgoal_tac "b♯([(ca,c)]∙N)")
apply(simp add: fresh_left calc_atm fresh_prod fresh_atm)
apply(rule sym)
done

text ‹3rd lemma›

lemma CUT_SNa_aux:
assumes a1: "<a>:M ∈ (∥<B>∥)"
and     a2: "SNa M"
and     a3: "(x):N ∈ (∥(B)∥)"
and     a4: "SNa N"
shows   "SNa (Cut <a>.M (x).N)"
using a1 a2 a3 a4
apply(induct B M N arbitrary: a x rule: my_wf_induct_triple''[OF wf_measure_triple])
apply(rule SNaI)
apply(drule Cut_a_redu_elim)
apply(erule disjE)
(* left-inner reduction *)
apply(erule exE)
apply(erule conjE)+
apply(simp)
apply(drule_tac x="x1" in meta_spec)
apply(drule_tac x="M'a" in meta_spec)
apply(drule_tac x="x3" in meta_spec)
apply(drule conjunct2)
apply(drule mp)
apply(rule conjI)
apply(simp)
apply(rule disjI1)
apply(drule_tac x="a" in spec)
apply(drule mp)
apply(drule mp)
apply(drule_tac x="x" in spec)
apply(simp)
apply(erule disjE)
(* right-inner reduction *)
apply(erule exE)
apply(erule conjE)+
apply(simp)
apply(drule_tac x="x1" in meta_spec)
apply(drule_tac x="x2" in meta_spec)
apply(drule_tac x="N'" in meta_spec)
apply(drule conjunct2)
apply(drule mp)
apply(rule conjI)
apply(simp)
apply(rule disjI2)
apply(drule_tac x="a" in spec)
apply(drule mp)
apply(drule mp)
apply(assumption)
apply(drule_tac x="x" in spec)
apply(drule mp)
apply(drule mp)
apply(assumption)
apply(erule disjE)
(******** c-reduction *********)
apply(drule Cut_c_redu_elim)
(* c-left reduction*)
apply(erule disjE)
apply(erule conjE)
apply(frule_tac B="x1" in fic_CANDS)
apply(simp)
apply(erule disjE)
(* in AXIOMSc *)
apply(erule exE)+
apply(erule disjE)
apply(simp)
apply(rule impI)
apply(simp)
apply(subgoal_tac "fic (Ax y b) b")(*A*)
apply(simp)
(*A*)
apply(auto)[1]
apply(simp)
apply(rule impI)
apply(simp)
apply(subgoal_tac "fic (Ax ([(a,aa)]∙y) a) a")(*B*)
apply(simp)
(*B*)
apply(auto)[1]
(* in BINDINGc *)
apply(simp)
apply(drule BINDINGc_elim)
apply(simp)
(* c-right reduction*)
apply(erule conjE)
apply(frule_tac B="x1" in fin_CANDS)
apply(simp)
apply(erule disjE)
(* in AXIOMSc *)
apply(erule exE)+
apply(erule disjE)
apply(simp)
apply(rule impI)
apply(simp)
apply(subgoal_tac "fin (Ax xa b) xa")(*A*)
apply(simp)
(*A*)
apply(auto)[1]
apply(simp)
apply(rule impI)
apply(simp)
apply(subgoal_tac "fin (Ax x ([(x,xa)]∙b)) x")(*B*)
apply(simp)
(*B*)
apply(auto)[1]
(* in BINDINGc *)
apply(simp)
apply(drule BINDINGn_elim)
apply(simp)
(*********** l-reductions ************)
apply(drule Cut_l_redu_elim)
apply(erule disjE)
(* ax1 *)
apply(erule exE)
apply(simp)
apply(erule disjE)
(* ax2 *)
apply(erule exE)
apply(erule disjE)
(* LNot *)
apply(erule exE)+
apply(auto)[1]
apply(frule_tac excluded_m)
apply(assumption)
apply(erule disjE)
(* one of them in BINDING *)
apply(erule disjE)
apply(drule fin_elims)
apply(drule fic_elims)
apply(simp)
apply(drule BINDINGc_elim)
apply(drule_tac x="x" in spec)
apply(drule_tac x="NotL <b>.N' x" in spec)
apply(simp)
apply(generate_fresh "coname")
apply(subgoal_tac "fresh_fun (λa'. Cut <a'>.NotR (y).M'a a' (x).NotL <b>.N' x)
=  Cut <c>.NotR (y).M'a c (x).NotL <b>.N' x")
apply(simp)
apply(subgoal_tac "Cut <c>.NotR (y).M'a c (x).NotL <b>.N' x ⟶⇩a Cut <b>.N' (y).M'a")
apply(simp only: a_preserves_SNa)
apply(rule al_redu)
apply(rule better_LNot_intro)
apply(simp)
apply(simp)
apply(fresh_fun_simp (no_asm))
apply(simp)
(* other case of in BINDING *)
apply(drule fin_elims)
apply(drule fic_elims)
apply(simp)
apply(drule BINDINGn_elim)
apply(drule_tac x="a" in spec)
apply(drule_tac x="NotR (y).M'a a" in spec)
apply(simp)
apply(generate_fresh "name")
apply(subgoal_tac "fresh_fun (λx'. Cut <a>.NotR (y).M'a a (x').NotL <b>.N' x')
= Cut <a>.NotR (y).M'a a (c).NotL <b>.N' c")
apply(simp)
apply(subgoal_tac "Cut <a>.NotR (y).M'a a (c).NotL <b>.N' c ⟶⇩a Cut <b>.N' (y).M'a")
apply(simp only: a_preserves_SNa)
apply(rule al_redu)
apply(rule better_LNot_intro)
apply(simp)
apply(simp)
apply(fresh_fun_simp (no_asm))
apply(simp)
(* none of them in BINDING *)
apply(simp)
apply(erule conjE)
apply(frule CAND_NotR_elim)
apply(assumption)
apply(erule exE)
apply(frule CAND_NotL_elim)
apply(assumption)
apply(erule exE)
apply(simp only: ty.inject)
apply(drule_tac x="B'" in meta_spec)
apply(drule_tac x="N'" in meta_spec)
apply(drule_tac x="M'a" in meta_spec)
apply(erule conjE)+
apply(drule mp)
apply(simp)
apply(drule_tac x="b" in spec)
apply(rotate_tac 13)
apply(drule mp)
apply(assumption)
apply(rotate_tac 13)
apply(drule mp)
apply(drule_tac x="y" in spec)
apply(rotate_tac 13)
apply(drule mp)
apply(assumption)
apply(rotate_tac 13)
apply(drule mp)
apply(assumption)
(* LAnd1 case *)
apply(erule disjE)
apply(erule exE)+
apply(auto)[1]
apply(frule_tac excluded_m)
apply(assumption)
apply(erule disjE)
(* one of them in BINDING *)
apply(erule disjE)
apply(drule fin_elims)
apply(drule fic_elims)
apply(simp)
apply(drule BINDINGc_elim)
apply(drule_tac x="x" in spec)
apply(drule_tac x="AndL1 (y).N' x" in spec)
apply(simp)
apply(generate_fresh "coname")
apply(subgoal_tac "fresh_fun (λa'. Cut <a'>.AndR <b>.M1 <c>.M2 a' (x).AndL1 (y).N' x)
= Cut <ca>.AndR <b>.M1 <c>.M2 ca (x).AndL1 (y).N' x")
apply(simp)
apply(subgoal_tac "Cut <ca>.AndR <b>.M1 <c>.M2 ca (x).AndL1 (y).N' x ⟶⇩a Cut <b>.M1 (y).N'")
apply(auto intro: a_preserves_SNa)[1]
apply(rule al_redu)
apply(rule better_LAnd1_intro)
apply(simp)
apply(fresh_fun_simp (no_asm))
apply(simp)
(* other case of in BINDING *)
apply(drule fin_elims)
apply(drule fic_elims)
apply(simp)
apply(drule BINDINGn_elim)
apply(drule_tac x="a" in spec)
apply(drule_tac x="AndR <b>.M1 <c>.M2 a" in spec)
apply(simp)
apply(generate_fresh "name")
apply(subgoal_tac "fresh_fun (λz'. Cut <a>.AndR <b>.M1 <c>.M2 a (z').AndL1 (y).N' z')
= Cut <a>.AndR <b>.M1 <c>.M2 a (ca).AndL1 (y).N' ca")
apply(simp)
apply(subgoal_tac "Cut <a>.AndR <b>.M1 <c>.M2 a (ca).AndL1 (y).N' ca ⟶⇩a Cut <b>.M1 (y).N'")
apply(auto intro: a_preserves_SNa)[1]
apply(rule al_redu)
apply(rule better_LAnd1_intro)
apply(fresh_fun_simp (no_asm))
apply(simp)
(* none of them in BINDING *)
apply(simp)
apply(erule conjE)
apply(frule CAND_AndR_elim)
apply(assumption)
apply(erule exE)
apply(frule CAND_AndL1_elim)
apply(assumption)
apply(erule exE)+
apply(simp only: ty.inject)
apply(drule_tac x="B1" in meta_spec)
apply(drule_tac x="M1" in meta_spec)
apply(drule_tac x="N'" in meta_spec)
apply(erule conjE)+
apply(drule mp)
apply(simp)
apply(drule_tac x="b" in spec)
apply(rotate_tac 14)
apply(drule mp)
apply(assumption)
apply(rotate_tac 14)
apply(drule mp)
apply(drule_tac x="y" in spec)
apply(rotate_tac 15)
apply(drule mp)
apply(assumption)
apply(rotate_tac 15)
apply(drule mp)
apply(assumption)
(* LAnd2 case *)
apply(erule disjE)
apply(erule exE)+
apply(auto)[1]
apply(frule_tac excluded_m)
apply(assumption)
apply(erule disjE)
(* one of them in BINDING *)
apply(erule disjE)
apply(drule fin_elims)
apply(drule fic_elims)
apply(simp)
apply(drule BINDINGc_elim)
apply(drule_tac x="x" in spec)
apply(drule_tac x="AndL2 (y).N' x" in spec)
apply(simp)
apply(generate_fresh "coname")
apply(subgoal_tac "fresh_fun (λa'. Cut <a'>.AndR <b>.M1 <c>.M2 a' (x).AndL2 (y).N' x)
= Cut <ca>.AndR <b>.M1 <c>.M2 ca (x).AndL2 (y).N' x")
apply(simp)
apply(subgoal_tac "Cut <ca>.AndR <b>.M1 <c>.M2 ca (x).AndL2 (y).N' x ⟶⇩a Cut <c>.M2 (y).N'")
apply(auto intro: a_preserves_SNa)[1]
apply(rule al_redu)
apply(rule better_LAnd2_intro)
apply(simp)
apply(fresh_fun_simp (no_asm))
apply(simp)
(* other case of in BINDING *)
apply(drule fin_elims)
apply(drule fic_elims)
apply(simp)
apply(drule BINDINGn_elim)
apply(drule_tac x="a" in spec)
apply(drule_tac x="AndR <b>.M1 <c>.M2 a" in spec)
apply(simp)
apply(generate_fresh "name")
apply(subgoal_tac "fresh_fun (λz'. Cut <a>.AndR <b>.M1 <c>.M2 a (z').AndL2 (y).N' z')
= Cut <a>.AndR <b>.M1 <c>.M2 a (ca).AndL2 (y).N' ca")
apply(simp)
apply(subgoal_tac "Cut <a>.AndR <b>.M1 <c>.M2 a (ca).AndL2 (y).N' ca ⟶⇩a Cut <c>.M2 (y).N'")
apply(auto intro: a_preserves_SNa)[1]
apply(rule al_redu)
apply(rule better_LAnd2_intro)
apply(fresh_fun_simp (no_asm))
apply(simp)
(* none of them in BINDING *)
apply(simp)
apply(erule conjE)
apply(frule CAND_AndR_elim)
apply(assumption)
apply(erule exE)
apply(frule CAND_AndL2_elim)
apply(assumption)
apply(erule exE)+
apply(simp only: ty.inject)
apply(drule_tac x="B2" in meta_spec)
apply(drule_tac x="M2" in meta_spec)
apply(drule_tac x="N'" in meta_spec)
apply(erule conjE)+
apply(drule mp)
apply(simp)
apply(drule_tac x="c" in spec)
apply(rotate_tac 14)
apply(drule mp)
apply(assumption)
apply(rotate_tac 14)
apply(drule mp)
apply(drule_tac x="y" in spec)
apply(rotate_tac 15)
apply(drule mp)
apply(assumption)
apply(rotate_tac 15)
apply(drule mp)
apply(assumption)
(* LOr1 case *)
apply(erule disjE)
apply(erule exE)+
apply(auto)[1]
apply(frule_tac excluded_m)
apply(assumption)
apply(erule disjE)
(* one of them in BINDING *)
apply(erule disjE)
apply(drule fin_elims)
apply(drule fic_elims)
apply(simp)
apply(drule BINDINGc_elim)
apply(drule_tac x="x" in spec)
apply(drule_tac x="OrL (z).M1 (y).M2 x" in spec)
apply(simp)
apply(generate_fresh "coname")
apply(subgoal_tac "fresh_fun (λa'. Cut <a'>.OrR1 <b>.N' a' (x).OrL (z).M1 (y).M2 x)
= Cut <c>.OrR1 <b>.N' c (x).OrL (z).M1 (y).M2 x")
apply(simp)
apply(subgoal_tac "Cut <c>.OrR1 <b>.N' c (x).OrL (z).M1 (y).M2 x ⟶⇩a Cut <b>.N' (z).M1")
apply(auto intro: a_preserves_SNa)[1]
apply(rule al_redu)
apply(rule better_LOr1_intro)
apply(fresh_fun_simp (no_asm))
apply(simp)
(* other case of in BINDING *)
apply(drule fin_elims)
apply(drule fic_elims)
apply(simp)
apply(drule BINDINGn_elim)
apply(drule_tac x="a" in spec)
apply(drule_tac x="OrR1 <b>.N' a" in spec)
apply(simp)
apply(generate_fresh "name")
apply(subgoal_tac "fresh_fun (λz'. Cut <a>.OrR1 <b>.N' a (z').OrL (z).M1 (y).M2 z')
= Cut <a>.OrR1 <b>.N' a (c).OrL (z).M1 (y).M2 c")
apply(simp)
apply(subgoal_tac "Cut <a>.OrR1 <b>.N' a (c).OrL (z).M1 (y).M2 c ⟶⇩a Cut <b>.N' (z).M1")
apply(auto intro: a_preserves_SNa)[1]
apply(rule al_redu)
apply(rule better_LOr1_intro)
apply(fresh_fun_simp (no_asm))
apply(simp)
(* none of them in BINDING *)
apply(simp)
apply(erule conjE)
apply(frule CAND_OrR1_elim)
apply(assumption)
apply(erule exE)+
apply(frule CAND_OrL_elim)
apply(assumption)
apply(erule exE)+
apply(simp only: ty.inject)
apply(drule_tac x="B1" in meta_spec)
apply(drule_tac x="N'" in meta_spec)
apply(drule_tac x="M1" in meta_spec)
apply(erule conjE)+
apply(drule mp)
apply(simp)
apply(drule_tac x="b" in spec)
apply(rotate_tac 15)
apply(drule mp)
apply(assumption)
apply(rotate_tac 15)
apply(drule mp)
apply(drule_tac x="z" in spec)
apply(rotate_tac 15)
apply(drule mp)
apply(assumption)
apply(rotate_tac 15)
apply(drule mp)
apply(assumption)
(* LOr2 case *)
apply(erule disjE)
apply(erule exE)+
apply(auto)[1]
apply(frule_tac excluded_m)
apply(assumption)
apply(erule disjE)
(* one of them in BINDING *)
apply(erule disjE)
apply(drule fin_elims)
apply(drule fic_elims)
apply(simp)
apply(drule BINDINGc_elim)
apply(drule_tac x="x" in spec)
apply(drule_tac x="OrL (z).M1 (y).M2 x" in spec)
apply(simp)
apply(generate_fresh "coname")
apply(subgoal_tac "fresh_fun (λa'. Cut <a'>.OrR2 <b>.N' a' (x).OrL (z).M1 (y).M2 x)
= Cut <c>.OrR2 <b>.N' c (x).OrL (z).M1 (y).M2 x")
apply(simp)
apply(subgoal_tac "Cut <c>.OrR2 <b>.N' c (x).OrL (z).M1 (y).M2 x ⟶⇩a Cut <b>.N' (y).M2")
apply(auto intro: a_preserves_SNa)[1]
apply(rule al_redu)
apply(rule better_LOr2_intro)
apply(fresh_fun_simp (no_asm))
apply(simp)
(* other case of in BINDING *)
apply(drule fin_elims)
apply(drule fic_elims)
apply(simp)
apply(drule BINDINGn_elim)
apply(drule_tac x="a" in spec)
apply(drule_tac x="OrR2 <b>.N' a" in spec)
apply(simp)
apply(generate_fresh "name")
apply(subgoal_tac "fresh_fun (λz'. Cut <a>.OrR2 <b>.N' a (z').OrL (z).M1 (y).M2 z')
= Cut <a>.OrR2 <b>.N' a (c).OrL (z).M1 (y).M2 c")
apply(simp)
apply(subgoal_tac "Cut <a>.OrR2 <b>.N' a (c).OrL (z).M1 (y).M2 c ⟶⇩a Cut <b>.N' (y).M2")
apply(auto intro: a_preserves_SNa)[1]
apply(rule al_redu)
apply(rule better_LOr2_intro)
apply(fresh_fun_simp (no_asm))
apply(simp)
(* none of them in BINDING *)
apply(simp)
apply(erule conjE)
apply(frule CAND_OrR2_elim)
apply(assumption)
apply(erule exE)+
apply(frule CAND_OrL_elim)
apply(assumption)
apply(erule exE)+
apply(simp only: ty.inject)
apply(drule_tac x="B2" in meta_spec)
apply(drule_tac x="N'" in meta_spec)
apply(drule_tac x="M2" in meta_spec)
apply(erule conjE)+
apply(drule mp)
apply(simp)
apply(drule_tac x="b" in spec)
apply(rotate_tac 15)
apply(drule mp)
apply(assumption)
apply(rotate_tac 15)
apply(drule mp)
apply(drule_tac x="y" in spec)
apply(rotate_tac 15)
apply(drule mp)
apply(assumption)
apply(rotate_tac 15)
apply(drule mp)
apply(assumption)
(* LImp case *)
apply(erule exE)+
apply(auto)[1]
apply(frule_tac excluded_m)
apply(assumption)
apply(erule disjE)
(* one of them in BINDING *)
apply(erule disjE)
apply(drule fin_elims)
apply(drule fic_elims)
apply(simp)
apply(drule BINDINGc_elim)
apply(drule_tac x="x" in spec)
apply(drule_tac x="ImpL <c>.N1 (y).N2 x" in spec)
apply(simp)
apply(generate_fresh "coname")
apply(subgoal_tac "fresh_fun (λa'. Cut <a'>.ImpR (z).<b>.M'a a' (x).ImpL <c>.N1 (y).N2 x)
= Cut <ca>.ImpR (z).<b>.M'a ca (x).ImpL <c>.N1 (y).N2 x")
apply(simp)
apply(subgoal_tac "Cut <ca>.ImpR (z).<b>.M'a ca (x).ImpL <c>.N1 (y).N2 x ⟶⇩a
Cut <b>.Cut <c>.N1 (z).M'a (y).N2")
apply(auto intro: a_preserves_SNa)[1]
apply(rule al_redu)
apply(rule better_LImp_intro)
apply(simp)
apply(fresh_fun_simp (no_asm))
apply(simp)
(* other case of in BINDING *)
apply(drule fin_elims)
apply(drule fic_elims)
apply(simp)
apply(drule BINDINGn_elim)
apply(drule_tac x="a" in spec)
apply(drule_tac x="ImpR (z).<b>.M'a a" in spec)
apply(simp)
apply(generate_fresh "name")
apply(subgoal_tac "fresh_fun (λz'. Cut <a>.ImpR (z).<b>.M'a a (z').ImpL <c>.N1 (y).N2 z')
= Cut <a>.ImpR (z).<b>.M'a a (ca).ImpL <c>.N1 (y).N2 ca")
apply(simp)
apply(subgoal_tac "Cut <a>.ImpR (z).<b>.M'a a (ca).ImpL <c>.N1 (y).N2 ca ⟶⇩a
Cut <b>.Cut <c>.N1 (z).M'a (y).N2")
apply(auto intro: a_preserves_SNa)[1]
apply(rule al_redu)
apply(rule better_LImp_intro)
apply(simp)
apply(fresh_fun_simp (no_asm))
apply(simp)
(* none of them in BINDING *)
apply(erule conjE)
apply(frule CAND_ImpL_elim)
apply(assumption)
apply(erule exE)+
apply(frule CAND_ImpR_elim) (* check here *)
apply(assumption)
apply(erule exE)+
apply(erule conjE)+
apply(simp only: ty.inject)
apply(erule conjE)+
apply(case_tac "M'a=Ax z b")
(* case Ma = Ax z b *)
apply(rule_tac t="Cut <b>.(Cut <c>.N1 (z).M'a) (y).N2" and s="Cut <b>.(M'a{z:=<c>.N1}) (y).N2" in subst)
apply(simp)
apply(drule_tac x="c" in spec)
apply(drule_tac x="N1" in spec)
apply(drule mp)
apply(simp)
apply(drule_tac x="B2" in meta_spec)
apply(drule_tac x="M'a{z:=<c>.N1}" in meta_spec)
apply(drule_tac x="N2" in meta_spec)
apply(drule conjunct1)
apply(drule mp)
apply(simp)
apply(rotate_tac 17)
apply(drule_tac x="b" in spec)
apply(drule mp)
apply(assumption)
apply(drule mp)
apply(rotate_tac 17)
apply(drule_tac x="y" in spec)
apply(drule mp)
apply(assumption)
apply(drule mp)
apply(assumption)
(* case Ma ≠ Ax z b *)
apply(subgoal_tac "<b>:Cut <c>.N1 (z).M'a ∈ ∥<B2>∥") (* lemma *)
apply(frule_tac meta_spec)
apply(drule_tac x="B2" in meta_spec)
apply(drule_tac x="Cut <c>.N1 (z).M'a" in meta_spec)
apply(drule_tac x="N2" in meta_spec)
apply(erule conjE)+
apply(drule mp)
apply(simp)
apply(rotate_tac 20)
apply(drule_tac x="b" in spec)
apply(rotate_tac 20)
apply(drule mp)
apply(assumption)
apply(rotate_tac 20)
apply(drule mp)
apply(rotate_tac 20)
apply(drule_tac x="y" in spec)
apply(rotate_tac 20)
apply(drule mp)
apply(assumption)
apply(rotate_tac 20)
apply(drule mp)
apply(assumption)
(* lemma *)
apply(subgoal_tac "<b>:Cut <c>.N1 (z).M'a ∈ BINDINGc B2 (∥(B2)∥)") (* second lemma *)
(* second lemma *)
apply(rule exI)+
apply(rule conjI)
apply(rule refl)
apply(rule allI)+
apply(rule impI)
apply(generate_fresh "name")
apply(rule_tac t="Cut <c>.N1 (z).M'a" and s="Cut <c>.N1 (ca).([(ca,z)]∙M'a)" in subst)
apply(simp add: trm.inject alpha fresh_prod fresh_atm)
apply(rule_tac t="(Cut <c>.N1 (ca).([(ca,z)]∙M'a)){b:=(xa).P}"
and s="Cut <c>.N1 (ca).(([(ca,z)]∙M'a){b:=(xa).P})" in subst)
apply(rule sym)
apply(rule tricky_subst)
apply(simp)
apply(simp)
apply(clarify)
apply(drule pt_bij1[OF pt_name_inst, OF at_name_inst])
apply(drule_tac x="B1" in meta_spec)
apply(drule_tac x="N1" in meta_spec)
apply(drule_tac x="([(ca,z)]∙M'a){b:=(xa).P}" in meta_spec)
apply(drule conjunct1)
apply(drule mp)
apply(simp)
apply(rotate_tac 19)
apply(drule_tac x="c" in spec)
apply(drule mp)
apply(assumption)
apply(drule mp)
apply(rotate_tac 19)
apply(drule_tac x="ca" in spec)
apply(subgoal_tac "(ca):([(ca,z)]∙M'a){b:=(xa).P} ∈ ∥(B1)∥")(*A*)
apply(drule mp)
apply(assumption)
apply(drule mp)
apply(assumption)
(*A*)
apply(drule_tac x="[(ca,z)]∙xa" in spec)
apply(drule_tac x="[(ca,z)]∙P" in spec)
apply(rotate_tac 19)
apply(drule mp)
apply(rule conjI)
apply(rule conjI)
apply(drule_tac pi="[(ca,z)]" and x="(xa):P" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(drule_tac pi="[(ca,z)]" and X="∥(B1)∥" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(perm_simp)
done

(* parallel substitution *)

lemma CUT_SNa:
assumes a1: "<a>:M ∈ (∥<B>∥)"
and     a2: "(x):N ∈ (∥(B)∥)"
shows   "SNa (Cut <a>.M (x).N)"
using a1 a2
apply -
apply(rule CUT_SNa_aux[OF a1])
done

fun
findn :: "(name×coname×trm) list⇒name⇒(coname×trm) option"
where
"findn [] x = None"
| "findn ((y,c,P)#θ_n) x = (if y=x then Some (c,P) else findn θ_n x)"

lemma findn_eqvt[eqvt]:
fixes pi1::"name prm"
and   pi2::"coname prm"
shows "(pi1∙findn θ_n x) = findn (pi1∙θ_n) (pi1∙x)"
and   "(pi2∙findn θ_n x) = findn (pi2∙θ_n) (pi2∙x)"
apply(induct θ_n)
done

lemma findn_fresh:
assumes a: "x♯θ_n"
shows "findn θ_n x = None"
using a
apply(induct θ_n)
apply(auto simp add: fresh_list_cons fresh_atm fresh_prod)
done

fun
findc :: "(coname×name×trm) list⇒coname⇒(name×trm) option"
where
"findc [] x = None"
| "findc ((c,y,P)#θ_c) a = (if a=c then Some (y,P) else findc θ_c a)"

lemma findc_eqvt[eqvt]:
fixes pi1::"name prm"
and   pi2::"coname prm"
shows "(pi1∙findc θ_c a) = findc (pi1∙θ_c) (pi1∙a)"
and   "(pi2∙findc θ_c a) = findc (pi2∙θ_c) (pi2∙a)"
apply(induct θ_c)
done

lemma findc_fresh:
assumes a: "a♯θ_c"
shows "findc θ_c a = None"
using a
apply(induct θ_c)
apply(auto simp add: fresh_list_cons fresh_atm fresh_prod)
done

abbreviation
nmaps :: "(name×coname×trm) list ⇒ name ⇒ (coname×trm) option ⇒ bool" ("_ nmaps _ to _" [55,55,55] 55)
where
"θ_n nmaps x to P ≡ (findn θ_n x) = P"

abbreviation
cmaps :: "(coname×name×trm) list ⇒ coname ⇒ (name×trm) option ⇒ bool" ("_ cmaps _ to _" [55,55,55] 55)
where
"θ_c cmaps a to P ≡ (findc θ_c a) = P"

lemma nmaps_fresh:
shows "θ_n nmaps x to Some (c,P) ⟹ a♯θ_n ⟹ a♯(c,P)"
apply(induct θ_n)
apply(auto simp add: fresh_list_cons fresh_prod fresh_atm)
apply(case_tac "aa=x")
apply(auto)
apply(case_tac "aa=x")
apply(auto)
done

lemma cmaps_fresh:
shows "θ_c cmaps a to Some (y,P) ⟹ x♯θ_c ⟹ x♯(y,P)"
apply(induct θ_c)
apply(auto simp add: fresh_list_cons fresh_prod fresh_atm)
apply(case_tac "a=aa")
apply(auto)
apply(case_tac "a=aa")
apply(auto)
done

lemma nmaps_false:
shows "θ_n nmaps x to Some (c,P) ⟹ x♯θ_n ⟹ False"
apply(induct θ_n)
apply(auto simp add: fresh_list_cons fresh_prod fresh_atm)
done

lemma cmaps_false:
shows "θ_c cmaps c to Some (x,P) ⟹ c♯θ_c ⟹ False"
apply(induct θ_c)
apply(auto simp add: fresh_list_cons fresh_prod fresh_atm)
done

fun
lookupa :: "name⇒coname⇒(coname×name×trm) list⇒trm"
where
"lookupa x a [] = Ax x a"
| "lookupa x a ((c,y,P)#θ_c) = (if a=c then Cut <a>.Ax x a (y).P else lookupa x a θ_c)"

lemma lookupa_eqvt[eqvt]:
fixes pi1::"name prm"
and   pi2::"coname prm"
shows "(pi1∙(lookupa x a θ_c)) = lookupa (pi1∙x) (pi1∙a) (pi1∙θ_c)"
and   "(pi2∙(lookupa x a θ_c)) = lookupa (pi2∙x) (pi2∙a) (pi2∙θ_c)"
apply -
apply(induct θ_c)
apply(induct θ_c)
done

lemma lookupa_fire:
assumes a: "θ_c cmaps a to Some (y,P)"
shows "(lookupa x a θ_c) = Cut <a>.Ax x a (y).P"
using a
apply(induct θ_c arbitrary: x a y P)
apply(auto)
done

fun
lookupb :: "name⇒coname⇒(coname×name×trm) list⇒coname⇒trm⇒trm"
where
"lookupb x a [] c P = Cut <c>.P (x).Ax x a"
| "lookupb x a ((d,y,N)#θ_c) c P = (if a=d then Cut <c>.P (y).N  else lookupb x a θ_c c P)"

lemma lookupb_eqvt[eqvt]:
fixes pi1::"name prm"
and   pi2::"coname prm"
shows "(pi1∙(lookupb x a θ_c c P)) = lookupb (pi1∙x) (pi1∙a) (pi1∙θ_c) (pi1∙c) (pi1∙P)"
and   "(pi2∙(lookupb x a θ_c c P)) = lookupb (pi2∙x) (pi2∙a) (pi2∙θ_c) (pi2∙c) (pi2∙P)"
apply -
apply(induct θ_c)
apply(induct θ_c)
done

fun
lookup :: "name⇒coname⇒(name×coname×trm) list⇒(coname×name×trm) list⇒trm"
where
"lookup x a [] θ_c = lookupa x a θ_c"
| "lookup x a ((y,c,P)#θ_n) θ_c = (if x=y then (lookupb x a θ_c c P) else lookup x a θ_n θ_c)"

lemma lookup_eqvt[eqvt]:
fixes pi1::"name prm"
and   pi2::"coname prm"
shows "(pi1∙(lookup x a θ_n θ_c)) = lookup (pi1∙x) (pi1∙a) (pi1∙θ_n) (pi1∙θ_c)"
and   "(pi2∙(lookup x a θ_n θ_c)) = lookup (pi2∙x) (pi2∙a) (pi2∙θ_n) (pi2∙θ_c)"
apply -
apply(induct θ_n)
apply(induct θ_n)
done

fun
lookupc :: "name⇒coname⇒(name×coname×trm) list⇒trm"
where
"lookupc x a [] = Ax x a"
| "lookupc x a ((y,c,P)#θ_n) = (if x=y then P[c⊢c>a] else lookupc x a θ_n)"

lemma lookupc_eqvt[eqvt]:
fixes pi1::"name prm"
and   pi2::"coname prm"
shows "(pi1∙(lookupc x a θ_n)) = lookupc (pi1∙x) (pi1∙a) (pi1∙θ_n)"
and   "(pi2∙(lookupc x a θ_n)) = lookupc (pi2∙x) (pi2∙a) (pi2∙θ_n)"
apply -
apply(induct θ_n)