Theory Incompleteness.Functions

chapter‹Uniqueness Results: Syntactic Relations are Functions›

theory Functions
imports Coding_Predicates
begin

subsection ‹SeqStTermP›

lemma not_IndP_VarP: "{IndP x, VarP x} ⊢ A"
proof -
  obtain m::name  where "atom m ♯ (x,A)"
    by (metis obtain_fresh) 
  thus ?thesis
    by  (auto simp: fresh_Pair) (blast intro: ExFalso cut_same [OF VarP_cong [THEN Iff_MP_same]])
qed

text‹It IS a pair, but not just any pair.›
lemma IndP_HPairE: "insert (IndP (HPair (HPair Zero (HPair Zero Zero)) x)) H ⊢ A"
proof -
  obtain m::name  where "atom m ♯ (x,A)"
    by (metis obtain_fresh)
  hence "{ IndP (HPair (HPair Zero (HPair Zero Zero)) x) } ⊢ A"
    by (auto simp: IndP.simps [of m] HTuple_minus_1 intro: thin1)
  thus ?thesis
    by (metis Assume cut1)
qed

lemma atom_HPairE: 
  assumes "H ⊢ x EQ HPair (HPair Zero (HPair Zero Zero)) y"
    shows "insert (IndP x OR x NEQ v) H ⊢ A"
proof -
  have "{ IndP x OR x NEQ v, x EQ HPair (HPair Zero (HPair Zero Zero)) y } ⊢ A"
    by (auto intro!: OrdNotEqP_OrdP_E IndP_HPairE
             intro: cut_same [OF IndP_cong [THEN Iff_MP_same]] 
                    cut_same [OF OrdP_cong [THEN Iff_MP_same]])
  thus ?thesis
    by (metis Assume assms rcut2)
qed

lemma SeqStTermP_lemma:
  assumes "atom m ♯ (v,i,t,u,s,k,n,sm,sm',sn,sn')" "atom n ♯ (v,i,t,u,s,k,sm,sm',sn,sn')"
          "atom sm ♯ (v,i,t,u,s,k,sm',sn,sn')" "atom sm' ♯ (v,i,t,u,s,k,sn,sn')"
          "atom sn ♯ (v,i,t,u,s,k,sn')" "atom sn' ♯ (v,i,t,u,s,k)"
    shows "{ SeqStTermP v i t u s k }
           ⊢ ((t EQ v AND u EQ i) OR
              ((IndP t OR t NEQ v) AND u EQ t)) OR
              Ex m (Ex n (Ex sm (Ex sm' (Ex sn (Ex sn' (Var m IN k AND Var n IN k AND
                       SeqStTermP v i (Var sm) (Var sm') s (Var m) AND
                       SeqStTermP v i (Var sn) (Var sn') s (Var n) AND
                       t EQ Q_Eats (Var sm) (Var sn) AND
                       u EQ Q_Eats (Var sm') (Var sn')))))))"
