Theory II_Prelims

```chapter‹Syntactic Preliminaries for the Second Incompleteness Theorem›

theory II_Prelims
imports Pf_Predicates
begin

declare IndP.simps [simp del]

lemma VarP_Var [intro]: "H ⊢ VarP «Var i»"
proof -
have "{} ⊢ VarP «Var i»"
by (auto simp: Sigma_fm_imp_thm [OF VarP_sf] ground_fm_aux_def supp_conv_fresh)
thus ?thesis
by (rule thin0)
qed

lemma VarP_neq_IndP: "{t EQ v, VarP v, IndP t} ⊢ Fls"
proof -
obtain m::name where "atom m ♯ (t,v)"
by (metis obtain_fresh)
thus ?thesis
apply (auto simp: VarP_def IndP.simps [of m])
apply (rule cut_same [of _ "OrdP (Q_Ind (Var m))"])
apply (blast intro: Sym Trans OrdP_cong [THEN Iff_MP_same])
by (metis OrdP_HPairE)
qed

lemma OrdP_ORD_OF [intro]: "H ⊢ OrdP (ORD_OF n)"
proof -
have "{} ⊢ OrdP (ORD_OF n)"
by (induct n) (auto simp: OrdP_SUCC_I)
thus ?thesis
by (rule thin0)
qed

lemma Mem_HFun_Sigma_OrdP: "{HPair t u IN f, HFun_Sigma f} ⊢ OrdP t"
proof -
obtain x::name and y::name and z::name and x'::name and y'::name and z'::name
where "atom z ♯ (f,t,u,z',x,y,x',y')"  "atom z' ♯ (f,t,u,x,y,x',y')"
"atom x ♯ (f,t,u,y,x',y')"  "atom y ♯ (f,t,u,x',y')"
"atom x' ♯ (f,t,u,y')"  "atom y' ♯ (f,t,u)"
by (metis obtain_fresh)
thus ?thesis
apply (simp add: HFun_Sigma.simps [of z f z' x y x' y'])
apply (rule All2_E [where x="HPair t u", THEN rotate2], auto)
apply (rule All2_E [where x="HPair t u"], auto intro: OrdP_cong [THEN Iff_MP2_same])
done
qed

section ‹NotInDom›

nominal_function NotInDom :: "tm ⇒ tm ⇒ fm"
where "atom z ♯ (t, r) ⟹ NotInDom t r = All z (Neg (HPair t (Var z) IN r))"
by (auto simp: eqvt_def NotInDom_graph_aux_def flip_fresh_fresh) (metis obtain_fresh)

nominal_termination (eqvt)
by lexicographic_order

lemma NotInDom_fresh_iff [simp]: "a ♯ NotInDom t r ⟷ a ♯ (t, r)"
proof -
obtain j::name where "atom j ♯ (t,r)"
by (rule obtain_fresh)
thus ?thesis
by auto
qed

lemma subst_fm_NotInDom [simp]: "(NotInDom t r)(i::=x) = NotInDom (subst i x t) (subst i x r)"
proof -
obtain j::name where "atom j ♯ (i,x,t,r)"
by (rule obtain_fresh)
thus ?thesis
by (auto simp: NotInDom.simps [of j])
qed

lemma NotInDom_cong: "H ⊢ t EQ t' ⟹ H ⊢ r EQ r' ⟹ H ⊢ NotInDom t r IFF NotInDom t' r'"
by (rule P2_cong) auto

lemma NotInDom_Zero: "H ⊢ NotInDom t Zero"
proof -
obtain z::name where "atom z ♯ t"
by (metis obtain_fresh)
hence "{} ⊢ NotInDom t Zero"
by (auto simp: fresh_Pair)
thus ?thesis
by (rule thin0)
qed

lemma NotInDom_Fls: "{HPair d d' IN r, NotInDom d r} ⊢ A"
proof -
obtain z::name where "atom z ♯ (d,r)"
by (metis obtain_fresh)
hence "{HPair d d' IN r, NotInDom d r} ⊢ Fls"
by (auto intro!: Ex_I [where x=d'])
thus ?thesis
by (metis ExFalso)
qed

lemma NotInDom_Contra: "H ⊢ NotInDom d r ⟹ H ⊢ HPair x y IN r ⟹ insert (x EQ d) H ⊢ A"
by (rule NotInDom_Fls [THEN cut2, THEN ExFalso])
(auto intro: thin1 NotInDom_cong [OF Assume Refl, THEN Iff_MP2_same])

section ‹Restriction of a Sequence to a Domain›

nominal_function RestrictedP :: "tm ⇒ tm ⇒ tm ⇒ fm"
where "⟦atom x ♯ (y,f,k,g); atom y ♯ (f,k,g)⟧ ⟹
RestrictedP f k g =
g SUBS f AND
All x (All y (HPair (Var x) (Var y) IN g IFF
(Var x) IN k AND HPair (Var x) (Var y) IN f))"
by (auto simp: eqvt_def RestrictedP_graph_aux_def flip_fresh_fresh) (metis obtain_fresh)

nominal_termination (eqvt)
by lexicographic_order

lemma RestrictedP_fresh_iff [simp]: "a ♯ RestrictedP f k g ⟷ a ♯ f ∧ a ♯ k ∧ a ♯ g"
proof -
obtain x::name and y::name where "atom x ♯ (y,f,k,g)" "atom y ♯ (f,k,g)"
by (metis obtain_fresh)
thus ?thesis
by auto
qed

lemma subst_fm_RestrictedP [simp]:
"(RestrictedP f k g)(i::=u) = RestrictedP (subst i u f) (subst i u k) (subst i u g)"
proof -
obtain x::name and y::name  where "atom x ♯ (y,f,k,g,i,u)" "atom y ♯ (f,k,g,i,u)"
by (metis obtain_fresh)
thus ?thesis
by (auto simp: RestrictedP.simps [of x y])
qed

lemma RestrictedP_cong:
"⟦H ⊢ f EQ f'; H ⊢ k EQ A'; H ⊢ g EQ g'⟧
⟹ H ⊢ RestrictedP f k g IFF RestrictedP f' A' g'"
by (rule P3_cong) auto

lemma RestrictedP_Zero: "H ⊢ RestrictedP Zero k Zero"
proof -
obtain x::name and y::name  where "atom x ♯ (y,k)" "atom y ♯ (k)"
by (metis obtain_fresh)
hence "{} ⊢ RestrictedP Zero k Zero"
by (auto simp: RestrictedP.simps [of x y])
thus ?thesis
by (rule thin0)
qed

lemma RestrictedP_Mem: "{ RestrictedP s k s', HPair a b IN s, a IN k } ⊢ HPair a b IN s'"
proof -
obtain x::name and y::name where "atom x ♯ (y,s,k,s',a,b)" "atom y ♯ (s,k,s',a,b)"
by (metis obtain_fresh)
thus ?thesis
apply (auto simp: RestrictedP.simps [of x y])
apply (rule All_E [where x=a, THEN rotate2], auto)
apply (rule All_E [where x=b], auto intro: Iff_E2)
done
qed

lemma RestrictedP_imp_Subset: "{RestrictedP s k s'} ⊢ s' SUBS s"
proof -
obtain x::name and y::name where "atom x ♯ (y,s,k,s')" "atom y ♯ (s,k,s')"
by (metis obtain_fresh)
thus ?thesis
by (auto simp: RestrictedP.simps [of x y])
qed

lemma RestrictedP_Mem2:
"{ RestrictedP s k s', HPair a b IN s' } ⊢ HPair a b IN s AND a IN k"
proof -
obtain x::name and y::name where "atom x ♯ (y,s,k,s',a,b)" "atom y ♯ (s,k,s',a,b)"
by (metis obtain_fresh)
thus ?thesis
apply (auto simp: RestrictedP.simps [of x y] intro: Subset_D)
apply (rule All_E [where x=a, THEN rotate2], auto)
apply (rule All_E [where x=b], auto intro: Iff_E1)
done
qed

lemma RestrictedP_Mem_D: "H ⊢ RestrictedP s k t ⟹ H ⊢ a IN t ⟹ insert (a IN s) H ⊢ A ⟹ H ⊢ A"
by (metis RestrictedP_imp_Subset Subset_E cut1)

lemma RestrictedP_Eats:
"{ RestrictedP s k s', a IN k } ⊢ RestrictedP (Eats s (HPair a b)) k (Eats s' (HPair a b))" (*<*)
proof -
obtain x::name and y::name
where "atom x ♯ (y,s,k,s',a,b)" "atom y ♯ (s,k,s',a,b)"
by (metis obtain_fresh)
thus ?thesis
apply (auto simp: RestrictedP.simps [of x y])
apply (metis Assume Subset_Eats_I Subset_trans)
apply (metis Mem_Eats_I2 Refl)
apply (rule Swap, auto)
apply (rule All_E [where x="Var x", THEN rotate2], auto)
apply (rule All_E [where x="Var y"], simp)
apply (metis Assume Conj_E Iff_E1)
apply (blast intro: Subset_D)
apply (blast intro: Mem_cong [THEN Iff_MP2_same])
apply (metis Assume AssumeH(2) HPair_cong Mem_Eats_I2)
apply (rule All_E [where x="Var x", THEN rotate3], auto)
apply (rule All_E [where x="Var y"], simp)
apply (metis Assume AssumeH(2) Conj_I Iff_E2 Mem_Eats_I1)
apply (blast intro: Mem_Eats_I2 HPair_cong)
done
qed (*>*)

lemma exists_RestrictedP:
assumes s: "atom s ♯ (f,k)"
shows  "H ⊢ Ex s (RestrictedP f k (Var s))" (*<*)
proof -
obtain j::name and x::name and y::name and z::name
where atoms: "atom j ♯ (k,z,s)"  "atom x ♯ (j,k,z,s)"  "atom y ♯ (x,j,k,z,s)"  "atom z ♯ (s,k)"
by (metis obtain_fresh)
have "{} ⊢ Ex s (RestrictedP (Var z) k (Var s))"
apply (rule Ind [of j z]) using atoms s
apply simp_all
apply (rule Ex_I [where x=Zero], simp add: RestrictedP_Zero)
apply (rule All_I)+
apply (auto del: Ex_EH)
apply (rule thin1)
apply (rule Ex_E)
proof (rule Cases [where A="Ex x (Ex y ((Var x) IN k AND Var j EQ HPair (Var x) (Var y)))"], auto)
show "{Var x IN k, Var j EQ HPair (Var x) (Var y), RestrictedP (Var z) k (Var s)}
⊢ Ex s (RestrictedP (Eats (Var z) (Var j)) k (Var s))"
apply (rule Ex_I [where x="Eats (Var s) (HPair (Var x) (Var y))"])
using atoms s apply auto
apply (rule RestrictedP_cong [OF _ Refl Refl, THEN Iff_MP2_same])
apply (blast intro: Eats_cong [OF Refl])
apply (rule Var_Eq_subst_Iff [THEN rotate2, THEN Iff_MP_same])
apply (auto intro: RestrictedP_Eats [THEN cut2])
done
next
obtain u::name and v::name
where uv: "atom u ♯ (x,y,z,s,j,k)" "atom v ♯ (u,x,y,z,s,j,k)"
by (metis obtain_fresh)
show "{Neg (Ex x (Ex y (Var x IN k AND Var j EQ HPair (Var x) (Var y)))),
RestrictedP (Var z) k (Var s)} ⊢
Ex s (RestrictedP (Eats (Var z) (Var j)) k (Var s))"
apply (rule Ex_I [where x="Var s"])
using uv atoms
apply (auto simp: RestrictedP.simps [of u v])
apply (metis Assume Subset_Eats_I Subset_trans)
apply (rule Swap, auto)
apply (rule All_E [THEN rotate4, of _ _ "Var u"], auto)
apply (rule All_E [where x="Var v"], simp)
apply (metis Assume Conj_E Iff_E1)
apply (rule Mem_Eats_I1)
apply (metis Assume AssumeH(3) Subset_D)
apply (rule All_E [where x="Var u", THEN rotate5], auto)
apply (rule All_E [where x="Var v"], simp)
apply (metis Assume AssumeH(2) Conj_I Iff_E2)
apply (rule ContraProve [THEN rotate3])
apply (rule Ex_I [where x="Var u"], simp)
apply (rule Ex_I [where x="Var v"], auto intro: Sym)
done
qed
hence "{} ⊢ (Ex s (RestrictedP (Var z) k (Var s)))(z::=f)"
by (rule Subst) simp
thus ?thesis using atoms s
by simp (rule thin0)
qed (*>*)

lemma cut_RestrictedP:
assumes s: "atom s ♯ (f,k,A)" and "∀C ∈ H. atom s ♯ C"
shows  "insert (RestrictedP f k (Var s)) H ⊢ A ⟹ H ⊢ A"
apply (rule cut_same [OF exists_RestrictedP [of s]])
using assms apply auto
done

lemma RestrictedP_NotInDom: "{ RestrictedP s k s', Neg (j IN k) } ⊢ NotInDom j s'"
proof -
obtain x::name and y::name and z::name
where "atom x ♯ (y,s,j,k,s')" "atom y ♯ (s,j,k,s')" "atom z ♯ (s,j,k,s')"
by (metis obtain_fresh)
thus ?thesis
apply (auto simp: RestrictedP.simps [of x y] NotInDom.simps [of z])
apply (rule All_E [where x=j, THEN rotate3], auto)
apply (rule All_E, auto intro: Conj_E1 Iff_E1)
done
qed

declare RestrictedP.simps [simp del]

section ‹Applications to LstSeqP›

lemma HFun_Sigma_Eats:
assumes "H ⊢ HFun_Sigma r" "H ⊢ NotInDom d r" "H ⊢ OrdP d"
shows "H ⊢ HFun_Sigma (Eats r (HPair d d'))" (*<*)
proof -
obtain x::name and y::name and z::name and x'::name and y'::name and z'::name and z''::name
where "atom z'' ♯ (r,d,d',z,z',x,y,x',y')"
and "atom z ♯ (r,d,d',z',x,y,x',y')" and "atom z' ♯ (r,d,d',x,y,x',y')"
and "atom x ♯ (r,d,d',y,x',y')" and "atom y ♯ (r,d,d',x',y')"
and "atom x' ♯ (r,d,d',y')" and "atom y' ♯ (r,d,d')"
by (metis obtain_fresh)
hence "{ HFun_Sigma r, NotInDom d r, OrdP d } ⊢ HFun_Sigma (Eats r (HPair d d'))"
apply (auto simp: HFun_Sigma.simps [of z _ z' x y x' y'])
― ‹case 1›
apply (rule Ex_I [where x = "Var z"], simp)
apply (rule Neg_Imp_I, blast)
apply (rule All_E [where x = "Var z'"], auto)
― ‹case 2›
apply (rule Ex_I [where x = "Var z"], simp)
apply (rule Neg_Imp_I, blast)
apply (rule All_E [where x = "Var z"], simp)
apply (rule Imp_E, auto del: Disj_EH)
apply (rule thin1)
apply (rule thin1)
apply (rule Ex_I [where x = "Var x"], simp)
apply (rule Ex_I [where x = "Var y"], simp)
apply (rule Ex_I [where x = d], simp)
apply (rule Ex_I [where x = d'], auto)
apply (blast intro: Disj_I1 OrdNotEqP_I NotInDom_Contra Mem_cong [THEN Iff_MP_same])
― ‹case 3›
apply (rule Ex_I [where x = "Var z'"])
apply (subst subst_fm_Ex_with_renaming [where i'=z''] | subst subst_fm.simps)+
apply (rule Ex_I [where x = "Var z'", THEN Swap], simp)
apply (rule Neg_I)
apply (rule Imp_E, auto del: Disj_EH)
apply (rule thin1)
apply (rule thin1)
apply (rule Ex_I [where x = d], simp)
apply (rule Ex_I [where x = d'], simp)
apply (rule Ex_I [where x = "Var x"], simp)
apply (rule Ex_I [where x = "Var y"], auto)
apply (blast intro: Disj_I1 Sym_L OrdNotEqP_I NotInDom_Contra Mem_cong [THEN Iff_MP_same])
― ‹case 4›
apply (rule rotate2 [OF Swap])
apply (rule Ex_I [where x = d], auto)
apply (rule Ex_I [where x = d'], auto)
apply (rule Ex_I [where x = d], auto)
apply (rule Ex_I [where x = d'], auto intro: Disj_I2)
done
thus ?thesis using assms
by (rule cut3)
qed (*>*)

lemma HFun_Sigma_single [iff]: "H ⊢ OrdP d ⟹ H ⊢ HFun_Sigma (Eats Zero (HPair d d'))"
by (metis HFun_Sigma_Eats HFun_Sigma_Zero NotInDom_Zero)

lemma LstSeqP_single [iff]: "H ⊢ LstSeqP (Eats Zero (HPair Zero x)) Zero x"
by (auto simp: LstSeqP.simps intro!: OrdP_SUCC_I HDomain_Incl_Eats_I Mem_Eats_I2)

lemma NotInDom_LstSeqP_Eats:
"{ NotInDom (SUCC k) s, LstSeqP s k y } ⊢ LstSeqP (Eats s (HPair (SUCC k) z)) (SUCC k) z"
by (auto simp: LstSeqP.simps intro: HDomain_Incl_Eats_I Mem_Eats_I2 OrdP_SUCC_I HFun_Sigma_Eats)

lemma RestrictedP_HDomain_Incl: "{HDomain_Incl s k, RestrictedP s k s'} ⊢ HDomain_Incl s' k"
proof -
obtain u::name and v::name and x::name and y::name and z::name
where "atom u ♯ (v,s,k,s')" "atom v ♯ (s,k,s')"
"atom x ♯ (s,k,s',u,v,y,z)" "atom y ♯ (s,k,s',u,v,z)" "atom z ♯ (s,k,s',u,v)"
by (metis obtain_fresh)
thus ?thesis
apply (auto simp: HDomain_Incl.simps [of x _ _ y z])
apply (rule Ex_I [where x="Var x"], auto)
apply (rule Ex_I [where x="Var y"], auto)
apply (rule Ex_I [where x="Var z"], simp)
apply (rule Var_Eq_subst_Iff [THEN Iff_MP_same, THEN rotate2])
apply (auto simp: RestrictedP.simps [of u v])
apply (rule All_E [where x="Var x", THEN rotate2], auto)
apply (rule All_E [where x="Var y"])
apply (auto intro: Iff_E ContraProve Mem_cong [THEN Iff_MP_same])
done
qed

lemma RestrictedP_HFun_Sigma: "{HFun_Sigma s, RestrictedP s k s'} ⊢ HFun_Sigma s'"
by (metis Assume RestrictedP_imp_Subset Subset_HFun_Sigma rcut2)

lemma RestrictedP_LstSeqP:
"{ RestrictedP s (SUCC k) s', LstSeqP s k y } ⊢ LstSeqP s' k y"
by (auto simp: LstSeqP.simps
intro: Mem_Neg_refl cut2 [OF RestrictedP_HDomain_Incl]
cut2 [OF RestrictedP_HFun_Sigma] cut3 [OF RestrictedP_Mem])

lemma RestrictedP_LstSeqP_Eats:
"{ RestrictedP s (SUCC k) s', LstSeqP s k y }
⊢ LstSeqP (Eats s' (HPair (SUCC k) z)) (SUCC k) z"
by (blast intro: Mem_Neg_refl cut2 [OF NotInDom_LstSeqP_Eats]
cut2 [OF RestrictedP_NotInDom] cut2 [OF RestrictedP_LstSeqP])

subsection‹Predicate form, defined on sequences›

nominal_function SeqHaddP :: "tm ⇒ tm ⇒ tm ⇒ tm ⇒ fm"
where "⟦atom l ♯ (sl,s,k,j); atom sl ♯ (s,j)⟧ ⟹
SeqHaddP s j k y = LstSeqP s k y AND
HPair Zero j IN s AND
All2 l k (Ex sl (HPair (Var l) (Var sl) IN s AND
HPair (SUCC (Var l)) (SUCC (Var sl)) IN s))"
by (auto simp: eqvt_def SeqHaddP_graph_aux_def flip_fresh_fresh) (metis obtain_fresh)

nominal_termination (eqvt)
by lexicographic_order

lemma SeqHaddP_fresh_iff [simp]: "a ♯ SeqHaddP s j k y ⟷ a ♯ s ∧ a ♯ j ∧ a ♯ k ∧ a ♯ y"
proof -
obtain l::name and sl::name where "atom l ♯ (sl,s,k,j)" "atom sl ♯ (s,j)"
by (metis obtain_fresh)
thus ?thesis
by force
qed

"(SeqHaddP s j k y)(i::=t) = SeqHaddP (subst i t s) (subst i t j) (subst i t k) (subst i t y)"
proof -
obtain l::name and sl::name where "atom l ♯ (s,k,j,sl,t,i)" "atom sl ♯ (s,k,j,t,i)"
by (metis obtain_fresh)
thus ?thesis
by (auto simp: SeqHaddP.simps [where l=l and sl=sl])
qed

nominal_function HaddP :: "tm ⇒ tm ⇒ tm ⇒ fm"
where "⟦atom s ♯ (x,y,z)⟧ ⟹
HaddP x y z = Ex s (SeqHaddP (Var s) x y z)"
by (auto simp: eqvt_def HaddP_graph_aux_def flip_fresh_fresh) (metis obtain_fresh)

nominal_termination (eqvt)
by lexicographic_order

lemma HaddP_fresh_iff [simp]: "a ♯ HaddP x y z ⟷ a ♯ x ∧ a ♯ y ∧ a ♯ z"
proof -
obtain s::name where "atom s ♯ (x,y,z)"
by (metis obtain_fresh)
thus ?thesis
by force
qed

lemma HaddP_subst [simp]: "(HaddP x y z)(i::=t) = HaddP (subst i t x) (subst i t y) (subst i t z)"
proof -
obtain s::name where "atom s ♯ (x,y,z,t,i)"
by (metis obtain_fresh)
thus ?thesis
by (auto simp: HaddP.simps [of s])
qed

lemma HaddP_cong: "⟦H ⊢ t EQ t'; H ⊢ u EQ u'; H ⊢ v EQ v'⟧ ⟹ H ⊢ HaddP t u v IFF HaddP t' u' v'"
by (rule P3_cong) auto

proof -
obtain s::name and l::name and sl::name where "atom l ♯ (sl,s,x)" "atom sl ♯ (s,x)" "atom s ♯ x"
by (metis obtain_fresh)
hence "{} ⊢ HaddP x Zero x"
intro!: Mem_Eats_I2 Ex_I [where x="Eats Zero (HPair Zero x)"])
thus ?thesis
by (rule thin0)
qed

proof -
obtain s::name and l::name and sl::name
where "atom l ♯ (sl,s,x,y,z)" "atom sl ♯ (s,x,y,z)" "atom s ♯ (x,y,z)"
by (metis obtain_fresh)
thus ?thesis
qed

proof -
obtain s::name and s'::name and l::name and sl::name
where "atom s' ♯ (l,sl,s,x,y,z)" "atom l ♯ (sl,s,x,y,z)" "atom sl ♯ (s,x,y,z)" "atom s ♯ (x,y,z)"
by (metis obtain_fresh)
hence "{HaddP x y z, OrdP y} ⊢ HaddP x (SUCC y) (SUCC z)"
apply (rule cut_RestrictedP [of s' "Var s" "SUCC y"], auto)
apply (rule Ex_I [where x="Eats (Var s') (HPair (SUCC y) (SUCC z))"])
apply (auto intro!: Mem_SUCC_EH)
apply (metis rotate2 RestrictedP_LstSeqP_Eats rotate3 thin1)
apply (blast intro: Mem_Eats_I1 cut3 [OF RestrictedP_Mem] cut1 [OF Zero_In_SUCC])
apply (rule Ex_I [where x="Var l"], auto)
apply (rule Ex_I [where x="Var sl"], auto)
apply (blast intro: Mem_Eats_I1 cut3 [OF RestrictedP_Mem] Mem_SUCC_I1)
apply (blast intro: Mem_Eats_I1 cut3 [OF RestrictedP_Mem] OrdP_IN_SUCC)
apply (rule ContraProve [THEN rotate2])
apply (rule Var_Eq_subst_Iff [THEN Iff_MP_same], simp add: LstSeqP.simps)
apply (rule Ex_I [where x=z])
apply (force intro: Mem_Eats_I1 Mem_Eats_I2 cut3 [OF RestrictedP_Mem] Mem_SUCC_I2)
done
thus ?thesis
qed (*>*)

subsection‹Proving that these relations are functions›

proof -
obtain l::name and sl::name where "atom l ♯ (s,w,z,sl)" "atom sl ♯ (s,w)"
by (metis obtain_fresh)
thus ?thesis
by (auto simp: SeqHaddP.simps [of l sl] LstSeqP.simps intro: HFun_Sigma_E)
qed

assumes y': "atom y' ♯ (s,j,k,y)"
shows "{SeqHaddP s j (SUCC k) y} ⊢ Ex y' (SeqHaddP s j k (Var y') AND y EQ SUCC (Var y'))"
proof -
obtain l::name and sl::name  where "atom l ♯ (s,j,k,y,y',sl)" "atom sl ♯ (s,j,k,y,y')"
by (metis obtain_fresh)
thus ?thesis using y'
apply (auto simp: SeqHaddP.simps [where s=s and l=l and sl=sl])
apply (rule All2_SUCC_E' [where t=k, THEN rotate2], auto)
apply (auto intro!: Ex_I [where x="Var sl"])
apply (blast intro: LstSeqP_SUCC) ― ‹showing @{term"SeqHaddP s j k (Var sl)"}›
apply (blast intro: LstSeqP_EQ)
done
qed

assumes "H ⊢ SeqHaddP s j (SUCC k) y"  "atom y' ♯ (s,j,k,y)"
shows "H ⊢ Ex y' (SeqHaddP s j k (Var y') AND y EQ SUCC (Var y'))"
by (metis SeqHaddP_SUCC_lemma [THEN cut1] assms)

lemma SeqHaddP_unique: "{OrdP x, SeqHaddP s w x y, SeqHaddP s' w x y'} ⊢ y' EQ y" (*<*)
proof -
obtain i::name and j::name and j'::name and k::name and sl::name and sl'::name
and l::name and ji::name and ji'::name
where ij: "atom i ♯ (s,s',w,y,y')" "atom j ♯ (s,s',w,i,x,y,y')" "atom j' ♯ (s,s',w,i,j,x,y,y')"
and atoms: "atom k ♯ (s,s',w,i,j,j')" "atom sl ♯ (s,s',w,i,j,j',k)" "atom sl' ♯ (s,s',w,i,j,j',k,sl)"
"atom ji ♯ (s,s',w,i,j,j',k,sl,sl')"  "atom ji' ♯ (s,s',w,i,j,j',k,sl,sl',ji)"
by (metis obtain_fresh)
have "{OrdP (Var i)}
⊢ All j (All j' (SeqHaddP s w (Var i) (Var j) IMP (SeqHaddP s' w (Var i) (Var j') IMP Var j' EQ Var j)))"
apply (rule OrdInd2H)
using ij atoms apply auto
apply (metis SeqHaddP_Zero_E [THEN cut1] Assume AssumeH(2) Sym Trans)
― ‹SUCC case›
apply (rule cut_same [OF SeqHaddP_SUCC [where y' = ji and s=s]], auto)
apply (rule cut_same [OF SeqHaddP_SUCC [where y' = ji' and s=s']], auto)
apply (rule Ex_I [where x = "Var ji"], auto)
apply (rule All_E [where x = "Var ji'"], auto)
apply (blast intro: Trans [OF Hyp] Sym intro!: SUCC_cong)
done
hence "{OrdP (Var i)}
⊢ (All j' (SeqHaddP s w (Var i) (Var j) IMP (SeqHaddP s' w (Var i) (Var j') IMP Var j' EQ Var j)))(j::=y)"
by (metis All_D)
hence "{OrdP (Var i)}
⊢ All j' (SeqHaddP s w (Var i) y IMP (SeqHaddP s' w (Var i) (Var j') IMP Var j' EQ y))"
using ij by simp
hence "{OrdP (Var i)}
⊢ (SeqHaddP s w (Var i) y IMP (SeqHaddP s' w (Var i) (Var j') IMP Var j' EQ y))(j'::=y')"
by (metis All_D)
hence "{OrdP (Var i)} ⊢ SeqHaddP s w (Var i) y IMP (SeqHaddP s' w (Var i) y' IMP y' EQ y)"
using ij by simp
hence "{} ⊢ (OrdP (Var i) IMP SeqHaddP s w (Var i) y IMP (SeqHaddP s' w (Var i) y' IMP y' EQ y))(i::=x)"
by (metis Imp_I Subst emptyE)
thus ?thesis
using ij by simp (metis DisjAssoc2 Disj_commute anti_deduction)
qed (*>*)

proof -
obtain s::name and s'::name  where "atom s ♯ (w,x,y,y')" "atom s' ♯ (w,x,y,y',s)"
by (metis obtain_fresh)
hence "{OrdP x, HaddP w x y, HaddP w x y'} ⊢ y' EQ y"
by (auto simp: HaddP.simps [of s _ _ y]  HaddP.simps [of s' _ _ y']
thus ?thesis
qed

lemma HaddP_Zero1: assumes "H ⊢ OrdP x" shows "H ⊢ HaddP Zero x x"
proof -
fix k::name
have "{ OrdP (Var k) } ⊢ HaddP Zero (Var k) (Var k)"
hence "{} ⊢ OrdP (Var k) IMP HaddP Zero (Var k) (Var k)"
by (metis Imp_I)
hence "{} ⊢ (OrdP (Var k) IMP HaddP Zero (Var k) (Var k))(k::=x)"
by (rule Subst) auto
hence "{} ⊢ OrdP x IMP HaddP Zero x x"
by simp
thus ?thesis using assms
by (metis MP_same thin0)
qed

lemma HaddP_Zero_D1: "insert (HaddP Zero x y) H ⊢ x EQ y"

lemma HaddP_Zero_D2: "insert (HaddP x Zero y) H ⊢ x EQ y"

assumes "H ⊢ HaddP x (SUCC y) z" "atom z' ♯ (x,y,z)"
shows "H ⊢ Ex z' (HaddP x y (Var z') AND z EQ SUCC (Var z'))"
proof -
obtain s::name and s'::name  where "atom s ♯ (x,y,z,z')" "atom s' ♯ (x,y,z,z',s)"
by (metis obtain_fresh)
hence "{ HaddP x (SUCC y) z } ⊢ Ex z' (HaddP x y (Var z') AND z EQ SUCC (Var z'))"
using assms
apply (auto simp: HaddP.simps [of s _ _ ]  HaddP.simps [of s' _ _ ])
apply (rule cut_same [OF SeqHaddP_SUCC_lemma [of z']], auto)
apply (rule Ex_I, auto)+
done
thus ?thesis
by (metis assms(1) cut1)
qed

proof -
obtain i::name and j::name and z'::name
where atoms: "atom i ♯ (x,y,z)"  "atom j ♯ (i,x,y,z)"  "atom z' ♯ (x,i,j)"
by (metis obtain_fresh)
have "{OrdP (Var i)} ⊢ All j (HaddP x (Var i) (Var j) IMP HaddP (SUCC x) (Var i) (SUCC (Var j)))"
(is "_ ⊢ ?scheme")
proof (rule OrdInd2H)
show "{} ⊢ ?scheme(i::=Zero)"
using atoms apply auto
apply (rule Var_Eq_subst_Iff [THEN Sym_L, THEN Iff_MP_same], auto intro: HaddP_Zero2)
done
next
show "{} ⊢ All i (OrdP (Var i) IMP ?scheme IMP ?scheme(i::=SUCC (Var i)))"
using atoms
apply auto
apply (rule cut_same [OF HaddP_SUCC_Ex2 [where z'=z']], auto)
apply (rule Ex_I [where x="Var z'"], auto)
apply (rule Var_Eq_subst_Iff [THEN Iff_MP_same, THEN rotate3], simp)
by (metis Assume HaddP_SUCC2 cut1 thin1)
qed
hence "{OrdP (Var i)} ⊢ (HaddP x (Var i) (Var j) IMP HaddP (SUCC x) (Var i) (SUCC (Var j)))(j::=z)"
by (rule All_D)
hence "{OrdP (Var i)} ⊢ HaddP x (Var i) z IMP HaddP (SUCC x) (Var i) (SUCC z)"
using atoms by auto
hence "{} ⊢ HaddP x (Var i) z IMP HaddP (SUCC x) (Var i) (SUCC z)"
hence "{} ⊢ (HaddP x (Var i) z IMP HaddP (SUCC x) (Var i) (SUCC z))(i::=y)"
using atoms by (force intro!: Subst)
thus ?thesis
using atoms by simp (metis anti_deduction)
qed (*>*)

proof -
obtain i::name and j::name and z'::name
where atoms: "atom i ♯ (x,y,z)"  "atom j ♯ (i,x,y,z)"  "atom z' ♯ (x,i,j)"
by (metis obtain_fresh)
have "{OrdP (Var i), OrdP x} ⊢ All j (HaddP x (Var i) (Var j) IMP HaddP (Var i) x (Var j))"
(is "_ ⊢ ?scheme")
proof (rule OrdInd2H)
show "{OrdP x} ⊢ ?scheme(i::=Zero)"
using atoms apply auto
apply (rule Var_Eq_subst_Iff [THEN Sym_L, THEN Iff_MP_same], auto intro: HaddP_Zero1)
done
next
show "{OrdP x} ⊢ All i (OrdP (Var i) IMP ?scheme IMP ?scheme(i::=SUCC (Var i)))"
using atoms
apply auto
apply (rule cut_same [OF HaddP_SUCC_Ex2 [where z'=z']], auto)
apply (rule Ex_I [where x="Var z'"], auto)
apply (rule rotate3)
apply (rule Var_Eq_subst_Iff [THEN Iff_MP_same], simp)
by (metis Assume HaddP_SUCC1 cut1 thin1)
qed
hence "{OrdP (Var i), OrdP x} ⊢ (HaddP x (Var i) (Var j) IMP HaddP (Var i) x (Var j))(j::=z)"
by (rule All_D)
hence "{OrdP (Var i), OrdP x} ⊢ HaddP x (Var i) z IMP HaddP (Var i) x z"
using atoms by auto
hence "{OrdP x} ⊢ HaddP x (Var i) z IMP HaddP (Var i) x z"
hence "{OrdP x} ⊢ (HaddP x (Var i) z IMP HaddP (Var i) x z)(i::=y)"
using atoms by (force intro!: Subst)
thus ?thesis
using atoms by simp (metis anti_deduction)
qed (*>*)

assumes "atom i ♯ (x,y,z)"
shows "insert (HaddP (SUCC x) y z) (insert (OrdP x) H)
⊢ Ex i (HaddP x y (Var i) AND z EQ SUCC (Var i))"
proof -
have "{ HaddP (SUCC x) y z, OrdP x } ⊢ Ex i (HaddP x y (Var i) AND z EQ SUCC (Var i))"
apply (rule cut_same [OF HaddP_commute [THEN cut2]])
apply (blast intro: OrdP_SUCC_I)+
apply (rule cut_same [OF HaddP_SUCC_Ex2 [where z'=i]], blast)
using assms apply auto
apply (auto intro!: Ex_I [where x="Var i"])
thus ?thesis
by (metis Assume AssumeH(2) cut2)
qed

lemma HaddP_inv2: "{HaddP x y z, HaddP x y' z, OrdP x} ⊢ y' EQ y" (*<*)
proof -
obtain i::name and j::name and u::name and u'::name
where atoms: "atom i ♯ (x,y,y',z)"  "atom j ♯ (i,x,y,y',z)"
"atom u ♯ (x,y,y',i,j)" "atom u' ♯ (x,y,y',u,i,j)"
by (metis obtain_fresh)
have "{OrdP (Var i)} ⊢ All j (HaddP (Var i) y (Var j) IMP HaddP (Var i) y' (Var j) IMP y' EQ y)"
(is "_ ⊢ ?scheme")
proof (rule OrdInd2H)
show "{} ⊢ ?scheme(i::=Zero)"
using atoms
by auto (metis HaddP_Zero_D1 Sym Trans thin1)
next
show "{} ⊢ All i (OrdP (Var i) IMP ?scheme IMP ?scheme(i::=SUCC (Var i)))"
using atoms
apply auto
apply (rule cut_same [OF HaddP_SUCC_Ex1 [where y=y and i=u, THEN cut2]], auto)
apply (rule Ex_I [where x="Var u"], auto)
apply (rule cut_same [OF HaddP_SUCC_Ex1 [where y=y' and i=u', THEN cut2]], auto)
apply (rule cut_same [where A="SUCC (Var u) EQ SUCC (Var u')"])
apply (auto intro: Sym Trans)
apply (rule rotate4 [OF ContraProve])
apply (rule Var_Eq_subst_Iff [THEN Iff_MP_same], force)
done
qed
hence "{OrdP (Var i)} ⊢ (HaddP (Var i) y (Var j) IMP HaddP (Var i) y' (Var j) IMP y' EQ y)(j::=z)"
by (rule All_D)
hence "{OrdP (Var i)} ⊢ HaddP (Var i) y z IMP HaddP (Var i) y' z IMP y' EQ y"
using atoms by auto
hence "{} ⊢ OrdP (Var i) IMP HaddP (Var i) y z IMP HaddP (Var i) y' z IMP y' EQ y"
by (metis Imp_I)
hence "{} ⊢ (OrdP (Var i) IMP HaddP (Var i) y z IMP HaddP (Var i) y' z IMP y' EQ y)(i::=x)"
using atoms by (force intro!: Subst)
thus ?thesis
using atoms by simp (metis DisjAssoc2 Disj_commute anti_deduction)
qed (*>*)

lemma Mem_imp_subtract: (*<*)
assumes "H ⊢ x IN y" "H ⊢ OrdP y" and k: "atom (k::name) ♯ (x,y)"
shows  "H ⊢ Ex k (HaddP x (Var k) y AND Zero IN (Var k))"
proof -
obtain i::name
where atoms: "atom i ♯ (x,y,k)"
by (metis obtain_fresh)
have "{OrdP (Var i)} ⊢ x IN Var i IMP Ex k (HaddP x (Var k) (Var i) AND Zero IN (Var k))"
(is "_ ⊢ ?scheme")
proof (rule OrdInd2H)
show "{} ⊢ ?scheme(i::=Zero)"
by auto
next
show "{} ⊢ All i (OrdP (Var i) IMP ?scheme IMP ?scheme(i::=SUCC (Var i)))"
using atoms k
apply (auto intro!: Mem_SUCC_EH)
apply (rule Ex_I [where x="SUCC (Var k)"], auto)
apply (metis AssumeH(4) HaddP_SUCC2 cut1 insert_commute)
apply (blast intro: Mem_SUCC_I1)
apply (rule Ex_I [where x="SUCC Zero"], auto)
apply (rule thin1)
apply (rule Var_Eq_subst_Iff [THEN Sym_L, THEN Iff_MP_same], simp)
apply (rule Ex_I [where x="SUCC (Var k)"], auto intro: Mem_SUCC_I1)
apply (metis AssumeH(4) HaddP_SUCC2 cut1 insert_commute)
done
qed
hence "{} ⊢ OrdP (Var i) IMP x IN Var i IMP Ex k (HaddP x (Var k) (Var i) AND Zero IN (Var k))"
by (metis Imp_I)
hence "{} ⊢ (OrdP (Var i) IMP x IN Var i IMP Ex k (HaddP x (Var k) (Var i) AND Zero IN (Var k)))(i::=y)"
by (force intro!: Subst)
thus ?thesis using assms atoms
by simp (metis (no_types) anti_deduction cut2)
qed (*>*)

assumes "H ⊢ HaddP x y z" "H ⊢ OrdP x"  shows "H ⊢ OrdP z"  (*<*)
proof -
obtain i::name and j::name and k::name
where atoms: "atom i ♯ (x,y,z)"  "atom j ♯ (i,x,y,z)"  "atom k ♯ (i,j,x,y,z)"
by (metis obtain_fresh)
have "{OrdP (Var i), OrdP x} ⊢ All j (HaddP x (Var i) (Var j) IMP OrdP (Var j))"
(is "_ ⊢ ?scheme")
proof (rule OrdInd2H)
show "{OrdP x} ⊢ ?scheme(i::=Zero)"
using atoms
by (auto intro: HaddP_Zero_D2 OrdP_cong [THEN Iff_MP_same])
next
show "{OrdP x} ⊢ All i (OrdP (Var i) IMP ?scheme IMP ?scheme(i::=SUCC (Var i)))"
using atoms
apply auto
apply (rule cut_same [OF HaddP_SUCC_Ex2 [where z'=k]], auto)
apply (rule Ex_I [where x="Var k"], auto)
apply (rule Var_Eq_subst_Iff [THEN Iff_MP_same, THEN rotate3], auto intro: OrdP_SUCC_I)
done
qed
hence "{OrdP (Var i), OrdP x} ⊢ (HaddP x (Var i) (Var j) IMP OrdP (Var j))(j::=z)"
by (rule All_D)
hence "{OrdP (Var i), OrdP x} ⊢ (HaddP x (Var i) z IMP OrdP z)"
using atoms by simp
hence "{OrdP x} ⊢ HaddP x (Var i) z IMP OrdP z"
hence "{OrdP x} ⊢ (HaddP x (Var i) z IMP OrdP z)(i::=y)"
using atoms by (force intro!: Subst)
thus ?thesis using assms atoms
by simp (metis anti_deduction cut2)
qed (*>*)

assumes "H ⊢ HaddP x y' z'" "H ⊢ HaddP x y z" "H ⊢ OrdP x"
shows "H ⊢ z' IN z IFF y' IN y" (*<*)
proof -
obtain i::name and j::name and j'::name and k::name and k'::name
where atoms: "atom i ♯ (x,y,y',z,z')" "atom j ♯ (i,x,y,y',z,z')" "atom j' ♯ (i,j,x,y,y',z,z')"
"atom k ♯ (i,j,j',x,y,y',z,z')" "atom k' ♯ (i,j,j',k,x,y,y',z,z')"
by (metis obtain_fresh)
have "{OrdP (Var i)}
⊢ All j (All j' (HaddP (Var i) y' (Var j') IMP (HaddP (Var i) y (Var j) IMP
((Var j') IN (Var j) IFF y' IN y))))"
(is "_ ⊢ ?scheme")
proof (rule OrdInd2H)
show "{} ⊢ ?scheme(i::=Zero)"
using atoms apply simp
apply (rule All_I Imp_I Ex_EH)+
apply (rule cut_same [where A="Var j EQ y"])
apply (rule cut_same [where A="Var j' EQ y'"])
apply (rule Var_Eq_subst_Iff [THEN Iff_MP_same], simp)
apply (rule thin1)
apply (rule Var_Eq_subst_Iff [THEN Iff_MP_same], auto)
done
next
show "{} ⊢ All i (OrdP (Var i) IMP ?scheme IMP ?scheme(i::=SUCC (Var i)))"
using atoms apply simp
apply (rule All_I Imp_I Ex_EH)+
apply (rule cut_same [OF HaddP_SUCC_Ex1 [of k "Var i" y "Var j", THEN cut2]], simp_all)
apply (rule AssumeH Conj_EH Ex_EH)+
apply (rule cut_same [OF HaddP_SUCC_Ex1 [of k' "Var i" y' "Var j'", THEN cut2]], simp_all)
apply (rule AssumeH Conj_EH Ex_EH)+
apply (rule rotate7)
apply (rule All_E [where x = "Var k"], simp)
apply (rule All_E [where x = "Var k'"], simp_all)
apply (rule Imp_E AssumeH)+
apply (rule Iff_trans)
prefer 2
apply (rule AssumeH)
apply (rule Var_Eq_subst_Iff [THEN Iff_MP_same, THEN rotate3], simp)
apply (rule Var_Eq_subst_Iff [THEN Iff_MP_same, THEN rotate5], simp)
done
qed
hence "{OrdP (Var i)}
⊢ (All j' (HaddP (Var i) y' (Var j') IMP (HaddP (Var i) y (Var j) IMP ((Var j') IN (Var j) IFF y' IN y))))(j::=z)"
by (metis All_D)
hence "{OrdP (Var i)}
⊢ (All j' (HaddP (Var i) y' (Var j') IMP (HaddP (Var i) y z IMP ((Var j') IN z IFF y' IN y))))"
using atoms by simp
hence "{OrdP (Var i)}
⊢ (HaddP (Var i) y' (Var j') IMP (HaddP (Var i) y z IMP ((Var j') IN z IFF y' IN y)))(j'::=z')"
by (metis All_D)
hence "{OrdP (Var i)} ⊢ HaddP (Var i) y' z' IMP (HaddP (Var i) y z IMP (z' IN z IFF y' IN y))"
using atoms by simp
hence "{} ⊢ (OrdP (Var i) IMP HaddP (Var i) y' z' IMP (HaddP (Var i) y z IMP (z' IN z IFF y' IN y)))(i::=x)"
by (metis Imp_I Subst emptyE)
thus ?thesis
using atoms by simp (metis assms MP_null MP_same)
qed (*>*)

assumes "H ⊢ HaddP x' y z'" "H ⊢ HaddP x y z" "H ⊢ x' IN x" "H ⊢ OrdP x"
shows "H ⊢ z' IN z"
proof -
have "H ⊢ OrdP x'"
by (metis Ord_IN_Ord assms(3) assms(4))
hence "H ⊢ HaddP y x' z'" "H ⊢ HaddP y x z"
by (blast intro: assms HaddP_commute [THEN cut2])+
thus ?thesis
qed

assumes "H ⊢ HaddP k1 k2 k" "H ⊢ OrdP k1"
"insert (x IN k1) H ⊢ A"
"insert (Var i IN k2) (insert (HaddP k1 (Var i) x) H) ⊢ A"
and i: "atom (i::name) ♯ (k1,k2,k,x,A)" and "∀C ∈ H. atom i ♯ C"
shows "insert (x IN k) H ⊢ A" (*<*)
proof -
obtain j::name where j: "atom j ♯ (k1,k2,k,x)"
by (metis obtain_fresh)
have seq: "{HaddP k1 k2 k, x IN k, OrdP k1} ⊢ x IN k1 OR (Ex i (HaddP k1 (Var i) x AND Var i IN k2))"
apply (rule AssumeH)+
apply (rule cut_same [OF Ord_IN_Ord])
apply (rule AssumeH)+
apply (rule OrdP_linear [of _ x k1], (rule AssumeH)+)
proof -
show "{x IN k1, OrdP x, OrdP k, HaddP k1 k2 k, x IN k, OrdP k1} ⊢ x IN k1 OR Ex i (HaddP k1 (Var i) x AND Var i IN k2)"
by (blast intro: Disj_I1)
next
show "{x EQ k1, OrdP x, OrdP k, HaddP k1 k2 k, x IN k, OrdP k1} ⊢ x IN k1 OR Ex i (HaddP k1 (Var i) x AND Var i IN k2)"
apply (rule cut_same [OF Zero_In_OrdP [of k2, THEN cut1]])
apply auto
apply (rule cut_same [where A="HaddP x Zero k"])
apply (blast intro: HaddP_cong [THEN Iff_MP_same] Sym)
apply (rule cut_same [where A="x EQ k"])
apply (blast intro: Mem_non_refl Mem_cong [THEN Iff_MP_same])
apply (rule Disj_I2)
apply (rule Ex_I [where x=Zero])
using i apply auto
done
next
show "{k1 IN x, OrdP x, OrdP k, HaddP k1 k2 k, x IN k, OrdP k1} ⊢ x IN k1 OR Ex i (HaddP k1 (Var i) x AND Var i IN k2)"
apply (rule Disj_I2)
apply (rule cut_same [OF Mem_imp_subtract [of _ k1 x j]])
apply (rule AssumeH)+
using i j apply auto
apply (rule Ex_I [where x="Var j"], auto intro: HaddP_Mem_cancel_left [THEN Iff_MP_same])
done
qed
show ?thesis using assms
by (force intro: cut_same [OF seq [THEN cut3]] thin1 simp: insert_commute)
qed (*>*)

assumes "H ⊢ HaddP x y z" "H ⊢ z IN x" "H ⊢ OrdP x"
shows "H ⊢ A"
proof -
obtain i::name and j::name and k::name
where atoms: "atom i ♯ (x,y,z)" "atom j ♯ (i,x,y,z)" "atom k ♯ (i,j,x,y,z)"
by (metis obtain_fresh)
have "{OrdP (Var i)}  ⊢ All j (HaddP (Var i) y (Var j) IMP Neg ((Var j) IN (Var i)))"
(is "_ ⊢ ?scheme")
proof (rule OrdInd2H)
show "{} ⊢ ?scheme(i::=Zero)"
using atoms by auto
next
show "{} ⊢ All i (OrdP (Var i) IMP ?scheme IMP ?scheme(i::=SUCC (Var i)))"
using  atoms apply auto
apply (rule cut_same [OF HaddP_SUCC_Ex1 [of k "Var i" y "Var j", THEN cut2]], auto)
apply (rule Ex_I [where x="Var k"], auto)
apply (blast intro: OrdP_IN_SUCC_D Mem_cong [OF _ Refl, THEN Iff_MP_same])
done
qed
hence "{OrdP (Var i)} ⊢ (HaddP (Var i) y (Var j) IMP Neg ((Var j) IN (Var i)))(j::=z)"
by (metis All_D)
hence "{} ⊢ OrdP (Var i) IMP HaddP (Var i) y z IMP Neg (z IN (Var i))"
using atoms by simp (metis Imp_I)
hence "{} ⊢ (OrdP (Var i) IMP HaddP (Var i) y z IMP Neg (z IN (Var i)))(i::=x)"
by (metis Subst emptyE)
thus ?thesis
using atoms by simp (metis MP_same MP_null Neg_D assms)
qed (*>*)

assumes "H ⊢ OrdP y" "atom j ♯ (x,y)"
shows "H ⊢ Ex j (HaddP x y (Var j))"
proof -
obtain i::name
where atoms: "atom i ♯ (j,x,y)"
by (metis obtain_fresh)
have "{OrdP (Var i)} ⊢ Ex j (HaddP x (Var i) (Var j))"
(is "_ ⊢ ?scheme")
proof (rule OrdInd2H)
show "{} ⊢ ?scheme(i::=Zero)"
using atoms assms
by (force intro!: Ex_I [where x=x] HaddP_Zero2)
next
show "{} ⊢ All i (OrdP (Var i) IMP ?scheme IMP ?scheme(i::=SUCC (Var i)))"
using atoms assms
apply auto
apply (auto intro!: Ex_I [where x="SUCC (Var j)"] HaddP_SUCC2)
done
qed
hence "{} ⊢ OrdP (Var i) IMP Ex j (HaddP x (Var i) (Var j))"
by (metis Imp_I)
hence "{} ⊢ (OrdP (Var i) IMP Ex j (HaddP x (Var i) (Var j)))(i::=y)"
using atoms by (force intro!: Subst)
thus ?thesis
using atoms assms by simp (metis MP_null assms(1))
qed

assumes "H ⊢ HaddP x y z" "H ⊢ OrdP x" shows "H ⊢ x IN SUCC z"
proof -
have "{HaddP x y z, OrdP x} ⊢ x IN SUCC z"
apply (rule OrdP_linear [of _ x "SUCC z"])
apply (metis Assume Mem_SUCC_I2 OrdP_IN_SUCC_D Sym_L thin1 thin2, blast)
apply (blast intro: HaddP_Mem_contra Mem_SUCC_Refl OrdP_Trans)
done
thus ?thesis
by (rule cut2) (auto intro: assms)
qed

section ‹A Shifted Sequence›

nominal_function ShiftP :: "tm ⇒ tm ⇒ tm ⇒ tm ⇒ fm"
where "⟦atom x ♯ (x',y,z,f,del,k); atom x' ♯ (y,z,f,del,k); atom y ♯ (z,f,del,k); atom z ♯ (f,del,g,k)⟧ ⟹
ShiftP f k del g =
All z (Var z IN g IFF
(Ex x (Ex x' (Ex y ((Var z) EQ HPair (Var x') (Var y) AND
HaddP del (Var x) (Var x') AND
HPair (Var x) (Var y) IN f AND Var x IN k)))))"
by (auto simp: eqvt_def ShiftP_graph_aux_def flip_fresh_fresh) (metis obtain_fresh)

nominal_termination (eqvt)
by lexicographic_order

lemma ShiftP_fresh_iff [simp]: "a ♯ ShiftP f k del g ⟷ a ♯ f ∧ a ♯ k ∧ a ♯ del ∧ a ♯ g"
proof -
obtain x::name and x'::name and y::name and z::name
where "atom x ♯ (x',y,z,f,del,k)" "atom x' ♯ (y,z,f,del,k)"
"atom y ♯ (z,f,del,k)" "atom z ♯ (f,del,g,k)"
by (metis obtain_fresh)
thus ?thesis
by auto
qed

lemma subst_fm_ShiftP [simp]:
"(ShiftP f k del g)(i::=u) = ShiftP (subst i u f) (subst i u k) (subst i u del) (subst i u g)"
proof -
obtain x::name and x'::name and y::name and z::name
where "atom x ♯ (x',y,z,f,del,k,i,u)" "atom x' ♯ (y,z,f,del,k,i,u)"
"atom y ♯ (z,f,del,k,i,u)" "atom z ♯ (f,del,g,k,i,u)"
by (metis obtain_fresh)
thus ?thesis
by (auto simp: ShiftP.simps [of x x' y z])
qed

lemma ShiftP_Zero: "{} ⊢ ShiftP Zero k d Zero"
proof -
obtain x::name and x'::name and y::name and z::name
where "atom x ♯ (x',y,z,k,d)" "atom x' ♯ (y,z,k,d)" "atom y ♯ (z,k,d)" "atom z ♯ (k,d)"
by (metis obtain_fresh)
thus ?thesis
by (auto simp: ShiftP.simps [of x x' y z])
qed

lemma ShiftP_Mem1:
"{ShiftP f k del g, HPair a b IN f, HaddP del a a', a IN k} ⊢ HPair a' b IN g"
proof -
obtain x::name and x'::name and y::name and z::name
where "atom x ♯ (x',y,z,f,del,k,a,a',b)" "atom x' ♯ (y,z,f,del,k,a,a',b)"
"atom y ♯ (z,f,del,k,a,a',b)" "atom z ♯ (f,del,g,k,a,a',b)"
by (metis obtain_fresh)
thus ?thesis
apply (auto simp: ShiftP.simps [of x x' y z])
apply (rule All_E [where x="HPair a' b"], auto intro!: Iff_E2)
apply (rule Ex_I [where x=a], simp)
apply (rule Ex_I [where x="a'"], simp)
apply (rule Ex_I [where x=b], auto intro: Mem_Eats_I1)
done
qed

lemma ShiftP_Mem2:
assumes "atom u ♯ (f,k,del,a,b)"
shows  "{ShiftP f k del g, HPair a b IN g} ⊢ Ex u ((Var u) IN k AND HaddP del (Var u) a AND HPair (Var u) b IN f)"
proof -
obtain x::name and x'::name and y::name and z::name
where atoms: "atom x ♯ (x',y,z,f,del,g,k,a,u,b)" "atom x' ♯ (y,z,f,del,g,k,a,u,b)"
"atom y ♯ (z,f,del,g,k,a,u,b)" "atom z ♯ (f,del,g,k,a,u,b)"
by (metis obtain_fresh)
thus ?thesis using assms
apply (auto simp: ShiftP.simps [of x x' y z])
apply (rule All_E [where x="HPair a b"])
apply (auto intro!: Iff_E1 [OF Assume])
apply (rule Ex_I [where x="Var x"])
apply (auto intro: Mem_cong [OF HPair_cong Refl, THEN Iff_MP2_same])
apply (blast intro: HaddP_cong [OF Refl Refl, THEN Iff_MP2_same])
done
qed

lemma ShiftP_Mem_D:
assumes "H ⊢ ShiftP f k del g" "H ⊢ a IN g"
"atom x ♯ (x',y,a,f,del,k)" "atom x' ♯ (y,a,f,del,k)" "atom y ♯ (a,f,del,k)"
shows  "H ⊢ (Ex x (Ex x' (Ex y (a EQ HPair (Var x') (Var y) AND
HaddP del (Var x) (Var x') AND
HPair (Var x) (Var y) IN f AND Var x IN k))))"
(is "_ ⊢ ?concl")
proof -
obtain z::name where "atom z ♯ (x,x',y,f,del,g,k,a)"
by (metis obtain_fresh)
hence "{ShiftP f k del g, a IN g} ⊢ ?concl" using assms
by (auto simp: ShiftP.simps [of x x' y z]) (rule All_E [where x=a], auto intro: Iff_E1)
thus ?thesis
by (rule cut2) (rule assms)+
qed

lemma ShiftP_Eats_Eats:
"{ShiftP f k del g, HaddP del a a', a IN k}
⊢ ShiftP (Eats f (HPair a b)) k del (Eats g (HPair a' b))" (*<*)
proof -
obtain x::name and x'::name and y::name and z::name
where "atom x ♯ (x',y,z,f,del,g,k,a,a',b)" "atom x' ♯ (y,z,f,del,g,k,a,a',b)"
"atom y ♯ (z,f,del,g,k,a,a',b)" "atom z ♯ (f,del,g,k,a,a',b)"
by (metis obtain_fresh)
thus ?thesis
apply (auto simp: ShiftP.simps [of x x' y z] intro!: Iff_I [THEN Swap])
apply (rule All_E [where x="Var z", THEN rotate2], simp)
apply (rule Iff_E)
apply auto [1]
apply (rule Ex_I [where x="Var x"], simp)
apply (rule Ex_I [where x="Var x'"], simp)
apply (rule Ex_I [where x="Var y"], simp)
apply (blast intro: Mem_Eats_I1, blast)
apply (rule Ex_I [where x=a], simp)
apply (rule Ex_I [where x="a'"], simp)
apply (rule Ex_I [where x=b], simp)
apply (metis Assume AssumeH(3) AssumeH(4) Conj_I Mem_Eats_I2 Refl)
apply (rule All_E [where x="Var z", THEN rotate5], auto)
apply (rule Mem_Eats_I1)
apply (rule Iff_MP2_same [OF Hyp], blast)
apply (rule Ex_I [where x="Var x"], simp)
apply (rule Ex_I [where x="Var x'"], simp)
apply (rule Ex_I [where x="Var y"], auto)
apply (rule Var_Eq_subst_Iff [THEN Iff_MP_same, THEN rotate5], simp)
done
qed (*>*)

lemma ShiftP_Eats_Neg:
assumes "atom u ♯ (u',v,f,k,del,g,c)" "atom u' ♯ (v,f,k,del,g,c)" "atom v ♯ (f,k,del,g,c)"
shows
"{ShiftP f k del g,
Neg (Ex u (Ex u' (Ex v (c EQ HPair (Var u) (Var v) AND Var u IN k AND HaddP del (Var u) (Var u')))))}
⊢ ShiftP (Eats f c) k del g"  (*<*)
proof -
obtain x::name and x'::name and y::name and z::name
where atoms: "atom x ♯ (x',y,z,u,u',v,f,k,del,g,c)" "atom x' ♯ (y,z,u,u',v,f,k,del,g,c)"
"atom y ♯ (z,u,u',v,f,k,del,g,c)" "atom z ♯ (u,u',v,f,k,del,g,c)"
by (metis obtain_fresh)
thus ?thesis using assms
apply (auto simp: ShiftP.simps [of x x' y z] intro!: Iff_I [THEN Swap])
apply (rule All_E [where x="Var z", THEN rotate3])
apply (auto intro!: Iff_E1 [OF Assume])
apply (rule Ex_I [where x="Var x"], simp)
apply (rule Ex_I [where x="Var x'"], simp)
apply (rule Ex_I [where x="Var y"], simp)
apply (blast intro: Mem_Eats_I1)
apply (rule All_E [where x="Var z", THEN rotate6], simp)
apply (rule Iff_E2)
apply (rule Ex_I [where x="Var x"], simp)
apply (rule Ex_I [where x="Var x'"], simp)
apply (rule Ex_I [where x="Var y"])
apply (auto intro: Mem_Eats_I1)
apply (rule Swap [THEN rotate5]```