Theory Incompleteness.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 (auto simp add: flip_fresh_fresh)
    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])


section‹Ordinal Addition›

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

lemma SeqHaddP_subst [simp]:
  "(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

declare SeqHaddP.simps [simp del]

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

declare HaddP.simps [simp del]

lemma HaddP_Zero2: "H ⊢ HaddP x Zero x"
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"
    by (auto simp: HaddP.simps [of s] SeqHaddP.simps [of l sl]
          intro!: Mem_Eats_I2 Ex_I [where x="Eats Zero (HPair Zero x)"])
  thus ?thesis
    by (rule thin0)
qed

lemma HaddP_imp_OrdP: "{HaddP x y z} ⊢ OrdP y" 
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
    by (auto simp: HaddP.simps [of s] SeqHaddP.simps [of l sl] LstSeqP.simps)
qed

lemma HaddP_SUCC2: "{HaddP x y z} ⊢ HaddP x (SUCC y) (SUCC z)" (*<*)
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 (auto simp: HaddP.simps [of s] SeqHaddP.simps [of l sl])
    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
   by (metis Assume HaddP_imp_OrdP cut2)
qed (*>*)

subsection‹Proving that these relations are functions›

lemma SeqHaddP_Zero_E: "{SeqHaddP s w Zero z} ⊢ w EQ z"
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

lemma SeqHaddP_SUCC_lemma:
  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

lemma SeqHaddP_SUCC:
  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 (*>*)

lemma HaddP_unique: "{HaddP w x y, HaddP w x y'} ⊢ y' EQ y"
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'] 
             intro: SeqHaddP_unique [THEN cut3])
  thus ?thesis 
    by (metis HaddP_imp_OrdP cut_same thin1)
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)"
    by (rule OrdInd2H [where i=k]) (auto intro: HaddP_Zero2 HaddP_SUCC2 [THEN cut1])
  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"
  by (metis Assume HaddP_imp_OrdP HaddP_Zero1 HaddP_unique [THEN cut2] rcut1)

lemma HaddP_Zero_D2: "insert (HaddP x Zero y) H ⊢ x EQ y"
  by (metis Assume HaddP_Zero2 HaddP_unique [THEN cut2])

lemma HaddP_SUCC_Ex2:
  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

lemma HaddP_SUCC1: "{ HaddP x y z } ⊢ HaddP (SUCC x) y (SUCC z)" (*<*)
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 cut_same [OF HaddP_Zero_D2])
        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)"
    by (metis HaddP_imp_OrdP Imp_cut)
  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 (*>*)

lemma HaddP_commute: "{HaddP x y z, OrdP x} ⊢ HaddP y x z" (*<*)
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 cut_same [OF HaddP_Zero_D2])
        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"
    by (metis HaddP_imp_OrdP Imp_cut)
  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 (*>*)

lemma HaddP_SUCC_Ex1:
  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"])
    by (metis AssumeH(2) HaddP_commute [THEN cut2] HaddP_imp_OrdP rotate2 thin1)
  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 (metis HaddP_SUCC2 HaddP_Zero2 cut1) 
        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 (*>*)

lemma HaddP_OrdP:
  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"
    by (metis HaddP_imp_OrdP Imp_cut)
  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 (*>*)

lemma HaddP_Mem_cancel_left: 
  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 (metis HaddP_Zero_D1 Sym)
        apply (rule cut_same [where A="Var j' EQ y'"])
        apply (metis HaddP_Zero_D1 Sym thin1)
        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)
        apply (blast intro!: HaddP_OrdP OrdP_IN_SUCC_Iff)
        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 (*>*)

lemma HaddP_Mem_cancel_right_Mem: 
  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
    by (blast intro: assms HaddP_imp_OrdP [THEN cut1] HaddP_Mem_cancel_left [THEN Iff_MP2_same])
qed

lemma HaddP_Mem_cases:
  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 cut_same [OF HaddP_OrdP])
    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 (metis AssumeH(4) HaddP_imp_OrdP 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 (metis HaddP_Zero_D2)
        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
        apply (rule HaddP_cong [THEN Iff_MP_same])
        apply (rule AssumeH Refl HaddP_Zero2)+
        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 (*>*)

lemma HaddP_Mem_contra: 
  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 (*>*)

lemma exists_HaddP:
  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)
        apply (metis HaddP_SUCC2 insert_commute thin1)
        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

lemma HaddP_Mem_I: 
  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 (auto intro: OrdP_SUCC_I HaddP_OrdP)
    apply (rule HaddP_Mem_contra, blast)
    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)
    apply (blast intro: Mem_Eats_I2 HaddP_cong [THEN Iff_MP_same] HaddP_unique [THEN cut2] HPair_cong)
    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])
    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: Sym Mem_Eats_I1)
    done
qed (*>*)

lemma exists_ShiftP:
  assumes t: "atom t ♯ (s,k,del)"
  shows "H ⊢ Ex t (ShiftP s k del (Var t))" (*<*)