proof -
  obtain l::name and sl::name and sl'::name
    where "atom l ♯ (v,i,t,u,s,k,sl,sl',m,n,sm,sm',sn,sn')"
          "atom sl ♯ (v,i,t,u,s,k,sl',m,n,sm,sm',sn,sn')"
          "atom sl' ♯ (v,i,t,u,s,k,m,n,sm,sm',sn,sn')"
    by (metis obtain_fresh)
  thus ?thesis using assms
    apply (simp add: SeqStTermP.simps [of l s k v i sl sl' m n sm sm' sn sn'])
    apply (rule Conj_EH Ex_EH All2_SUCC_E [THEN rotate2] | simp)+
    apply (rule cut_same [where A = "HPair t u EQ HPair (Var sl) (Var sl')"])
    apply (metis Assume AssumeH(4) LstSeqP_EQ)
    apply clarify
    apply (rule Disj_EH)
    apply (rule Disj_I1)
    apply (rule anti_deduction)
    apply (rule Var_Eq_subst_Iff [THEN Sym_L, THEN Iff_MP_same])
    apply (rule Sym_L [THEN rotate2])
    apply (rule Var_Eq_subst_Iff [THEN Iff_MP_same], force)
    ― ‹now the quantified case›
    ― ‹auto could be used but is VERY SLOW›
    apply (rule Ex_EH Conj_EH)+
    apply simp_all
    apply (rule 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 sm'"], simp)
    apply (rule Ex_I [where x = "Var sn"], simp)
    apply (rule Ex_I [where x = "Var sn'"], simp)
    apply (simp_all add: SeqStTermP.simps [of l s _ v i sl sl' m n sm sm' sn sn'])
    apply ((rule Conj_I)+, blast intro: LstSeqP_Mem)+
    ― ‹first SeqStTermP subgoal›
    apply (rule All2_Subset [OF Hyp], blast)
    apply (blast intro!: SUCC_Subset_Ord LstSeqP_OrdP, blast, simp)
    ― ‹next SeqStTermP 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 SeqStTermP_unique: "{SeqStTermP v a t u s kk, SeqStTermP v a t u' s' kk'} ⊢ u' EQ u"
proof -
  obtain i::name and j::name and j'::name and k::name and k'::name and l::name
     and m::name and n::name and sm::name and sn::name and sm'::name and sn'::name
     and m2::name and n2::name and sm2::name and sn2::name and sm2'::name and sn2'::name
    where atoms:  "atom i ♯ (s,s',v,a,t,u,u')"   "atom j ♯ (s,s',v,a,t,i,t,u,u')"
                  "atom j' ♯ (s,s',v,a,t,i,j,t,u,u')"
                  "atom k ♯ (s,s',v,a,t,u,u',kk',i,j,j')" "atom k' ♯ (s,s',v,a,t,u,u',k,i,j,j')"
                  "atom l ♯ (s,s',v,a,t,i,j,j',k,k')"
                  "atom m ♯ (s,s',v,a,i,j,j',k,k',l)"   "atom n ♯ (s,s',v,a,i,j,j',k,k',l,m)"
                  "atom sm ♯ (s,s',v,a,i,j,j',k,k',l,m,n)"  "atom sn ♯ (s,s',v,a,i,j,j',k,k',l,m,n,sm)"
                  "atom sm' ♯ (s,s',v,a,i,j,j',k,k',l,m,n,sm,sn)"   "atom sn' ♯ (s,s',v,a,i,j,j',k,k',l,m,n,sm,sn,sm')"
                  "atom m2 ♯ (s,s',v,a,i,j,j',k,k',l,m,n,sm,sn,sm',sn')"   "atom n2 ♯ (s,s',v,a,i,j,j',k,k',l,m,n,sm,sn,sm',sn',m2)"
                  "atom sm2 ♯ (s,s',v,a,i,j,j',k,k',l,m,n,sm,sn,sm',sn',m2,n2)"  "atom sn2 ♯ (s,s',v,a,i,j,j',k,k',l,m,n,sm,sn,sm',sn',m2,n2,sm2)"
                  "atom sm2' ♯ (s,s',v,a,i,j,j',k,k',l,m,n,sm,sn,sm',sn',m2,n2,sm2,sn2)"   "atom sn2' ♯ (s,s',v,a,i,j,j',k,k',l,m,n,sm,sn,sm',sn',m2,n2,sm2,sn2,sm2')"
    by (metis obtain_fresh)
  have "{ OrdP (Var k), VarP v }
       ⊢ All i (All j (All j' (All k' (SeqStTermP v a (Var i) (Var j) s (Var k)
                                  IMP (SeqStTermP v a (Var i) (Var j') s' (Var k') IMP Var j' EQ Var j)))))"
    apply (rule OrdIndH [where j=l])
    using atoms apply auto
    apply (rule Swap)
    apply (rule cut_same)
    apply (rule cut1 [OF SeqStTermP_lemma [of m v a "Var i" "Var j" s "Var k" n sm sm' sn sn']], simp_all, blast)
    apply (rule cut_same)
    apply (rule cut1 [OF SeqStTermP_lemma [of m2 v a "Var i" "Var j'" s' "Var k'" n2 sm2 sm2' sn2 sn2']], simp_all, blast)
    apply (rule Disj_EH Conj_EH)+
    ― ‹case 1, both sides equal @{term v}›
    apply (blast intro: Trans Sym)
    ― ‹case 2, @{term "Var i EQ v"} and also @{term "IndP (Var i) OR Var i NEQ v"}›
    apply (rule Conj_EH Disj_EH)+
    apply (blast intro: IndP_cong [THEN Iff_MP_same] not_IndP_VarP [THEN cut2])
    apply (metis Assume OrdNotEqP_E)
    ― ‹case 3, both a variable and a pair›
    apply (rule Ex_EH Conj_EH)+
    apply simp_all
    apply (rule cut_same [where A = "VarP (Q_Eats (Var sm) (Var sn))"])
    apply (blast intro: Trans Sym VarP_cong [where x=v, THEN Iff_MP_same] Hyp, blast)
    ― ‹towards remaining cases›
    apply (rule Disj_EH Ex_EH)+
    ― ‹case 4, @{term "Var i EQ v"} and also @{term "IndP (Var i) OR Var i NEQ v"}›
    apply (blast intro: IndP_cong [THEN Iff_MP_same] not_IndP_VarP [THEN cut2] OrdNotEqP_E)
    ― ‹case 5, @{term "Var i EQ v"} for both›
    apply (blast intro: Trans Sym)
    ― ‹case 6, both an atom and a pair›
    apply (rule Ex_EH Conj_EH)+
    apply simp_all 
    apply (rule atom_HPairE)
    apply (simp add: HTuple.simps)
    apply (blast intro: Trans)
    ― ‹towards remaining cases›
    apply (rule Conj_EH Disj_EH Ex_EH)+
    apply simp_all
    ― ‹case 7, both an atom and a pair›
    apply (rule cut_same [where A = "VarP (Q_Eats (Var sm2) (Var sn2))"])
    apply (blast intro: Trans Sym VarP_cong [where x=v, THEN Iff_MP_same] Hyp, blast)
    ― ‹case 8, both an atom and a pair›
    apply (rule Ex_EH Conj_EH)+
    apply simp_all
    apply (rule atom_HPairE)
    apply (simp add: HTuple.simps)
    apply (blast intro: Trans)
    ― ‹case 9, two Eats terms›
    apply (rule Ex_EH Disj_EH Conj_EH)+
    apply simp_all
    apply (rule All_E' [OF Hyp, where x="Var m"], blast)
    apply (rule All_E' [OF Hyp, where x="Var n"], blast, simp)
    apply (rule Disj_EH, blast intro: thin1 ContraProve)+
    apply (rule All_E [where x="Var sm"], simp)
    apply (rule All_E [where x="Var sm'"], simp)
    apply (rule All_E [where x="Var sm2'"], simp)
    apply (rule All_E [where x="Var m2"], simp)
    apply (rule All_E [where x="Var sn", THEN rotate2], simp)
    apply (rule All_E [where x="Var sn'"], simp)
    apply (rule All_E [where x="Var sn2'"], simp)
    apply (rule All_E [where x="Var n2"], simp)
    apply (rule cut_same [where A = "Q_Eats (Var sm) (Var sn) EQ Q_Eats (Var sm2) (Var sn2)"])
    apply (blast intro: Sym Trans, clarify)
    apply (rule cut_same [where A = "SeqStTermP v a (Var sn) (Var sn2') s' (Var n2)"])
    apply (blast intro: Hyp SeqStTermP_cong [OF Hyp Refl Refl, THEN Iff_MP2_same])
    apply (rule cut_same [where A = "SeqStTermP v a (Var sm) (Var sm2') s' (Var m2)"])
    apply (blast intro: Hyp SeqStTermP_cong [OF Hyp Refl Refl, THEN Iff_MP2_same])
    apply (rule Disj_EH, blast intro: thin1 ContraProve)+
    apply (blast intro: HPair_cong Trans [OF Hyp Sym])
    done
  hence p1: "{OrdP (Var k), VarP v}
             ⊢ (All j (All j' (All k' (SeqStTermP v a (Var i) (Var j) s (Var k)
                 IMP (SeqStTermP v a (Var i) (Var j') s' (Var k') IMP Var j' EQ Var j)))))(i::=t)"
    by (metis All_D)
  have p2: "{OrdP (Var k), VarP v}
         ⊢ (All j' (All k' (SeqStTermP v a t (Var j) s (Var k)
                 IMP (SeqStTermP v a t (Var j') s' (Var k') IMP Var j' EQ Var j))))(j::=u)"
    apply (rule All_D)
    using atoms p1 by simp
  have p3: "{OrdP (Var k), VarP v}
             ⊢ (All k' (SeqStTermP v a t u s (Var k) IMP (SeqStTermP v a t (Var j') s' (Var k') IMP Var j' EQ u)))(j'::=u')"
    apply (rule All_D)
    using atoms p2 by simp
  have p4: "{OrdP (Var k), VarP v}
          ⊢ (SeqStTermP v a t u s (Var k) IMP (SeqStTermP v a t u' s' (Var k') IMP u' EQ u))(k'::=kk')"
    apply (rule All_D)
    using atoms p3 by simp
  hence "{SeqStTermP v a t u s (Var k), VarP v} ⊢ SeqStTermP v a t u s (Var k) IMP (SeqStTermP v a t u' s' kk' IMP u' EQ u)"
    using atoms apply simp
    by (metis SeqStTermP_imp_OrdP rcut1)
  hence "{VarP v} ⊢ ((SeqStTermP v a t u s (Var k) IMP (SeqStTermP v a t u' s' kk' IMP u' EQ u)))"
    by (metis Assume MP_same Imp_I)
  hence "{VarP v} ⊢ ((SeqStTermP v a t u s (Var k) IMP (SeqStTermP v a t u' s' kk' IMP u' EQ u)))(k::=kk)"
   using atoms by (force intro!: Subst)
  hence "{VarP v} ⊢ SeqStTermP v a t u s kk IMP (SeqStTermP v a t u' s' kk' IMP u' EQ u)"
    using atoms by simp
  hence "{SeqStTermP v a t u s kk} ⊢ SeqStTermP v a t u s kk IMP (SeqStTermP v a t u' s' kk' IMP u' EQ u)"
    by (metis SeqStTermP_imp_VarP rcut1)
  thus ?thesis
    by (metis Assume AssumeH(2) MP_same rcut1)
qed


theorem SubstTermP_unique: "{SubstTermP v tm t u, SubstTermP v tm t u'} ⊢ u' EQ u"
proof -
  obtain s::name and s'::name and k::name and k'::name
    where "atom s ♯ (v,tm,t,u,u',k,k')" "atom s' ♯ (v,tm,t,u,u',k,k',s)"
          "atom k ♯ (v,tm,t,u,u')" "atom k' ♯ (v,tm,t,u,u',k)"
    by (metis obtain_fresh)
  thus ?thesis
    by (auto simp: SubstTermP.simps [of s v tm t u k]  SubstTermP.simps [of s' v tm t u' k'])
       (metis SeqStTermP_unique rotate3 thin1)
qed

subsection‹@{term SubstAtomicP}›

lemma SubstTermP_eq:
  "⟦H ⊢ SubstTermP v tm x z; insert (SubstTermP v tm y z) H ⊢ A⟧ ⟹ insert (x EQ y) H ⊢ A"
  by (metis Assume rotate2 Iff_E1 cut_same thin1 SubstTermP_cong [OF Refl Refl _ Refl])

lemma SubstAtomicP_unique: "{SubstAtomicP v tm x y, SubstAtomicP v tm x y'} ⊢ y' EQ y"
proof -
  obtain t::name and ts::name and u::name and us::name
     and t'::name and ts'::name and u'::name and us'::name
    where "atom t ♯ (v,tm,x,y,y',ts,u,us)"  "atom ts ♯ (v,tm,x,y,y',u,us)"
          "atom u ♯ (v,tm,x,y,y',us)"       "atom us ♯ (v,tm,x,y,y')"
          "atom t' ♯ (v,tm,x,y,y',t,ts,u,us,ts',u',us')" "atom ts' ♯ (v,tm,x,y,y',t,ts,u,us,u',us')"
          "atom u' ♯ (v,tm,x,y,y',t,ts,u,us,us')"        "atom us' ♯ (v,tm,x,y,y',t,ts,u,us)"
    by (metis obtain_fresh)
  thus ?thesis
    apply (simp add: SubstAtomicP.simps [of t v tm x y ts u us]
                     SubstAtomicP.simps [of t' v tm x y' ts' u' us'])
    apply (rule Ex_EH Disj_EH Conj_EH)+
    apply simp_all
    apply (rule Eq_Trans_E [OF Hyp], auto simp: HTS)
    apply (rule SubstTermP_eq [THEN thin1], blast)
    apply (rule SubstTermP_eq [THEN rotate2], blast)
    apply (rule Trans [OF Hyp Sym], blast)
    apply (rule Trans [OF Hyp], blast)
    apply (metis Assume AssumeH(8) HPair_cong Refl cut2 [OF SubstTermP_unique] thin1)
    apply (rule Eq_Trans_E [OF Hyp], blast, force simp add: HTS)
    apply (rule Eq_Trans_E [OF Hyp], blast, force simp add: HTS)
    apply (rule Eq_Trans_E [OF Hyp], auto simp: HTS)
    apply (rule SubstTermP_eq [THEN thin1], blast)
    apply (rule SubstTermP_eq [THEN rotate2], blast)
    apply (rule Trans [OF Hyp Sym], blast)
    apply (rule Trans [OF Hyp], blast)
    apply (metis Assume AssumeH(8) HPair_cong Refl cut2 [OF SubstTermP_unique] thin1)
    done
qed

subsection‹@{term SeqSubstFormP}›

lemma SeqSubstFormP_lemma:
  assumes "atom m ♯ (v,u,x,y,s,k,n,sm,sm',sn,sn')" "atom n ♯ (v,u,x,y,s,k,sm,sm',sn,sn')"
          "atom sm ♯ (v,u,x,y,s,k,sm',sn,sn')"  "atom sm' ♯ (v,u,x,y,s,k,sn,sn')"
          "atom sn ♯ (v,u,x,y,s,k,sn')"         "atom sn' ♯ (v,u,x,y,s,k)"
  shows "{ SeqSubstFormP v u x y s k }
         ⊢ SubstAtomicP v u x y  OR
           Ex m (Ex n (Ex sm (Ex sm' (Ex sn (Ex sn' (Var m IN k AND Var n IN k AND
                       SeqSubstFormP v u (Var sm) (Var sm') s (Var m) AND
                       SeqSubstFormP v u (Var sn) (Var sn') s (Var n) AND
                       (((x EQ Q_Disj (Var sm) (Var sn) AND y EQ Q_Disj (Var sm') (Var sn')) OR
                        (x EQ Q_Neg (Var sm) AND y EQ Q_Neg (Var sm')) OR
                        (x EQ Q_Ex (Var sm) AND y EQ Q_Ex (Var sm'))))))))))"
proof -
  obtain l::name and sl::name and sl'::name
    where "atom l ♯ (v,u,x,y,s,k,sl,sl',m,n,sm,sm',sn,sn')"
          "atom sl ♯ (v,u,x,y,s,k,sl',m,n,sm,sm',sn,sn')"
          "atom sl' ♯ (v,u,x,y,s,k,m,n,sm,sm',sn,sn')"
    by (metis obtain_fresh)
  thus ?thesis using assms
    apply (simp add: SeqSubstFormP.simps [of l s k v u sl sl' m n sm sm' sn sn'])
    apply (rule Conj_EH Ex_EH All2_SUCC_E [THEN rotate2] | simp)+
    apply (rule cut_same [where A = "HPair x y EQ HPair (Var sl) (Var sl')"])
    apply (metis Assume AssumeH(4) LstSeqP_EQ)
    apply clarify
    apply (rule Disj_EH)
    apply (blast intro: Disj_I1 SubstAtomicP_cong [THEN Iff_MP2_same])
    ― ‹now the quantified cases›
    apply (rule Ex_EH Conj_EH)+
    apply simp_all
    apply (rule 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 sm'"], simp)
    apply (rule Ex_I [where x = "Var sn"], simp)
    apply (rule Ex_I [where x = "Var sn'"], simp)
    apply (simp_all add: SeqSubstFormP.simps [of l s _ v u sl sl' m n sm sm' sn sn'])
    apply ((rule Conj_I)+, blast intro: LstSeqP_Mem)+
    ― ‹first SeqSubstFormP subgoal›
    apply (rule All2_Subset [OF Hyp], blast)
    apply (blast intro!: SUCC_Subset_Ord LstSeqP_OrdP, blast, simp)
    ― ‹next SeqSubstFormP 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 pairs›
    apply (rule anti_deduction [THEN thin1])
    apply (rule Sym_L [THEN rotate4])
    apply (rule Var_Eq_subst_Iff [THEN Iff_MP_same])
    apply (rule Sym_L [THEN rotate5])
    apply (rule Var_Eq_subst_Iff [THEN Iff_MP_same], force)
    done
qed

lemma 
  shows Neg_SubstAtomicP_Fls:  "{y EQ Q_Neg z,  SubstAtomicP v tm y y'} ⊢ Fls"    (is ?thesis1)
    and Disj_SubstAtomicP_Fls: "{y EQ Q_Disj z w, SubstAtomicP v tm y y'} ⊢ Fls"  (is ?thesis2)
    and Ex_SubstAtomicP_Fls:   "{y EQ Q_Ex z,   SubstAtomicP v tm y y'} ⊢ Fls"    (is ?thesis3)
proof -
  obtain t::name and u::name and t'::name  and u'::name
    where "atom t ♯ (z,w,v,tm,y,y',t',u,u')" "atom t' ♯ (z,w,v,tm,y,y',u,u')"
          "atom u ♯ (z,w,v,tm,y,y',u')" "atom u' ♯ (z,w,v,tm,y,y')"
    by (metis obtain_fresh)
  thus ?thesis1 ?thesis2 ?thesis3
    by (auto simp: SubstAtomicP.simps [of t v tm y y' t' u u'] HTS  intro: Eq_Trans_E [OF Hyp])
qed

lemma SeqSubstFormP_eq:
  "⟦H ⊢ SeqSubstFormP v tm x z s k; insert (SeqSubstFormP v tm y z s k) H ⊢ A⟧ 
   ⟹ insert (x EQ y) H ⊢ A"
  apply (rule cut_same [OF SeqSubstFormP_cong [OF Assume Refl Refl Refl, THEN Iff_MP_same]])
  apply (auto simp: insert_commute intro: thin1)
  done

lemma SeqSubstFormP_unique: "{SeqSubstFormP v a x y s kk, SeqSubstFormP v a x y' s' kk'} ⊢ y' EQ y"
proof -
  obtain i::name and j::name and j'::name and k::name and k'::name and l::name
     and m::name and n::name and sm::name and sn::name and sm'::name and sn'::name
     and m2::name and n2::name and sm2::name and sn2::name and sm2'::name and sn2'::name
    where atoms:  "atom i ♯ (s,s',v,a,x,y,y')"   "atom j ♯ (s,s',v,a,x,i,x,y,y')"
                  "atom j' ♯ (s,s',v,a,x,i,j,x,y,y')"
                  "atom k ♯ (s,s',v,a,x,y,y',kk',i,j,j')" "atom k' ♯ (s,s',v,a,x,y,y',k,i,j,j')"
                  "atom l ♯ (s,s',v,a,x,i,j,j',k,k')"
                  "atom m ♯ (s,s',v,a,i,j,j',k,k',l)"   "atom n ♯ (s,s',v,a,i,j,j',k,k',l,m)"
                  "atom sm ♯ (s,s',v,a,i,j,j',k,k',l,m,n)"  "atom sn ♯ (s,s',v,a,i,j,j',k,k',l,m,n,sm)"
                  "atom sm' ♯ (s,s',v,a,i,j,j',k,k',l,m,n,sm,sn)"   "atom sn' ♯ (s,s',v,a,i,j,j',k,k',l,m,n,sm,sn,sm')"
                  "atom m2 ♯ (s,s',v,a,i,j,j',k,k',l,m,n,sm,sn,sm',sn')"   "atom n2 ♯ (s,s',v,a,i,j,j',k,k',l,m,n,sm,sn,sm',sn',m2)"
                  "atom sm2 ♯ (s,s',v,a,i,j,j',k,k',l,m,n,sm,sn,sm',sn',m2,n2)"  "atom sn2 ♯ (s,s',v,a,i,j,j',k,k',l,m,n,sm,sn,sm',sn',m2,n2,sm2)"
                  "atom sm2' ♯ (s,s',v,a,i,j,j',k,k',l,m,n,sm,sn,sm',sn',m2,n2,sm2,sn2)"   "atom sn2' ♯ (s,s',v,a,i,j,j',k,k',l,m,n,sm,sn,sm',sn',m2,n2,sm2,sn2,sm2')"
    by (metis obtain_fresh)
  have "{ OrdP (Var k) }
       ⊢ All i (All j (All j' (All k' (SeqSubstFormP v a (Var i) (Var j) s (Var k)
                                  IMP (SeqSubstFormP v a (Var i) (Var j') s' (Var k') IMP Var j' EQ Var j)))))"
    apply (rule OrdIndH [where j=l])
    using atoms apply auto
    apply (rule Swap)
    apply (rule cut_same)
    apply (rule cut1 [OF SeqSubstFormP_lemma [of m v a "Var i" "Var j" s "Var k" n sm sm' sn sn']], simp_all, blast)
    apply (rule cut_same)
    apply (rule cut1 [OF SeqSubstFormP_lemma [of m2 v a "Var i" "Var j'" s' "Var k'" n2 sm2 sm2' sn2 sn2']], simp_all, blast)
    apply (rule Disj_EH Conj_EH)+
    ― ‹case 1, both sides are atomic›
    apply (blast intro: cut2 [OF SubstAtomicP_unique])
    ― ‹case 2, atomic and also not›
    apply (rule Ex_EH Conj_EH Disj_EH)+
    apply simp_all
    apply (metis Assume AssumeH(7) Disj_I1 Neg_I anti_deduction cut2 [OF Disj_SubstAtomicP_Fls])
    apply (rule Conj_EH Disj_EH)+
    apply (metis Assume AssumeH(7) Disj_I1 Neg_I anti_deduction cut2 [OF Neg_SubstAtomicP_Fls])
    apply (rule Conj_EH)+
    apply (metis Assume AssumeH(7) Disj_I1 Neg_I anti_deduction cut2 [OF Ex_SubstAtomicP_Fls])
    ― ‹towards remaining cases›
    apply (rule Conj_EH Disj_EH Ex_EH)+
    apply simp_all
    apply (metis Assume AssumeH(7) Disj_I1 Neg_I anti_deduction cut2 [OF Disj_SubstAtomicP_Fls])
    apply (rule Conj_EH Disj_EH)+
    apply (metis Assume AssumeH(7) Disj_I1 Neg_I anti_deduction cut2 [OF Neg_SubstAtomicP_Fls])
    apply (rule Conj_EH)+
    apply (metis Assume AssumeH(7) Disj_I1 Neg_I anti_deduction cut2 [OF Ex_SubstAtomicP_Fls])
    ― ‹towards remaining cases›
    apply (rule Conj_EH Disj_EH Ex_EH)+
    apply simp_all
    ― ‹case two Disj terms›
    apply (rule All_E' [OF Hyp, where x="Var m"], blast)
    apply (rule All_E' [OF Hyp, where x="Var n"], blast, simp)
    apply (rule Disj_EH, blast intro: thin1 ContraProve)+
    apply (rule All_E [where x="Var sm"], simp)
    apply (rule All_E [where x="Var sm'"], simp)
    apply (rule All_E [where x="Var sm2'"], simp)
    apply (rule All_E [where x="Var m2"], simp)
    apply (rule All_E [where x="Var sn", THEN rotate2], simp)
    apply (rule All_E [where x="Var sn'"], simp)
    apply (rule All_E [where x="Var sn2'"], simp)
    apply (rule All_E [where x="Var n2"], simp)
    apply (rule rotate3)
    apply (rule Eq_Trans_E [OF Hyp], blast)
    apply (clarsimp simp add: HTS)
    apply (rule thin1)
    apply (rule Disj_EH [OF ContraProve], blast intro: thin1 SeqSubstFormP_eq)+
    apply (blast intro: HPair_cong Trans [OF Hyp Sym])
    ― ‹towards remaining cases›
    apply (rule Conj_EH Disj_EH)+
    ― ‹Negation = Disjunction?›
    apply (rule Eq_Trans_E [OF Hyp], blast, force simp add: HTS)
   ― ‹Existential = Disjunction?›
    apply (rule Conj_EH)
    apply (rule Eq_Trans_E [OF Hyp], blast, force simp add: HTS)
     ― ‹towards remaining cases›
    apply (rule Conj_EH Disj_EH Ex_EH)+
    apply simp_all
    ― ‹Disjunction = Negation?›
    apply (rule Eq_Trans_E [OF Hyp], blast, force simp add: HTS)
    apply (rule Conj_EH Disj_EH)+
    ― ‹case two Neg terms›
    apply (rule Eq_Trans_E [OF Hyp], blast, clarify)
    apply (rule thin1)
    apply (rule All_E' [OF Hyp, where x="Var m"], blast, simp)
    apply (rule Disj_EH, blast intro: thin1 ContraProve)+
    apply (rule All_E [where x="Var sm"], simp)
    apply (rule All_E [where x="Var sm'"], simp)
    apply (rule All_E [where x="Var sm2'"], simp)
    apply (rule All_E [where x="Var m2"], simp)
    apply (rule Disj_EH [OF ContraProve], blast intro: SeqSubstFormP_eq Sym_L)+
    apply (blast intro: HPair_cong Sym Trans [OF Hyp])
    ― ‹Existential = Negation?›
    apply (rule Conj_EH)+
    apply (rule Eq_Trans_E [OF Hyp], blast, force simp add: HTS)
     ― ‹towards remaining cases›
    apply (rule Conj_EH Disj_EH Ex_EH)+
    apply simp_all
    ― ‹Disjunction = Existential›
    apply (rule Eq_Trans_E [OF Hyp], blast, force simp add: HTS)
    apply (rule Conj_EH Disj_EH Ex_EH)+
    ― ‹Negation = Existential›
    apply (rule Eq_Trans_E [OF Hyp], blast, force simp add: HTS)
   ― ‹case two Ex terms›
    apply (rule Conj_EH)+
    apply (rule Eq_Trans_E [OF Hyp], blast, clarify)
    apply (rule thin1)
    apply (rule All_E' [OF Hyp, where x="Var m"], blast, simp)
    apply (rule Disj_EH, blast intro: thin1 ContraProve)+
    apply (rule All_E [where x="Var sm"], simp)
    apply (rule All_E [where x="Var sm'"], simp)
    apply (rule All_E [where x="Var sm2'"], simp)
    apply (rule All_E [where x="Var m2"], simp)
    apply (rule Disj_EH [OF ContraProve], blast intro: SeqSubstFormP_eq Sym_L)+
    apply (blast intro: HPair_cong Sym Trans [OF Hyp])
    done
  hence p1: "{OrdP (Var k)}
             ⊢ (All j (All j' (All k' (SeqSubstFormP v a (Var i) (Var j) s (Var k)
                 IMP (SeqSubstFormP v a (Var i) (Var j') s' (Var k') IMP Var j' EQ Var j)))))(i::=x)"
    by (metis All_D)
  have p2: "{OrdP (Var k)}
            ⊢ (All j' (All k' (SeqSubstFormP v a x (Var j) s (Var k)
                 IMP (SeqSubstFormP v a x (Var j') s' (Var k') IMP Var j' EQ Var j))))(j::=y)"
    apply (rule All_D)
    using atoms p1 by simp
  have p3: "{OrdP (Var k)}
            ⊢ (All k' (SeqSubstFormP v a x y s (Var k) 
                 IMP (SeqSubstFormP v a x (Var j') s' (Var k') IMP Var j' EQ y)))(j'::=y')"
    apply (rule All_D)
    using atoms p2 by simp
  have p4: "{OrdP (Var k)}
          ⊢ (SeqSubstFormP v a x y s (Var k) IMP (SeqSubstFormP v a x y' s' (Var k') IMP y' EQ y))(k'::=kk')"
    apply (rule All_D)
    using atoms p3 by simp
  hence "{OrdP (Var k)} ⊢ SeqSubstFormP v a x y s (Var k) IMP (SeqSubstFormP v a x y' s' kk' IMP y' EQ y)"
    using atoms by simp
  hence "{SeqSubstFormP v a x y s (Var k)} 
         ⊢ SeqSubstFormP v a x y s (Var k) IMP (SeqSubstFormP v a x y' s' kk' IMP y' EQ y)"
    by (metis SeqSubstFormP_imp_OrdP rcut1)
  hence "{} ⊢ SeqSubstFormP v a x y s (Var k) IMP (SeqSubstFormP v a x y' s' kk' IMP y' EQ y)"
    by (metis Assume Disj_Neg_2 Disj_commute anti_deduction Imp_I)
  hence "{} ⊢ ((SeqSubstFormP v a x y s (Var k) IMP (SeqSubstFormP v a x y' s' kk' IMP y' EQ y)))(k::=kk)"
    using atoms by (force intro!: Subst)
  thus ?thesis
    using atoms by simp (metis DisjAssoc2 Disj_commute anti_deduction)
qed

subsection‹@{term SubstFormP}›

theorem SubstFormP_unique: "{SubstFormP v tm x y, SubstFormP v tm x y'} ⊢ y' EQ y"
proof -
  obtain s::name and s'::name and k::name and k'::name
    where "atom s ♯ (v,tm,x,y,y',k,k')" "atom s' ♯ (v,tm,x,y,y',k,k',s)"
          "atom k ♯ (v,tm,x,y,y')" "atom k' ♯ (v,tm,x,y,y',k)"
    by (metis obtain_fresh)
  thus ?thesis
    by (force simp: SubstFormP.simps [of s v tm x y k]  SubstFormP.simps [of s' v tm x y' k']
                    SeqSubstFormP_unique rotate3 thin1)
qed

end