Theory Goedel_I

chapter ‹Section 6 Material and Gödel's First Incompleteness Theorem›

theory Goedel_I
imports Pf_Predicates Functions II_Prelims
begin

section‹The Function W and Lemma 6.1›

subsection‹Predicate form, defined on sequences›

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

nominal_termination (eqvt)
  by lexicographic_order

lemma
  shows SeqWRP_fresh_iff [simp]: "a ♯ SeqWRP s k y ⟷ a ♯ s ∧ a ♯ k ∧ a ♯ y" (is ?thesis1)
    and SeqWRP_sf [iff]:         "Sigma_fm (SeqWRP s k y)"  (is ?thsf)
    and SeqWRP_imp_OrdP:         "{SeqWRP s k t} ⊢ OrdP k" (is ?thOrd)
    and SeqWRP_LstSeqP:          "{SeqWRP s k t} ⊢ LstSeqP s k t" (is ?thlstseq)
proof -
  obtain l::name and sl::name where "atom l ♯ (s,k,sl)" "atom sl ♯ (s)"
    by (metis obtain_fresh)
  thus ?thesis1 ?thsf ?thOrd ?thlstseq
      by (auto intro: LstSeqP_OrdP[THEN cut1])
qed

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

lemma SeqWRP_cong:
  assumes "H ⊢ s EQ s'" and  "H ⊢ k EQ k'" and  "H ⊢ y EQ y'"
  shows "H ⊢ SeqWRP s k y IFF SeqWRP s' k' y'"
  by (rule P3_cong [OF _ assms], auto)

declare SeqWRP.simps [simp del]

subsection‹Predicate form of W›

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

nominal_termination (eqvt)
  by lexicographic_order

lemma
  shows WRP_fresh_iff [simp]: "a ♯ WRP x y ⟷ a ♯ x ∧ a ♯ y" (is ?thesis1)
    and sigma_fm_WRP [simp]:  "Sigma_fm (WRP x y)"  (is ?thsf)
proof -
  obtain s::name where "atom s ♯ (x,y)"
    by (metis obtain_fresh)
  thus ?thesis1 ?thsf
    by auto
qed

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

lemma WRP_cong: "H ⊢ t EQ t' ⟹ H ⊢ u EQ u' ⟹ H ⊢ WRP t u IFF WRP t' u'"
  by (rule P2_cong) auto

declare WRP.simps [simp del]

lemma ground_WRP [simp]: "ground_fm (WRP x y) ⟷ ground x ∧ ground y"
  by (auto simp: ground_aux_def ground_fm_aux_def supp_conv_fresh)

lemma SeqWRP_Zero: "{} ⊢ SyntaxN.Ex s (SeqWRP (Var s) Zero Zero)"
proof -
  obtain l sl :: name where "atom l ♯ (s, sl)" "atom sl ♯ s" by (metis obtain_fresh)
  then show ?thesis
    apply (subst SeqWRP.simps[of l _ _ sl]; simp)
    apply (rule Ex_I[where x="(Eats Zero (HPair Zero Zero))"], simp)
    apply (auto intro!: Mem_Eats_I2)
    done
qed

lemma WRP_Zero: "{} ⊢ WRP Zero Zero"
  by (subst WRP.simps[of undefined]) (auto simp: SeqWRP_Zero)

lemma SeqWRP_HPair_Zero_Zero: "{SeqWRP s k y} ⊢ HPair Zero Zero IN s"
proof -
  let ?vs = "(s,k,y)"
  obtain l::name and sl::name
    where "atom l ♯ (?vs,sl)" "atom sl ♯ (?vs)" by (metis obtain_fresh)
  then show ?thesis
    by (subst SeqWRP.simps[of l _ _ sl]) auto
qed

lemma SeqWRP_Succ:
  assumes "atom s ♯ (s1,k1,y)"
  shows "{SeqWRP s1 k1 y} ⊢ SyntaxN.Ex s (SeqWRP (Var s) (SUCC k1) (Q_Succ y))"