proof -
  obtain i::name and j::name
    where i: "atom (i::name) ♯ (s,t,k,del)" and j: "atom (j::name) ♯ (i,s,t,k,del)" 
    by (metis obtain_fresh) 
  have "{} ⊢ Ex t (ShiftP (Var i) k del (Var t))" (is "{} ⊢ ?scheme")
  proof (rule Ind [of j])
    show "atom j ♯ (i, ?scheme)" using j
      by simp 
  next
    show "{} ⊢ ?scheme(i::=Zero)" using i t
      by (auto intro!: Ex_I [where x=Zero] simp: ShiftP_Zero)
  next
    obtain x::name and x'::name and y::name 
    where atoms: "atom x ♯ (x',y,s,k,del,t,i,j)" "atom x' ♯ (y,s,k,del,t,i,j)" 
                 "atom y ♯ (s,k,del,t,i,j)" 
      by (metis obtain_fresh)
    let ?caseA = "Ex x (Ex x' (Ex y ((Var j) EQ HPair (Var x) (Var y) AND Var x IN k AND 
                                     HaddP del (Var x) (Var x'))))"
    show "{} ⊢ All i (All j (?scheme IMP ?scheme(i::=Var j) IMP ?scheme(i::=Eats (Var i) (Var j))))"
      using i j atoms
      apply (auto del: Ex_EH)
      apply (rule Ex_E)
      apply (auto del: Ex_EH)
      apply (rule Ex_E)
      apply (auto del: Ex_EH)
      apply (rule thin1, auto)
      proof (rule Cases [where A="?caseA"]) 
        show "{?caseA, ShiftP (Var i) k del (Var t)} 
              ⊢ Ex t (ShiftP (Eats (Var i) (Var j)) k del (Var t))"
          using i j t atoms
          apply (auto simp del: ShiftP.simps)
          apply (rule Ex_I [where x="Eats (Var t) (HPair (Var x') (Var y))"], auto)
          apply (rule Var_Eq_subst_Iff [THEN Iff_MP_same, THEN rotate3])
          apply (auto intro: ShiftP_Eats_Eats [THEN cut3])
          done
      next
        show "{Neg ?caseA, ShiftP (Var i) k del (Var t)} 
              ⊢ Ex t (ShiftP (Eats (Var i) (Var j)) k del (Var t))"
          using atoms
          by (auto intro!: Ex_I [where x="Var t"] ShiftP_Eats_Neg [of x x' y, THEN cut2] 
                   simp: ShiftP_Zero)
      qed
  qed
  hence "{} ⊢ (Ex t (ShiftP (Var i) k del (Var t)))(i::=s)"
    by (blast intro: Subst)
  thus ?thesis using i t 
    by (auto intro: thin0)
qed (*>*)


section ‹Union of Two Sets›

nominal_function UnionP :: "tm ⇒ tm ⇒ tm ⇒ fm"
  where "atom i ♯ (x,y,z) ⟹ UnionP x y z = All i (Var i IN z IFF (Var i IN x OR Var i IN y))"
by (auto simp: eqvt_def UnionP_graph_aux_def flip_fresh_fresh) (metis obtain_fresh)

nominal_termination (eqvt)
  by lexicographic_order

lemma UnionP_fresh_iff [simp]: "a ♯ UnionP x y z ⟷ a ♯ x ∧ a ♯ y ∧ a ♯ z"
proof -
  obtain i::name where "atom i ♯ (x,y,z)"
    by (metis obtain_fresh)
  thus ?thesis
    by auto
qed

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

lemma Union_Zero1: "H ⊢ UnionP Zero x x"
proof -
  obtain i::name where "atom i ♯ x"
    by (metis obtain_fresh)
  hence "{} ⊢ UnionP Zero x x"
    by (auto simp: UnionP.simps [of i] intro: Disj_I2)
  thus ?thesis
    by (metis thin0)
qed

lemma Union_Eats: "{UnionP x y z} ⊢ UnionP (Eats x a) y (Eats z a)"
proof -
  obtain i::name where "atom i ♯ (x,y,z,a)"
    by (metis obtain_fresh)
  thus ?thesis
    apply (auto simp: UnionP.simps [of i])
    apply (rule Ex_I [where x="Var i"])
    apply (auto intro: Iff_E1 [THEN rotate2] Iff_E2 [THEN rotate2] Mem_Eats_I1 Mem_Eats_I2 Disj_I1 Disj_I2)
    done
qed

lemma exists_Union_lemma: 
  assumes z: "atom z ♯ (i,y)" and i: "atom i ♯ y"
  shows "{} ⊢ Ex z (UnionP (Var i) y (Var z))"
proof -
  obtain j::name where j: "atom j ♯ (y,z,i)"
    by (metis obtain_fresh) 
  show "{} ⊢ Ex z (UnionP (Var i) y (Var z))"
    apply (rule Ind [of j i]) using j z i
    apply simp_all
    apply (rule Ex_I [where x=y], simp add: Union_Zero1)
    apply (auto del: Ex_EH)
    apply (rule Ex_E)
    apply (rule NegNeg_E)
    apply (rule Ex_E)
    apply (auto del: Ex_EH)
    apply (rule thin1, force intro: Ex_I [where x="Eats (Var z) (Var j)"] Union_Eats)
    done
qed    

lemma exists_UnionP: 
  assumes z: "atom z ♯ (x,y)"  shows "H ⊢ Ex z (UnionP x y (Var z))"
proof -
  obtain i::name  where i: "atom i ♯ (y,z)"
    by (metis obtain_fresh) 
  hence "{} ⊢ Ex z (UnionP (Var i) y (Var z))"
    by (metis exists_Union_lemma fresh_Pair fresh_at_base(2) z)
  hence "{} ⊢ (Ex z (UnionP (Var i) y (Var z)))(i::=x)"
    by (metis Subst empty_iff)
  thus ?thesis using i z
    by (simp add: thin0)
qed

lemma UnionP_Mem1: "{ UnionP x y z, a IN x } ⊢ a IN z"
proof -
  obtain i::name where "atom i ♯ (x,y,z,a)"
    by (metis obtain_fresh)
  thus ?thesis
    by (force simp: UnionP.simps [of i] intro: All_E [where x=a] Disj_I1 Iff_E2)
qed

lemma UnionP_Mem2: "{ UnionP x y z, a IN y } ⊢ a IN z"
proof -
  obtain i::name where "atom i ♯ (x,y,z,a)"
    by (metis obtain_fresh)
  thus ?thesis
    by (force simp: UnionP.simps [of i] intro: All_E [where x=a] Disj_I2 Iff_E2)
qed

lemma UnionP_Mem: "{ UnionP x y z, a IN z } ⊢ a IN x OR a IN y"
proof -
  obtain i::name where "atom i ♯ (x,y,z,a)"
    by (metis obtain_fresh)
  thus ?thesis
    by (force simp: UnionP.simps [of i] intro: All_E [where x=a] Iff_E1)
qed

lemma UnionP_Mem_E:
  assumes "H ⊢ UnionP x y z"
      and "insert (a IN x) H ⊢ A"
      and "insert (a IN y) H ⊢ A"
    shows "insert (a IN z) H ⊢ A"
  using assms
  by (blast intro: rotate2 cut_same [OF UnionP_Mem [THEN cut2]] thin1) 

  
section ‹Append on Sequences›

nominal_function SeqAppendP :: "tm ⇒ tm ⇒ tm ⇒ tm ⇒ tm ⇒ fm"
  where "⟦atom g1 ♯ (g2,f1,k1,f2,k2,g); atom g2 ♯ (f1,k1,f2,k2,g)⟧ ⟹
    SeqAppendP f1 k1 f2 k2 g =
      (Ex g1 (Ex g2 (RestrictedP f1 k1 (Var g1) AND 
                     ShiftP f2 k2 k1 (Var g2) AND 
                     UnionP (Var g1) (Var g2) g)))"
by (auto simp: eqvt_def SeqAppendP_graph_aux_def flip_fresh_fresh) (metis obtain_fresh)

nominal_termination (eqvt)
  by lexicographic_order

lemma SeqAppendP_fresh_iff [simp]: 
  "a ♯ SeqAppendP f1 k1 f2 k2 g ⟷ a ♯ f1 ∧ a ♯ k1 ∧ a ♯ f2 ∧ a ♯ k2 ∧ a ♯ g"       
proof -
  obtain g1::name and g2::name
    where "atom g1 ♯ (g2,f1,k1,f2,k2,g)" "atom g2 ♯ (f1,k1,f2,k2,g)"
    by (metis obtain_fresh)
  thus ?thesis
    by auto
qed

lemma subst_fm_SeqAppendP [simp]:
  "(SeqAppendP f1 k1 f2 k2 g)(i::=u) = 
   SeqAppendP (subst i u f1) (subst i u k1) (subst i u f2) (subst i u k2) (subst i u g)"
proof -
  obtain g1::name and g2::name 
  where "atom g1 ♯ (g2,f1,k1,f2,k2,g,i,u)" "atom g2 ♯ (f1,k1,f2,k2,g,i,u)" 
    by (metis obtain_fresh)
  thus ?thesis
    by (auto simp: SeqAppendP.simps [of g1 g2])
qed

lemma exists_SeqAppendP:
  assumes "atom g ♯ (f1,k1,f2,k2)"
  shows "H ⊢ Ex g (SeqAppendP f1 k1 f2 k2 (Var g))"
proof -
  obtain g1::name and g2::name
  where atoms: "atom g1 ♯ (g2,f1,k1,f2,k2,g)" "atom g2 ♯ (f1,k1,f2,k2,g)"
    by (metis obtain_fresh)
  hence "{} ⊢ Ex g (SeqAppendP f1 k1 f2 k2 (Var g))"
    using assms
    apply (auto simp: SeqAppendP.simps [of g1 g2])
    apply (rule cut_same [OF exists_RestrictedP [of g1 f1 k1]], auto)
    apply (rule cut_same [OF exists_ShiftP [of g2 f2 k2 k1]], auto)
    apply (rule cut_same [OF exists_UnionP [of g "Var g1" "Var g2"]], auto)
    apply (rule Ex_I [where x="Var g"], simp)
    apply (rule Ex_I [where x="Var g1"], simp)
    apply (rule Ex_I [where x="Var g2"], auto)
    done
  thus ?thesis using assms
    by (metis thin0)
qed

lemma SeqAppendP_Mem1: "{SeqAppendP f1 k1 f2 k2 g, HPair x y IN f1, x IN k1} ⊢ HPair x y IN g"
proof -
  obtain g1::name and g2::name
    where "atom g1 ♯ (g2,f1,k1,f2,k2,g,x,y)" "atom g2 ♯ (f1,k1,f2,k2,g,x,y)"
    by (metis obtain_fresh)
  thus ?thesis
    by (auto simp: SeqAppendP.simps [of g1 g2] intro: UnionP_Mem1 [THEN cut2] RestrictedP_Mem [THEN cut3])
qed

lemma SeqAppendP_Mem2: "{SeqAppendP f1 k1 f2 k2 g, HaddP k1 x x', x IN k2, HPair x y IN f2} ⊢ HPair x' y IN g"
proof -
  obtain g1::name and g2::name
    where "atom g1 ♯ (g2,f1,k1,f2,k2,g,x,x',y)" "atom g2 ♯ (f1,k1,f2,k2,g,x,x',y)"
    by (metis obtain_fresh)
  thus ?thesis
    by (auto simp: SeqAppendP.simps [of g1 g2] intro: UnionP_Mem2 [THEN cut2] ShiftP_Mem1 [THEN cut4])
qed

lemma SeqAppendP_Mem_E: 
  assumes "H ⊢ SeqAppendP f1 k1 f2 k2 g" 
      and "insert (HPair x y IN f1) (insert (x IN k1) H) ⊢ A" 
      and "insert (HPair (Var u) y IN f2) (insert (HaddP k1 (Var u) x) (insert (Var u IN k2) H)) ⊢ A"
      and u: "atom u ♯ (f1,k1,f2,k2,x,y,g,A)" "∀C ∈ H. atom u ♯ C"
  shows "insert (HPair x y IN g) H ⊢ A" (*<*)
proof -
  obtain g1::name and g2::name
  where atoms: "atom g1 ♯ (g2,f1,k1,f2,k2,g,x,y,u)" "atom g2 ♯ (f1,k1,f2,k2,g,x,y,u)"
    by (metis obtain_fresh)
  hence "{SeqAppendP f1 k1 f2 k2 g, HPair x y IN g} 
         ⊢ (HPair x y IN f1 AND x IN k1) OR Ex u ((Var u) IN k2 AND HaddP k1 (Var u) x AND HPair (Var u) y IN f2)"
    using u
    apply (auto simp: SeqAppendP.simps [of g1 g2])
    apply (rule UnionP_Mem_E [THEN rotate4])
    apply (rule AssumeH)+
    apply (blast intro: Disj_I1 cut_same [OF RestrictedP_Mem2 [THEN cut2]])
    apply (rule Disj_I2)
    apply (rule cut_same [OF ShiftP_Mem2 [where u=u, THEN cut2]])
    defer 1
    apply force+
    done
  thus ?thesis 
    apply (rule cut_same [OF _ [THEN cut2]])
    using assms
    apply (auto intro: thin1 rotate2 thin3 thin4)
    done
qed (*>*)

section ‹LstSeqP and SeqAppendP›

lemma HDomain_Incl_SeqAppendP:  ― ‹The And eliminates the need to prove @{text cut5}›
  "{SeqAppendP f1 k1 f2 k2 g, HDomain_Incl f1 k1 AND HDomain_Incl f2 k2, 
    HaddP k1 k2 k, OrdP k1} ⊢ HDomain_Incl g k" (*<*)
proof -
  obtain x::name and y::name and z::name and i::name 
    where "atom x ♯ (f1,k1,f2,k2,g,k,y,z,i)"  "atom y ♯ (f1,k1,f2,k2,g,k,z,i)"  
          "atom z ♯ (f1,k1,f2,k2,g,k,i)"  "atom i ♯ (f1,k1,f2,k2,g,k)"
    by (metis obtain_fresh) 
  thus ?thesis
    apply (auto simp: HDomain_Incl.simps [of x _ _ y z])
    apply (rule HaddP_Mem_cases [where i=i, THEN rotate2], auto)
    ― ‹case 1›
    apply (rule All_E' [where x = "Var x"], blast, auto)
    apply (rule ContraProve [THEN rotate4])
    apply (rule Ex_I [where x = "Var y"], auto)
    apply (rule Ex_I [where x = "Var z"], auto)
    apply (rule Var_Eq_subst_Iff [THEN Iff_MP_same, THEN rotate2], simp)
    apply (rule SeqAppendP_Mem1 [THEN cut3], auto)
    apply (rule Mem_cong [OF Assume Refl, THEN Iff_MP_same], auto)
    ― ‹case 2›
    apply (rule Ex_I [where x = "Var i"], auto)
    apply (rule ContraProve [THEN rotate5])
    apply (rule Ex_I [where x = "Var y"], simp)
    apply (rule Ex_I [where x = "HPair (Var x) (Var y)"], auto)
    apply (blast intro: SeqAppendP_Mem2 [THEN cut4] Mem_cong [OF _ Refl, THEN Iff_MP_same])
    done
qed (*>*)

declare SeqAppendP.simps [simp del]

lemma HFun_Sigma_SeqAppendP:
  "{SeqAppendP f1 k1 f2 k2 g, HFun_Sigma f1, HFun_Sigma f2, OrdP k1} ⊢ HFun_Sigma g" (*<*)
proof -
  obtain x::name and y::name and z::name 
     and x'::name and y'::name and z'::name and g1::name and g2::name
     and v::name and v'::name and w::name
    where atoms: 
       "atom v ♯ (v',w,g1,g2,z,z',x,y,x',y',f1,k1,f2,k2,g)" "atom v' ♯ (w,g1,g2,z,z',x,y,x',y',f1,k1,f2,k2,g)"
       "atom w ♯ (g1,g2,z,z',x,y,x',y',f1,k1,f2,k2,g)" 
       "atom g1 ♯ (g2,z,z',x,y,x',y',f1,k1,f2,k2,g)" "atom g2 ♯ (z,z',x,y,x',y',f1,k1,f2,k2,g)"
       "atom z ♯ (z',x,y,x',y',f1,k1,f2,k2,g)" "atom z' ♯ (x,y,x',y',f1,k1,f2,k2,g)"
       "atom x ♯ (y,x',y',f1,k1,f2,k2,g)" "atom y ♯ (x',y',f1,k1,f2,k2,g)" 
       "atom x' ♯ (y',f1,k1,f2,k2,g)" "atom y' ♯ (f1,k1,f2,k2,g)" 
    by (metis obtain_fresh) 
  thus ?thesis
    apply (simp add: HFun_Sigma.simps [of z g z' x y x' y'] SeqAppendP.simps [of g1 g2])
    apply (rule Ex_EH Conj_EH All_I Imp_I)+
    apply (rule cut_same [OF UnionP_Mem [where a = "Var z", THEN cut2]])
    apply (rule AssumeH)+
    apply (rule Disj_E)
    apply (rule cut_same [OF UnionP_Mem [where a = "Var z'", THEN cut2]])
    apply (rule AssumeH)+
    apply (rule thin1 [where A="UnionP (Var g1) (Var g2) g", THEN rotate6])
    apply (rule Disj_E)
    ― ‹case 1/1›
    apply (rule thin1 [where A="ShiftP f2 k2 k1 (Var g2)", THEN rotate5])
    apply (rule RestrictedP_Mem_D [where a = "Var z"])
    apply (rule AssumeH)+
    apply (rule RestrictedP_Mem_D [where a = "Var z'"])
    apply (rule AssumeH)+
    apply (simp add: HFun_Sigma.simps [of z f1 z' x y x' y'])
    apply (rule All2_E [where x = "Var z", THEN rotate8], simp_all, blast)
    apply (rule All2_E [where x = "Var z'"], simp_all, blast)
    apply (rule Ex_EH Conj_EH)+
    apply simp_all
    apply (rule Ex_I [where x="Var x"], simp)
    apply (rule Ex_I [where x="Var y"], simp)
    apply (rule Ex_I [where x="Var x'"], simp)
    apply (rule Ex_I [where x="Var y'"], simp)
    apply (rule Conj_I, blast)+
    apply blast
    ― ‹case 1/2›
    apply (rule RestrictedP_Mem_D [where a = "Var z"])
    apply (rule AssumeH)+
    apply (rule thin1 [where A="Var z IN g", THEN rotate5])
    apply (rule thin1 [where A="Var z' IN g", THEN rotate4])
    apply (rule cut_same [OF HFun_Sigma_Mem_imp_HPair [of _ f1 "Var z" x y]], simp_all)
    apply (rule AssumeH)+
    apply (rule cut_same [OF ShiftP_Mem_D [where x=v and x'=v' and y=w]])
    apply (rule AssumeH Ex_EH Conj_EH)+
    apply auto [3]
    apply (rule AssumeH Ex_EH Conj_EH)+
    apply simp_all
    apply (rule Ex_I [where x="Var x"], simp)
    apply (rule Ex_I [where x="Var y"], simp)
    apply (rule Ex_I [where x="Var v'"], simp)
    apply (rule Ex_I [where x="Var w"], simp)
    apply auto [1]
    apply (blast intro: Mem_HFun_Sigma_OrdP [THEN cut2] Mem_cong [OF _ Refl, THEN Iff_MP_same])
    apply (blast intro: Hyp HaddP_OrdP)
    apply (rule cut_same [OF RestrictedP_Mem2 [THEN cut2]])
    apply (rule AssumeH)+
    apply (blast intro: Mem_cong [OF _ Refl, THEN Iff_MP_same])
    apply (blast intro: Hyp Mem_cong [OF _ Refl, THEN Iff_MP_same] HaddP_Mem_contra)
    ― ‹END of case 1/2›
    apply (rule cut_same [OF UnionP_Mem [where a = "Var z'", THEN cut2]])
    apply (rule AssumeH)+
    apply (rule thin1 [where A="UnionP (Var g1) (Var g2) g", THEN rotate6])
    apply (rule Disj_E)
    ― ‹case 2/1›
    apply (rule RestrictedP_Mem_D [where a = "Var z'"])
    apply (rule AssumeH)+
    apply (rule thin1 [where A="Var z IN g", THEN rotate5])
    apply (rule thin1 [where A="Var z' IN g", THEN rotate4])
    apply (rule cut_same [OF HFun_Sigma_Mem_imp_HPair [of _ f1 "Var z'" x y]], simp_all)
    apply (rule AssumeH)+
    apply (rule cut_same [OF ShiftP_Mem_D [where x=v and x'=v' and y=w]])
    apply (rule AssumeH Ex_EH Conj_EH)+
    apply auto [3]
    apply (rule AssumeH Ex_EH Conj_EH)+
    apply simp_all
    apply (rule Ex_I [where x="Var v'"], simp)
    apply (rule Ex_I [where x="Var w"], simp)
    apply (rule Ex_I [where x="Var x"], simp)
    apply (rule Ex_I [where x="Var y"], simp)
    apply auto [1]
    apply (blast intro: Hyp HaddP_OrdP)
    apply (blast intro: Mem_HFun_Sigma_OrdP [THEN cut2] Mem_cong [OF _ Refl, THEN Iff_MP_same])
    apply (rule cut_same [OF RestrictedP_Mem2 [THEN cut2]])
    apply (rule AssumeH)+
    apply (blast intro: Mem_cong [OF _ Refl, THEN Iff_MP_same])
    apply (blast intro: Mem_cong [OF _ Refl, THEN Iff_MP2_same] HaddP_Mem_contra Hyp)
    ― ‹case 2/2›
    apply (rule cut_same [OF ShiftP_Mem_D [where x=x and x'=x' and y=y and a = "Var z"]])
    apply (rule AssumeH Ex_EH Conj_EH)+
    apply simp_all
    apply (rule cut_same [OF ShiftP_Mem_D [where x=v and x'=v' and y=w and a = "Var z'"]])
    apply (rule AssumeH Ex_EH Conj_EH)+
    apply simp_all
    apply (rule thin1 [where A="ShiftP f2 k2 k1 (Var g2)", THEN rotate7])
    apply (rule thin1 [where A="RestrictedP f1 k1 (Var g1)", THEN rotate7])
    apply (rule AssumeH Ex_EH Conj_EH)+
    apply simp_all
    apply (rule Ex_I [where x="Var x'"], simp)
    apply (rule Ex_I [where x="Var y"], simp)
    apply (rule Ex_I [where x="Var v'"], simp)
    apply (rule Ex_I [where x="Var w"], auto intro: Hyp HaddP_OrdP)
    apply (rule cut_same [where A="Var x EQ Var v"])
    apply (blast intro: HaddP_inv2 [THEN cut3] HaddP_cong [OF Refl Refl, THEN Iff_MP_same] Hyp)
    apply (rule HFun_Sigma_E [where r=f2])
    apply (auto intro: Hyp Var_Eq_subst_Iff [THEN Iff_MP_same])
    done
qed (*>*)

lemma LstSeqP_SeqAppendP:
  assumes "H ⊢ SeqAppendP f1 (SUCC k1) f2 (SUCC k2) g"
          "H ⊢ LstSeqP f1 k1 y1" "H ⊢ LstSeqP f2 k2 y2" "H ⊢ HaddP k1 k2 k" 
  shows "H ⊢ LstSeqP g (SUCC k) y2"
proof -
  have "{SeqAppendP f1 (SUCC k1) f2 (SUCC k2) g, LstSeqP f1 k1 y1, LstSeqP f2 k2 y2, HaddP k1 k2 k} 
   ⊢ LstSeqP g (SUCC k) y2"
    apply (auto simp: LstSeqP.simps intro: HaddP_OrdP OrdP_SUCC_I)
    apply (rule HDomain_Incl_SeqAppendP [THEN cut4])
    apply (rule AssumeH Conj_I)+
    apply (blast intro: HaddP_SUCC1 [THEN cut1] HaddP_SUCC2 [THEN cut1])
    apply (blast intro: HaddP_OrdP OrdP_SUCC_I)
    apply (rule HFun_Sigma_SeqAppendP [THEN cut4])
    apply (auto intro: HaddP_OrdP OrdP_SUCC_I)
    apply (blast intro: Mem_SUCC_Refl HaddP_SUCC1 [THEN cut1] HaddP_SUCC2 [THEN cut1] 
                        SeqAppendP_Mem2 [THEN cut4])
    done
  thus ?thesis using assms
    by (rule cut4)
qed

lemma SeqAppendP_NotInDom: "{SeqAppendP f1 k1 f2 k2 g, HaddP k1 k2 k, OrdP k1} ⊢ NotInDom k g"
proof -
  obtain x::name and z::name 
    where "atom x ♯ (z,f1,k1,f2,k2,g,k)"  "atom z ♯ (f1,k1,f2,k2,g,k)"
    by (metis obtain_fresh)
  thus ?thesis
    apply (auto simp: NotInDom.simps [of z])
    apply (rule SeqAppendP_Mem_E [where u=x])
    apply (rule AssumeH)+
    apply (blast intro: HaddP_Mem_contra, simp_all)
    apply (rule cut_same [where A="(Var x) EQ k2"])
    apply (blast intro: HaddP_inv2 [THEN cut3])
    apply (blast intro: Mem_non_refl [where x=k2] Mem_cong [OF _ Refl, THEN Iff_MP_same])
    done
qed

lemma LstSeqP_SeqAppendP_Eats:
  assumes "H ⊢ SeqAppendP f1 (SUCC k1) f2 (SUCC k2) g"
          "H ⊢ LstSeqP f1 k1 y1" "H ⊢ LstSeqP f2 k2 y2" "H ⊢ HaddP k1 k2 k" 
  shows "H ⊢ LstSeqP (Eats g (HPair (SUCC (SUCC k)) z)) (SUCC (SUCC k)) z"
proof -
  have "{SeqAppendP f1 (SUCC k1) f2 (SUCC k2) g, LstSeqP f1 k1 y1, LstSeqP f2 k2 y2, HaddP k1 k2 k} 
        ⊢ LstSeqP (Eats g (HPair (SUCC (SUCC k)) z)) (SUCC (SUCC k)) z"
    apply (rule cut2 [OF NotInDom_LstSeqP_Eats]) 
    apply (rule SeqAppendP_NotInDom [THEN cut3])
    apply (rule AssumeH)
    apply (metis HaddP_SUCC1 HaddP_SUCC2 cut1 thin1)
    apply (metis Assume LstSeqP_OrdP OrdP_SUCC_I insert_commute)
    apply (blast intro: LstSeqP_SeqAppendP)
    done
  thus ?thesis using assms
    by (rule cut4)
qed

section ‹Substitution and Abstraction on Terms›

subsection ‹Atomic cases›

lemma SeqStTermP_Var_same:
  assumes "atom s ♯ (k,v,i)" "atom k ♯ (v,i)"
    shows "{VarP v} ⊢ Ex s (Ex k (SeqStTermP v i v i (Var s) (Var k)))"
proof -
  obtain l::name and sl::name and sl'::name and m::name and sm::name and sm'::name
     and n::name and sn::name and sn'::name
    where "atom l ♯ (v,i,s,k,sl,sl',m,n,sm,sm',sn,sn')"
          "atom sl ♯ (v,i,s,k,sl',m,n,sm,sm',sn,sn')"
          "atom sl' ♯ (v,i,s,k,m,n,sm,sm',sn,sn')"
          "atom m ♯ (v,i,s,k,n,sm,sm',sn,sn')" "atom n ♯ (v,i,s,k,sm,sm',sn,sn')"
          "atom sm ♯ (v,i,s,k,sm',sn,sn')" "atom sm' ♯ (v,i,s,k,sn,sn')"
          "atom sn ♯ (v,i,s,k,sn')" "atom sn' ♯ (v,i,s,k)"
    by (metis obtain_fresh)
  thus ?thesis using assms
    apply (simp add: SeqStTermP.simps [of l _ _ v i sl sl' m n sm sm' sn sn'])
    apply (rule Ex_I [where x = "Eats Zero (HPair Zero (HPair v i))"], simp)
    apply (rule Ex_I [where x = Zero], auto intro!: Mem_SUCC_EH)
    apply (rule Ex_I [where x = v], simp)
    apply (rule Ex_I [where x = i], auto intro: Disj_I1 Mem_Eats_I2 HPair_cong)
    done
qed

lemma SeqStTermP_Var_diff:
  assumes "atom s ♯ (k,v,w,i)" "atom k ♯ (v,w,i)"
    shows "{VarP v, VarP w, Neg (v EQ w) } ⊢ Ex s (Ex k (SeqStTermP v i w w (Var s) (Var k)))"
proof -
  obtain l::name and sl::name and sl'::name and m::name and sm::name and sm'::name
     and n::name and sn::name and sn'::name
    where "atom l ♯ (v,w,i,s,k,sl,sl',m,n,sm,sm',sn,sn')"
          "atom sl ♯ (v,w,i,s,k,sl',m,n,sm,sm',sn,sn')"
          "atom sl' ♯ (v,w,i,s,k,m,n,sm,sm',sn,sn')"
          "atom m ♯ (v,w,i,s,k,n,sm,sm',sn,sn')" "atom n ♯ (v,w,i,s,k,sm,sm',sn,sn')"
          "atom sm ♯ (v,w,i,s,k,sm',sn,sn')" "atom sm' ♯ (v,w,i,s,k,sn,sn')"
          "atom sn ♯ (v,w,i,s,k,sn')" "atom sn' ♯ (v,w,i,s,k)"
    by (metis obtain_fresh)
  thus ?thesis using assms
    apply (simp add: SeqStTermP.simps [of l _ _ v i sl sl' m n sm sm' sn sn'])
    apply (rule Ex_I [where x = "Eats Zero (HPair Zero (HPair w w))"], simp)
    apply (rule Ex_I [where x = Zero], auto intro!: Mem_SUCC_EH)
    apply (rule rotate2 [OF Swap])
    apply (rule Ex_I [where x = w], simp)
    apply (rule Ex_I [where x = w], auto simp: VarP_def)
    apply (blast intro: HPair_cong Mem_Eats_I2)
    apply (blast intro: Sym OrdNotEqP_I Disj_I1 Disj_I2)
    done
qed

lemma SeqStTermP_Zero:
  assumes "atom s ♯ (k,v,i)" "atom k ♯ (v,i)"
    shows "{VarP v} ⊢ Ex s (Ex k (SeqStTermP v i Zero Zero (Var s) (Var k)))" (*<*)
proof -
  obtain l::name and sl::name and sl'::name and m::name and sm::name and sm'::name
     and n::name and sn::name and sn'::name
    where "atom l ♯ (v,i,s,k,sl,sl',m,n,sm,sm',sn,sn')"
          "atom sl ♯ (v,i,s,k,sl',m,n,sm,sm',sn,sn')"
          "atom sl' ♯ (v,i,s,k,m,n,sm,sm',sn,sn')"
          "atom m ♯ (v,i,s,k,n,sm,sm',sn,sn')" "atom n ♯ (v,i,s,k,sm,sm',sn,sn')"
          "atom sm ♯ (v,i,s,k,sm',sn,sn')" "atom sm' ♯ (v,i,s,k,sn,sn')"
          "atom sn ♯ (v,i,s,k,sn')" "atom sn' ♯ (v,i,s,k)"
    by (metis obtain_fresh)
  thus ?thesis using assms
    apply (simp add: SeqStTermP.simps [of l _ _ v i sl sl' m n sm sm' sn sn'])
    apply (rule Ex_I [where x = "Eats Zero (HPair Zero (HPair Zero Zero))"], simp)
    apply (rule Ex_I [where x = Zero], auto intro!: Mem_SUCC_EH)
    apply (rule Ex_I [where x = Zero], simp)
    apply (rule Ex_I [where x = Zero], simp)
    apply (rule Conj_I)
    apply (force intro: Var_Eq_subst_Iff [THEN Iff_MP_same] Mem_Eats_I2)
    apply (force simp: VarP_def OrdNotEqP.simps intro: Disj_I1 Disj_I2)
    done
qed (*>*)

corollary SubstTermP_Zero: "{TermP t} ⊢ SubstTermP «Var v» t Zero Zero"
proof -
  obtain s::name and k::name where "atom s ♯ (v,t,k)"  "atom k ♯ (v,t)"
    by (metis obtain_fresh)
  thus ?thesis 
    by (auto simp: SubstTermP.simps [of s _ _ _ _ k] intro: SeqStTermP_Zero [THEN cut1])
qed

corollary SubstTermP_Var_same: "{VarP v, TermP t} ⊢ SubstTermP v t v t"
proof -
  obtain s::name and k::name where "atom s ♯ (v,t,k)" "atom k ♯ (v,t)"
    by (metis obtain_fresh)
  thus ?thesis 
    by (auto simp: SubstTermP.simps [of s _ _ _ _ k] intro: SeqStTermP_Var_same [THEN cut1])
qed

corollary SubstTermP_Var_diff: "{VarP v, VarP w, Neg (v EQ w), TermP t} ⊢ SubstTermP v t w w"
proof -
  obtain s::name and k::name where "atom s ♯ (v,w,t,k)" "atom k ♯ (v,w,t)"
    by (metis obtain_fresh)
  thus ?thesis 
    by (auto simp: SubstTermP.simps [of s _ _ _ _ k] intro: SeqStTermP_Var_diff [THEN cut3])
qed

lemma SeqStTermP_Ind:
  assumes "atom s ♯ (k,v,t,i)" "atom k ♯ (v,t,i)"
    shows "{VarP v, IndP t} ⊢ Ex s (Ex k (SeqStTermP v i t t (Var s) (Var k)))"
proof -
  obtain l::name and sl::name and sl'::name and m::name and sm::name and sm'::name
     and n::name and sn::name and sn'::name
    where "atom l ♯ (v,t,i,s,k,sl,sl',m,n,sm,sm',sn,sn')"
          "atom sl ♯ (v,t,i,s,k,sl',m,n,sm,sm',sn,sn')"
          "atom sl' ♯ (v,t,i,s,k,m,n,sm,sm',sn,sn')"
          "atom m ♯ (v,t,i,s,k,n,sm,sm',sn,sn')" "atom n ♯ (v,t,i,s,k,sm,sm',sn,sn')"
          "atom sm ♯ (v,t,i,s,k,sm',sn,sn')" "atom sm' ♯ (v,t,i,s,k,sn,sn')"
          "atom sn ♯ (v,t,i,s,k,sn')" "atom sn' ♯ (v,t,i,s,k)"
    by (metis obtain_fresh)
  thus ?thesis using assms
    apply (simp add: SeqStTermP.simps [of l _ _ v i sl sl' m n sm sm' sn sn'])
    apply (rule Ex_I [where x = "Eats Zero (HPair Zero (HPair t t))"], simp)
    apply (rule Ex_I [where x = Zero], auto intro!: Mem_SUCC_EH)
    apply (rule Ex_I [where x = t], simp)
    apply (rule Ex_I [where x = t], auto intro: HPair_cong Mem_Eats_I2)
    apply (blast intro: Disj_I1 Disj_I2 VarP_neq_IndP)
    done
qed

corollary SubstTermP_Ind: "{VarP v, IndP w, TermP t} ⊢ SubstTermP v t w w"
proof -
  obtain s::name and k::name where "atom s ♯ (v,w,t,k)" "atom k ♯ (v,w,t)"
    by (metis obtain_fresh)
  thus ?thesis 
    by (force simp: SubstTermP.simps [of s _ _ _ _ k]
              intro: SeqStTermP_Ind [THEN cut2])
qed
 
subsection ‹Non-atomic cases›

lemma SeqStTermP_Eats:
  assumes sk: "atom s ♯ (k,s1,s2,k1,k2,t1,t2,u1,u2,v,i)"
              "atom k ♯ (t1,t2,u1,u2,v,i)"
    shows "{SeqStTermP v i t1 u1 s1 k1, SeqStTermP v i t2 u2 s2 k2} 
           ⊢ Ex s (Ex k (SeqStTermP v i (Q_Eats t1 t2) (Q_Eats u1 u2) (Var s) (Var k)))" (*<*)
proof -
  obtain km::name and kn::name and j::name and k'::name and l::name and sl::name and sl'::name  
     and m::name and n::name and sm::name and sm'::name and sn::name and sn'::name
    where atoms2: "atom km ♯ (s1,s2,s,k1,k2,k,t1,t2,u1,u2,v,i,kn,j,k',l,sl,sl',m,n,sm,sm',sn,sn')"
         "atom kn ♯ (s1,s2,s,k1,k2,k,t1,t2,u1,u2,v,i,j,k',l,sl,sl',m,n,sm,sm',sn,sn')"
         "atom j  ♯ (s1,s2,s,k1,k2,k,t1,t2,u1,u2,v,i,k',l,sl,sl',m,n,sm,sm',sn,sn')"
      and atoms: "atom k' ♯ (s1,s2,s,k1,k2,k,t1,t2,u1,u2,v,i,l,sl,sl',m,n,sm,sm',sn,sn')"
         "atom l  ♯ (s1,s2,s,k1,k2,k,t1,t2,u1,u2,v,i,sl,sl',m,n,sm,sm',sn,sn')"
         "atom sl ♯ (s1,s2,s,k1,k2,k,t1,t2,u1,u2,v,i,sl',m,n,sm,sm',sn,sn')" 
         "atom sl'♯ (s1,s2,s,k1,k2,k,t1,t2,u1,u2,v,i,m,n,sm,sm',sn,sn')"
         "atom m  ♯ (s1,s2,s,k1,k2,k,t1,t2,u1,u2,v,i,n,sm,sm',sn,sn')" 
         "atom n  ♯ (s1,s2,s,k1,k2,k,t1,t2,u1,u2,v,i,sm,sm',sn,sn')"
         "atom sm ♯ (s1,s2,s,k1,k2,k,t1,t2,u1,u2,v,i,sm',sn,sn')" 
         "atom sm'♯ (s1,s2,s,k1,k2,k,t1,t2,u1,u2,v,i,sn,sn')"
         "atom sn ♯ (s1,s2,s,k1,k2,k,t1,t2,u1,u2,v,i,sn')" 
         "atom sn'♯ (s1,s2,s,k1,k2,k,t1,t2,u1,u2,v,i)"
    by (metis obtain_fresh) 
  let ?hyp = "{HaddP k1 k2 (Var k'), OrdP k1, OrdP k2, SeqAppendP s1 (SUCC k1) s2 (SUCC k2) (Var s), SeqStTermP v i t1 u1 s1 k1, SeqStTermP v i t2 u2 s2 k2}"
  show ?thesis
     using sk atoms
     apply (auto simp: SeqStTermP.simps [of l "Var s" _ _ _ sl sl' m n sm sm' sn sn'])
     apply (rule cut_same [where A="OrdP k1 AND OrdP k2"])
     apply (metis Conj_I SeqStTermP_imp_OrdP thin1 thin2)
     apply (rule cut_same [OF exists_SeqAppendP [of s s1 "SUCC k1" s2 "SUCC k2"]])
     apply (rule AssumeH Ex_EH Conj_EH | simp)+
     apply (rule cut_same [OF exists_HaddP [where j=k' and x=k1 and y=k2]])
     apply (rule AssumeH Ex_EH Conj_EH | simp)+
     apply (rule Ex_I [where x="Eats (Var s) (HPair (SUCC (SUCC (Var k'))) (HPair (Q_Eats t1 t2) (Q_Eats u1 u2)))"])
     apply (simp_all (no_asm_simp))
     apply (rule Ex_I [where x="SUCC (SUCC (Var k'))"], simp)
     apply (rule Conj_I [OF _ Conj_I])
     apply (metis SeqStTermP_imp_VarP thin1)
     apply (blast intro: LstSeqP_SeqAppendP_Eats SeqStTermP_imp_LstSeqP [THEN cut1])
     proof (rule All2_SUCC_I, simp_all)
       show "?hyp ⊢ Ex sl (Ex sl'
              (HPair (SUCC (SUCC (Var k'))) (HPair (Var sl) (Var sl')) IN Eats (Var s) (HPair (SUCC (SUCC (Var k'))) (HPair (Q_Eats t1 t2) (Q_Eats u1 u2))) AND
               ((Var sl EQ v AND Var sl' EQ i OR (IndP (Var sl) OR Var sl NEQ v) AND Var sl' EQ Var sl) OR
                Ex m (Ex n (Ex sm (Ex sm' (Ex sn (Ex sn'
                 (Var m IN SUCC (SUCC (Var k')) AND
                  Var n IN SUCC (SUCC (Var k')) AND
                  HPair (Var m) (HPair (Var sm) (Var sm')) IN Eats (Var s) (HPair (SUCC (SUCC (Var k'))) (HPair (Q_Eats t1 t2) (Q_Eats u1 u2))) AND
                  HPair (Var n) (HPair (Var sn) (Var sn')) IN Eats (Var s) (HPair (SUCC (SUCC (Var k'))) (HPair (Q_Eats t1 t2) (Q_Eats u1 u2))) AND
                  Var sl EQ Q_Eats (Var sm) (Var sn) AND Var sl' EQ Q_Eats (Var sm') (Var sn'))))))))))"
       ― ‹verifying the final values›
       apply (rule Ex_I [where x="Q_Eats t1 t2"])
       using sk atoms apply simp
       apply (rule Ex_I [where x="Q_Eats u1 u2"], simp)
       apply (rule Conj_I, metis Mem_Eats_I2 Refl)
       apply (rule Disj_I2)
       apply (rule Ex_I [where x=k1], simp)
       apply (rule Ex_I [where x="SUCC (Var k')"], simp)
       apply (rule Ex_I [where x=t1], simp)
       apply (rule Ex_I [where x=u1], simp)
       apply (rule Ex_I [where x=t2], simp)
       apply (rule Ex_I [where x=u2], simp)
       apply (rule Conj_I)
       apply (blast intro: HaddP_Mem_I LstSeqP_OrdP Mem_SUCC_I1)
       apply (rule Conj_I [OF Mem_SUCC_Refl Conj_I])
       apply (blast intro: Mem_Eats_I1 SeqAppendP_Mem1 [THEN cut3] Mem_SUCC_Refl SeqStTermP_imp_LstSeqP [THEN cut1] 
                           LstSeqP_imp_Mem)
       apply (blast intro: Mem_Eats_I1 SeqAppendP_Mem2 [THEN cut4] Mem_SUCC_Refl SeqStTermP_imp_LstSeqP [THEN cut1] 
                           HaddP_SUCC1 [THEN cut1] LstSeqP_imp_Mem)
       done
     next
       show "?hyp ⊢ All2 l (SUCC (SUCC (Var k')))
                (Ex sl (Ex sl'
                  (HPair (Var l) (HPair (Var sl) (Var sl')) IN Eats (Var s) (HPair (SUCC (SUCC (Var k'))) (HPair (Q_Eats t1 t2) (Q_Eats u1 u2))) AND
                   ((Var sl EQ v AND Var sl' EQ i OR (IndP (Var sl) OR Var sl NEQ v) AND Var sl' EQ Var sl) OR
                    Ex m (Ex n (Ex sm (Ex sm' (Ex sn (Ex sn'
                       (Var m IN Var l AND
                        Var n IN Var l AND
                        HPair (Var m) (HPair (Var sm) (Var sm')) IN Eats (Var s) (HPair (SUCC (SUCC (Var k'))) (HPair (Q_Eats t1 t2) (Q_Eats u1 u2))) AND
                        HPair (Var n) (HPair (Var sn) (Var sn')) IN Eats (Var s) (HPair (SUCC (SUCC (Var k'))) (HPair (Q_Eats t1 t2) (Q_Eats u1 u2))) AND
                        Var sl EQ Q_Eats (Var sm) (Var sn) AND Var sl' EQ Q_Eats (Var sm') (Var sn')))))))))))"
     ― ‹verifying the sequence buildup›
     apply (rule cut_same [where A="HaddP (SUCC k1) (SUCC k2) (SUCC (SUCC (Var k')))"])
     apply (blast intro: HaddP_SUCC1 [THEN cut1] HaddP_SUCC2 [THEN cut1])
     apply (rule All_I Imp_I)+
     apply (rule HaddP_Mem_cases [where i=j])
     using sk atoms atoms2 apply simp_all
     apply (rule AssumeH)
     apply (blast intro: OrdP_SUCC_I LstSeqP_OrdP)
     ― ‹... the sequence buildup via s1›
     apply (simp add: SeqStTermP.simps [of l s1 _ _ _ sl sl' m n sm sm' sn sn'])
     apply (rule AssumeH Ex_EH Conj_EH)+
     apply (rule All2_E [THEN rotate2])
     apply (simp | rule AssumeH Ex_EH Conj_EH)+
     apply (rule Ex_I [where x="Var sl"], simp)
     apply (rule Ex_I [where x="Var sl'"], simp)
     apply (rule Conj_I)
     apply (metis Mem_Eats_I1 SeqAppendP_Mem1 rotate3 thin2 thin4)
     apply (rule AssumeH Disj_IE1H Ex_EH Conj_EH)+
     apply (rule Ex_I [where x="Var m"], simp)
     apply (rule Ex_I [where x="Var n"], simp)
     apply (rule Ex_I [where x="Var sm"], simp)
     apply (rule Ex_I [where x="Var sm'"], simp)
     apply (rule Ex_I [where x="Var sn"], simp)
     apply (rule Ex_I [where x="Var sn'"], simp_all)
     apply (rule Conj_I, rule AssumeH)+
     apply (blast del: Disj_EH intro: OrdP_Trans [OF OrdP_SUCC_I] Mem_Eats_I1 [OF SeqAppendP_Mem1 [THEN cut3]] Hyp)
     ― ‹... the sequence buildup via s2›
     apply (simp add: SeqStTermP.simps [of l s2 _ _ _ sl sl' m n sm sm' sn sn'])
     apply (rule AssumeH Ex_EH Conj_EH)+
     apply (rule All2_E [THEN rotate2])
     apply (simp | rule AssumeH Ex_EH Conj_EH)+
     apply (rule Ex_I [where x="Var sl"], simp)
     apply (rule Ex_I [where x="Var sl'"], simp)
     apply (rule cut_same [where A="OrdP (Var j)"])
     apply (metis HaddP_imp_OrdP rotate2 thin2)
     apply (rule Conj_I)
     apply (blast intro: Mem_Eats_I1 SeqAppendP_Mem2 [THEN cut4] del: Disj_EH)
     apply (rule AssumeH Disj_IE1H Ex_EH Conj_EH)+
     apply simp_all
     apply (rule cut_same [OF exists_HaddP [where j=km and x="SUCC k1" and y="Var m"]])
     apply (blast intro!: Ord_IN_Ord, simp)
     apply (rule cut_same [OF exists_HaddP [where j=kn and x="SUCC k1" and y="Var n"]])
     apply (blast intro!: Ord_IN_Ord, simp)
     apply (rule AssumeH Ex_EH Conj_EH | simp)+
     apply (rule Ex_I [where x="Var km"], simp)
     apply (rule Ex_I [where x="Var kn"], simp)
     apply (rule Ex_I [where x="Var sm"], simp)
     apply (rule Ex_I [where x="Var sm'"], simp)
     apply (rule Ex_I [where x="Var sn"], simp)
     apply (rule Ex_I [where x="Var sn'"], simp_all)
     apply (rule Conj_I [OF _ Conj_I])
     apply (blast intro!: HaddP_Mem_cancel_left [THEN Iff_MP2_same] OrdP_SUCC_I intro: LstSeqP_OrdP Hyp)+
     apply (blast intro: OrdP_Trans Hyp Mem_Eats_I1 SeqAppendP_Mem2 [THEN cut4] HaddP_imp_OrdP [THEN cut1])
     done
   qed
qed (*>*)

theorem SubstTermP_Eats:
   "{SubstTermP v i t1 u1, SubstTermP v i t2 u2} ⊢ SubstTermP v i (Q_Eats t1 t2) (Q_Eats u1 u2)"
proof -
  obtain k1::name and s1::name and k2::name and s2::name and k::name and s::name
    where "atom s1 ♯ (v,i,t1,u1,t2,u2)" "atom k1 ♯ (v,i,t1,u1,t2,u2,s1)"  
          "atom s2 ♯ (v,i,t1,u1,t2,u2,k1,s1)" "atom k2 ♯ (v,i,t1,u1,t2,u2,s2,k1,s1)"
          "atom s  ♯ (v,i,t1,u1,t2,u2,k2,s2,k1,s1)"
          "atom k  ♯ (v,i,t1,u1,t2,u2,s,k2,s2,k1,s1)" 
    by (metis obtain_fresh)
   thus ?thesis
     by (auto intro!: SeqStTermP_Eats [THEN cut2]
              simp: SubstTermP.simps [of s _ _ _ "(Q_Eats u1 u2)" k] 
                    SubstTermP.simps [of s1 v i t1 u1 k1]  
                    SubstTermP.simps [of s2 v i t2 u2 k2])
qed

subsection ‹Substitution over a constant›

lemma SeqConstP_lemma:
  assumes "atom m ♯ (s,k,c,n,sm,sn)"  "atom n ♯ (s,k,c,sm,sn)" 
          "atom sm ♯ (s,k,c,sn)"      "atom sn ♯ (s,k,c)"
    shows "{ SeqConstP s k c }
           ⊢ c EQ Zero OR
             Ex m (Ex n (Ex sm (Ex sn (Var m IN k AND Var n IN k AND
                   SeqConstP s (Var m) (Var sm) AND
                   SeqConstP s (Var n) (Var sn) AND
                   c EQ Q_Eats (Var sm) (Var sn)))))"  (*<*)
proof -
  obtain l::name and sl::name where "atom l ♯ (s,k,c,sl,m,n,sm,sn)" "atom sl ♯ (s,k,c,m,n,sm,sn)"
    by (metis obtain_fresh)
  thus ?thesis using assms
    apply (simp add: SeqCTermP.simps [of l s k sl m n sm sn])
    apply (rule Conj_EH)+
    apply (rule All2_SUCC_E [THEN rotate2], auto del: Disj_EH)
    apply (rule cut_same [where A = "c EQ (Var sl)"])
    apply (metis Assume AssumeH(4) LstSeqP_EQ)
    apply (rule Disj_EH)
    apply (blast intro: Disj_I1 Sym Trans)
    ― ‹now the quantified case›
    apply (auto intro!: Disj_I2)
    apply (rule Ex_I [where x = "Var m"], simp)
    apply (rule Ex_I [where x = "Var n"], simp)
    apply (rule Ex_I [where x = "Var sm"], simp)
    apply (rule Ex_I [where x = "Var sn"], simp)
    apply (simp_all add: SeqCTermP.simps [of l s _ sl m n sm sn])
    apply ((rule Conj_I)+, blast intro: LstSeqP_Mem)+
    ― ‹first SeqCTermP subgoal›
    apply (rule All2_Subset [OF Hyp], blast)
    apply (blast intro!: SUCC_Subset_Ord LstSeqP_OrdP, blast, simp)
    ― ‹next SeqCTermP subgoal›
    apply ((rule Conj_I)+, blast intro: LstSeqP_Mem)+
    apply (rule All2_Subset [OF Hyp], blast)
    apply (blast intro!: SUCC_Subset_Ord LstSeqP_OrdP, blast, simp)
    ― ‹finally, the equality pair›
    apply (blast intro: Trans)
    done
qed (*>*)

lemma SeqConstP_imp_SubstTermP: "{SeqConstP s kk c, TermP t} ⊢ SubstTermP «Var w» t c c" (*<*)
proof -
  obtain j::name and k::name and l::name and sl::name and m::name and n::name and sm::name and sn::name
    where atoms: "atom j ♯ (s,kk,c,t,k,l,sl,m,n,sm,sn)"  "atom k ♯ (s,kk,c,t,l,sl,m,n,sm,sn)" 
                 "atom l ♯ (s,kk,c,t,sl,m,n,sm,sn)"   "atom sl ♯ (s,kk,c,t,m,n,sm,sn)"
                 "atom m ♯ (s,kk,c,t,n,sm,sn)"  "atom n ♯ (s,kk,c,t,sm,sn)" 
                 "atom sm ♯ (s,kk,c,t,sn)"      "atom sn ♯ (s,kk,c,t)"
    by (metis obtain_fresh)
  have "{ OrdP (Var k), TermP t } ⊢ All j (SeqConstP s (Var k) (Var j) IMP SubstTermP «Var w» t (Var j) (Var j))"
        (is "_ ⊢ ?scheme")
    proof (rule OrdIndH [where j=l])
      show "atom l ♯ (k, ?scheme)" using atoms
        by simp 
    next
      show "{TermP t} ⊢ All k (OrdP (Var k) IMP (All2 l (Var k) (?scheme(k::= Var l)) IMP ?scheme))"
        using atoms apply auto
        apply (rule Swap)
        apply (rule cut_same)
        apply (rule cut1 [OF SeqConstP_lemma [of m s "Var k" "Var j" n sm sn]], auto)
        ― ‹case 1, @{term Zero}›
        apply (rule Var_Eq_subst_Iff [THEN Iff_MP_same])
        apply (auto intro: SubstTermP_Zero [THEN cut1])
        ― ‹case 2, @{term Q_Eats}›
        apply (rule Var_Eq_subst_Iff [THEN Iff_MP_same, THEN rotate2], simp)
        apply (rule SubstTermP_Eats [THEN cut2])
        ― ‹First argument›
        apply (rule All2_E' [OF Hyp, where x="Var m"], blast+, simp_all)
        apply (force intro: All_E [where x="Var sm"])
        ― ‹Second argument›
        apply (rule All2_E' [OF Hyp, where x="Var n"], blast+, simp_all)
        apply (rule All_E [where x="Var sn"], auto)
        done
    qed
  hence "{OrdP (Var k), TermP t} ⊢ (SeqConstP s (Var k) (Var j) IMP SubstTermP «Var w» t (Var j) (Var j))(j::=c)"
    by (metis All_D)
  hence "{TermP t} ⊢ (SeqConstP s (Var k) c IMP SubstTermP «Var w» t c c)"
    using atoms by simp (metis Imp_cut SeqCTermP_imp_OrdP)
  hence "{TermP t} ⊢ (SeqConstP s (Var k) c IMP SubstTermP «Var w» t c c)(k::=kk)"
    using atoms by (force intro!: Subst)
  thus ?thesis
    using atoms by (simp add: anti_deduction) 
qed (*>*)

theorem SubstTermP_Const: "{ConstP c, TermP t} ⊢ SubstTermP «Var w» t c c"
proof -
  obtain s::name and k::name where "atom s ♯ (c,t,w,k)" "atom k ♯ (c,t,w)" 
    by (metis obtain_fresh)
  thus ?thesis
    by (auto simp: CTermP.simps [of k s c] SeqConstP_imp_SubstTermP)
qed


section ‹Substitution on Formulas›

subsection ‹Membership›

lemma SubstAtomicP_Mem: 
  "{SubstTermP v i x x', SubstTermP v i y y'} ⊢ SubstAtomicP v i (Q_Mem x y) (Q_Mem x' y')"
proof -
  obtain t::name and u::name and t'::name and u'::name 
    where "atom t ♯ (v,i,x,x',y,y',t',u,u')" "atom t' ♯ (v,i,x,x',y,y',u,u')"
          "atom u ♯ (v,i,x,x',y,y',u')" "atom u' ♯ (v,i,x,x',y,y')"
    by (metis obtain_fresh) 
  thus ?thesis
    apply (simp add: SubstAtomicP.simps [of t _ _ _ _ t' u u'])
    apply (rule Ex_I [where x = x], simp)
    apply (rule Ex_I [where x = y], simp)
    apply (rule Ex_I [where x = x'], simp)
    apply (rule Ex_I [where x = y'], auto intro: Disj_I2)
    done
qed

lemma SeqSubstFormP_Mem:
  assumes "atom s ♯ (k,x,y,x',y',v,i)" "atom k ♯ (x,y,x',y',v,i)"
    shows "{SubstTermP v i x x', SubstTermP v i y y'} 
           ⊢ Ex s (Ex k (SeqSubstFormP v i (Q_Mem x y) (Q_Mem x' y') (Var s) (Var k)))"
proof -
  let ?vs = "(s,k,x,y,x',y',v,i)"
  obtain l::name and sl::name and sl'::name and m::name and n::name and sm::name and sm'::name and sn::name and sn'::name
    where "atom l ♯ (?vs,sl,sl',m,n,sm,sm',sn,sn')"
          "atom sl ♯ (?vs,sl',m,n,sm,sm',sn,sn')" "atom sl' ♯ (?vs,m,n,sm,sm',sn,sn')"
          "atom m ♯ (?vs,n,sm,sm',sn,sn')" "atom n ♯ (?vs,sm,sm',sn,sn')"
          "atom sm ♯ (?vs,sm',sn,sn')" "atom sm' ♯ (?vs,sn,sn')"
          "atom sn ♯ (?vs,sn')" "atom sn' ♯ ?vs"
    by (metis obtain_fresh) 
  thus ?thesis
    using assms
    apply (auto simp: SeqSubstFormP.simps [of l "Var s" _ _ _ sl sl' m n sm sm' sn sn'])
    apply (rule Ex_I [where x = "Eats Zero (HPair Zero (HPair (Q_Mem x y) (Q_Mem x' y')))"], simp)
    apply (rule Ex_I [where x = Zero], auto intro!: Mem_SUCC_EH)
    apply (rule Ex_I [where x = "Q_Mem x y"], simp)
    apply (rule Ex_I [where x = "Q_Mem x' y'"], auto intro: Mem_Eats_I2 HPair_cong)
    apply (blast intro: SubstAtomicP_Mem [THEN cut2] Disj_I1)
    done
qed

lemma SubstFormP_Mem: 
  "{SubstTermP v i x x', SubstTermP v i y y'} ⊢ SubstFormP v i (Q_Mem x y) (Q_Mem x' y')"
proof -
  obtain k1::name and s1::name and k2::name and s2::name and k::name and s::name
    where "atom s1 ♯ (v,i,x,y,x',y')" "atom k1 ♯ (v,i,x,y,x',y',s1)"  
       "atom s2 ♯ (v,i,x,y,x',y',k1,s1)" "atom k2 ♯ (v,i,x,y,x',y',s2,k1,s1)"
       "atom s  ♯ (v,i,x,y,x',y',k2,s2,k1,s1)" "atom k  ♯ (v,i,x,y,x',y',s,k2,s2,k1,s1)" 
    by (metis obtain_fresh)
  thus ?thesis
    by (auto simp: SubstFormP.simps [of s v i "(Q_Mem x y)" _ k] 
                   SubstFormP.simps [of s1 v i x x' k1]  
                   SubstFormP.simps [of s2 v i y y' k2]
             intro: SubstTermP_imp_TermP SubstTermP_imp_VarP SeqSubstFormP_Mem thin1)
qed

subsection ‹Equality›

lemma SubstAtomicP_Eq:
  "{SubstTermP v i x x', SubstTermP v i y y'} ⊢ SubstAtomicP v i (Q_Eq x y) (Q_Eq x' y')"
proof -
  obtain t::name and u::name and t'::name  and u'::name 
    where "atom t ♯ (v,i,x,x',y,y',t',u,u')" "atom t' ♯ (v,i,x,x',y,y',u,u')"
          "atom u ♯ (v,i,x,x',y,y',u')" "atom u' ♯ (v,i,x,x',y,y')"
    by (metis obtain_fresh) 
  thus ?thesis
    apply (simp add: SubstAtomicP.simps [of t _ _ _ _ t' u u'])
    apply (rule Ex_I [where x = x], simp)
    apply (rule Ex_I [where x = y], simp)
    apply (rule Ex_I [where x = x'], simp)
    apply (rule Ex_I [where x = y'], auto intro: Disj_I1)
    done
qed

lemma SeqSubstFormP_Eq:
  assumes sk: "atom s ♯ (k,x,y,x',y',v,i)" "atom k ♯ (x,y,x',y',v,i)"
    shows "{SubstTermP v i x x', SubstTermP v i y y'} 
           ⊢ Ex s (Ex k (SeqSubstFormP v i (Q_Eq x y) (Q_Eq x' y') (Var s) (Var k)))"
proof -
  let ?vs = "(s,k,x,y,x',y',v,i)"
  obtain l::name and sl::name and sl'::name and m::name and n::name and sm::name and sm'::name and sn::name and sn'::name
    where "atom l ♯ (?vs,sl,sl',m,n,sm,sm',sn,sn')"
          "atom sl ♯ (?vs,sl',m,n,sm,sm',sn,sn')" "atom sl' ♯ (?vs,m,n,sm,sm',sn,sn')"
          "atom m ♯ (?vs,n,sm,sm',sn,sn')" "atom n ♯ (?vs,sm,sm',sn,sn')"
          "atom sm ♯ (?vs,sm',sn,sn')" "atom sm' ♯ (?vs,sn,sn')"
          "atom sn ♯ (?vs,sn')" "atom sn' ♯ ?vs"
    by (metis obtain_fresh) 
  thus ?thesis
    using sk
    apply (auto simp: SeqSubstFormP.simps [of l "Var s" _ _ _ sl sl' m n sm sm' sn sn'])
    apply (rule Ex_I [where x = "Eats Zero (HPair Zero (HPair (Q_Eq x y) (Q_Eq x' y')))"], simp)
    apply (rule Ex_I [where x = Zero], auto intro!: Mem_SUCC_EH)
    apply (rule Ex_I [where x = "Q_Eq x y"], simp)
    apply (rule Ex_I [where x = "Q_Eq x' y'"], auto)
    apply (metis Mem_Eats_I2 Assume HPair_cong Refl)
    apply (blast intro: SubstAtomicP_Eq [THEN cut2] Disj_I1)
    done
qed

lemma SubstFormP_Eq: 
  "{SubstTermP v i x x', SubstTermP v i y y'} ⊢ SubstFormP v i (Q_Eq x y) (Q_Eq x' y')"
proof -
  obtain k1::name and s1::name and k2::name and s2::name and k::name and s::name
    where "atom s1 ♯ (v,i,x,y,x',y')" "atom k1 ♯ (v,i,x,y,x',y',s1)"  
          "atom s2 ♯ (v,i,x,y,x',y',k1,s1)" "atom k2 ♯ (v,i,x,y,x',y',s2,k1,s1)"
          "atom s  ♯ (v,i,x,y,x',y',k2,s2,k1,s1)" "atom k  ♯ (v,i,x,y,x',y',s,k2,s2,k1,s1)" 
    by (metis obtain_fresh)
  thus ?thesis
    by (auto simp: SubstFormP.simps [of s v i "(Q_Eq x y)" _ k] 
                   SubstFormP.simps [of s1 v i x x' k1]  
                   SubstFormP.simps [of s2 v i y y' k2] 
             intro: SeqSubstFormP_Eq SubstTermP_imp_TermP SubstTermP_imp_VarP thin1)
qed

subsection ‹Negation›

lemma SeqSubstFormP_Neg:
  assumes "atom s ♯ (k,s1,k1,x,x',v,i)" "atom k ♯ (s1,k1,x,x',v,i)"
    shows "{SeqSubstFormP v i x x' s1 k1, TermP i, VarP v} 
           ⊢ Ex s (Ex k (SeqSubstFormP v i (Q_Neg x) (Q_Neg x') (Var s) (Var k)))" (*<*)
proof -
  let ?vs = "(s1,k1,s,k,x,x',v,i)"
  obtain l::name and sl::name and sl'::name and m::name and n::name and 
         sm::name and sm'::name and sn::name and sn'::name
    where atoms:
         "atom l ♯ (?vs,sl,sl',m,n,sm,sm',sn,sn')"
         "atom sl ♯ (?vs,sl',m,n,sm,sm',sn,sn')" "atom sl' ♯ (?vs,m,n,sm,sm',sn,sn')"
         "atom m ♯ (?vs,n,sm,sm',sn,sn')" "atom n ♯ (?vs,sm,sm',sn,sn')"
         "atom sm ♯ (?vs,sm',sn,sn')" "atom sm' ♯ (?vs,sn,sn')"
         "atom sn ♯ (?vs,sn')" "atom sn' ♯ ?vs"
    by (metis obtain_fresh) 
  let ?hyp = "{RestrictedP s1 (SUCC k1) (Var s), OrdP k1, SeqSubstFormP v i x x' s1 k1, TermP i, VarP v}"
  show ?thesis
     using assms atoms
     apply (auto simp: SeqSubstFormP.simps [of l "Var s" _ _ _ sl sl' m n sm sm' sn sn'])
     apply (rule cut_same [where A="OrdP k1"])
     apply (metis SeqSubstFormP_imp_OrdP thin2)
     apply (rule cut_same [OF exists_RestrictedP [of s s1 "SUCC k1"]])
     apply (rule AssumeH Ex_EH Conj_EH | simp)+
     apply (rule Ex_I [where x="Eats (Var s) (HPair (SUCC k1) (HPair (Q_Neg x) (Q_Neg x')))"])
     apply (simp_all (no_asm_simp))
     apply (rule Ex_I [where x="(SUCC k1)"])
     apply (simp add: flip_fresh_fresh)
     apply (rule Conj_I)
     apply (blast intro: RestrictedP_LstSeqP_Eats [THEN cut2] SeqSubstFormP_imp_LstSeqP [THEN cut1])
     proof (rule All2_SUCC_I, simp_all)
       show "?hyp ⊢ Ex sl (Ex sl'
              (HPair (SUCC k1) (HPair (Var sl) (Var sl')) IN Eats (Var s) (HPair (SUCC k1) (HPair (Q_Neg x) (Q_Neg x'))) AND
               (SubstAtomicP v i (Var sl) (Var sl') OR
                Ex m (Ex n
                   (Ex sm (Ex sm'
                       (Ex sn (Ex sn'
                       (Var m IN SUCC k1 AND
                        Var n IN SUCC k1 AND
                        HPair (Var m) (HPair (Var sm) (Var sm')) IN Eats (Var s) (HPair (SUCC k1) (HPair (Q_Neg x) (Q_Neg x'))) AND
                        HPair (Var n) (HPair (Var sn) (Var sn')) IN Eats (Var s) (HPair (SUCC k1) (HPair (Q_Neg x) (Q_Neg x'))) AND
                        (Var sl EQ Q_Disj (Var sm) (Var sn) AND Var sl' EQ Q_Disj (Var sm') (Var sn') OR
                          Var sl EQ Q_Neg (Var sm) AND Var sl' EQ Q_Neg (Var sm') OR Var sl EQ Q_Ex (Var sm) AND Var sl' EQ Q_Ex (Var sm')))))))))))"
       ― ‹verifying the final values›
       apply (rule Ex_I [where x="Q_Neg x"])
       using assms atoms apply simp
       apply (rule Ex_I [where x="Q_Neg x'"], simp)
       apply (rule Conj_I, metis Mem_Eats_I2 Refl)
       apply (rule Disj_I2)
       apply (rule Ex_I [where x=k1], simp)
       apply (rule Ex_I [where x=k1], simp)
       apply (rule Ex_I [where x=x], simp)
       apply (rule_tac x=x' in Ex_I, simp)
       apply (rule Ex_I [where x=x], simp)
       apply (rule_tac x=x' in Ex_I, simp)
       apply (rule Conj_I [OF Mem_SUCC_Refl])+
       apply (blast intro: Disj_I1 Disj_I2 Mem_Eats_I1 RestrictedP_Mem [THEN cut3] Mem_SUCC_Refl 
                     SeqSubstFormP_imp_LstSeqP [THEN cut1] LstSeqP_imp_Mem)
       done
     next
       show "?hyp ⊢ All2 l (SUCC k1)
                (Ex sl (Ex sl'
                    (HPair (Var l) (HPair (Var sl) (Var sl')) IN Eats (Var s) (HPair (SUCC k1) (HPair (Q_Neg x) (Q_Neg x'))) AND
                     (SubstAtomicP v i (Var sl) (Var sl') OR
                      Ex m (Ex n
                         (Ex sm (Ex sm'
                             (Ex sn (Ex sn'
                                 (Var m IN Var l AND
                                  Var n IN Var l AND
                                  HPair (Var m) (HPair (Var sm) (Var sm')) IN Eats (Var s) (HPair (SUCC k1) (HPair (Q_Neg x) (Q_Neg x'))) AND
                                  HPair (Var n) (HPair (Var sn) (Var sn')) IN Eats (Var s) (HPair (SUCC k1) (HPair (Q_Neg x) (Q_Neg x'))) AND
                                  (Var sl EQ Q_Disj (Var sm) (Var sn) AND Var sl' EQ Q_Disj (Var sm') (Var sn') OR
                            Var sl EQ Q_Neg (Var sm) AND Var sl' EQ Q_Neg (Var sm') OR Var sl EQ Q_Ex (Var sm) AND Var sl' EQ Q_Ex (Var sm'))))))))))))"
     ― ‹verifying the sequence buildup›
     apply (rule All_I Imp_I)+
     using assms atoms apply simp_all
     ― ‹... the sequence buildup via s1›
     apply (simp add: SeqSubstFormP.simps [of l s1 _ _ _ sl sl' m n sm sm' sn sn'])
     apply (rule AssumeH Ex_EH Conj_EH)+
     apply (rule All2_E [THEN rotate2], auto del: Disj_EH)
     apply (rule Ex_I [where x="Var sl"], simp)
     apply (rule Ex_I [where x="Var sl'"], simp)
     apply (rule Conj_I)
     apply (blast intro: Mem_Eats_I1 [OF RestrictedP_Mem [THEN cut3]] del: Disj_EH)
     apply (rule AssumeH Disj_IE1H Ex_EH Conj_EH)+
     apply (rule Ex_I [where x="Var m"], simp)
     apply (rule Ex_I [where x="Var n"], simp)
     apply (rule Ex_I [where x="Var sm"], simp)
     apply (rule Ex_I [where x="Var sm'"], simp)
     apply (rule Ex_I [where x="Var sn"], simp)
     apply (rule Ex_I [where x="Var sn'"], auto del: Disj_EH)
     apply (blast intro: Mem_Eats_I1 [OF RestrictedP_Mem [THEN cut3]] OrdP_Trans [OF OrdP_SUCC_I])+
     done
   qed
qed (*>*)

theorem SubstFormP_Neg: "{SubstFormP v i x x'} ⊢ SubstFormP v i (Q_Neg x) (Q_Neg x')"
proof -
  obtain k1::name and s1::name and k::name and s::name
    where "atom s1 ♯ (v,i,x,x')"        "atom k1 ♯ (v,i,x,x',s1)"  
          "atom s  ♯ (v,i,x,x',k1,s1)"  "atom k  ♯ (v,i,x,x',s,k1,s1)" 
     by (metis obtain_fresh)
   thus ?thesis
     by (force simp: SubstFormP.simps [of s v i "Q_Neg x" _ k] SubstFormP.simps [of s1 v i x x' k1] 
               intro: SeqSubstFormP_Neg [THEN cut3])
qed

subsection ‹Disjunction›

lemma SeqSubstFormP_Disj:
  assumes "atom s ♯ (k,s1,s2,k1,k2,x,y,x',y',v,i)" "atom k ♯ (s1,s2,k1,k2,x,y,x',y',v,i)"
    shows "{SeqSubstFormP v i x x' s1 k1, 
            SeqSubstFormP v i y y' s2 k2, TermP i, VarP v} 
           ⊢ Ex s (Ex k (SeqSubstFormP v i (Q_Disj x y) (Q_Disj x' y') (Var s) (Var k)))" (*<*)
proof -
  let ?vs = "(s1,s2,s,k1,k2,k,x,y,x',y',v,i)"
  obtain km::name and kn::name and j::name and k'::name 
     and l::name and sl::name and sl'::name and m::name and n::name  
     and sm::name and sm'::name and sn::name and sn'::name
    where atoms2: "atom km ♯ (kn,j,k',l,s1,s2,s,k1,k2,k,x,y,x',y',v,i,sl,sl',m,n,sm,sm',sn,sn')"
         "atom kn ♯ (j,k',l,s1,s2,s,k1,k2,k,x,y,x',y',v,i,sl,sl',m,n,sm,sm',sn,sn')"
         "atom j ♯ (k',l,s1,s2,s,k1,k2,k,x,y,x',y',v,i,sl,sl',m,n,sm,sm',sn,sn')"
     and atoms: "atom k' ♯ (l,s1,s2,s,k1,k2,k,x,y,x',y',v,i,sl,sl',m,n,sm,sm',sn,sn')" 
         "atom l ♯ (s1,s2,s,k1,k2,k,x,y,x',y',v,i,sl,sl',m,n,sm,sm',sn,sn')"
         "atom sl ♯ (s1,s2,s,k1,k2,k,x,y,x',y',v,i,sl',m,n,sm,sm',sn,sn')" 
         "atom sl' ♯ (s1,s2,s,k1,k2,k,x,y,x',y',v,i,m,n,sm,sm',sn,sn')"
         "atom m ♯ (s1,s2,s,k1,k2,k,x,y,x',y',v,i,n,sm,sm',sn,sn')" 
         "atom n ♯ (s1,s2,s,k1,k2,k,x,y,x',y',v,i,sm,sm',sn,sn')"
         "atom sm ♯ (s1,s2,s,k1,k2,k,x,y,x',y',v,i,sm',sn,sn')" 
         "atom sm' ♯ (s1,s2,s,k1,k2,k,x,y,x',y',v,i,sn,sn')"
         "atom sn ♯ (s1,s2,s,k1,k2,k,x,y,x',y',v,i,sn')" 
         "atom sn' ♯ (s1,s2,s,k1,k2,k,x,y,x',y',v,i)"
    by (metis obtain_fresh) 
  let ?hyp = "{HaddP k1 k2 (Var k'), OrdP k1, OrdP k2, SeqAppendP s1 (SUCC k1) s2 (SUCC k2) (Var s),
               SeqSubstFormP v i x x' s1 k1, SeqSubstFormP v i y y' s2 k2, TermP i, VarP v}"
  show ?thesis
     using assms atoms
     apply (auto simp: SeqSubstFormP.simps [of l "Var s" _ _ _ sl sl' m n sm sm' sn sn'])
     apply (rule cut_same [where A="OrdP k1 AND OrdP k2"])
     apply (metis Conj_I SeqSubstFormP_imp_OrdP thin1 thin2)
     apply (rule cut_same [OF exists_SeqAppendP [of s s1 "SUCC k1" s2 "SUCC k2"]])
     apply (rule AssumeH Ex_EH Conj_EH | simp)+
     apply (rule cut_same [OF exists_HaddP [where j=k' and x=k1 and y=k2]])
     apply (rule AssumeH Ex_EH Conj_EH | simp)+
     apply (rule Ex_I [where x="Eats (Var s) (HPair (SUCC(SUCC(Var k'))) (HPair(Q_Disj x y)(Q_Disj x' y')))"])
     apply (simp_all (no_asm_simp))
     apply (rule Ex_I [where x="SUCC (SUCC (Var k'))"], simp)
     apply (rule Conj_I)
     apply (blast intro: LstSeqP_SeqAppendP_Eats SeqSubstFormP_imp_LstSeqP [THEN cut1])
     proof (rule All2_SUCC_I, simp_all)
       show "?hyp ⊢ Ex sl (Ex sl'
                 (HPair (SUCC (SUCC (Var k'))) (HPair (Var sl) (Var sl')) IN
                  Eats (Var s) (HPair (SUCC (SUCC (Var k'))) (HPair (Q_Disj x y) (Q_Disj x' y'))) AND
                  (SubstAtomicP v i (Var sl) (Var sl') OR
                   Ex m (Ex n (Ex sm (Ex sm' (Ex sn (Ex sn'
                      (Var m IN SUCC (SUCC (Var k')) AND
                       Var n IN SUCC (SUCC (Var k')) AND
                       HPair (Var m) (HPair (Var sm) (Var sm')) IN
                       Eats (Var s) (HPair (SUCC (SUCC (Var k'))) (HPair (Q_Disj x y) (Q_Disj x' y'))) AND
                       HPair (Var n) (HPair (Var sn) (Var sn')) IN
                       Eats (Var s) (HPair (SUCC (SUCC (Var k'))) (HPair (Q_Disj x y) (Q_Disj x' y'))) AND
                       (Var sl EQ Q_Disj (Var sm) (Var sn) AND Var sl' EQ Q_Disj (Var sm') (Var sn') OR
                          Var sl EQ Q_Neg (Var sm) AND Var sl' EQ Q_Neg (Var sm') OR Var sl EQ Q_Ex (Var sm) AND Var sl' EQ Q_Ex (Var sm')))))))))))"
       ― ‹verifying the final values›
       apply (rule Ex_I [where x="Q_Disj x y"])
       using assms atoms apply simp
       apply (rule Ex_I [where x="Q_Disj x' y'"], simp)
       apply (rule Conj_I, metis Mem_Eats_I2 Refl)
       apply (rule Disj_I2)
       apply (rule Ex_I [where x=k1], simp)
       apply (rule Ex_I [where x="SUCC (Var k')"], simp)
       apply (rule Ex_I [where x=x], simp)
       apply (rule_tac x=x' in Ex_I, simp)
       apply (rule Ex_I [where x=y], simp)
       apply (rule_tac x=y' in Ex_I, simp)
       apply (rule Conj_I)
       apply (blast intro: HaddP_Mem_I LstSeqP_OrdP Mem_SUCC_I1)
       apply (rule Conj_I [OF Mem_SUCC_Refl])
       apply (blast intro: Disj_I1 Mem_Eats_I1 Mem_SUCC_Refl SeqSubstFormP_imp_LstSeqP [THEN cut1] 
           LstSeqP_imp_Mem SeqAppendP_Mem1 [THEN cut3] SeqAppendP_Mem2 [THEN cut4] HaddP_SUCC1 [THEN cut1])
       done
     next
       show "?hyp ⊢  All2 l (SUCC (SUCC (Var k')))
     (Ex sl
       (Ex sl'
         (HPair (Var l) (HPair (Var sl) (Var sl')) IN
          Eats (Var s) (HPair (SUCC (SUCC (Var k'))) (HPair (Q_Disj x y) (Q_Disj x' y'))) AND
          (SubstAtomicP v i (Var sl) (Var sl') OR
           Ex m (Ex n
              (Ex sm (Ex sm'
                  (Ex sn (Ex sn'
                      (Var m IN Var l AND
                       Var n IN Var l AND
                       HPair (Var m) (HPair (Var sm) (Var sm')) IN
                       Eats (Var s) (HPair (SUCC (SUCC (Var k'))) (HPair (Q_Disj x y) (Q_Disj x' y'))) AND
                       HPair (Var n) (HPair (Var sn) (Var sn')) IN
                       Eats (Var s) (HPair (SUCC (SUCC (Var k'))) (HPair (Q_Disj x y) (Q_Disj x' y'))) AND
                       (Var sl EQ Q_Disj (Var sm) (Var sn) AND Var sl' EQ Q_Disj (Var sm') (Var sn') OR
                            Var sl EQ Q_Neg (Var sm) AND Var sl' EQ Q_Neg (Var sm') OR Var sl EQ Q_Ex (Var sm) AND Var sl' EQ Q_Ex (Var sm'))))))))))))"
     ― ‹verifying the sequence buildup›
     apply (rule cut_same [where A="HaddP (SUCC k1) (SUCC k2) (SUCC (SUCC (Var k')))"])
     apply (blast intro: HaddP_SUCC1 [THEN cut1] HaddP_SUCC2 [THEN cut1])
     apply (rule All_I Imp_I)+
     apply (rule HaddP_Mem_cases [where i=j])
     using assms atoms atoms2 apply simp_all
     apply (rule AssumeH)
     apply (blast intro: OrdP_SUCC_I LstSeqP_OrdP)
     ― ‹... the sequence buildup via s1›
     apply (simp add: SeqSubstFormP.simps [of l s1 _ _ _ sl sl' m n sm sm' sn sn'])
     apply (rule AssumeH Ex_EH Conj_EH)+
     apply (rule All2_E [THEN rotate2])
     apply (simp | rule AssumeH Ex_EH Conj_EH)+
     apply (rule Ex_I [where x="Var sl"], simp)
     apply (rule Ex_I [where x="Var sl'"], simp)
     apply (rule Conj_I [OF Mem_Eats_I1])
     apply (metis SeqAppendP_Mem1 rotate3 thin2 thin4)
     apply (rule AssumeH Disj_IE1H Ex_EH Conj_EH)+
     apply (rule Ex_I [where x="Var m"], simp)
     apply (rule Ex_I [where x="Var n"], simp)
     apply (rule Ex_I [where x="Var sm"], simp)
     apply (rule Ex_I [where x="Var sm'"], simp)
     apply (rule Ex_I [where x="Var sn"], simp)
     apply (rule Ex_I [where x="Var sn'"], simp_all (no_asm_simp))
     apply (rule Conj_I, rule AssumeH)+
     apply (rule Conj_I)
     apply (blast intro: OrdP_Trans [OF OrdP_SUCC_I] Mem_Eats_I1 [OF SeqAppendP_Mem1 [THEN cut3]] Hyp)
     apply (blast intro: Disj_I1 Disj_I2 OrdP_Trans [OF OrdP_SUCC_I] Mem_Eats_I1 [OF SeqAppendP_Mem1 [THEN cut3]] Hyp)
     ― ‹... the sequence buildup via s2›
     apply (simp add: SeqSubstFormP.simps [of l s2 _ _ _ sl sl' m n sm sm' sn sn'])
     apply (rule AssumeH Ex_EH Conj_EH)+
     apply (rule All2_E [THEN rotate2])
     apply (simp | rule AssumeH Ex_EH Conj_EH)+
     apply (rule Ex_I [where x="Var sl"], simp)
     apply (rule Ex_I [where x="Var sl'"], simp)
     apply (rule cut_same [where A="OrdP (Var j)"])
     apply (metis HaddP_imp_OrdP rotate2 thin2)
     apply (rule Conj_I)
     apply (blast intro: Mem_Eats_I1 SeqAppendP_Mem2 [THEN cut4] del: Disj_EH)
     apply (rule AssumeH Disj_IE1H Ex_EH Conj_EH)+
     apply (rule cut_same [OF exists_HaddP [where j=km and x="SUCC k1" and y="Var m"]])
     apply (blast intro: Ord_IN_Ord, simp)
     apply (rule cut_same [OF exists_HaddP [where j=kn and x="SUCC k1" and y="Var n"]])
     apply (metis AssumeH(6) Ord_IN_Ord0 rotate8, simp)
     apply (rule AssumeH Ex_EH Conj_EH | simp)+
     apply (rule Ex_I [where x="Var km"], simp)
     apply (rule Ex_I [where x="Var kn"], simp)
     apply (rule Ex_I [where x="Var sm"], simp)
     apply (rule Ex_I [where x="Var sm'"], simp)
     apply (rule Ex_I [where x="Var sn"], simp)
     apply (rule Ex_I [where x="Var sn'"], simp_all (no_asm_simp))
     apply (rule Conj_I [OF _ Conj_I])
     apply (blast intro!: HaddP_Mem_cancel_left [THEN Iff_MP2_same] OrdP_SUCC_I intro: LstSeqP_OrdP Hyp)+
     apply (blast del: Disj_EH  intro: OrdP_Trans Hyp 
                  intro!: Mem_Eats_I1 SeqAppendP_Mem2 [THEN cut4] HaddP_imp_OrdP [THEN cut1])
     done
   qed
qed (*>*)

theorem SubstFormP_Disj: 
  "{SubstFormP v i x x', SubstFormP v i y y'} ⊢ SubstFormP v i (Q_Disj x y) (Q_Disj x' y')"
proof -
  obtain k1::name and s1::name and k2::name and s2::name and k::name and s::name
    where "atom s1 ♯ (v,i,x,y,x',y')"        "atom k1 ♯ (v,i,x,y,x',y',s1)"  
          "atom s2 ♯ (v,i,x,y,x',y',k1,s1)"  "atom k2 ♯ (v,i,x,y,x',y',s2,k1,s1)"
          "atom s  ♯ (v,i,x,y,x',y',k2,s2,k1,s1)" "atom k  ♯ (v,i,x,y,x',y',s,k2,s2,k1,s1)" 
    by (metis obtain_fresh)
   thus ?thesis
     by (force simp: SubstFormP.simps [of s v i "Q_Disj x y" _ k] 
                     SubstFormP.simps [of s1 v i x x' k1]  
                     SubstFormP.simps [of s2 v i y y' k2]
               intro: SeqSubstFormP_Disj [THEN cut4])
qed

subsection ‹Existential›

lemma SeqSubstFormP_Ex:
  assumes "atom s ♯ (k,s1,k1,x,x',v,i)" "atom k ♯ (s1,k1,x,x',v,i)"
    shows "{SeqSubstFormP v i x x' s1 k1, TermP i, VarP v} 
           ⊢ Ex s (Ex k (SeqSubstFormP v i (Q_Ex x) (Q_Ex x') (Var s) (Var k)))" (*<*)
proof -
  obtain l::name and sl::name and sl'::name and m::name and n::name
     and sm::name and sm'::name and sn::name and sn'::name
    where atoms:
         "atom l ♯ (s1,k1,s,k,x,x',v,i,sl,sl',m,n,sm,sm',sn,sn')"
         "atom sl ♯ (s1,k1,s,k,x,x',v,i,sl',m,n,sm,sm',sn,sn')" 
         "atom sl' ♯ (s1,k1,s,k,x,x',v,i,m,n,sm,sm',sn,sn')"
         "atom m ♯ (s1,k1,s,k,x,x',v,i,n,sm,sm',sn,sn')" 
         "atom n ♯ (s1,k1,s,k,x,x',v,i,sm,sm',sn,sn')"
         "atom sm ♯ (s1,k1,s,k,x,x',v,i,sm',sn,sn')" 
         "atom sm' ♯ (s1,k1,s,k,x,x',v,i,sn,sn')"
         "atom sn ♯ (s1,k1,s,k,x,x',v,i,sn')" 
         "atom sn' ♯ (s1,k1,s,k,x,x',v,i)"
    by (metis obtain_fresh) 
  let ?hyp = "{RestrictedP s1 (SUCC k1) (Var s), OrdP k1, SeqSubstFormP v i x x' s1 k1, TermP i, VarP v}"
  show ?thesis
     using assms atoms
     apply (auto simp: SeqSubstFormP.simps [of l "Var s" _ _ _ sl sl' m n sm sm' sn sn'])
     apply (rule cut_same [where A="OrdP k1"])
     apply (metis SeqSubstFormP_imp_OrdP thin2)
     apply (rule cut_same [OF exists_RestrictedP [of s s1 "SUCC k1"]])
     apply (rule AssumeH Ex_EH Conj_EH | simp)+
     apply (rule Ex_I [where x="Eats (Var s) (HPair (SUCC k1) (HPair (Q_Ex x) (Q_Ex x')))"], simp)
     apply (rule Ex_I [where x="(SUCC k1)"], simp)
     apply (rule Conj_I)
     apply (blast intro: RestrictedP_LstSeqP_Eats [THEN cut2] SeqSubstFormP_imp_LstSeqP [THEN cut1])
     proof (rule All2_SUCC_I, simp_all)
       show "?hyp ⊢ Ex sl (Ex sl'
          (HPair (SUCC k1) (HPair (Var sl) (Var sl')) IN Eats (Var s) (HPair (SUCC k1) (HPair (Q_Ex x) (Q_Ex x'))) AND
           (SubstAtomicP v i (Var sl) (Var sl') OR
            Ex m (Ex n
               (Ex sm (Ex sm'
                   (Ex sn (Ex sn'
                       (Var m IN SUCC k1 AND
                        Var n IN SUCC k1 AND
                        HPair (Var m) (HPair (Var sm) (Var sm')) IN Eats (Var s) (HPair (SUCC k1) (HPair (Q_Ex x) (Q_Ex x'))) AND
                        HPair (Var n) (HPair (Var sn) (Var sn')) IN Eats (Var s) (HPair (SUCC k1) (HPair (Q_Ex x) (Q_Ex x'))) AND
                        (Var sl EQ Q_Disj (Var sm) (Var sn) AND Var sl' EQ Q_Disj (Var sm') (Var sn') OR
                          Var sl EQ Q_Neg (Var sm) AND Var sl' EQ Q_Neg (Var sm') OR Var sl EQ Q_Ex (Var sm) AND Var sl' EQ Q_Ex (Var sm')))))))))))"
       ― ‹verifying the final values›
       apply (rule Ex_I [where x="Q_Ex x"])
       using assms atoms apply simp
       apply (rule Ex_I [where x="Q_Ex x'"], simp)
       apply (rule Conj_I, metis Mem_Eats_I2 Refl)
       apply (rule Disj_I2)
       apply (rule Ex_I [where x=k1], simp)
       apply (rule Ex_I [where x=k1], simp)
       apply (rule Ex_I [where x=x], simp)
       apply (rule_tac x=x' in Ex_I, simp)
       apply (rule Ex_I [where x=x], simp)
       apply (rule_tac x=x' in Ex_I, simp)
       apply (rule Conj_I [OF Mem_SUCC_Refl])+
       apply (blast intro: Disj_I2 Mem_Eats_I1 RestrictedP_Mem [THEN cut3] Mem_SUCC_Refl 
                      SeqSubstFormP_imp_LstSeqP [THEN cut1] LstSeqP_imp_Mem)
       done
     next
       show "?hyp 
             ⊢ All2 l (SUCC k1)
                (Ex sl (Ex sl'
                    (HPair (Var l) (HPair (Var sl) (Var sl')) IN Eats (Var s) (HPair (SUCC k1) (HPair (Q_Ex x) (Q_Ex x'))) AND
                     (SubstAtomicP v i (Var sl) (Var sl') OR
                      Ex m (Ex n
                         (Ex sm (Ex sm'
                             (Ex sn (Ex sn'
                                 (Var m IN Var l AND
                                  Var n IN Var l AND
                                  HPair (Var m) (HPair (Var sm) (Var sm')) IN Eats (Var s) (HPair (SUCC k1) (HPair (Q_Ex x) (Q_Ex x'))) AND
                                  HPair (Var n) (HPair (Var sn) (Var sn')) IN Eats (Var s) (HPair (SUCC k1) (HPair (Q_Ex x) (Q_Ex x'))) AND
                                  (Var sl EQ Q_Disj (Var sm) (Var sn) AND Var sl' EQ Q_Disj (Var sm') (Var sn') OR
                            Var sl EQ Q_Neg (Var sm) AND Var sl' EQ Q_Neg (Var sm') OR Var sl EQ Q_Ex (Var sm) AND Var sl' EQ Q_Ex (Var sm'))))))))))))"
     ― ‹verifying the sequence buildup›
     using assms atoms 
     ― ‹... the sequence buildup via s1›
     apply (auto simp add: SeqSubstFormP.simps [of l s1 _ _ _ sl sl' m n sm sm' sn sn'])
     apply (rule Swap)
     apply (rule All2_E, auto del: Disj_EH)
     apply (rule Ex_I [where x="Var sl"], simp)
     apply (rule Ex_I [where x="Var sl'"], simp)
     apply (rule Conj_I)
     apply (blast intro: Mem_Eats_I1 [OF RestrictedP_Mem [THEN cut3]] del: Disj_EH)
     apply (rule AssumeH Disj_IE1H Ex_EH Conj_EH)+
     apply (rule Ex_I [where x="Var m"], simp)
     apply (rule Ex_I [where x="Var n"], simp)
     apply (rule Ex_I [where x="Var sm"], simp)
     apply (rule Ex_I [where x="Var sm'"], simp)
     apply (rule Ex_I [where x="Var sn"], simp)
     apply (rule Ex_I [where x="Var sn'"])
     apply (auto intro: Mem_Eats_I1 [OF RestrictedP_Mem [THEN cut3]] OrdP_Trans [OF OrdP_SUCC_I] del: Disj_EH)
     done
   qed
qed (*>*)

theorem SubstFormP_Ex: "{SubstFormP v i x x'} ⊢ SubstFormP v i (Q_Ex x) (Q_Ex x')"
proof -
  obtain k1::name and s1::name and k::name and s::name
    where "atom s1 ♯ (v,i,x,x')"        "atom k1 ♯ (v,i,x,x',s1)"  
          "atom s  ♯ (v,i,x,x',k1,s1)"  "atom k  ♯ (v,i,x,x',s,k1,s1)" 
     by (metis obtain_fresh)
   thus ?thesis
     by (force simp: SubstFormP.simps [of s v i "Q_Ex x" _ k] SubstFormP.simps [of s1 v i x x' k1] 
               intro: SeqSubstFormP_Ex [THEN cut3])
qed


section ‹Constant Terms›

lemma ConstP_Zero: "{} ⊢ ConstP Zero"
  by (auto intro: Sigma_fm_imp_thm [OF CTermP_sf] simp: Const_0 ground_fm_aux_def supp_conv_fresh)

lemma SeqConstP_Eats:
  assumes "atom s ♯ (k,s1,s2,k1,k2,t1,t2)" "atom k ♯ (s1,s2,k1,k2,t1,t2)"
    shows "{SeqConstP s1 k1 t1, SeqConstP s2 k2 t2}
           ⊢ Ex s (Ex k (SeqConstP (Var s) (Var k) (Q_Eats t1 t2)))" (*<*)
proof -
  obtain km::name and kn::name and j::name and k'::name 
     and l::name and sl::name and m::name and n::name and sm::name and sn::name
    where atoms:
         "atom km ♯ (kn,j,k',l,s1,s2,s,k1,k2,k,t1,t2,sl,m,n,sm,sn)"
         "atom kn ♯ (j,k',l,s1,s2,s,k1,k2,k,t1,t2,sl,m,n,sm,sn)"
         "atom j ♯ (k',l,s1,s2,s,k1,k2,k,t1,t2,sl,m,n,sm,sn)" 
         "atom k' ♯ (l,s1,s2,s,k1,k2,k,t1,t2,sl,m,n,sm,sn)"
         "atom l ♯ (s1,s2,s,k1,k2,k,t1,t2,sl,m,n,sm,sn)" 
         "atom sl ♯ (s1,s2,s,k1,k2,k,t1,t2,m,n,sm,sn)"
         "atom m ♯ (s1,s2,s,k1,k2,k,t1,t2,n,sm,sn)" 
         "atom n ♯ (s1,s2,s,k1,k2,k,t1,t2,sm,sn)"
         "atom sm ♯ (s1,s2,s,k1,k2,k,t1,t2,sn)" 
         "atom sn ♯ (s1,s2,s,k1,k2,k,t1,t2)"
    by (metis obtain_fresh) 
  let ?hyp = "{HaddP k1 k2 (Var k'), OrdP k1, OrdP k2, SeqAppendP s1 (SUCC k1) s2 (SUCC k2) (Var s), 
              SeqConstP s1 k1 t1, SeqConstP s2 k2 t2}"
  show ?thesis
     using assms atoms
     apply (auto simp: SeqCTermP.simps [of l "Var s" _ sl m n sm sn])
     apply (rule cut_same [where A="OrdP k1 AND OrdP k2"])
     apply (metis Conj_I SeqCTermP_imp_OrdP thin1 thin2)
     apply (rule cut_same [OF exists_SeqAppendP [of s s1 "SUCC k1" s2 "SUCC k2"]])
     apply (rule AssumeH Ex_EH Conj_EH | simp)+
     apply (rule cut_same [OF exists_HaddP [where j=k' and x=k1 and y=k2]])
     apply (rule AssumeH Ex_EH Conj_EH | simp)+
     apply (rule Ex_I [where x="Eats (Var s) (HPair (SUCC (SUCC (Var k'))) (Q_Eats t1 t2))"], simp)
     apply (rule Ex_I [where x="SUCC (SUCC (Var k'))"], simp)
     apply (rule Conj_I)
     apply (blast intro: LstSeqP_SeqAppendP_Eats SeqCTermP_imp_LstSeqP [THEN cut1])
     proof (rule All2_SUCC_I, simp_all)
       show "?hyp ⊢ Ex sl (HPair (SUCC (SUCC (Var k'))) (Var sl) IN Eats (Var s) 
                          (HPair (SUCC (SUCC (Var k'))) (Q_Eats t1 t2))   AND
                (Var sl EQ Zero OR Fls OR
                 Ex m (Ex n(Ex sm (Ex sn
                      (Var m IN SUCC (SUCC (Var k')) AND
                       Var n IN SUCC (SUCC (Var k')) AND
                       HPair (Var m) (Var sm) IN Eats (Var s) (HPair (SUCC (SUCC (Var k'))) (Q_Eats t1 t2)) AND
                       HPair (Var n) (Var sn) IN Eats (Var s) (HPair (SUCC (SUCC (Var k'))) (Q_Eats t1 t2)) AND
                       Var sl EQ Q_Eats (Var sm) (Var sn)))))))"
       ― ‹verifying the final values›
       apply (rule Ex_I [where x="Q_Eats t1 t2"])
       using assms atoms apply simp
       apply (rule Conj_I, metis Mem_Eats_I2 Refl)
       apply (rule Disj_I2)+
       apply (rule Ex_I [where x=k1], simp)
       apply (rule Ex_I [where x="SUCC (Var k')"], simp)
       apply (rule Ex_I [where x=t1], simp)
       apply (rule Ex_I [where x=t2], simp)
       apply (rule Conj_I)
       apply (blast intro: HaddP_Mem_I LstSeqP_OrdP Mem_SUCC_I1)
       apply (blast intro: Mem_Eats_I1 SeqAppendP_Mem1 [THEN cut3] SeqAppendP_Mem2 [THEN cut4]
                 Mem_SUCC_Refl SeqCTermP_imp_LstSeqP [THEN cut1] LstSeqP_imp_Mem HaddP_SUCC1 [THEN cut1])
       done
     next
       show "?hyp ⊢ All2 l (SUCC (SUCC (Var k')))
                 (Ex sl
                   (HPair (Var l) (Var sl) IN Eats (Var s) (HPair (SUCC (SUCC (Var k'))) (Q_Eats t1 t2)) AND
                    (Var sl EQ Zero OR Fls OR
                     Ex m (Ex n (Ex sm (Ex sn
                          (Var m IN Var l AND
                           Var n IN Var l AND
                           HPair (Var m) (Var sm) IN Eats (Var s) (HPair (SUCC (SUCC (Var k'))) (Q_Eats t1 t2)) AND
                           HPair (Var n) (Var sn) IN Eats (Var s) (HPair (SUCC (SUCC (Var k'))) (Q_Eats t1 t2)) AND
                           Var sl EQ Q_Eats (Var sm) (Var sn))))))))"
     ― ‹verifying the sequence buildup›
     apply (rule cut_same [where A="HaddP (SUCC k1) (SUCC k2) (SUCC (SUCC (Var k')))"])
     apply (blast intro: HaddP_SUCC1 [THEN cut1] HaddP_SUCC2 [THEN cut1])
     apply (rule All_I Imp_I)+
     apply (rule HaddP_Mem_cases [where i=j])
     using assms atoms apply simp_all
     apply (rule AssumeH)
     apply (blast intro: OrdP_SUCC_I LstSeqP_OrdP)
     ― ‹... the sequence buildup via s1›
     apply (simp add: SeqCTermP.simps [of l s1 _ sl m n sm sn])
     apply (rule AssumeH Ex_EH Conj_EH)+
     apply (rule All2_E [THEN rotate2], auto del: Disj_EH)
     apply (rule Ex_I [where x="Var sl"], simp)
     apply (rule Conj_I)
     apply (rule Mem_Eats_I1)
     apply (metis SeqAppendP_Mem1 rotate3 thin2 thin4)
     apply (rule AssumeH Disj_IE1H Ex_EH Conj_EH)+
     apply simp_all
     apply (rule Ex_I [where x="Var m"], simp)
     apply (rule Ex_I [where x="Var n"], simp)
     apply (rule Ex_I [where x="Var sm"], simp)
     apply (rule Ex_I [where x="Var sn"], simp)
     apply (rule Conj_I, rule AssumeH)+
     apply (blast del: Disj_EH intro: OrdP_Trans [OF OrdP_SUCC_I] Mem_Eats_I1 [OF SeqAppendP_Mem1 [THEN cut3]] Hyp)
     ― ‹... the sequence buildup via s2›
     apply (simp add: SeqCTermP.simps [of l s2 _ sl m n sm sn])
     apply (rule AssumeH Ex_EH Conj_EH)+
     apply (rule All2_E [THEN rotate2], auto del: Disj_EH)
     apply (rule Ex_I [where x="Var sl"], simp)
     apply (rule cut_same [where A="OrdP (Var j)"])
     apply (metis HaddP_imp_OrdP rotate2 thin2)
     apply (rule Conj_I)
     apply (blast intro: Mem_Eats_I1 SeqAppendP_Mem2 [THEN cut4] del: Disj_EH)
     apply (rule AssumeH Disj_IE1H Ex_EH Conj_EH)+
     apply (rule cut_same [OF exists_HaddP [where j=km and x="SUCC k1" and y="Var m"]])
     apply (blast intro: Ord_IN_Ord, simp)
     apply (rule cut_same [OF exists_HaddP [where j=kn and x="SUCC k1" and y="Var n"]])
     apply (metis AssumeH(6) Ord_IN_Ord0 rotate8, simp)
     apply (rule AssumeH Ex_EH Conj_EH | simp)+
     apply (rule Ex_I [where x="Var km"], simp)
     apply (rule Ex_I [where x="Var kn"], simp)
     apply (rule Ex_I [where x="Var sm"], simp)
     apply (rule Ex_I [where x="Var sn"], simp_all)
     apply (rule Conj_I [OF _ Conj_I])
     apply (blast intro!: HaddP_Mem_cancel_left [THEN Iff_MP2_same] OrdP_SUCC_I intro: LstSeqP_OrdP Hyp)+
     apply (blast del: Disj_EH  intro: OrdP_Trans Hyp 
                  intro!: Mem_Eats_I1 SeqAppendP_Mem2 [THEN cut4] HaddP_imp_OrdP [THEN cut1])
     done
   qed
qed (*>*)

theorem ConstP_Eats: "{ConstP t1, ConstP t2} ⊢ ConstP (Q_Eats t1 t2)"
proof -
  obtain k1::name and s1::name and k2::name and s2::name and k::name and s::name
    where "atom s1 ♯ (t1,t2)" "atom k1 ♯ (t1,t2,s1)"  
          "atom s2 ♯ (t1,t2,k1,s1)" "atom k2 ♯ (t1,t2,s2,k1,s1)"
          "atom s  ♯ (t1,t2,k2,s2,k1,s1)" "atom k  ♯ (t1,t2,s,k2,s2,k1,s1)" 
    by (metis obtain_fresh)
   thus ?thesis
     by (auto simp: CTermP.simps [of k s "(Q_Eats t1 t2)"] 
                    CTermP.simps [of k1 s1 t1]  CTermP.simps [of k2 s2 t2]
              intro!:  SeqConstP_Eats [THEN cut2])
qed


section ‹Proofs›

lemma PrfP_inference:
  assumes "atom s ♯ (k,s1,s2,k1,k2,α1,α2,β)" "atom k ♯ (s1,s2,k1,k2,α1,α2,β)"
    shows "{PrfP s1 k1 α1, PrfP s2 k2 α2, ModPonP α1 α2 β OR ExistsP α1 β OR SubstP α1 β} 
           ⊢ Ex k (Ex s (PrfP (Var s) (Var k) β))" (*<*)
proof -
  obtain km::name and kn::name and j::name and k'::name 
     and l::name and sl::name and m::name and n::name and sm::name and sn::name
    where atoms:
         "atom km ♯ (kn,j,k',l,s1,s2,s,k1,k2,k,α1,α2,β,sl,m,n,sm,sn)"
         "atom kn ♯ (j,k',l,s1,s2,s,k1,k2,k,α1,α2,β,sl,m,n,sm,sn)"
         "atom j ♯ (k',l,s1,s2,s,k1,k2,k,α1,α2,β,sl,m,n,sm,sn)"
         "atom k' ♯ (l,s1,s2,s,k1,k2,k,α1,α2,β,sl,m,n,sm,sn)" 
         "atom l ♯ (s1,s2,s,k1,k2,k,α1,α2,β,sl,m,n,sm,sn)"
         "atom sl ♯ (s1,s2,s,k1,k2,k,α1,α2,β,m,n,sm,sn)" 
         "atom m ♯ (s1,s2,s,k1,k2,k,α1,α2,β,n,sm,sn)" 
         "atom n ♯ (s1,s2,s,k1,k2,k,α1,α2,β,sm,sn)" 
         "atom sm ♯ (s1,s2,s,k1,k2,k,α1,α2,β,sn)" 
         "atom sn ♯ (s1,s2,s,k1,k2,k,α1,α2,β)"
    by (metis obtain_fresh) 
  let ?hyp = "{HaddP k1 k2 (Var k'), OrdP k1, OrdP k2, SeqAppendP s1 (SUCC k1) s2 (SUCC k2) (Var s), 
              PrfP s1 k1 α1, PrfP s2 k2 α2, ModPonP α1 α2 β OR ExistsP α1 β OR SubstP α1 β}"
  show ?thesis
     using assms atoms
     apply (simp add: PrfP.simps [of l "Var s" sl m n sm sn])
     apply (rule cut_same [where A="OrdP k1 AND OrdP k2"])
     apply (metis Conj_I PrfP_imp_OrdP thin1 thin2)
     apply (rule cut_same [OF exists_SeqAppendP [of s s1 "SUCC k1" s2 "SUCC k2"]])
     apply (rule AssumeH Ex_EH Conj_EH | simp)+
     apply (rule cut_same [OF exists_HaddP [where j=k' and x=k1 and y=k2]])
     apply (rule AssumeH Ex_EH Conj_EH | simp)+
     apply (rule Ex_I [where x="SUCC (SUCC (Var k'))"], simp)
     apply (rule Ex_I [where x="Eats (Var s) (HPair (SUCC (SUCC (Var k'))) β)"], simp)
     apply (rule Conj_I)
     apply (blast intro: LstSeqP_SeqAppendP_Eats PrfP_imp_LstSeqP [THEN cut1])
     proof (rule All2_SUCC_I, simp_all)
       show "?hyp ⊢ Ex sn
                 (HPair (SUCC (SUCC (Var k'))) (Var sn) IN Eats (Var s) (HPair (SUCC (SUCC (Var k'))) β) AND
                  (AxiomP (Var sn) OR
                   Ex m (Ex l (Ex sm (Ex sl
                      (Var m IN SUCC (SUCC (Var k')) AND
                       Var l IN SUCC (SUCC (Var k')) AND
                       HPair (Var m) (Var sm) IN Eats (Var s) (HPair (SUCC (SUCC (Var k'))) β) AND
                       HPair (Var l) (Var sl) IN Eats (Var s) (HPair (SUCC (SUCC (Var k'))) β) AND
                       (ModPonP (Var sm) (Var sl) (Var sn) OR ExistsP (Var sm) (Var sn) OR SubstP (Var sm) (Var sn))))))))"
       ― ‹verifying the final values›
       apply (rule Ex_I [where x="β"])
       using assms atoms apply simp
       apply (rule Conj_I, metis Mem_Eats_I2 Refl)
       apply (rule Disj_I2)
       apply (rule Ex_I [where x=k1], simp)
       apply (rule Ex_I [where x="SUCC (Var k')"], simp)
       apply (rule_tac x=α1 in Ex_I, simp)
       apply (rule_tac x=α2 in Ex_I, simp)
       apply (rule Conj_I)
       apply (blast intro: HaddP_Mem_I LstSeqP_OrdP Mem_SUCC_I1)
       apply (rule Conj_I [OF Mem_SUCC_Refl Conj_I])
       apply (blast intro: Mem_Eats_I1 SeqAppendP_Mem1 [THEN cut3] Mem_SUCC_Refl PrfP_imp_LstSeqP [THEN cut1] LstSeqP_imp_Mem)
       apply (blast del: Disj_EH  intro: Mem_Eats_I1 SeqAppendP_Mem2 [THEN cut4] Mem_SUCC_Refl 
                     PrfP_imp_LstSeqP [THEN cut1] HaddP_SUCC1 [THEN cut1] LstSeqP_imp_Mem)
       done
     next
       show "?hyp ⊢ All2 n (SUCC (SUCC (Var k')))
               (Ex sn
                 (HPair (Var n) (Var sn) IN Eats (Var s) (HPair (SUCC (SUCC (Var k'))) β) AND
                  (AxiomP (Var sn) OR
                   Ex m (Ex l (Ex sm (Ex sl
                      (Var m IN Var n AND
                       Var l IN Var n AND
                       HPair (Var m) (Var sm) IN Eats (Var s) (HPair (SUCC (SUCC (Var k'))) β) AND
                       HPair (Var l) (Var sl) IN Eats (Var s) (HPair (SUCC (SUCC (Var k'))) β) AND
                       (ModPonP (Var sm) (Var sl) (Var sn) OR ExistsP (Var sm) (Var sn) OR SubstP (Var sm) (Var sn)))))))))"
     ― ‹verifying the sequence buildup›
     apply (rule cut_same [where A="HaddP (SUCC k1) (SUCC k2) (SUCC (SUCC (Var k')))"])
     apply (blast intro: HaddP_SUCC1 [THEN cut1] HaddP_SUCC2 [THEN cut1])
     apply (rule All_I Imp_I)+
     apply (rule HaddP_Mem_cases [where i=j])
     using assms atoms apply simp_all
     apply (rule AssumeH)
     apply (blast intro: OrdP_SUCC_I LstSeqP_OrdP)
     ― ‹... the sequence buildup via s1›
     apply (simp add: PrfP.simps [of l s1 sl m n sm sn])
     apply (rule AssumeH Ex_EH Conj_EH)+
     apply (rule All2_E [THEN rotate2])
     apply (rule AssumeH Ex_EH Conj_EH | simp)+
     apply (rule Ex_I [where x="Var sn"], simp)
     apply (rule Conj_I)
     apply (rule Mem_Eats_I1)
     apply (metis SeqAppendP_Mem1 rotate3 thin2 thin4)
     apply (rule AssumeH Disj_IE1H Ex_EH Conj_EH)+
     apply (rule Ex_I [where x="Var m"], simp)
     apply (rule Ex_I [where x="Var l"], simp)
     apply (rule Ex_I [where x="Var sm"], simp)
     apply (rule Ex_I [where x="Var sl"], simp_all)
     apply (rule Conj_I, rule AssumeH)+
     apply (blast del: Disj_EH intro: OrdP_Trans [OF OrdP_SUCC_I] Mem_Eats_I1 [OF SeqAppendP_Mem1 [THEN cut3]] Hyp)
     ― ‹... the sequence buildup via s2›
     apply (simp add: PrfP.simps [of l s2 sl m n sm sn])
     apply (rule AssumeH Ex_EH Conj_EH)+
     apply (rule All2_E [THEN rotate2])
     apply (rule AssumeH Ex_EH Conj_EH | simp)+
     apply (rule Ex_I [where x="Var sn"], simp)
     apply (rule cut_same [where A="OrdP (Var j)"])
     apply (metis HaddP_imp_OrdP rotate2 thin2)
     apply (rule Conj_I)
     apply (blast intro!: Mem_Eats_I1 SeqAppendP_Mem2 [THEN cut4] del: Disj_EH)
     apply (rule AssumeH Disj_IE1H Ex_EH Conj_EH)+
     apply (rule cut_same [OF exists_HaddP [where j=km and x="SUCC k1" and y="Var m"]])
     apply (blast intro: Ord_IN_Ord, simp)
     apply (rule cut_same [OF exists_HaddP [where j=kn and x="SUCC k1" and y="Var l"]])
     apply (blast intro!: Ord_IN_Ord)
     apply (rule AssumeH Ex_EH Conj_EH | simp)+
     apply (rule Ex_I [where x="Var km"], simp)
     apply (rule Ex_I [where x="Var kn"], simp)
     apply (rule Ex_I [where x="Var sm"], simp)
     apply (rule Ex_I [where x="Var sl"], simp_all)
     apply (rule Conj_I [OF _ Conj_I])
     apply (blast intro!: HaddP_Mem_cancel_left [THEN Iff_MP2_same] OrdP_SUCC_I intro: LstSeqP_OrdP Hyp)+
     apply (blast del: Disj_EH  intro: OrdP_Trans Hyp 
                  intro!: Mem_Eats_I1 SeqAppendP_Mem2 [THEN cut4] HaddP_imp_OrdP [THEN cut1])
     done
   qed
qed (*>*)

corollary PfP_inference: "{PfP α1, PfP α2, ModPonP α1 α2 β OR ExistsP α1 β OR SubstP α1 β} ⊢ PfP β"
proof -
  obtain k1::name and s1::name and k2::name and s2::name and k::name and s::name
    where "atom s1 ♯ (α1,α2,β)" "atom k1 ♯ (α1,α2,β,s1)"  
          "atom s2 ♯ (α1,α2,β,k1,s1)""atom k2 ♯ (α1,α2,β,s2,k1,s1)"
          "atom s  ♯ (α1,α2,β,k2,s2,k1,s1)"
          "atom k  ♯ (α1,α2,β,s,k2,s2,k1,s1)" 
    by (metis obtain_fresh)
   thus ?thesis
     apply (simp add: PfP.simps [of k s β] PfP.simps [of k1 s1 α1]  PfP.simps [of k2 s2 α2])
     apply (auto intro!: PrfP_inference [of s k "Var s1" "Var s2", THEN cut3] del: Disj_EH)
     done
qed

theorem PfP_implies_SubstForm_PfP: 
   assumes "H ⊢ PfP y" "H ⊢ SubstFormP x t y z"
     shows "H ⊢ PfP z"
proof -
  obtain u::name and v::name
    where atoms: "atom u ♯ (t,x,y,z,v)"   "atom v ♯ (t,x,y,z)"
    by (metis obtain_fresh) 
  show ?thesis
    apply (rule PfP_inference [of y, THEN cut3])
    apply (rule assms)+
    using atoms
    apply (auto simp: SubstP.simps [of u _ _ v] intro!: Disj_I2)
    apply (rule Ex_I [where x=x], simp)
    apply (rule Ex_I [where x=t], simp add: assms)
    done
qed

theorem PfP_implies_ModPon_PfP: "⟦H ⊢ PfP (Q_Imp x y); H ⊢ PfP x⟧ ⟹ H ⊢ PfP y" 
  by (force intro: PfP_inference [of x, THEN cut3] Disj_I1  simp add: ModPonP_def)

corollary PfP_implies_ModPon_PfP_quot: "⟦H ⊢ PfP «α IMP β»; H ⊢ PfP «α»⟧ ⟹ H ⊢ PfP «β»" 
  by (auto simp: quot_fm_def intro: PfP_implies_ModPon_PfP)

end