proof -
  let ?vs = "(s,s1,k1,y)"
  obtain l::name and sl::name and l1::name and sl1::name
    where atoms:
      "atom l ♯ (?vs,sl1,l1,sl)"
      "atom sl ♯ (?vs,sl1,l1)"
      "atom l1 ♯ (?vs,sl1)"
      "atom sl1 ♯ (?vs)"
    by (metis obtain_fresh)
  let ?hyp = "{RestrictedP s1 (SUCC k1) (Var s), OrdP k1, SeqWRP s1 k1 y}"
  show ?thesis
    using assms atoms
    apply (auto simp: SeqWRP.simps [of l "Var s" _ sl])
    apply (rule cut_same [where A="OrdP k1"])
    apply (rule SeqWRP_imp_OrdP)
    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)  (Q_Succ y))"])
      apply (simp_all (no_asm_simp))
    apply (rule Conj_I)
    apply (blast intro: RestrictedP_LstSeqP_Eats[THEN cut2] SeqWRP_LstSeqP[THEN cut1])
    apply (rule Conj_I)
     apply (rule Mem_Eats_I1)
     apply (blast intro: RestrictedP_Mem[THEN cut3] SeqWRP_HPair_Zero_Zero[THEN cut1] Zero_In_SUCC[THEN cut1])
  proof (rule All2_SUCC_I, simp_all)
    show "?hyp ⊢  SyntaxN.Ex sl
     (HPair k1 (Var sl) IN Eats (Var s) (HPair (SUCC k1) (Q_Succ y)) AND
      HPair (SUCC k1) (Q_Succ (Var sl)) IN
      Eats (Var s) (HPair (SUCC k1) (Q_Succ y)))"
      ― ‹verifying the final values›
      apply (rule Ex_I [where x="y"])
      using assms atoms apply simp
      apply (rule Conj_I[rotated])
       apply (rule Mem_Eats_I2, rule Refl)
     apply (rule Mem_Eats_I1)
      apply (rule RestrictedP_Mem[THEN cut3])
        apply (rule AssumeH)
       apply (simp add: LstSeqP_imp_Mem SeqWRP_LstSeqP thin1)
      apply (rule Mem_SUCC_Refl)
      done
  next
    show "?hyp ⊢ All2 l k1
     (SyntaxN.Ex sl
       (HPair (Var l) (Var sl) IN
        Eats (Var s) (HPair (SUCC k1) (Q_Succ y)) AND
        HPair (SUCC (Var l)) (Q_Succ (Var sl)) IN
        Eats (Var s) (HPair (SUCC k1) (Q_Succ y))))"
      ― ‹verifying the sequence buildup›
      apply (rule All_I Imp_I)+
      using assms atoms apply simp_all
        ― ‹... the sequence buildup via s1›
    apply (simp add: SeqWRP.simps [of l s1 _ sl])
      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 (blast intro: Mem_Eats_I1 [OF RestrictedP_Mem [THEN cut3]] Mem_SUCC_I1)
      apply (blast intro: Mem_Eats_I1 [OF RestrictedP_Mem [THEN cut3]] OrdP_IN_SUCC)
      done
  qed
qed (*>*)

lemma WRP_Succ: "{OrdP i, WRP i y} ⊢ WRP (SUCC i) (Q_Succ y)"
proof -
  obtain s t :: name where "atom s ♯ (i, y)" "atom t ♯ (s,i, y)" by (metis obtain_fresh)
  then show ?thesis
    by (subst WRP.simps[of s], simp, subst WRP.simps[of t], simp) (force intro: SeqWRP_Succ[THEN cut1])
qed

lemma WRP: "{} ⊢ WRP (ORD_OF i) «ORD_OF i»"
  by (induct i)
    (auto simp: WRP_Zero quot_Succ intro!: WRP_Succ[THEN cut2])

lemma prove_WRP:  "{} ⊢ WRP «Var x» ««Var x»»"
  unfolding quot_Var quot_Succ
  by (rule WRP_Succ[THEN cut2]) (auto simp: WRP)

subsection‹Proving that these relations are functions›

lemma SeqWRP_Zero_E:
  assumes "insert (y EQ Zero) H ⊢ A"  "H ⊢ k EQ Zero"
  shows "insert (SeqWRP s k y) H ⊢ A"
proof -
  obtain l::name and sl::name
    where "atom l ♯ (s,k,sl)" "atom sl ♯ (s)"
    by (metis obtain_fresh)
  thus ?thesis
    apply (auto simp: SeqWRP.simps [where s=s and l=l and sl=sl])
    apply (rule cut_same [where A = "LstSeqP s Zero y"])
    apply (blast intro: thin1 assms  LstSeqP_cong [OF Refl _ Refl, THEN Iff_MP_same])
    apply (rule cut_same [where A = "y EQ Zero"])
    apply (blast intro: LstSeqP_EQ)
    apply (metis rotate2 assms(1) thin1)
    done
qed

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

lemma SeqWRP_SUCC_E:
  assumes y': "atom y' ♯ (s,k,y)" and k': "H ⊢ k' EQ (SUCC k)"
  shows "insert (SeqWRP s k' y) H  ⊢ Ex y' (SeqWRP s k (Var y') AND y EQ Q_Succ (Var y'))"
  using SeqWRP_cong [OF Refl k' Refl] cut1 [OF SeqWRP_SUCC_lemma [of y' s k y]]
  by (metis Assume Iff_MP_left Iff_sym y')

lemma SeqWRP_unique: "{OrdP x, SeqWRP s x y, SeqWRP s' 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 pi::name
    where  i: "atom i ♯ (s,s',y,y')" and j: "atom j ♯ (s,s',i,x,y,y')" and j': "atom j' ♯ (s,s',i,j,x,y,y')"
      and atoms: "atom k ♯ (s,s',i,j,j')" "atom sl ♯ (s,s',i,j,j',k)" "atom sl' ♯ (s,s',i,j,j',k,sl)"
                 "atom pi ♯ (s,s',i,j,j',k,sl,sl')"
    by (metis obtain_fresh)
  have "{OrdP (Var i)} ⊢ All j (All j' (SeqWRP s (Var i) (Var j) IMP (SeqWRP s' (Var i) (Var j') IMP Var j' EQ Var j)))"
    apply (rule OrdIndH [where j=k])
    using i j j' atoms apply auto
    apply (rule rotate4)
    apply (rule OrdP_cases_E [where k=pi], simp_all)
    ― ‹Zero case›
    apply (rule SeqWRP_Zero_E [THEN rotate3])
    prefer 2 apply blast
    apply (rule SeqWRP_Zero_E [THEN rotate4])
    prefer 2 apply blast
    apply (blast intro: ContraProve [THEN rotate4] Sym Trans)
    ― ‹SUCC case›
    apply (rule Ex_I [where x = "Var pi"], auto)
    apply (metis ContraProve EQ_imp_SUBS2 Mem_SUCC_I2 Refl Subset_D)
    apply (rule cut_same)
    apply (rule SeqWRP_SUCC_E [of sl' s' "Var pi", THEN rotate4], auto)
    apply (rule cut_same)
    apply (rule SeqWRP_SUCC_E [of sl s "Var pi", THEN rotate7], auto)
    apply (rule All_E [where x = "Var sl", THEN rotate5], simp)
    apply (rule All_E [where x = "Var sl'"], simp)
    apply (rule Imp_E, blast)+
    apply (rule cut_same [OF Q_Succ_cong [OF Assume]])
    apply (blast intro: Trans [OF Hyp Sym] HPair_cong)
    done
  hence "{OrdP (Var i)} ⊢ (All j' (SeqWRP s (Var i) (Var j) IMP (SeqWRP s' (Var i) (Var j') IMP Var j' EQ Var j)))(j::=y)"
    by (metis All_D)
  hence "{OrdP (Var i)} ⊢ (SeqWRP s (Var i) y IMP (SeqWRP s' (Var i) (Var j') IMP Var j' EQ y))(j'::=y')"
    using j j'
    by simp (drule All_D [where x=y'], simp)
  hence "{} ⊢ OrdP (Var i) IMP (SeqWRP s (Var i) y IMP (SeqWRP s' (Var i) y' IMP y' EQ y))"
    using j j'
    by simp (metis Imp_I)
  hence "{} ⊢ (OrdP (Var i) IMP (SeqWRP s (Var i) y IMP (SeqWRP s' (Var i) y' IMP y' EQ y)))(i::=x)"
    by (metis Subst emptyE)
  thus ?thesis using i
    by simp (metis anti_deduction insert_commute)
qed

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

section‹The Function HF and Lemma 6.2›

subsection ‹Defining the syntax: quantified body›

nominal_function SeqHRP :: "tm ⇒ tm ⇒ tm ⇒ tm ⇒ fm"
  where "⟦atom l ♯ (s,k,sl,sl',m,n,sm,sm',sn,sn');
          atom sl ♯ (s,sl',m,n,sm,sm',sn,sn');
          atom sl' ♯ (s,m,n,sm,sm',sn,sn');
          atom m ♯ (s,n,sm,sm',sn,sn');
          atom n ♯ (s,sm,sm',sn,sn');
          atom sm ♯ (s,sm',sn,sn');
          atom sm' ♯ (s,sn,sn');
          atom sn ♯ (s,sn');
          atom sn' ♯ (s)⟧ ⟹
    SeqHRP x x' s k =
      LstSeqP s k (HPair x x') AND
      All2 l (SUCC k) (Ex sl (Ex sl' (HPair (Var l) (HPair (Var sl) (Var sl')) IN s AND
                ((OrdP (Var sl) AND WRP (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 s AND
                       HPair (Var n) (HPair (Var sn) (Var sn')) IN s AND
                       Var sl EQ HPair (Var sm) (Var sn) AND
                       Var sl' EQ Q_HPair (Var sm') (Var sn')))))))))))"
by (auto simp: eqvt_def SeqHRP_graph_aux_def flip_fresh_fresh) (metis obtain_fresh)

nominal_termination (eqvt)
  by lexicographic_order

lemma
 shows SeqHRP_fresh_iff [simp]:
      "a ♯ SeqHRP x x' s k ⟷ a ♯ x ∧ a ♯ x' ∧ a ♯ s ∧ a ♯ k"  (is ?thesis1)
  and SeqHRP_sf [iff]:  "Sigma_fm (SeqHRP x x' s k)"  (is ?thsf)
  and SeqHRP_imp_OrdP: "{ SeqHRP x y s k } ⊢ OrdP k"  (is ?thord)
  and SeqHRP_imp_LstSeqP: "{ SeqHRP x y s k } ⊢ LstSeqP s k (HPair x y)"  (is ?thlstseq)
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 ♯ (s,k,sl,sl',m,n,sm,sm',sn,sn')"
         "atom sl ♯ (s,sl',m,n,sm,sm',sn,sn')" "atom sl' ♯ (s,m,n,sm,sm',sn,sn')"
         "atom m ♯ (s,n,sm,sm',sn,sn')" "atom n ♯ (s,sm,sm',sn,sn')"
         "atom sm ♯ (s,sm',sn,sn')" "atom sm' ♯ (s,sn,sn')"
         "atom sn ♯ (s,sn')" "atom sn' ♯ (s)"
    by (metis obtain_fresh)
  thus ?thesis1 ?thsf ?thord ?thlstseq
    by (auto intro: LstSeqP_OrdP)
qed

lemma SeqHRP_subst [simp]:
      "(SeqHRP x x' s k)(i::=t) = SeqHRP (subst i t x) (subst i t x') (subst i t s) (subst i t 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 "atom l ♯ (s,k,t,i,sl,sl',m,n,sm,sm',sn,sn')"
          "atom sl ♯ (s,t,i,sl',m,n,sm,sm',sn,sn')"
          "atom sl' ♯ (s,t,i,m,n,sm,sm',sn,sn')"
          "atom m ♯ (s,t,i,n,sm,sm',sn,sn')" "atom n ♯ (s,t,i,sm,sm',sn,sn')"
          "atom sm ♯ (s,t,i,sm',sn,sn')" "atom sm' ♯ (s,t,i,sn,sn')"
          "atom sn ♯ (s,t,i,sn')" "atom sn' ♯ (s,t,i)"
    by (metis obtain_fresh)
  thus ?thesis
    by (auto simp: SeqHRP.simps [of l _ _ sl sl' m n sm sm' sn sn'])
qed

lemma SeqHRP_cong:
  assumes "H ⊢ x EQ x'" and "H ⊢ y EQ y'" "H ⊢ s EQ s'" and  "H ⊢ k EQ k'"
  shows "H ⊢ SeqHRP x y s k IFF SeqHRP x' y' s' k'"
  by (rule P4_cong [OF _ assms], auto)

subsection ‹Defining the syntax: main predicate›

nominal_function HRP :: "tm ⇒ tm ⇒ fm"
  where "⟦atom s ♯ (x,x',k); atom k ♯ (x,x')⟧ ⟹
         HRP x x' = Ex s (Ex k (SeqHRP x x' (Var s) (Var k)))"
  by (auto simp: eqvt_def HRP_graph_aux_def flip_fresh_fresh) (metis obtain_fresh)

nominal_termination (eqvt)
  by lexicographic_order

lemma
 shows HRP_fresh_iff [simp]: "a ♯ HRP x x' ⟷ a ♯ x ∧ a ♯ x'"  (is ?thesis1)
   and HRP_sf [iff]:         "Sigma_fm (HRP x x')"  (is ?thsf)
proof -
  obtain s::name and k::name  where "atom s ♯ (x,x',k)"  "atom k ♯ (x,x')"
    by (metis obtain_fresh)
  thus ?thesis1 ?thsf
    by auto
qed

lemma HRP_subst [simp]: "(HRP x x')(i::=t) = HRP (subst i t x) (subst i t x')"
proof -
  obtain s::name and k::name where "atom s ♯ (x,x',t,i,k)"  "atom k ♯ (x,x',t,i)"
    by (metis obtain_fresh)
  thus ?thesis
    by (auto simp: HRP.simps [of s _ _ k])
qed

subsection‹Proving that these relations are functions›

lemma SeqHRP_lemma:
  assumes "atom m ♯ (x,x',s,k,n,sm,sm',sn,sn')" "atom n ♯ (x,x',s,k,sm,sm',sn,sn')"
          "atom sm ♯ (x,x',s,k,sm',sn,sn')" "atom sm' ♯ (x,x',s,k,sn,sn')"
          "atom sn ♯ (x,x',s,k,sn')" "atom sn' ♯ (x,x',s,k)"
    shows "{ SeqHRP x x' s k }
         ⊢ (OrdP x AND WRP x x') OR
             Ex m (Ex n (Ex sm (Ex sm' (Ex sn (Ex sn' (Var m IN k AND Var n IN k AND
                       SeqHRP (Var sm) (Var sm') s (Var m) AND
                       SeqHRP (Var sn) (Var sn') s (Var n) AND
                       x EQ HPair (Var sm) (Var sn) AND
                       x' EQ Q_HPair (Var sm') (Var sn')))))))"
proof -
  obtain l::name and sl::name and sl'::name
    where atoms:
          "atom l ♯ (x,x',s,k,sl,sl',m,n,sm,sm',sn,sn')"
          "atom sl ♯ (x,x',s,k,sl',m,n,sm,sm',sn,sn')"
          "atom sl' ♯ (x,x',s,k,m,n,sm,sm',sn,sn')"
    by (metis obtain_fresh)
  thus ?thesis using atoms assms
    apply (simp add: SeqHRP.simps [of l s k sl sl' m n sm sm' sn sn'])
    apply (rule Conj_E)
    apply (rule All2_SUCC_E' [where t=k, THEN rotate2], simp_all)
    apply (rule rotate2)
    apply (rule Ex_E Conj_E)+
    apply (rule cut_same [where A = "HPair x x' EQ HPair (Var sl) (Var sl')"])
    apply (metis Assume LstSeqP_EQ rotate4, simp_all, clarify)
    apply (rule Disj_E [THEN rotate4])
    apply (rule Disj_I1)
    apply (metis Assume AssumeH(3) Sym thin1  Iff_MP_same [OF Conj_cong [OF OrdP_cong WRP_cong] Assume])
    ― ‹auto could be used but is VERY SLOW›
    apply (rule Disj_I2)
    apply (rule Ex_E 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 sm'"], simp)
    apply (rule Ex_I [where x = "Var sn"], simp)
    apply (rule Ex_I [where x = "Var sn'"], simp)
    apply (simp add: SeqHRP.simps [of l _ _ sl sl' m n sm sm' sn sn'])
    apply (rule Conj_I, blast)+
    ― ‹first SeqHRP subgoal›
    apply (rule Conj_I)+
    apply (blast intro: LstSeqP_Mem)
    apply (rule All2_Subset [OF Hyp], blast)
    apply (blast intro!: SUCC_Subset_Ord LstSeqP_OrdP, blast, simp)
    ― ‹next SeqHRP subgoal›
    apply (rule Conj_I)+
    apply (blast intro: LstSeqP_Mem)
    apply (rule All2_Subset [OF Hyp], blast)
    apply (auto intro!: SUCC_Subset_Ord LstSeqP_OrdP)
    ― ‹finally, the equality pair›
    apply (blast intro: Trans)+
    done
qed

lemma SeqHRP_unique: "{SeqHRP x y s u, SeqHRP x y' s' u'} ⊢ 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',y,y')"   "atom j ♯ (s,s',i,x,y,y')"  "atom j' ♯ (s,s',i,j,x,y,y')"
                  "atom k ♯ (s,s',x,y,y',u',i,j,j')" "atom k' ♯ (s,s',x,y,y',k,i,j,j')" "atom l ♯ (s,s',i,j,j',k,k')"
                  "atom m ♯ (s,s',i,j,j',k,k',l)"   "atom n ♯ (s,s',i,j,j',k,k',l,m)"
                  "atom sm ♯ (s,s',i,j,j',k,k',l,m,n)"  "atom sn ♯ (s,s',i,j,j',k,k',l,m,n,sm)"
                  "atom sm' ♯ (s,s',i,j,j',k,k',l,m,n,sm,sn)"   "atom sn' ♯ (s,s',i,j,j',k,k',l,m,n,sm,sn,sm')"
                  "atom m2 ♯ (s,s',i,j,j',k,k',l,m,n,sm,sn,sm',sn')"   "atom n2 ♯ (s,s',i,j,j',k,k',l,m,n,sm,sn,sm',sn',m2)"
                  "atom sm2 ♯ (s,s',i,j,j',k,k',l,m,n,sm,sn,sm',sn',m2,n2)"  "atom sn2 ♯ (s,s',i,j,j',k,k',l,m,n,sm,sn,sm',sn',m2,n2,sm2)"
                  "atom sm2' ♯ (s,s',i,j,j',k,k',l,m,n,sm,sn,sm',sn',m2,n2,sm2,sn2)"   "atom sn2' ♯ (s,s',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' (SeqHRP (Var i) (Var j) s (Var k) IMP (SeqHRP (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 SeqHRP_lemma [of m "Var i" "Var j" s "Var k" n sm sm' sn sn']], simp_all, blast)
    apply (rule cut_same)
    apply (rule cut1 [OF SeqHRP_lemma [of m2 "Var i" "Var j'" s' "Var k'" n2 sm2 sm2' sn2 sn2']], simp_all, blast)
    apply (rule Disj_EH Conj_EH)+
    ― ‹case 1, both are ordinals›
    apply (blast intro: cut3 [OF WRP_unique])
    ― ‹case 2, @{term "OrdP (Var i)"} but also a pair›
    apply (rule Conj_EH Ex_EH)+
    apply simp_all
    apply (rule cut_same [where A = "OrdP (HPair (Var sm) (Var sn))"])
    apply (blast intro: OrdP_cong [OF Hyp, THEN Iff_MP_same], blast)
    ― ‹towards second two cases›
    apply (rule Ex_E Disj_EH Conj_EH)+
    ― ‹case 3, @{term "OrdP (Var i)"} but also a pair›
    apply (rule cut_same [where A = "OrdP (HPair (Var sm2) (Var sn2))"])
    apply (blast intro: OrdP_cong [OF Hyp, THEN Iff_MP_same], blast)
    ― ‹case 4, two pairs›
    apply (rule Ex_E Disj_EH Conj_EH)+
    apply (rule All_E' [OF Hyp, where x="Var m"], blast)
    apply (rule All_E' [OF Hyp, where x="Var n"], blast, simp_all)
    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 = "HPair (Var sm) (Var sn) EQ HPair (Var sm2) (Var sn2)"])
    apply (blast intro: Sym Trans)
    apply (rule cut_same [where A = "SeqHRP (Var sn) (Var sn2') s' (Var n2)"])
    apply (blast intro: SeqHRP_cong [OF Hyp Refl Refl, THEN Iff_MP2_same])
    apply (rule cut_same [where A = "SeqHRP (Var sm) (Var sm2') s' (Var m2)"])
    apply (blast intro: SeqHRP_cong [OF Hyp Refl Refl, THEN Iff_MP2_same])
    apply (rule Disj_EH, blast intro: thin1 ContraProve)+
    apply (blast intro: Trans [OF Hyp Sym] intro!: HPair_cong)
    done
  hence "{OrdP (Var k)}
         ⊢ All j (All j' (All k' (SeqHRP x (Var j) s (Var k)
               IMP (SeqHRP x (Var j') s' (Var k') IMP Var j' EQ Var j))))"
    apply (rule All_D [where x = x, THEN cut_same])
    using atoms by auto
  hence "{OrdP (Var k)}
         ⊢ All j' (All k' (SeqHRP x y s (Var k) IMP (SeqHRP x (Var j') s' (Var k') IMP Var j' EQ y)))"
    apply (rule All_D [where x = y, THEN cut_same])
    using atoms by auto
  hence "{OrdP (Var k)}
          ⊢ All k' (SeqHRP x y s (Var k) IMP (SeqHRP x y' s' (Var k') IMP y' EQ y))"
    apply (rule All_D [where x = y', THEN cut_same])
    using atoms by auto
  hence "{OrdP (Var k)} ⊢ SeqHRP x y s (Var k) IMP (SeqHRP x y' s' u' IMP y' EQ y)"
    apply (rule All_D [where x = u', THEN cut_same])
    using atoms by auto
  hence "{SeqHRP x y s (Var k)} ⊢ SeqHRP x y s (Var k) IMP (SeqHRP x y' s' u' IMP y' EQ y)"
    by (metis SeqHRP_imp_OrdP cut1)
  hence "{} ⊢ ((SeqHRP x y s (Var k) IMP (SeqHRP x y' s' u' IMP y' EQ y)))(k::=u)"
    by (metis Subst emptyE Assume MP_same Imp_I)
  hence "{} ⊢ SeqHRP x y s u IMP (SeqHRP x y' s' u' IMP y' EQ y)"
    using atoms by simp
  thus ?thesis
    by (metis anti_deduction insert_commute)
qed

theorem HRP_unique: "{HRP x y, HRP x y'} ⊢ y' EQ y"
proof -
  obtain s::name and s'::name and k::name and k'::name
    where "atom s ♯ (x,y,y')" "atom s' ♯ (x,y,y',s)"
          "atom k ♯ (x,y,y',s,s')" "atom k' ♯ (x,y,y',s,s',k)"
    by (metis obtain_fresh)
  thus ?thesis
    by (auto simp: SeqHRP_unique HRP.simps [of s x y k]  HRP.simps [of s' x y' k'])
qed

lemma HRP_ORD_OF: "{} ⊢ HRP (ORD_OF i) «ORD_OF i»"
proof -
  let ?vs = "(i)"
  obtain s k 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 s ♯ (?vs,sl,sl',m,n,sm,sm',sn,sn',l,k)"
      "atom k ♯ (?vs,sl,sl',m,n,sm,sm',sn,sn',l)"
      "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)
  then show ?thesis
  apply (subst HRP.simps[of s _ _ k]; simp)
    apply (subst SeqHRP.simps[of l _ _ sl sl' m n sm sm' sn sn']; simp?)
    apply (rule Ex_I[where x="Eats Zero (HPair Zero (HPair (ORD_OF i) «ORD_OF i»))"]; simp)
    apply (rule Ex_I[where x="Zero"]; simp)
    apply (rule Conj_I[OF LstSeqP_single])
    apply (rule All2_SUCC_I, simp)
     apply auto [2]
    apply (rule Ex_I[where x="ORD_OF i"], simp)
    apply (rule Ex_I[where x="«ORD_OF i»"], simp)
    apply (auto intro!: Disj_I1 WRP Mem_Eats_I2)
    done
qed

lemma SeqHRP_HPair:
  assumes "atom s ♯ (k,s1,s2,k1,k2,x,y,x',y')" "atom k ♯ (s1,s2,k1,k2,x,y,x',y')"
  shows "{SeqHRP x x' s1 k1,
            SeqHRP y y' s2 k2}
           ⊢ Ex s (Ex k (SeqHRP (HPair x y) (Q_HPair x' y') (Var s) (Var k)))" (*<*)
proof -
  let ?vs = "(s1,s2,s,k1,k2,k,x,y,x',y')"
  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',sl,sl',m,n,sm,sm',sn,sn')"
      "atom kn ♯ (j,k',l,s1,s2,s,k1,k2,k,x,y,x',y',sl,sl',m,n,sm,sm',sn,sn')"
      "atom j ♯ (k',l,s1,s2,s,k1,k2,k,x,y,x',y',sl,sl',m,n,sm,sm',sn,sn')"
      and atoms: "atom k' ♯ (l,s1,s2,s,k1,k2,k,x,y,x',y',sl,sl',m,n,sm,sm',sn,sn')"
      "atom l ♯ (s1,s2,s,k1,k2,k,x,y,x',y',sl,sl',m,n,sm,sm',sn,sn')"
      "atom sl ♯ (s1,s2,s,k1,k2,k,x,y,x',y',sl',m,n,sm,sm',sn,sn')"
      "atom sl' ♯ (s1,s2,s,k1,k2,k,x,y,x',y',m,n,sm,sm',sn,sn')"
      "atom m ♯ (s1,s2,s,k1,k2,k,x,y,x',y',n,sm,sm',sn,sn')"
      "atom n ♯ (s1,s2,s,k1,k2,k,x,y,x',y',sm,sm',sn,sn')"
      "atom sm ♯ (s1,s2,s,k1,k2,k,x,y,x',y',sm',sn,sn')"
      "atom sm' ♯ (s1,s2,s,k1,k2,k,x,y,x',y',sn,sn')"
      "atom sn ♯ (s1,s2,s,k1,k2,k,x,y,x',y',sn')"
      "atom sn' ♯ (s1,s2,s,k1,k2,k,x,y,x',y')"
    by (metis obtain_fresh)
  let ?hyp = "{HaddP k1 k2 (Var k'), OrdP k1, OrdP k2, SeqAppendP s1 (SUCC k1) s2 (SUCC k2) (Var s),
               SeqHRP x x' s1 k1, SeqHRP y y' s2 k2}"
  show ?thesis
    using assms atoms
    apply (auto simp: SeqHRP.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 SeqHRP_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(HPair x y)(Q_HPair 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 SeqHRP_imp_LstSeqP [THEN cut1])
  proof (rule All2_SUCC_I, simp_all)
    show "?hyp ⊢     SyntaxN.Ex sl
     (SyntaxN.Ex sl'
       (HPair (SUCC (SUCC (Var k'))) (HPair (Var sl) (Var sl')) IN
        Eats (Var s) (HPair (SUCC (SUCC (Var k'))) (HPair (HPair x y) (Q_HPair x' y'))) AND
        (OrdP (Var sl) AND WRP (Var sl) (Var sl') OR
         SyntaxN.Ex m
          (SyntaxN.Ex n
            (SyntaxN.Ex sm
              (SyntaxN.Ex sm'
                (SyntaxN.Ex sn
                  (SyntaxN.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 (HPair x y) (Q_HPair x' y'))) AND
                     HPair (Var n) (HPair (Var sn) (Var sn')) IN
                     Eats (Var s) (HPair (SUCC (SUCC (Var k'))) (HPair (HPair x y) (Q_HPair x' y'))) AND
                     Var sl EQ HPair (Var sm) (Var sn) AND Var sl' EQ Q_HPair (Var sm') (Var sn'))))))))))"
      ― ‹verifying the final values›
      apply (rule Ex_I [where x="HPair x y"])
      using assms atoms apply simp
      apply (rule Ex_I [where x="Q_HPair 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 SeqHRP_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')))
     (SyntaxN.Ex sl
       (SyntaxN.Ex sl'
         (HPair (Var l) (HPair (Var sl) (Var sl')) IN
          Eats (Var s) (HPair (SUCC (SUCC (Var k'))) (HPair (HPair x y) (Q_HPair x' y'))) AND
          (OrdP (Var sl) AND WRP (Var sl) (Var sl') OR
           SyntaxN.Ex m
            (SyntaxN.Ex n
              (SyntaxN.Ex sm
                (SyntaxN.Ex sm'
                  (SyntaxN.Ex sn
                    (SyntaxN.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 (HPair x y) (Q_HPair x' y'))) AND
                       HPair (Var n) (HPair (Var sn) (Var sn')) IN
                       Eats (Var s) (HPair (SUCC (SUCC (Var k'))) (HPair (HPair x y) (Q_HPair x' y'))) AND
                       Var sl EQ HPair (Var sm) (Var sn) AND Var sl' EQ Q_HPair (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 atoms2 apply simp_all
          apply (rule AssumeH)
         apply (blast intro: OrdP_SUCC_I LstSeqP_OrdP)
        ― ‹... the sequence buildup via s1›
        apply (simp add: SeqHRP.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: SeqHRP.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 (*>*)

lemma HRP_HPair: "{HRP x x', HRP y y'} ⊢ HRP (HPair x y) (Q_HPair x' y')"
proof -
  obtain k1::name and s1::name and k2::name and s2::name and k::name and s::name
    where "atom s1 ♯ (x,y,x',y')"        "atom k1 ♯ (x,y,x',y',s1)"
      "atom s2 ♯ (x,y,x',y',k1,s1)"  "atom k2 ♯ (x,y,x',y',s2,k1,s1)"
      "atom s  ♯ (x,y,x',y',k2,s2,k1,s1)" "atom k  ♯ (x,y,x',y',s,k2,s2,k1,s1)"
    by (metis obtain_fresh)
  thus ?thesis
    by (force simp: HRP.simps [of s "HPair x y" _ k]
        HRP.simps [of s1 x _ k1]
        HRP.simps [of s2 y _ k2]
        intro: SeqHRP_HPair [THEN cut2])
qed

lemma HRP_HPair_quot: "{HRP x «x», HRP y «y»} ⊢ HRP (HPair x y) «HPair x y»"
  using HRP_HPair[of x "«x»" y "«y»"]
  unfolding HPair_def quot_simps by auto

lemma prove_HRP_coding_tm: fixes t::tm shows "coding_tm t ⟹ {} ⊢ HRP t «t»"
  by (induct t rule: coding_tm.induct)
    (auto simp: quot_simps HRP_ORD_OF HRP_HPair_quot[THEN cut2])

lemmas prove_HRP = prove_HRP_coding_tm[OF quot_fm_coding]

section‹The Function K and Lemma 6.3›

nominal_function KRP :: "tm ⇒ tm ⇒ tm ⇒ fm"
  where "atom y ♯ (v,x,x') ⟹
         KRP v x x' = Ex y (HRP x (Var y) AND SubstFormP v (Var y) x x')"
  by (auto simp: eqvt_def KRP_graph_aux_def flip_fresh_fresh) (metis obtain_fresh)

nominal_termination (eqvt)
  by lexicographic_order

lemma KRP_fresh_iff [simp]: "a ♯ KRP v x x' ⟷ a ♯ v ∧ a ♯ x ∧ a ♯ x'"
proof -
  obtain y::name where "atom y ♯ (v,x,x')"
    by (metis obtain_fresh)
  thus ?thesis
    by auto
qed

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

declare KRP.simps [simp del]

lemma prove_SubstFormP: "{} ⊢ SubstFormP «Var i» ««A»» «A» «A(i::=«A»)»"
  using SubstFormP by blast

lemma prove_KRP: "{} ⊢ KRP «Var i» «A» «A(i::=«A»)»"
  by (auto simp: KRP.simps [of y]
           intro!: Ex_I [where x="««A»»"] prove_HRP prove_SubstFormP)

lemma KRP_unique: "{KRP v x y, KRP v x y'} ⊢ y' EQ y"
proof -
  obtain u::name and u'::name where "atom u ♯ (v,x,y,y')" "atom u' ♯ (v,x,y,y',u)"
    by (metis obtain_fresh)
  thus ?thesis
    by (auto simp: KRP.simps [of u v x y] KRP.simps [of u' v x y']
             intro: SubstFormP_cong [THEN Iff_MP2_same]
                    SubstFormP_unique [THEN cut2] HRP_unique [THEN cut2])
qed

lemma KRP_subst_fm: "{KRP «Var i» «β» (Var j)} ⊢ Var j EQ «β(i::=«β»)»"
  by (metis KRP_unique cut0 prove_KRP)

end