[STATEMENT]
lemma QuoteP_Eats: "{QuoteP t1 u1, QuoteP t2 u2} \<turnstile> QuoteP (Eats t1 t2) (Q_Eats u1 u2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {QuoteP t1 u1, QuoteP t2 u2} \<turnstile> QuoteP (Eats t1 t2) (Q_Eats u1 u2)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. {QuoteP t1 u1, QuoteP t2 u2} \<turnstile> QuoteP (Eats t1 t2) (Q_Eats u1 u2)
[PROOF STEP]
obtain k1::name and s1::name and k2::name and s2::name and k::name and s::name
    where "atom s1 \<sharp> (t1,u1,t2,u2)"             "atom k1 \<sharp> (t1,u1,t2,u2,s1)"
          "atom s2 \<sharp> (t1,u1,t2,u2,k1,s1)"       "atom k2 \<sharp> (t1,u1,t2,u2,s2,k1,s1)"
          "atom s  \<sharp> (t1,u1,t2,u2,k2,s2,k1,s1)" "atom k  \<sharp> (t1,u1,t2,u2,s,k2,s2,k1,s1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>s1 k1 s2 k2 s k. \<lbrakk>atom s1 \<sharp> (t1, u1, t2, u2); atom k1 \<sharp> (t1, u1, t2, u2, s1); atom s2 \<sharp> (t1, u1, t2, u2, k1, s1); atom k2 \<sharp> (t1, u1, t2, u2, s2, k1, s1); atom s \<sharp> (t1, u1, t2, u2, k2, s2, k1, s1); atom k \<sharp> (t1, u1, t2, u2, s, k2, s2, k1, s1)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis obtain_fresh)
[PROOF STATE]
proof (state)
this:
atom s1 \<sharp> (t1, u1, t2, u2)
atom k1 \<sharp> (t1, u1, t2, u2, s1)
atom s2 \<sharp> (t1, u1, t2, u2, k1, s1)
atom k2 \<sharp> (t1, u1, t2, u2, s2, k1, s1)
atom s \<sharp> (t1, u1, t2, u2, k2, s2, k1, s1)
atom k \<sharp> (t1, u1, t2, u2, s, k2, s2, k1, s1)

goal (1 subgoal):
 1. {QuoteP t1 u1, QuoteP t2 u2} \<turnstile> QuoteP (Eats t1 t2) (Q_Eats u1 u2)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
atom s1 \<sharp> (t1, u1, t2, u2)
atom k1 \<sharp> (t1, u1, t2, u2, s1)
atom s2 \<sharp> (t1, u1, t2, u2, k1, s1)
atom k2 \<sharp> (t1, u1, t2, u2, s2, k1, s1)
atom s \<sharp> (t1, u1, t2, u2, k2, s2, k1, s1)
atom k \<sharp> (t1, u1, t2, u2, s, k2, s2, k1, s1)

goal (1 subgoal):
 1. {QuoteP t1 u1, QuoteP t2 u2} \<turnstile> QuoteP (Eats t1 t2) (Q_Eats u1 u2)
[PROOF STEP]
by (auto simp: QuoteP.simps [of s _ "(Q_Eats u1 u2)" k]
                   QuoteP.simps [of s1 t1 u1 k1] QuoteP.simps [of s2 t2 u2 k2]
             intro!: SeqQuoteP_Eats [THEN cut2])
[PROOF STATE]
proof (state)
this:
{QuoteP t1 u1, QuoteP t2 u2} \<turnstile> QuoteP (Eats t1 t2) (Q_Eats u1 u2)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma exists_QuoteP:
  assumes j: "atom j \<sharp> x"  shows "{} \<turnstile> Ex j (QuoteP x (Var j))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {} \<turnstile> SyntaxN.Ex j (QuoteP x (Var j))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. {} \<turnstile> SyntaxN.Ex j (QuoteP x (Var j))
[PROOF STEP]
obtain i::name and j'::name and k::name
    where atoms: "atom i \<sharp> (j,x)"  "atom j' \<sharp> (i,j,x)"  "atom (k::name) \<sharp> (i,j,j',x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>i j' k. \<lbrakk>atom i \<sharp> (j, x); atom j' \<sharp> (i, j, x); atom k \<sharp> (i, j, j', x)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis obtain_fresh)
[PROOF STATE]
proof (state)
this:
atom i \<sharp> (j, x)
atom j' \<sharp> (i, j, x)
atom k \<sharp> (i, j, j', x)

goal (1 subgoal):
 1. {} \<turnstile> SyntaxN.Ex j (QuoteP x (Var j))
[PROOF STEP]
have "{} \<turnstile> Ex j (QuoteP (Var i) (Var j))" (is "{} \<turnstile> ?scheme")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {} \<turnstile> SyntaxN.Ex j (QuoteP (Var i) (Var j))
[PROOF STEP]
proof (rule Ind [of k])
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. atom k \<sharp> (?i, SyntaxN.Ex j (QuoteP (Var i) (Var j)))
 2. {} \<turnstile> (SyntaxN.Ex j (QuoteP (Var i) (Var j)))(?i::=Zero)
 3. {} \<turnstile> SyntaxN.All ?i (SyntaxN.All k (SyntaxN.Ex j (QuoteP (Var i) (Var j)) IMP (SyntaxN.Ex j (QuoteP (Var i) (Var j)))(?i::=Var k) IMP (SyntaxN.Ex j (QuoteP (Var i) (Var j)))(?i::=Eats (Var ?i) (Var k))))
[PROOF STEP]
show "atom k \<sharp> (i, ?scheme)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. atom k \<sharp> (i, SyntaxN.Ex j (QuoteP (Var i) (Var j)))
[PROOF STEP]
using atoms
[PROOF STATE]
proof (prove)
using this:
atom i \<sharp> (j, x)
atom j' \<sharp> (i, j, x)
atom k \<sharp> (i, j, j', x)

goal (1 subgoal):
 1. atom k \<sharp> (i, SyntaxN.Ex j (QuoteP (Var i) (Var j)))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
atom k \<sharp> (i, SyntaxN.Ex j (QuoteP (Var i) (Var j)))

goal (2 subgoals):
 1. {} \<turnstile> (SyntaxN.Ex j (QuoteP (Var i) (Var j)))(i::=Zero)
 2. {} \<turnstile> SyntaxN.All i (SyntaxN.All k (SyntaxN.Ex j (QuoteP (Var i) (Var j)) IMP (SyntaxN.Ex j (QuoteP (Var i) (Var j)))(i::=Var k) IMP (SyntaxN.Ex j (QuoteP (Var i) (Var j)))(i::=Eats (Var i) (Var k))))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. {} \<turnstile> (SyntaxN.Ex j (QuoteP (Var i) (Var j)))(i::=Zero)
 2. {} \<turnstile> SyntaxN.All i (SyntaxN.All k (SyntaxN.Ex j (QuoteP (Var i) (Var j)) IMP (SyntaxN.Ex j (QuoteP (Var i) (Var j)))(i::=Var k) IMP (SyntaxN.Ex j (QuoteP (Var i) (Var j)))(i::=Eats (Var i) (Var k))))
[PROOF STEP]
show "{} \<turnstile> ?scheme(i::=Zero)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {} \<turnstile> (SyntaxN.Ex j (QuoteP (Var i) (Var j)))(i::=Zero)
[PROOF STEP]
using j atoms
[PROOF STATE]
proof (prove)
using this:
atom j \<sharp> x
atom i \<sharp> (j, x)
atom j' \<sharp> (i, j, x)
atom k \<sharp> (i, j, j', x)

goal (1 subgoal):
 1. {} \<turnstile> (SyntaxN.Ex j (QuoteP (Var i) (Var j)))(i::=Zero)
[PROOF STEP]
by (auto intro: Ex_I [where x=Zero] simp add: QuoteP_Zero)
[PROOF STATE]
proof (state)
this:
{} \<turnstile> (SyntaxN.Ex j (QuoteP (Var i) (Var j)))(i::=Zero)

goal (1 subgoal):
 1. {} \<turnstile> SyntaxN.All i (SyntaxN.All k (SyntaxN.Ex j (QuoteP (Var i) (Var j)) IMP (SyntaxN.Ex j (QuoteP (Var i) (Var j)))(i::=Var k) IMP (SyntaxN.Ex j (QuoteP (Var i) (Var j)))(i::=Eats (Var i) (Var k))))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. {} \<turnstile> SyntaxN.All i (SyntaxN.All k (SyntaxN.Ex j (QuoteP (Var i) (Var j)) IMP (SyntaxN.Ex j (QuoteP (Var i) (Var j)))(i::=Var k) IMP (SyntaxN.Ex j (QuoteP (Var i) (Var j)))(i::=Eats (Var i) (Var k))))
[PROOF STEP]
show "{} \<turnstile> All i (All k (?scheme IMP ?scheme(i::=Var k) IMP ?scheme(i::=Eats (Var i) (Var k))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {} \<turnstile> SyntaxN.All i (SyntaxN.All k (SyntaxN.Ex j (QuoteP (Var i) (Var j)) IMP (SyntaxN.Ex j (QuoteP (Var i) (Var j)))(i::=Var k) IMP (SyntaxN.Ex j (QuoteP (Var i) (Var j)))(i::=Eats (Var i) (Var k))))
[PROOF STEP]
apply (rule All_I Imp_I)+
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. {(SyntaxN.Ex j (QuoteP (Var i) (Var j)))(i::=Var k), SyntaxN.Ex j (QuoteP (Var i) (Var j))} \<turnstile> (SyntaxN.Ex j (QuoteP (Var i) (Var j)))(i::=Eats (Var i) (Var k))
 2. \<forall>C\<in>{}. atom k \<sharp> C
 3. \<forall>C\<in>{}. atom i \<sharp> C
[PROOF STEP]
using atoms assms
[PROOF STATE]
proof (prove)
using this:
atom i \<sharp> (j, x)
atom j' \<sharp> (i, j, x)
atom k \<sharp> (i, j, j', x)
atom j \<sharp> x

goal (3 subgoals):
 1. {(SyntaxN.Ex j (QuoteP (Var i) (Var j)))(i::=Var k), SyntaxN.Ex j (QuoteP (Var i) (Var j))} \<turnstile> (SyntaxN.Ex j (QuoteP (Var i) (Var j)))(i::=Eats (Var i) (Var k))
 2. \<forall>C\<in>{}. atom k \<sharp> C
 3. \<forall>C\<in>{}. atom i \<sharp> C
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>atom i \<sharp> (j, x); atom j' \<sharp> (i, j, x); atom k \<sharp> (i, j, j', x); atom j \<sharp> x\<rbrakk> \<Longrightarrow> {SyntaxN.Ex j (QuoteP (Var k) (Var j)), SyntaxN.Ex j (QuoteP (Var i) (Var j))} \<turnstile> SyntaxN.Ex j (QuoteP (Eats (Var i) (Var k)) (Var j))
[PROOF STEP]
apply (rule Ex_E)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>atom i \<sharp> (j, x); atom j' \<sharp> (i, j, x); atom k \<sharp> (i, j, j', x); atom j \<sharp> x\<rbrakk> \<Longrightarrow> {QuoteP (Var k) (Var j), SyntaxN.Ex j (QuoteP (Var i) (Var j))} \<turnstile> SyntaxN.Ex j (QuoteP (Eats (Var i) (Var k)) (Var j))
 2. \<lbrakk>atom i \<sharp> (j, x); atom j' \<sharp> (i, j, x); atom k \<sharp> (i, j, j', x); atom j \<sharp> x\<rbrakk> \<Longrightarrow> atom j \<sharp> SyntaxN.Ex j (QuoteP (Eats (Var i) (Var k)) (Var j))
 3. \<lbrakk>atom i \<sharp> (j, x); atom j' \<sharp> (i, j, x); atom k \<sharp> (i, j, j', x); atom j \<sharp> x\<rbrakk> \<Longrightarrow> \<forall>C\<in>{SyntaxN.Ex j (QuoteP (Var i) (Var j))}. atom j \<sharp> C
[PROOF STEP]
apply (rule Ex_E_with_renaming [where i'=j', THEN rotate2], auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>atom i \<sharp> (j, x); atom j' \<sharp> (i, j, x); atom k \<sharp> (i, j, j', x); atom j \<sharp> x\<rbrakk> \<Longrightarrow> {QuoteP (Var i) (Var j'), QuoteP (Var k) (Var j)} \<turnstile> SyntaxN.Ex j (QuoteP (Eats (Var i) (Var k)) (Var j))
[PROOF STEP]
apply (rule Ex_I [where x= "Q_Eats (Var j') (Var j)"], auto intro: QuoteP_Eats)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
{} \<turnstile> SyntaxN.All i (SyntaxN.All k (SyntaxN.Ex j (QuoteP (Var i) (Var j)) IMP (SyntaxN.Ex j (QuoteP (Var i) (Var j)))(i::=Var k) IMP (SyntaxN.Ex j (QuoteP (Var i) (Var j)))(i::=Eats (Var i) (Var k))))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
{} \<turnstile> SyntaxN.Ex j (QuoteP (Var i) (Var j))

goal (1 subgoal):
 1. {} \<turnstile> SyntaxN.Ex j (QuoteP x (Var j))
[PROOF STEP]
hence "{} \<turnstile> (Ex j (QuoteP (Var i) (Var j))) (i::= x)"
[PROOF STATE]
proof (prove)
using this:
{} \<turnstile> SyntaxN.Ex j (QuoteP (Var i) (Var j))

goal (1 subgoal):
 1. {} \<turnstile> (SyntaxN.Ex j (QuoteP (Var i) (Var j)))(i::=x)
[PROOF STEP]
by (rule Subst) auto
[PROOF STATE]
proof (state)
this:
{} \<turnstile> (SyntaxN.Ex j (QuoteP (Var i) (Var j)))(i::=x)

goal (1 subgoal):
 1. {} \<turnstile> SyntaxN.Ex j (QuoteP x (Var j))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
{} \<turnstile> (SyntaxN.Ex j (QuoteP (Var i) (Var j)))(i::=x)

goal (1 subgoal):
 1. {} \<turnstile> SyntaxN.Ex j (QuoteP x (Var j))
[PROOF STEP]
using atoms j
[PROOF STATE]
proof (prove)
using this:
{} \<turnstile> (SyntaxN.Ex j (QuoteP (Var i) (Var j)))(i::=x)
atom i \<sharp> (j, x)
atom j' \<sharp> (i, j, x)
atom k \<sharp> (i, j, j', x)
atom j \<sharp> x

goal (1 subgoal):
 1. {} \<turnstile> SyntaxN.Ex j (QuoteP x (Var j))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{} \<turnstile> SyntaxN.Ex j (QuoteP x (Var j))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma QuoteP_imp_ConstP: "{ QuoteP x y } \<turnstile> ConstP y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {QuoteP x y} \<turnstile> ConstP y
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. {QuoteP x y} \<turnstile> ConstP y
[PROOF STEP]
obtain j::name and j'::name and l::name and s::name and k::name
     and m::name and n::name and sm::name and sn::name and sm'::name and sn'::name
    where atoms: "atom j \<sharp> (x,y,s,k,j',l,m,n,sm,sm',sn,sn')"
             "atom j' \<sharp> (x,y,s,k,l,m,n,sm,sm',sn,sn')"
             "atom l \<sharp> (s,k,m,n,sm,sm',sn,sn')"
             "atom m \<sharp> (s,k,n,sm,sm',sn,sn')" "atom n \<sharp> (s,k,sm,sm',sn,sn')"
             "atom sm \<sharp> (s,k,sm',sn,sn')" "atom sm' \<sharp> (s,k,sn,sn')"
             "atom sn \<sharp> (s,k,sn')" "atom sn' \<sharp> (s,k)" "atom s \<sharp> (k,x,y)" "atom k \<sharp> (x,y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>j s k j' l m n sm sm' sn sn'. \<lbrakk>atom j \<sharp> (x, y, s, k, j', l, m, n, sm, sm', sn, sn'); atom j' \<sharp> (x, y, s, k, l, m, n, sm, sm', sn, sn'); atom l \<sharp> (s, k, m, n, sm, sm', sn, sn'); atom m \<sharp> (s, k, n, sm, sm', sn, sn'); atom n \<sharp> (s, k, sm, sm', sn, sn'); atom sm \<sharp> (s, k, sm', sn, sn'); atom sm' \<sharp> (s, k, sn, sn'); atom sn \<sharp> (s, k, sn'); atom sn' \<sharp> (s, k); atom s \<sharp> (k, x, y); atom k \<sharp> (x, y)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis obtain_fresh)
[PROOF STATE]
proof (state)
this:
atom j \<sharp> (x, y, s, k, j', l, m, n, sm, sm', sn, sn')
atom j' \<sharp> (x, y, s, k, l, m, n, sm, sm', sn, sn')
atom l \<sharp> (s, k, m, n, sm, sm', sn, sn')
atom m \<sharp> (s, k, n, sm, sm', sn, sn')
atom n \<sharp> (s, k, sm, sm', sn, sn')
atom sm \<sharp> (s, k, sm', sn, sn')
atom sm' \<sharp> (s, k, sn, sn')
atom sn \<sharp> (s, k, sn')
atom sn' \<sharp> (s, k)
atom s \<sharp> (k, x, y)
atom k \<sharp> (x, y)

goal (1 subgoal):
 1. {QuoteP x y} \<turnstile> ConstP y
[PROOF STEP]
have "{OrdP (Var k)}
        \<turnstile> All j (All j' (SeqQuoteP (Var j) (Var j') (Var s) (Var k) IMP ConstP (Var j')))"
        (is "_ \<turnstile> ?scheme")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {OrdP (Var k)} \<turnstile> SyntaxN.All j (SyntaxN.All j' (SeqQuoteP (Var j) (Var j') (Var s) (Var k) IMP ConstP (Var j')))
[PROOF STEP]
proof (rule OrdIndH [where j=l])
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. atom l \<sharp> (k, SyntaxN.All j (SyntaxN.All j' (SeqQuoteP (Var j) (Var j') (Var s) (Var k) IMP ConstP (Var j'))))
 2. {} \<turnstile> SyntaxN.All k (OrdP (Var k) IMP All2 l (Var k) ((SyntaxN.All j (SyntaxN.All j' (SeqQuoteP (Var j) (Var j') (Var s) (Var k) IMP ConstP (Var j'))))(k::=Var l)) IMP SyntaxN.All j (SyntaxN.All j' (SeqQuoteP (Var j) (Var j') (Var s) (Var k) IMP ConstP (Var j'))))
[PROOF STEP]
show "atom l \<sharp> (k, ?scheme)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. atom l \<sharp> (k, SyntaxN.All j (SyntaxN.All j' (SeqQuoteP (Var j) (Var j') (Var s) (Var k) IMP ConstP (Var j'))))
[PROOF STEP]
using atoms
[PROOF STATE]
proof (prove)
using this:
atom j \<sharp> (x, y, s, k, j', l, m, n, sm, sm', sn, sn')
atom j' \<sharp> (x, y, s, k, l, m, n, sm, sm', sn, sn')
atom l \<sharp> (s, k, m, n, sm, sm', sn, sn')
atom m \<sharp> (s, k, n, sm, sm', sn, sn')
atom n \<sharp> (s, k, sm, sm', sn, sn')
atom sm \<sharp> (s, k, sm', sn, sn')
atom sm' \<sharp> (s, k, sn, sn')
atom sn \<sharp> (s, k, sn')
atom sn' \<sharp> (s, k)
atom s \<sharp> (k, x, y)
atom k \<sharp> (x, y)

goal (1 subgoal):
 1. atom l \<sharp> (k, SyntaxN.All j (SyntaxN.All j' (SeqQuoteP (Var j) (Var j') (Var s) (Var k) IMP ConstP (Var j'))))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
atom l \<sharp> (k, SyntaxN.All j (SyntaxN.All j' (SeqQuoteP (Var j) (Var j') (Var s) (Var k) IMP ConstP (Var j'))))

goal (1 subgoal):
 1. {} \<turnstile> SyntaxN.All k (OrdP (Var k) IMP All2 l (Var k) ((SyntaxN.All j (SyntaxN.All j' (SeqQuoteP (Var j) (Var j') (Var s) (Var k) IMP ConstP (Var j'))))(k::=Var l)) IMP SyntaxN.All j (SyntaxN.All j' (SeqQuoteP (Var j) (Var j') (Var s) (Var k) IMP ConstP (Var j'))))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. {} \<turnstile> SyntaxN.All k (OrdP (Var k) IMP All2 l (Var k) ((SyntaxN.All j (SyntaxN.All j' (SeqQuoteP (Var j) (Var j') (Var s) (Var k) IMP ConstP (Var j'))))(k::=Var l)) IMP SyntaxN.All j (SyntaxN.All j' (SeqQuoteP (Var j) (Var j') (Var s) (Var k) IMP ConstP (Var j'))))
[PROOF STEP]
show "{} \<turnstile> All k (OrdP (Var k) IMP (All2 l (Var k) (?scheme(k::= Var l)) IMP ?scheme))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {} \<turnstile> SyntaxN.All k (OrdP (Var k) IMP All2 l (Var k) ((SyntaxN.All j (SyntaxN.All j' (SeqQuoteP (Var j) (Var j') (Var s) (Var k) IMP ConstP (Var j'))))(k::=Var l)) IMP SyntaxN.All j (SyntaxN.All j' (SeqQuoteP (Var j) (Var j') (Var s) (Var k) IMP ConstP (Var j'))))
[PROOF STEP]
apply (rule All_I Imp_I)+
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. {SeqQuoteP (Var j) (Var j') (Var s) (Var k), All2 l (Var k) ((SyntaxN.All j (SyntaxN.All j' (SeqQuoteP (Var j) (Var j') (Var s) (Var k) IMP ConstP (Var j'))))(k::=Var l)), OrdP (Var k)} \<turnstile> ConstP (Var j')
 2. \<forall>C\<in>{All2 l (Var k) ((SyntaxN.All j (SyntaxN.All j' (SeqQuoteP (Var j) (Var j') (Var s) (Var k) IMP ConstP (Var j'))))(k::=Var l)), OrdP (Var k)}. atom j' \<sharp> C
 3. \<forall>C\<in>{All2 l (Var k) ((SyntaxN.All j (SyntaxN.All j' (SeqQuoteP (Var j) (Var j') (Var s) (Var k) IMP ConstP (Var j'))))(k::=Var l)), OrdP (Var k)}. atom j \<sharp> C
 4. \<forall>C\<in>{}. atom k \<sharp> C
[PROOF STEP]
using atoms
[PROOF STATE]
proof (prove)
using this:
atom j \<sharp> (x, y, s, k, j', l, m, n, sm, sm', sn, sn')
atom j' \<sharp> (x, y, s, k, l, m, n, sm, sm', sn, sn')
atom l \<sharp> (s, k, m, n, sm, sm', sn, sn')
atom m \<sharp> (s, k, n, sm, sm', sn, sn')
atom n \<sharp> (s, k, sm, sm', sn, sn')
atom sm \<sharp> (s, k, sm', sn, sn')
atom sm' \<sharp> (s, k, sn, sn')
atom sn \<sharp> (s, k, sn')
atom sn' \<sharp> (s, k)
atom s \<sharp> (k, x, y)
atom k \<sharp> (x, y)

goal (4 subgoals):
 1. {SeqQuoteP (Var j) (Var j') (Var s) (Var k), All2 l (Var k) ((SyntaxN.All j (SyntaxN.All j' (SeqQuoteP (Var j) (Var j') (Var s) (Var k) IMP ConstP (Var j'))))(k::=Var l)), OrdP (Var k)} \<turnstile> ConstP (Var j')
 2. \<forall>C\<in>{All2 l (Var k) ((SyntaxN.All j (SyntaxN.All j' (SeqQuoteP (Var j) (Var j') (Var s) (Var k) IMP ConstP (Var j'))))(k::=Var l)), OrdP (Var k)}. atom j' \<sharp> C
 3. \<forall>C\<in>{All2 l (Var k) ((SyntaxN.All j (SyntaxN.All j' (SeqQuoteP (Var j) (Var j') (Var s) (Var k) IMP ConstP (Var j'))))(k::=Var l)), OrdP (Var k)}. atom j \<sharp> C
 4. \<forall>C\<in>{}. atom k \<sharp> C
[PROOF STEP]
apply (simp_all add: fresh_at_base fresh_finite_set_at_base)
        \<comment> \<open>freshness finally proved!\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>atom j \<sharp> (x, y, s, k, j', l, m, n, sm, sm', sn, sn'); atom j' \<sharp> (x, y, s, k, l, m, n, sm, sm', sn, sn'); atom l \<sharp> (s, k, m, n, sm, sm', sn, sn'); atom m \<sharp> (s, k, n, sm, sm', sn, sn'); atom n \<sharp> (s, k, sm, sm', sn, sn'); atom sm \<sharp> (s, k, sm', sn, sn'); atom sm' \<sharp> (s, k, sn, sn'); atom sn \<sharp> (s, k, sn'); atom sn' \<sharp> (s, k); atom s \<sharp> (k, x, y); atom k \<sharp> (x, y)\<rbrakk> \<Longrightarrow> {SeqQuoteP (Var j) (Var j') (Var s) (Var k), All2 l (Var k) (SyntaxN.All j (SyntaxN.All j' (SeqQuoteP (Var j) (Var j') (Var s) (Var l) IMP ConstP (Var j')))), OrdP (Var k)} \<turnstile> ConstP (Var j')
[PROOF STEP]
apply (rule cut_same)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>atom j \<sharp> (x, y, s, k, j', l, m, n, sm, sm', sn, sn'); atom j' \<sharp> (x, y, s, k, l, m, n, sm, sm', sn, sn'); atom l \<sharp> (s, k, m, n, sm, sm', sn, sn'); atom m \<sharp> (s, k, n, sm, sm', sn, sn'); atom n \<sharp> (s, k, sm, sm', sn, sn'); atom sm \<sharp> (s, k, sm', sn, sn'); atom sm' \<sharp> (s, k, sn, sn'); atom sn \<sharp> (s, k, sn'); atom sn' \<sharp> (s, k); atom s \<sharp> (k, x, y); atom k \<sharp> (x, y)\<rbrakk> \<Longrightarrow> {SeqQuoteP (Var j) (Var j') (Var s) (Var k), All2 l (Var k) (SyntaxN.All j (SyntaxN.All j' (SeqQuoteP (Var j) (Var j') (Var s) (Var l) IMP ConstP (Var j')))), OrdP (Var k)} \<turnstile> ?A59
 2. \<lbrakk>atom j \<sharp> (x, y, s, k, j', l, m, n, sm, sm', sn, sn'); atom j' \<sharp> (x, y, s, k, l, m, n, sm, sm', sn, sn'); atom l \<sharp> (s, k, m, n, sm, sm', sn, sn'); atom m \<sharp> (s, k, n, sm, sm', sn, sn'); atom n \<sharp> (s, k, sm, sm', sn, sn'); atom sm \<sharp> (s, k, sm', sn, sn'); atom sm' \<sharp> (s, k, sn, sn'); atom sn \<sharp> (s, k, sn'); atom sn' \<sharp> (s, k); atom s \<sharp> (k, x, y); atom k \<sharp> (x, y)\<rbrakk> \<Longrightarrow> {?A59, SeqQuoteP (Var j) (Var j') (Var s) (Var k), All2 l (Var k) (SyntaxN.All j (SyntaxN.All j' (SeqQuoteP (Var j) (Var j') (Var s) (Var l) IMP ConstP (Var j')))), OrdP (Var k)} \<turnstile> ConstP (Var j')
[PROOF STEP]
apply (rule cut1 [OF SeqQuoteP_lemma [of m "Var j" "Var j'" "Var s" "Var k" n sm sm' sn sn']], simp_all, blast)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>atom j \<sharp> (x, y, s, k, j', l, m, n, sm, sm', sn, sn'); atom j' \<sharp> (x, y, s, k, l, m, n, sm, sm', sn, sn'); atom l \<sharp> (s, k, m, n, sm, sm', sn, sn'); atom m \<sharp> (s, k, n, sm, sm', sn, sn'); atom n \<sharp> (s, k, sm, sm', sn, sn'); atom sm \<sharp> (s, k, sm', sn, sn'); atom sm' \<sharp> (s, k, sn, sn'); atom sn \<sharp> (s, k, sn'); atom sn' \<sharp> (s, k); atom s \<sharp> (k, x, y); atom k \<sharp> (x, y)\<rbrakk> \<Longrightarrow> {Var j EQ Zero AND Var j' EQ Zero OR SyntaxN.Ex m (SyntaxN.Ex n (SyntaxN.Ex sm (SyntaxN.Ex sm' (SyntaxN.Ex sn (SyntaxN.Ex sn' (Var m IN Var k AND Var n IN Var k AND SeqQuoteP (Var sm) (Var sm') (Var s) (Var m) AND SeqQuoteP (Var sn) (Var sn') (Var s) (Var n) AND Var j EQ Eats (Var sm) (Var sn) AND Var j' EQ Q_Eats (Var sm') (Var sn'))))))), SeqQuoteP (Var j) (Var j') (Var s) (Var k), All2 l (Var k) (SyntaxN.All j (SyntaxN.All j' (SeqQuoteP (Var j) (Var j') (Var s) (Var l) IMP ConstP (Var j')))), OrdP (Var k)} \<turnstile> ConstP (Var j')
[PROOF STEP]
apply (rule Imp_I Disj_EH Conj_EH)+
        \<comment> \<open>case 1, Var j EQ Zero\<close>
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>atom j \<sharp> (x, y, s, k, j', l, m, n, sm, sm', sn, sn'); atom j' \<sharp> (x, y, s, k, l, m, n, sm, sm', sn, sn'); atom l \<sharp> (s, k, m, n, sm, sm', sn, sn'); atom m \<sharp> (s, k, n, sm, sm', sn, sn'); atom n \<sharp> (s, k, sm, sm', sn, sn'); atom sm \<sharp> (s, k, sm', sn, sn'); atom sm' \<sharp> (s, k, sn, sn'); atom sn \<sharp> (s, k, sn'); atom sn' \<sharp> (s, k); atom s \<sharp> (k, x, y); atom k \<sharp> (x, y)\<rbrakk> \<Longrightarrow> {Var j EQ Zero, Var j' EQ Zero, SeqQuoteP (Var j) (Var j') (Var s) (Var k), All2 l (Var k) (SyntaxN.All j (SyntaxN.All j' (SeqQuoteP (Var j) (Var j') (Var s) (Var l) IMP ConstP (Var j')))), OrdP (Var k)} \<turnstile> ConstP (Var j')
 2. \<lbrakk>atom j \<sharp> (x, y, s, k, j', l, m, n, sm, sm', sn, sn'); atom j' \<sharp> (x, y, s, k, l, m, n, sm, sm', sn, sn'); atom l \<sharp> (s, k, m, n, sm, sm', sn, sn'); atom m \<sharp> (s, k, n, sm, sm', sn, sn'); atom n \<sharp> (s, k, sm, sm', sn, sn'); atom sm \<sharp> (s, k, sm', sn, sn'); atom sm' \<sharp> (s, k, sn, sn'); atom sn \<sharp> (s, k, sn'); atom sn' \<sharp> (s, k); atom s \<sharp> (k, x, y); atom k \<sharp> (x, y)\<rbrakk> \<Longrightarrow> {SyntaxN.Ex m (SyntaxN.Ex n (SyntaxN.Ex sm (SyntaxN.Ex sm' (SyntaxN.Ex sn (SyntaxN.Ex sn' (Var m IN Var k AND Var n IN Var k AND SeqQuoteP (Var sm) (Var sm') (Var s) (Var m) AND SeqQuoteP (Var sn) (Var sn') (Var s) (Var n) AND Var j EQ Eats (Var sm) (Var sn) AND Var j' EQ Q_Eats (Var sm') (Var sn'))))))), SeqQuoteP (Var j) (Var j') (Var s) (Var k), All2 l (Var k) (SyntaxN.All j (SyntaxN.All j' (SeqQuoteP (Var j) (Var j') (Var s) (Var l) IMP ConstP (Var j')))), OrdP (Var k)} \<turnstile> ConstP (Var j')
[PROOF STEP]
apply (rule thin1)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>atom j \<sharp> (x, y, s, k, j', l, m, n, sm, sm', sn, sn'); atom j' \<sharp> (x, y, s, k, l, m, n, sm, sm', sn, sn'); atom l \<sharp> (s, k, m, n, sm, sm', sn, sn'); atom m \<sharp> (s, k, n, sm, sm', sn, sn'); atom n \<sharp> (s, k, sm, sm', sn, sn'); atom sm \<sharp> (s, k, sm', sn, sn'); atom sm' \<sharp> (s, k, sn, sn'); atom sn \<sharp> (s, k, sn'); atom sn' \<sharp> (s, k); atom s \<sharp> (k, x, y); atom k \<sharp> (x, y)\<rbrakk> \<Longrightarrow> {Var j' EQ Zero, SeqQuoteP (Var j) (Var j') (Var s) (Var k), All2 l (Var k) (SyntaxN.All j (SyntaxN.All j' (SeqQuoteP (Var j) (Var j') (Var s) (Var l) IMP ConstP (Var j')))), OrdP (Var k)} \<turnstile> ConstP (Var j')
 2. \<lbrakk>atom j \<sharp> (x, y, s, k, j', l, m, n, sm, sm', sn, sn'); atom j' \<sharp> (x, y, s, k, l, m, n, sm, sm', sn, sn'); atom l \<sharp> (s, k, m, n, sm, sm', sn, sn'); atom m \<sharp> (s, k, n, sm, sm', sn, sn'); atom n \<sharp> (s, k, sm, sm', sn, sn'); atom sm \<sharp> (s, k, sm', sn, sn'); atom sm' \<sharp> (s, k, sn, sn'); atom sn \<sharp> (s, k, sn'); atom sn' \<sharp> (s, k); atom s \<sharp> (k, x, y); atom k \<sharp> (x, y)\<rbrakk> \<Longrightarrow> {SyntaxN.Ex m (SyntaxN.Ex n (SyntaxN.Ex sm (SyntaxN.Ex sm' (SyntaxN.Ex sn (SyntaxN.Ex sn' (Var m IN Var k AND Var n IN Var k AND SeqQuoteP (Var sm) (Var sm') (Var s) (Var m) AND SeqQuoteP (Var sn) (Var sn') (Var s) (Var n) AND Var j EQ Eats (Var sm) (Var sn) AND Var j' EQ Q_Eats (Var sm') (Var sn'))))))), SeqQuoteP (Var j) (Var j') (Var s) (Var k), All2 l (Var k) (SyntaxN.All j (SyntaxN.All j' (SeqQuoteP (Var j) (Var j') (Var s) (Var l) IMP ConstP (Var j')))), OrdP (Var k)} \<turnstile> ConstP (Var j')
[PROOF STEP]
apply (rule Var_Eq_subst_Iff [THEN Iff_MP_same], simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>atom j \<sharp> (x, y, s, k, j', l, m, n, sm, sm', sn, sn'); atom j' \<sharp> (x, y, s, k, l, m, n, sm, sm', sn, sn'); atom l \<sharp> (s, k, m, n, sm, sm', sn, sn'); atom m \<sharp> (s, k, n, sm, sm', sn, sn'); atom n \<sharp> (s, k, sm, sm', sn, sn'); atom sm \<sharp> (s, k, sm', sn, sn'); atom sm' \<sharp> (s, k, sn, sn'); atom sn \<sharp> (s, k, sn'); atom sn' \<sharp> (s, k); atom s \<sharp> (k, x, y); atom k \<sharp> (x, y)\<rbrakk> \<Longrightarrow> {Var j' EQ Zero, SeqQuoteP (Var j) (Var j') (Var s) (Var k), All2 l (Var k) (SyntaxN.All j (SyntaxN.All j' (SeqQuoteP (Var j) (Var j') (Var s) (Var l) IMP ConstP (Var j')))), OrdP (Var k)} \<turnstile> ConstP Zero
 2. \<lbrakk>atom j \<sharp> (x, y, s, k, j', l, m, n, sm, sm', sn, sn'); atom j' \<sharp> (x, y, s, k, l, m, n, sm, sm', sn, sn'); atom l \<sharp> (s, k, m, n, sm, sm', sn, sn'); atom m \<sharp> (s, k, n, sm, sm', sn, sn'); atom n \<sharp> (s, k, sm, sm', sn, sn'); atom sm \<sharp> (s, k, sm', sn, sn'); atom sm' \<sharp> (s, k, sn, sn'); atom sn \<sharp> (s, k, sn'); atom sn' \<sharp> (s, k); atom s \<sharp> (k, x, y); atom k \<sharp> (x, y)\<rbrakk> \<Longrightarrow> {SyntaxN.Ex m (SyntaxN.Ex n (SyntaxN.Ex sm (SyntaxN.Ex sm' (SyntaxN.Ex sn (SyntaxN.Ex sn' (Var m IN Var k AND Var n IN Var k AND SeqQuoteP (Var sm) (Var sm') (Var s) (Var m) AND SeqQuoteP (Var sn) (Var sn') (Var s) (Var n) AND Var j EQ Eats (Var sm) (Var sn) AND Var j' EQ Q_Eats (Var sm') (Var sn'))))))), SeqQuoteP (Var j) (Var j') (Var s) (Var k), All2 l (Var k) (SyntaxN.All j (SyntaxN.All j' (SeqQuoteP (Var j) (Var j') (Var s) (Var l) IMP ConstP (Var j')))), OrdP (Var k)} \<turnstile> ConstP (Var j')
[PROOF STEP]
apply (metis thin0 ConstP_Zero)
        \<comment> \<open>case 2, @{term "Var j EQ Eats (Var sm) (Var sn)"}\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>atom j \<sharp> (x, y, s, k, j', l, m, n, sm, sm', sn, sn'); atom j' \<sharp> (x, y, s, k, l, m, n, sm, sm', sn, sn'); atom l \<sharp> (s, k, m, n, sm, sm', sn, sn'); atom m \<sharp> (s, k, n, sm, sm', sn, sn'); atom n \<sharp> (s, k, sm, sm', sn, sn'); atom sm \<sharp> (s, k, sm', sn, sn'); atom sm' \<sharp> (s, k, sn, sn'); atom sn \<sharp> (s, k, sn'); atom sn' \<sharp> (s, k); atom s \<sharp> (k, x, y); atom k \<sharp> (x, y)\<rbrakk> \<Longrightarrow> {SyntaxN.Ex m (SyntaxN.Ex n (SyntaxN.Ex sm (SyntaxN.Ex sm' (SyntaxN.Ex sn (SyntaxN.Ex sn' (Var m IN Var k AND Var n IN Var k AND SeqQuoteP (Var sm) (Var sm') (Var s) (Var m) AND SeqQuoteP (Var sn) (Var sn') (Var s) (Var n) AND Var j EQ Eats (Var sm) (Var sn) AND Var j' EQ Q_Eats (Var sm') (Var sn'))))))), SeqQuoteP (Var j) (Var j') (Var s) (Var k), All2 l (Var k) (SyntaxN.All j (SyntaxN.All j' (SeqQuoteP (Var j) (Var j') (Var s) (Var l) IMP ConstP (Var j')))), OrdP (Var k)} \<turnstile> ConstP (Var j')
[PROOF STEP]
apply (rule Imp_I Conj_EH Ex_EH)+
[PROOF STATE]
proof (prove)
goal (13 subgoals):
 1. \<lbrakk>atom j \<sharp> (x, y, s, k, j', l, m, n, sm, sm', sn, sn'); atom j' \<sharp> (x, y, s, k, l, m, n, sm, sm', sn, sn'); atom l \<sharp> (s, k, m, n, sm, sm', sn, sn'); atom m \<sharp> (s, k, n, sm, sm', sn, sn'); atom n \<sharp> (s, k, sm, sm', sn, sn'); atom sm \<sharp> (s, k, sm', sn, sn'); atom sm' \<sharp> (s, k, sn, sn'); atom sn \<sharp> (s, k, sn'); atom sn' \<sharp> (s, k); atom s \<sharp> (k, x, y); atom k \<sharp> (x, y)\<rbrakk> \<Longrightarrow> {Var j EQ Eats (Var sm) (Var sn), Var j' EQ Q_Eats (Var sm') (Var sn'), SeqQuoteP (Var sn) (Var sn') (Var s) (Var n), SeqQuoteP (Var sm) (Var sm') (Var s) (Var m), Var n IN Var k, Var m IN Var k, SeqQuoteP (Var j) (Var j') (Var s) (Var k), All2 l (Var k) (SyntaxN.All j (SyntaxN.All j' (SeqQuoteP (Var j) (Var j') (Var s) (Var l) IMP ConstP (Var j')))), OrdP (Var k)} \<turnstile> ConstP (Var j')
 2. \<lbrakk>atom j \<sharp> (x, y, s, k, j', l, m, n, sm, sm', sn, sn'); atom j' \<sharp> (x, y, s, k, l, m, n, sm, sm', sn, sn'); atom l \<sharp> (s, k, m, n, sm, sm', sn, sn'); atom m \<sharp> (s, k, n, sm, sm', sn, sn'); atom n \<sharp> (s, k, sm, sm', sn, sn'); atom sm \<sharp> (s, k, sm', sn, sn'); atom sm' \<sharp> (s, k, sn, sn'); atom sn \<sharp> (s, k, sn'); atom sn' \<sharp> (s, k); atom s \<sharp> (k, x, y); atom k \<sharp> (x, y)\<rbrakk> \<Longrightarrow> atom sn' \<sharp> ConstP (Var j')
 3. \<lbrakk>atom j \<sharp> (x, y, s, k, j', l, m, n, sm, sm', sn, sn'); atom j' \<sharp> (x, y, s, k, l, m, n, sm, sm', sn, sn'); atom l \<sharp> (s, k, m, n, sm, sm', sn, sn'); atom m \<sharp> (s, k, n, sm, sm', sn, sn'); atom n \<sharp> (s, k, sm, sm', sn, sn'); atom sm \<sharp> (s, k, sm', sn, sn'); atom sm' \<sharp> (s, k, sn, sn'); atom sn \<sharp> (s, k, sn'); atom sn' \<sharp> (s, k); atom s \<sharp> (k, x, y); atom k \<sharp> (x, y)\<rbrakk> \<Longrightarrow> \<forall>C\<in>{SeqQuoteP (Var j) (Var j') (Var s) (Var k), All2 l (Var k) (SyntaxN.All j (SyntaxN.All j' (SeqQuoteP (Var j) (Var j') (Var s) (Var l) IMP ConstP (Var j')))), OrdP (Var k)}. atom sn' \<sharp> C
 4. \<lbrakk>atom j \<sharp> (x, y, s, k, j', l, m, n, sm, sm', sn, sn'); atom j' \<sharp> (x, y, s, k, l, m, n, sm, sm', sn, sn'); atom l \<sharp> (s, k, m, n, sm, sm', sn, sn'); atom m \<sharp> (s, k, n, sm, sm', sn, sn'); atom n \<sharp> (s, k, sm, sm', sn, sn'); atom sm \<sharp> (s, k, sm', sn, sn'); atom sm' \<sharp> (s, k, sn, sn'); atom sn \<sharp> (s, k, sn'); atom sn' \<sharp> (s, k); atom s \<sharp> (k, x, y); atom k \<sharp> (x, y)\<rbrakk> \<Longrightarrow> atom sn \<sharp> ConstP (Var j')
 5. \<lbrakk>atom j \<sharp> (x, y, s, k, j', l, m, n, sm, sm', sn, sn'); atom j' \<sharp> (x, y, s, k, l, m, n, sm, sm', sn, sn'); atom l \<sharp> (s, k, m, n, sm, sm', sn, sn'); atom m \<sharp> (s, k, n, sm, sm', sn, sn'); atom n \<sharp> (s, k, sm, sm', sn, sn'); atom sm \<sharp> (s, k, sm', sn, sn'); atom sm' \<sharp> (s, k, sn, sn'); atom sn \<sharp> (s, k, sn'); atom sn' \<sharp> (s, k); atom s \<sharp> (k, x, y); atom k \<sharp> (x, y)\<rbrakk> \<Longrightarrow> \<forall>C\<in>{SeqQuoteP (Var j) (Var j') (Var s) (Var k), All2 l (Var k) (SyntaxN.All j (SyntaxN.All j' (SeqQuoteP (Var j) (Var j') (Var s) (Var l) IMP ConstP (Var j')))), OrdP (Var k)}. atom sn \<sharp> C
 6. \<lbrakk>atom j \<sharp> (x, y, s, k, j', l, m, n, sm, sm', sn, sn'); atom j' \<sharp> (x, y, s, k, l, m, n, sm, sm', sn, sn'); atom l \<sharp> (s, k, m, n, sm, sm', sn, sn'); atom m \<sharp> (s, k, n, sm, sm', sn, sn'); atom n \<sharp> (s, k, sm, sm', sn, sn'); atom sm \<sharp> (s, k, sm', sn, sn'); atom sm' \<sharp> (s, k, sn, sn'); atom sn \<sharp> (s, k, sn'); atom sn' \<sharp> (s, k); atom s \<sharp> (k, x, y); atom k \<sharp> (x, y)\<rbrakk> \<Longrightarrow> atom sm' \<sharp> ConstP (Var j')
 7. \<lbrakk>atom j \<sharp> (x, y, s, k, j', l, m, n, sm, sm', sn, sn'); atom j' \<sharp> (x, y, s, k, l, m, n, sm, sm', sn, sn'); atom l \<sharp> (s, k, m, n, sm, sm', sn, sn'); atom m \<sharp> (s, k, n, sm, sm', sn, sn'); atom n \<sharp> (s, k, sm, sm', sn, sn'); atom sm \<sharp> (s, k, sm', sn, sn'); atom sm' \<sharp> (s, k, sn, sn'); atom sn \<sharp> (s, k, sn'); atom sn' \<sharp> (s, k); atom s \<sharp> (k, x, y); atom k \<sharp> (x, y)\<rbrakk> \<Longrightarrow> \<forall>C\<in>{SeqQuoteP (Var j) (Var j') (Var s) (Var k), All2 l (Var k) (SyntaxN.All j (SyntaxN.All j' (SeqQuoteP (Var j) (Var j') (Var s) (Var l) IMP ConstP (Var j')))), OrdP (Var k)}. atom sm' \<sharp> C
 8. \<lbrakk>atom j \<sharp> (x, y, s, k, j', l, m, n, sm, sm', sn, sn'); atom j' \<sharp> (x, y, s, k, l, m, n, sm, sm', sn, sn'); atom l \<sharp> (s, k, m, n, sm, sm', sn, sn'); atom m \<sharp> (s, k, n, sm, sm', sn, sn'); atom n \<sharp> (s, k, sm, sm', sn, sn'); atom sm \<sharp> (s, k, sm', sn, sn'); atom sm' \<sharp> (s, k, sn, sn'); atom sn \<sharp> (s, k, sn'); atom sn' \<sharp> (s, k); atom s \<sharp> (k, x, y); atom k \<sharp> (x, y)\<rbrakk> \<Longrightarrow> atom sm \<sharp> ConstP (Var j')
 9. \<lbrakk>atom j \<sharp> (x, y, s, k, j', l, m, n, sm, sm', sn, sn'); atom j' \<sharp> (x, y, s, k, l, m, n, sm, sm', sn, sn'); atom l \<sharp> (s, k, m, n, sm, sm', sn, sn'); atom m \<sharp> (s, k, n, sm, sm', sn, sn'); atom n \<sharp> (s, k, sm, sm', sn, sn'); atom sm \<sharp> (s, k, sm', sn, sn'); atom sm' \<sharp> (s, k, sn, sn'); atom sn \<sharp> (s, k, sn'); atom sn' \<sharp> (s, k); atom s \<sharp> (k, x, y); atom k \<sharp> (x, y)\<rbrakk> \<Longrightarrow> \<forall>C\<in>{SeqQuoteP (Var j) (Var j') (Var s) (Var k), All2 l (Var k) (SyntaxN.All j (SyntaxN.All j' (SeqQuoteP (Var j) (Var j') (Var s) (Var l) IMP ConstP (Var j')))), OrdP (Var k)}. atom sm \<sharp> C
 10. \<lbrakk>atom j \<sharp> (x, y, s, k, j', l, m, n, sm, sm', sn, sn'); atom j' \<sharp> (x, y, s, k, l, m, n, sm, sm', sn, sn'); atom l \<sharp> (s, k, m, n, sm, sm', sn, sn'); atom m \<sharp> (s, k, n, sm, sm', sn, sn'); atom n \<sharp> (s, k, sm, sm', sn, sn'); atom sm \<sharp> (s, k, sm', sn, sn'); atom sm' \<sharp> (s, k, sn, sn'); atom sn \<sharp> (s, k, sn'); atom sn' \<sharp> (s, k); atom s \<sharp> (k, x, y); atom k \<sharp> (x, y)\<rbrakk> \<Longrightarrow> atom n \<sharp> ConstP (Var j')
A total of 13 subgoals...
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>atom j \<sharp> (x, y, s, k, j', l, m, n, sm, sm', sn, sn'); atom j' \<sharp> (x, y, s, k, l, m, n, sm, sm', sn, sn'); atom l \<sharp> (s, k, m, n, sm, sm', sn, sn'); atom m \<sharp> (s, k, n, sm, sm', sn, sn'); atom n \<sharp> (s, k, sm, sm', sn, sn'); atom sm \<sharp> (s, k, sm', sn, sn'); atom sm' \<sharp> (s, k, sn, sn'); atom sn \<sharp> (s, k, sn'); atom sn' \<sharp> (s, k); atom s \<sharp> (k, x, y); atom k \<sharp> (x, y)\<rbrakk> \<Longrightarrow> {Var j EQ Eats (Var sm) (Var sn), Var j' EQ Q_Eats (Var sm') (Var sn'), SeqQuoteP (Var sn) (Var sn') (Var s) (Var n), SeqQuoteP (Var sm) (Var sm') (Var s) (Var m), Var n IN Var k, Var m IN Var k, SeqQuoteP (Var j) (Var j') (Var s) (Var k), All2 l (Var k) (SyntaxN.All j (SyntaxN.All j' (SeqQuoteP (Var j) (Var j') (Var s) (Var l) IMP ConstP (Var j')))), OrdP (Var k)} \<turnstile> ConstP (Var j')
[PROOF STEP]
apply (rule Var_Eq_subst_Iff [THEN Iff_MP_same, THEN rotate2], simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>atom j \<sharp> (x, y, s, k, j', l, m, n, sm, sm', sn, sn'); atom j' \<sharp> (x, y, s, k, l, m, n, sm, sm', sn, sn'); atom l \<sharp> (s, k, m, n, sm, sm', sn, sn'); atom m \<sharp> (s, k, n, sm, sm', sn, sn'); atom n \<sharp> (s, k, sm, sm', sn, sn'); atom sm \<sharp> (s, k, sm', sn, sn'); atom sm' \<sharp> (s, k, sn, sn'); atom sn \<sharp> (s, k, sn'); atom sn' \<sharp> (s, k); atom s \<sharp> (k, x, y); atom k \<sharp> (x, y)\<rbrakk> \<Longrightarrow> {Var j' EQ Q_Eats (Var sm') (Var sn'), Var j EQ Eats (Var sm) (Var sn), SeqQuoteP (Var sn) (Var sn') (Var s) (Var n), SeqQuoteP (Var sm) (Var sm') (Var s) (Var m), Var n IN Var k, Var m IN Var k, SeqQuoteP (Var j) (Var j') (Var s) (Var k), All2 l (Var k) (SyntaxN.All j (SyntaxN.All j' (SeqQuoteP (Var j) (Var j') (Var s) (Var l) IMP ConstP (Var j')))), OrdP (Var k)} \<turnstile> ConstP (Q_Eats (Var sm') (Var sn'))
[PROOF STEP]
apply (rule ConstP_Eats [THEN cut2])
        \<comment> \<open>Operand 1. IH for sm\<close>
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>atom j \<sharp> (x, y, s, k, j', l, m, n, sm, sm', sn, sn'); atom j' \<sharp> (x, y, s, k, l, m, n, sm, sm', sn, sn'); atom l \<sharp> (s, k, m, n, sm, sm', sn, sn'); atom m \<sharp> (s, k, n, sm, sm', sn, sn'); atom n \<sharp> (s, k, sm, sm', sn, sn'); atom sm \<sharp> (s, k, sm', sn, sn'); atom sm' \<sharp> (s, k, sn, sn'); atom sn \<sharp> (s, k, sn'); atom sn' \<sharp> (s, k); atom s \<sharp> (k, x, y); atom k \<sharp> (x, y)\<rbrakk> \<Longrightarrow> {Var j' EQ Q_Eats (Var sm') (Var sn'), Var j EQ Eats (Var sm) (Var sn), SeqQuoteP (Var sn) (Var sn') (Var s) (Var n), SeqQuoteP (Var sm) (Var sm') (Var s) (Var m), Var n IN Var k, Var m IN Var k, SeqQuoteP (Var j) (Var j') (Var s) (Var k), All2 l (Var k) (SyntaxN.All j (SyntaxN.All j' (SeqQuoteP (Var j) (Var j') (Var s) (Var l) IMP ConstP (Var j')))), OrdP (Var k)} \<turnstile> ConstP (Var sm')
 2. \<lbrakk>atom j \<sharp> (x, y, s, k, j', l, m, n, sm, sm', sn, sn'); atom j' \<sharp> (x, y, s, k, l, m, n, sm, sm', sn, sn'); atom l \<sharp> (s, k, m, n, sm, sm', sn, sn'); atom m \<sharp> (s, k, n, sm, sm', sn, sn'); atom n \<sharp> (s, k, sm, sm', sn, sn'); atom sm \<sharp> (s, k, sm', sn, sn'); atom sm' \<sharp> (s, k, sn, sn'); atom sn \<sharp> (s, k, sn'); atom sn' \<sharp> (s, k); atom s \<sharp> (k, x, y); atom k \<sharp> (x, y)\<rbrakk> \<Longrightarrow> {Var j' EQ Q_Eats (Var sm') (Var sn'), Var j EQ Eats (Var sm) (Var sn), SeqQuoteP (Var sn) (Var sn') (Var s) (Var n), SeqQuoteP (Var sm) (Var sm') (Var s) (Var m), Var n IN Var k, Var m IN Var k, SeqQuoteP (Var j) (Var j') (Var s) (Var k), All2 l (Var k) (SyntaxN.All j (SyntaxN.All j' (SeqQuoteP (Var j) (Var j') (Var s) (Var l) IMP ConstP (Var j')))), OrdP (Var k)} \<turnstile> ConstP (Var sn')
[PROOF STEP]
apply (rule All2_E [where x="Var m", THEN rotate8], auto)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>atom j \<sharp> (x, y, s, k, j', l, m, n, sm, sm', sn, sn'); atom j' \<sharp> (x, y, s, k, l, m, n, sm, sm', sn, sn'); atom l \<sharp> (s, k, m, n, sm, sm', sn, sn'); atom m \<sharp> (s, k, n, sm, sm', sn, sn'); atom n \<sharp> (s, k, sm, sm', sn, sn'); atom sm \<sharp> (s, k, sm', sn, sn'); atom sm' \<sharp> (s, k, sn, sn'); atom sn \<sharp> (s, k, sn'); atom sn' \<sharp> (s, k); atom s \<sharp> (k, x, y); atom k \<sharp> (x, y)\<rbrakk> \<Longrightarrow> {SyntaxN.All j (SyntaxN.All j' (SeqQuoteP (Var j) (Var j') (Var s) (Var m) IMP ConstP (Var j'))), Var j' EQ Q_Eats (Var sm') (Var sn'), Var j EQ Eats (Var sm) (Var sn), SeqQuoteP (Var sn) (Var sn') (Var s) (Var n), SeqQuoteP (Var sm) (Var sm') (Var s) (Var m), Var n IN Var k, Var m IN Var k, SeqQuoteP (Var j) (Var j') (Var s) (Var k), OrdP (Var k)} \<turnstile> ConstP (Var sm')
 2. \<lbrakk>atom j \<sharp> (x, y, s, k, j', l, m, n, sm, sm', sn, sn'); atom j' \<sharp> (x, y, s, k, l, m, n, sm, sm', sn, sn'); atom l \<sharp> (s, k, m, n, sm, sm', sn, sn'); atom m \<sharp> (s, k, n, sm, sm', sn, sn'); atom n \<sharp> (s, k, sm, sm', sn, sn'); atom sm \<sharp> (s, k, sm', sn, sn'); atom sm' \<sharp> (s, k, sn, sn'); atom sn \<sharp> (s, k, sn'); atom sn' \<sharp> (s, k); atom s \<sharp> (k, x, y); atom k \<sharp> (x, y)\<rbrakk> \<Longrightarrow> {Var j' EQ Q_Eats (Var sm') (Var sn'), Var j EQ Eats (Var sm) (Var sn), SeqQuoteP (Var sn) (Var sn') (Var s) (Var n), SeqQuoteP (Var sm) (Var sm') (Var s) (Var m), Var n IN Var k, Var m IN Var k, SeqQuoteP (Var j) (Var j') (Var s) (Var k), All2 l (Var k) (SyntaxN.All j (SyntaxN.All j' (SeqQuoteP (Var j) (Var j') (Var s) (Var l) IMP ConstP (Var j')))), OrdP (Var k)} \<turnstile> ConstP (Var sn')
[PROOF STEP]
apply (rule All_E [where x="Var sm"], simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>atom j \<sharp> (x, y, s, k, j', l, m, n, sm, sm', sn, sn'); atom j' \<sharp> (x, y, s, k, l, m, n, sm, sm', sn, sn'); atom l \<sharp> (s, k, m, n, sm, sm', sn, sn'); atom m \<sharp> (s, k, n, sm, sm', sn, sn'); atom n \<sharp> (s, k, sm, sm', sn, sn'); atom sm \<sharp> (s, k, sm', sn, sn'); atom sm' \<sharp> (s, k, sn, sn'); atom sn \<sharp> (s, k, sn'); atom sn' \<sharp> (s, k); atom s \<sharp> (k, x, y); atom k \<sharp> (x, y)\<rbrakk> \<Longrightarrow> {SyntaxN.All j' (SeqQuoteP (Var sm) (Var j') (Var s) (Var m) IMP ConstP (Var j')), Var j' EQ Q_Eats (Var sm') (Var sn'), Var j EQ Eats (Var sm) (Var sn), SeqQuoteP (Var sn) (Var sn') (Var s) (Var n), SeqQuoteP (Var sm) (Var sm') (Var s) (Var m), Var n IN Var k, Var m IN Var k, SeqQuoteP (Var j) (Var j') (Var s) (Var k), OrdP (Var k)} \<turnstile> ConstP (Var sm')
 2. \<lbrakk>atom j \<sharp> (x, y, s, k, j', l, m, n, sm, sm', sn, sn'); atom j' \<sharp> (x, y, s, k, l, m, n, sm, sm', sn, sn'); atom l \<sharp> (s, k, m, n, sm, sm', sn, sn'); atom m \<sharp> (s, k, n, sm, sm', sn, sn'); atom n \<sharp> (s, k, sm, sm', sn, sn'); atom sm \<sharp> (s, k, sm', sn, sn'); atom sm' \<sharp> (s, k, sn, sn'); atom sn \<sharp> (s, k, sn'); atom sn' \<sharp> (s, k); atom s \<sharp> (k, x, y); atom k \<sharp> (x, y)\<rbrakk> \<Longrightarrow> {Var j' EQ Q_Eats (Var sm') (Var sn'), Var j EQ Eats (Var sm) (Var sn), SeqQuoteP (Var sn) (Var sn') (Var s) (Var n), SeqQuoteP (Var sm) (Var sm') (Var s) (Var m), Var n IN Var k, Var m IN Var k, SeqQuoteP (Var j) (Var j') (Var s) (Var k), All2 l (Var k) (SyntaxN.All j (SyntaxN.All j' (SeqQuoteP (Var j) (Var j') (Var s) (Var l) IMP ConstP (Var j')))), OrdP (Var k)} \<turnstile> ConstP (Var sn')
[PROOF STEP]
apply (rule All_E [where x="Var sm'"], auto)
        \<comment> \<open>Operand 2. IH for sm\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>atom j \<sharp> (x, y, s, k, j', l, m, n, sm, sm', sn, sn'); atom j' \<sharp> (x, y, s, k, l, m, n, sm, sm', sn, sn'); atom l \<sharp> (s, k, m, n, sm, sm', sn, sn'); atom m \<sharp> (s, k, n, sm, sm', sn, sn'); atom n \<sharp> (s, k, sm, sm', sn, sn'); atom sm \<sharp> (s, k, sm', sn, sn'); atom sm' \<sharp> (s, k, sn, sn'); atom sn \<sharp> (s, k, sn'); atom sn' \<sharp> (s, k); atom s \<sharp> (k, x, y); atom k \<sharp> (x, y)\<rbrakk> \<Longrightarrow> {Var j' EQ Q_Eats (Var sm') (Var sn'), Var j EQ Eats (Var sm) (Var sn), SeqQuoteP (Var sn) (Var sn') (Var s) (Var n), SeqQuoteP (Var sm) (Var sm') (Var s) (Var m), Var n IN Var k, Var m IN Var k, SeqQuoteP (Var j) (Var j') (Var s) (Var k), All2 l (Var k) (SyntaxN.All j (SyntaxN.All j' (SeqQuoteP (Var j) (Var j') (Var s) (Var l) IMP ConstP (Var j')))), OrdP (Var k)} \<turnstile> ConstP (Var sn')
[PROOF STEP]
apply (rule All2_E [where x="Var n", THEN rotate8], auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>atom j \<sharp> (x, y, s, k, j', l, m, n, sm, sm', sn, sn'); atom j' \<sharp> (x, y, s, k, l, m, n, sm, sm', sn, sn'); atom l \<sharp> (s, k, m, n, sm, sm', sn, sn'); atom m \<sharp> (s, k, n, sm, sm', sn, sn'); atom n \<sharp> (s, k, sm, sm', sn, sn'); atom sm \<sharp> (s, k, sm', sn, sn'); atom sm' \<sharp> (s, k, sn, sn'); atom sn \<sharp> (s, k, sn'); atom sn' \<sharp> (s, k); atom s \<sharp> (k, x, y); atom k \<sharp> (x, y)\<rbrakk> \<Longrightarrow> {SyntaxN.All j (SyntaxN.All j' (SeqQuoteP (Var j) (Var j') (Var s) (Var n) IMP ConstP (Var j'))), Var j' EQ Q_Eats (Var sm') (Var sn'), Var j EQ Eats (Var sm) (Var sn), SeqQuoteP (Var sn) (Var sn') (Var s) (Var n), SeqQuoteP (Var sm) (Var sm') (Var s) (Var m), Var n IN Var k, Var m IN Var k, SeqQuoteP (Var j) (Var j') (Var s) (Var k), OrdP (Var k)} \<turnstile> ConstP (Var sn')
[PROOF STEP]
apply (rule All_E [where x="Var sn"], simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>atom j \<sharp> (x, y, s, k, j', l, m, n, sm, sm', sn, sn'); atom j' \<sharp> (x, y, s, k, l, m, n, sm, sm', sn, sn'); atom l \<sharp> (s, k, m, n, sm, sm', sn, sn'); atom m \<sharp> (s, k, n, sm, sm', sn, sn'); atom n \<sharp> (s, k, sm, sm', sn, sn'); atom sm \<sharp> (s, k, sm', sn, sn'); atom sm' \<sharp> (s, k, sn, sn'); atom sn \<sharp> (s, k, sn'); atom sn' \<sharp> (s, k); atom s \<sharp> (k, x, y); atom k \<sharp> (x, y)\<rbrakk> \<Longrightarrow> {SyntaxN.All j' (SeqQuoteP (Var sn) (Var j') (Var s) (Var n) IMP ConstP (Var j')), Var j' EQ Q_Eats (Var sm') (Var sn'), Var j EQ Eats (Var sm) (Var sn), SeqQuoteP (Var sn) (Var sn') (Var s) (Var n), SeqQuoteP (Var sm) (Var sm') (Var s) (Var m), Var n IN Var k, Var m IN Var k, SeqQuoteP (Var j) (Var j') (Var s) (Var k), OrdP (Var k)} \<turnstile> ConstP (Var sn')
[PROOF STEP]
apply (rule All_E [where x="Var sn'"], auto)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
{} \<turnstile> SyntaxN.All k (OrdP (Var k) IMP All2 l (Var k) ((SyntaxN.All j (SyntaxN.All j' (SeqQuoteP (Var j) (Var j') (Var s) (Var k) IMP ConstP (Var j'))))(k::=Var l)) IMP SyntaxN.All j (SyntaxN.All j' (SeqQuoteP (Var j) (Var j') (Var s) (Var k) IMP ConstP (Var j'))))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
{OrdP (Var k)} \<turnstile> SyntaxN.All j (SyntaxN.All j' (SeqQuoteP (Var j) (Var j') (Var s) (Var k) IMP ConstP (Var j')))

goal (1 subgoal):
 1. {QuoteP x y} \<turnstile> ConstP y
[PROOF STEP]
hence "{OrdP(Var k)}
         \<turnstile> (All j' (SeqQuoteP (Var j) (Var j') (Var s) (Var k) IMP ConstP (Var j'))) (j::=x)"
[PROOF STATE]
proof (prove)
using this:
{OrdP (Var k)} \<turnstile> SyntaxN.All j (SyntaxN.All j' (SeqQuoteP (Var j) (Var j') (Var s) (Var k) IMP ConstP (Var j')))

goal (1 subgoal):
 1. {OrdP (Var k)} \<turnstile> (SyntaxN.All j' (SeqQuoteP (Var j) (Var j') (Var s) (Var k) IMP ConstP (Var j')))(j::=x)
[PROOF STEP]
by (metis All_D)
[PROOF STATE]
proof (state)
this:
{OrdP (Var k)} \<turnstile> (SyntaxN.All j' (SeqQuoteP (Var j) (Var j') (Var s) (Var k) IMP ConstP (Var j')))(j::=x)

goal (1 subgoal):
 1. {QuoteP x y} \<turnstile> ConstP y
[PROOF STEP]
hence "{OrdP(Var k)} \<turnstile> All j' (SeqQuoteP x (Var j') (Var s) (Var k) IMP ConstP (Var j'))"
[PROOF STATE]
proof (prove)
using this:
{OrdP (Var k)} \<turnstile> (SyntaxN.All j' (SeqQuoteP (Var j) (Var j') (Var s) (Var k) IMP ConstP (Var j')))(j::=x)

goal (1 subgoal):
 1. {OrdP (Var k)} \<turnstile> SyntaxN.All j' (SeqQuoteP x (Var j') (Var s) (Var k) IMP ConstP (Var j'))
[PROOF STEP]
using atoms
[PROOF STATE]
proof (prove)
using this:
{OrdP (Var k)} \<turnstile> (SyntaxN.All j' (SeqQuoteP (Var j) (Var j') (Var s) (Var k) IMP ConstP (Var j')))(j::=x)
atom j \<sharp> (x, y, s, k, j', l, m, n, sm, sm', sn, sn')
atom j' \<sharp> (x, y, s, k, l, m, n, sm, sm', sn, sn')
atom l \<sharp> (s, k, m, n, sm, sm', sn, sn')
atom m \<sharp> (s, k, n, sm, sm', sn, sn')
atom n \<sharp> (s, k, sm, sm', sn, sn')
atom sm \<sharp> (s, k, sm', sn, sn')
atom sm' \<sharp> (s, k, sn, sn')
atom sn \<sharp> (s, k, sn')
atom sn' \<sharp> (s, k)
atom s \<sharp> (k, x, y)
atom k \<sharp> (x, y)

goal (1 subgoal):
 1. {OrdP (Var k)} \<turnstile> SyntaxN.All j' (SeqQuoteP x (Var j') (Var s) (Var k) IMP ConstP (Var j'))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
{OrdP (Var k)} \<turnstile> SyntaxN.All j' (SeqQuoteP x (Var j') (Var s) (Var k) IMP ConstP (Var j'))

goal (1 subgoal):
 1. {QuoteP x y} \<turnstile> ConstP y
[PROOF STEP]
hence "{OrdP(Var k)} \<turnstile> (SeqQuoteP x (Var j') (Var s) (Var k) IMP ConstP (Var j')) (j'::=y)"
[PROOF STATE]
proof (prove)
using this:
{OrdP (Var k)} \<turnstile> SyntaxN.All j' (SeqQuoteP x (Var j') (Var s) (Var k) IMP ConstP (Var j'))

goal (1 subgoal):
 1. {OrdP (Var k)} \<turnstile> (SeqQuoteP x (Var j') (Var s) (Var k) IMP ConstP (Var j'))(j'::=y)
[PROOF STEP]
by (metis All_D)
[PROOF STATE]
proof (state)
this:
{OrdP (Var k)} \<turnstile> (SeqQuoteP x (Var j') (Var s) (Var k) IMP ConstP (Var j'))(j'::=y)

goal (1 subgoal):
 1. {QuoteP x y} \<turnstile> ConstP y
[PROOF STEP]
hence "{OrdP(Var k)} \<turnstile> SeqQuoteP x y (Var s) (Var k) IMP ConstP y"
[PROOF STATE]
proof (prove)
using this:
{OrdP (Var k)} \<turnstile> (SeqQuoteP x (Var j') (Var s) (Var k) IMP ConstP (Var j'))(j'::=y)

goal (1 subgoal):
 1. {OrdP (Var k)} \<turnstile> SeqQuoteP x y (Var s) (Var k) IMP ConstP y
[PROOF STEP]
using atoms
[PROOF STATE]
proof (prove)
using this:
{OrdP (Var k)} \<turnstile> (SeqQuoteP x (Var j') (Var s) (Var k) IMP ConstP (Var j'))(j'::=y)
atom j \<sharp> (x, y, s, k, j', l, m, n, sm, sm', sn, sn')
atom j' \<sharp> (x, y, s, k, l, m, n, sm, sm', sn, sn')
atom l \<sharp> (s, k, m, n, sm, sm', sn, sn')
atom m \<sharp> (s, k, n, sm, sm', sn, sn')
atom n \<sharp> (s, k, sm, sm', sn, sn')
atom sm \<sharp> (s, k, sm', sn, sn')
atom sm' \<sharp> (s, k, sn, sn')
atom sn \<sharp> (s, k, sn')
atom sn' \<sharp> (s, k)
atom s \<sharp> (k, x, y)
atom k \<sharp> (x, y)

goal (1 subgoal):
 1. {OrdP (Var k)} \<turnstile> SeqQuoteP x y (Var s) (Var k) IMP ConstP y
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
{OrdP (Var k)} \<turnstile> SeqQuoteP x y (Var s) (Var k) IMP ConstP y

goal (1 subgoal):
 1. {QuoteP x y} \<turnstile> ConstP y
[PROOF STEP]
hence "{ SeqQuoteP x y (Var s) (Var k) } \<turnstile> ConstP y"
[PROOF STATE]
proof (prove)
using this:
{OrdP (Var k)} \<turnstile> SeqQuoteP x y (Var s) (Var k) IMP ConstP y

goal (1 subgoal):
 1. {SeqQuoteP x y (Var s) (Var k)} \<turnstile> ConstP y
[PROOF STEP]
by (metis Imp_cut SeqQuoteP_imp_OrdP anti_deduction)
[PROOF STATE]
proof (state)
this:
{SeqQuoteP x y (Var s) (Var k)} \<turnstile> ConstP y

goal (1 subgoal):
 1. {QuoteP x y} \<turnstile> ConstP y
[PROOF STEP]
thus "{ QuoteP x y } \<turnstile> ConstP y"
[PROOF STATE]
proof (prove)
using this:
{SeqQuoteP x y (Var s) (Var k)} \<turnstile> ConstP y

goal (1 subgoal):
 1. {QuoteP x y} \<turnstile> ConstP y
[PROOF STEP]
using atoms
[PROOF STATE]
proof (prove)
using this:
{SeqQuoteP x y (Var s) (Var k)} \<turnstile> ConstP y
atom j \<sharp> (x, y, s, k, j', l, m, n, sm, sm', sn, sn')
atom j' \<sharp> (x, y, s, k, l, m, n, sm, sm', sn, sn')
atom l \<sharp> (s, k, m, n, sm, sm', sn, sn')
atom m \<sharp> (s, k, n, sm, sm', sn, sn')
atom n \<sharp> (s, k, sm, sm', sn, sn')
atom sm \<sharp> (s, k, sm', sn, sn')
atom sm' \<sharp> (s, k, sn, sn')
atom sn \<sharp> (s, k, sn')
atom sn' \<sharp> (s, k)
atom s \<sharp> (k, x, y)
atom k \<sharp> (x, y)

goal (1 subgoal):
 1. {QuoteP x y} \<turnstile> ConstP y
[PROOF STEP]
by (auto simp: QuoteP.simps [of s _ _ k])
[PROOF STATE]
proof (state)
this:
{QuoteP x y} \<turnstile> ConstP y

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma SeqQuoteP_imp_QuoteP: "{SeqQuoteP t u s k} \<turnstile> QuoteP t u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {SeqQuoteP t u s k} \<turnstile> QuoteP t u
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. {SeqQuoteP t u s k} \<turnstile> QuoteP t u
[PROOF STEP]
obtain s'::name and k'::name  where "atom s' \<sharp> (k',t,u,s,k)"  "atom k' \<sharp> (t,u,s,k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>s' k'. \<lbrakk>atom s' \<sharp> (k', t, u, s, k); atom k' \<sharp> (t, u, s, k)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis obtain_fresh)
[PROOF STATE]
proof (state)
this:
atom s' \<sharp> (k', t, u, s, k)
atom k' \<sharp> (t, u, s, k)

goal (1 subgoal):
 1. {SeqQuoteP t u s k} \<turnstile> QuoteP t u
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
atom s' \<sharp> (k', t, u, s, k)
atom k' \<sharp> (t, u, s, k)

goal (1 subgoal):
 1. {SeqQuoteP t u s k} \<turnstile> QuoteP t u
[PROOF STEP]
apply (simp add: QuoteP.simps [of s' _ _ k'])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>atom s' \<sharp> (k', t, u, s, k); atom k' \<sharp> (t, u, s, k)\<rbrakk> \<Longrightarrow> {SeqQuoteP t u s k} \<turnstile> SyntaxN.Ex s' (SyntaxN.Ex k' (SeqQuoteP t u (Var s') (Var k')))
[PROOF STEP]
apply (rule Ex_I [where x = s], simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>atom s' \<sharp> (k', t, u, s, k); atom k' \<sharp> (t, u, s, k)\<rbrakk> \<Longrightarrow> {SeqQuoteP t u s k} \<turnstile> SyntaxN.Ex k' (SeqQuoteP t u s (Var k'))
[PROOF STEP]
apply (rule Ex_I [where x = k], auto)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
{SeqQuoteP t u s k} \<turnstile> QuoteP t u

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma quote_all_empty [simp]: "quote_all p {} = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. quote_all p {} = {}
[PROOF STEP]
by (simp add: quote_all_def)


[STATEMENT]
lemma quote_all_insert [simp]:
  "quote_all p (insert i V) = insert (QuoteP (Var i) (Var (p \<bullet> i))) (quote_all p V)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. quote_all p (insert i V) = insert (QuoteP (Var i) (Var (p \<bullet> i))) (quote_all p V)
[PROOF STEP]
by (auto simp: quote_all_def)


[STATEMENT]
lemma finite_quote_all [simp]: "finite V \<Longrightarrow> finite (quote_all p V)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite V \<Longrightarrow> finite (quote_all p V)
[PROOF STEP]
by (induct rule: finite_induct) auto


[STATEMENT]
lemma fresh_quote_all [simp]: "finite V \<Longrightarrow> i \<sharp> quote_all p V \<longleftrightarrow> i \<sharp> V \<and> i \<sharp> p\<bullet>V"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite V \<Longrightarrow> i \<sharp> quote_all p V = (i \<sharp> V \<and> i \<sharp> p \<bullet> V)
[PROOF STEP]
by (induct rule: finite_induct) (auto simp: fresh_finite_insert)


[STATEMENT]
lemma fresh_quote_all_mem: "\<lbrakk>A \<in> quote_all p V; finite V; i \<sharp> V; i \<sharp> p \<bullet> V\<rbrakk> \<Longrightarrow> i \<sharp> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A \<in> quote_all p V; finite V; i \<sharp> V; i \<sharp> p \<bullet> V\<rbrakk> \<Longrightarrow> i \<sharp> A
[PROOF STEP]
by (metis Set.set_insert finite_insert finite_quote_all fresh_finite_insert fresh_quote_all)


[STATEMENT]
lemma quote_all_perm_eq:
  assumes "finite V" "atom i \<sharp> (p,V)" "atom i' \<sharp> (p,V)"
    shows "quote_all ((atom i \<rightleftharpoons> atom i') + p) V = quote_all p V"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. quote_all ((atom i \<rightleftharpoons> atom i') + p) V = quote_all p V
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. quote_all ((atom i \<rightleftharpoons> atom i') + p) V = quote_all p V
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. quote_all ((atom i \<rightleftharpoons> atom i') + p) V = quote_all p V
[PROOF STEP]
fix W
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. quote_all ((atom i \<rightleftharpoons> atom i') + p) V = quote_all p V
[PROOF STEP]
assume w: "W \<subseteq> V"
[PROOF STATE]
proof (state)
this:
W \<subseteq> V

goal (1 subgoal):
 1. quote_all ((atom i \<rightleftharpoons> atom i') + p) V = quote_all p V
[PROOF STEP]
have "finite W"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite W
[PROOF STEP]
by (metis \<open>finite V\<close> finite_subset w)
[PROOF STATE]
proof (state)
this:
finite W

goal (1 subgoal):
 1. quote_all ((atom i \<rightleftharpoons> atom i') + p) V = quote_all p V
[PROOF STEP]
hence "quote_all ((atom i \<rightleftharpoons> atom i') + p) W = quote_all p W"
[PROOF STATE]
proof (prove)
using this:
finite W

goal (1 subgoal):
 1. quote_all ((atom i \<rightleftharpoons> atom i') + p) W = quote_all p W
[PROOF STEP]
using w
[PROOF STATE]
proof (prove)
using this:
finite W
W \<subseteq> V

goal (1 subgoal):
 1. quote_all ((atom i \<rightleftharpoons> atom i') + p) W = quote_all p W
[PROOF STEP]
apply induction
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. {} \<subseteq> V \<Longrightarrow> quote_all ((atom i \<rightleftharpoons> atom i') + p) {} = quote_all p {}
 2. \<And>x F. \<lbrakk>finite F; x \<notin> F; F \<subseteq> V \<Longrightarrow> quote_all ((atom i \<rightleftharpoons> atom i') + p) F = quote_all p F; insert x F \<subseteq> V\<rbrakk> \<Longrightarrow> quote_all ((atom i \<rightleftharpoons> atom i') + p) (insert x F) = quote_all p (insert x F)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
finite V
atom i \<sharp> (p, V)
atom i' \<sharp> (p, V)

goal (2 subgoals):
 1. {} \<subseteq> V \<Longrightarrow> quote_all ((atom i \<rightleftharpoons> atom i') + p) {} = quote_all p {}
 2. \<And>x F. \<lbrakk>finite F; x \<notin> F; F \<subseteq> V \<Longrightarrow> quote_all ((atom i \<rightleftharpoons> atom i') + p) F = quote_all p F; insert x F \<subseteq> V\<rbrakk> \<Longrightarrow> quote_all ((atom i \<rightleftharpoons> atom i') + p) (insert x F) = quote_all p (insert x F)
[PROOF STEP]
apply (auto simp: fresh_Pair perm_commute)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; quote_all (p + (atom i \<rightleftharpoons> atom i')) F = quote_all p F; finite V; x \<in> V; F \<subseteq> V; atom i \<sharp> p; atom i \<sharp> V; atom i' \<sharp> p; atom i' \<sharp> V; QuoteP (Var x) (Var (p \<bullet> (atom i \<rightleftharpoons> atom i') \<bullet> x)) \<notin> quote_all p F\<rbrakk> \<Longrightarrow> QuoteP (Var x) (Var (p \<bullet> (atom i \<rightleftharpoons> atom i') \<bullet> x)) = QuoteP (Var x) (Var (p \<bullet> x))
 2. \<And>x F. \<lbrakk>finite F; x \<notin> F; quote_all (p + (atom i \<rightleftharpoons> atom i')) F = quote_all p F; finite V; x \<in> V; F \<subseteq> V; atom i \<sharp> p; atom i \<sharp> V; atom i' \<sharp> p; atom i' \<sharp> V; QuoteP (Var x) (Var (p \<bullet> x)) \<notin> quote_all p F\<rbrakk> \<Longrightarrow> QuoteP (Var x) (Var (p \<bullet> x)) = QuoteP (Var x) (Var (p \<bullet> (atom i \<rightleftharpoons> atom i') \<bullet> x))
[PROOF STEP]
apply (metis fresh_finite_set_at_base swap_at_base_simps(3))+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
quote_all ((atom i \<rightleftharpoons> atom i') + p) W = quote_all p W

goal (1 subgoal):
 1. quote_all ((atom i \<rightleftharpoons> atom i') + p) V = quote_all p V
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?W2 \<subseteq> V \<Longrightarrow> quote_all ((atom i \<rightleftharpoons> atom i') + p) ?W2 = quote_all p ?W2

goal (1 subgoal):
 1. quote_all ((atom i \<rightleftharpoons> atom i') + p) V = quote_all p V
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
?W2 \<subseteq> V \<Longrightarrow> quote_all ((atom i \<rightleftharpoons> atom i') + p) ?W2 = quote_all p ?W2

goal (1 subgoal):
 1. quote_all ((atom i \<rightleftharpoons> atom i') + p) V = quote_all p V
[PROOF STEP]
by (metis order_refl)
[PROOF STATE]
proof (state)
this:
quote_all ((atom i \<rightleftharpoons> atom i') + p) V = quote_all p V

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma QuoteP_imp_ConstP_F_hyps:
  assumes "Us \<subseteq> Vs" "{ConstP (F i) | i. i \<in> Us} \<turnstile> A"  shows "quote_all p Us \<turnstile> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. quote_all p Us \<turnstile> A
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. quote_all p Us \<turnstile> A
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. quote_all p Us \<turnstile> A
[PROOF STEP]
using finite_V [OF \<open>Us \<subseteq> Vs\<close>]  assms
[PROOF STATE]
proof (prove)
using this:
finite Us
Us \<subseteq> Vs
{ConstP (F i) |i. i \<in> Us} \<turnstile> A

goal (1 subgoal):
 1. quote_all p Us \<turnstile> A
[PROOF STEP]
proof (induction arbitrary: A rule: finite_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>A. \<lbrakk>{} \<subseteq> Vs; {ConstP (F i) |i. i \<in> {}} \<turnstile> A\<rbrakk> \<Longrightarrow> quote_all p {} \<turnstile> A
 2. \<And>x Fa A. \<lbrakk>finite Fa; x \<notin> Fa; \<And>A. \<lbrakk>Fa \<subseteq> Vs; {ConstP (F i) |i. i \<in> Fa} \<turnstile> A\<rbrakk> \<Longrightarrow> quote_all p Fa \<turnstile> A; insert x Fa \<subseteq> Vs; {ConstP (F i) |i. i \<in> insert x Fa} \<turnstile> A\<rbrakk> \<Longrightarrow> quote_all p (insert x Fa) \<turnstile> A
[PROOF STEP]
case empty
[PROOF STATE]
proof (state)
this:
{} \<subseteq> Vs
{ConstP (F i) |i. i \<in> {}} \<turnstile> A

goal (2 subgoals):
 1. \<And>A. \<lbrakk>{} \<subseteq> Vs; {ConstP (F i) |i. i \<in> {}} \<turnstile> A\<rbrakk> \<Longrightarrow> quote_all p {} \<turnstile> A
 2. \<And>x Fa A. \<lbrakk>finite Fa; x \<notin> Fa; \<And>A. \<lbrakk>Fa \<subseteq> Vs; {ConstP (F i) |i. i \<in> Fa} \<turnstile> A\<rbrakk> \<Longrightarrow> quote_all p Fa \<turnstile> A; insert x Fa \<subseteq> Vs; {ConstP (F i) |i. i \<in> insert x Fa} \<turnstile> A\<rbrakk> \<Longrightarrow> quote_all p (insert x Fa) \<turnstile> A
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
{} \<subseteq> Vs
{ConstP (F i) |i. i \<in> {}} \<turnstile> A

goal (1 subgoal):
 1. quote_all p {} \<turnstile> A
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
quote_all p {} \<turnstile> A

goal (1 subgoal):
 1. \<And>x Fa A. \<lbrakk>finite Fa; x \<notin> Fa; \<And>A. \<lbrakk>Fa \<subseteq> Vs; {ConstP (F i) |i. i \<in> Fa} \<turnstile> A\<rbrakk> \<Longrightarrow> quote_all p Fa \<turnstile> A; insert x Fa \<subseteq> Vs; {ConstP (F i) |i. i \<in> insert x Fa} \<turnstile> A\<rbrakk> \<Longrightarrow> quote_all p (insert x Fa) \<turnstile> A
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x Fa A. \<lbrakk>finite Fa; x \<notin> Fa; \<And>A. \<lbrakk>Fa \<subseteq> Vs; {ConstP (F i) |i. i \<in> Fa} \<turnstile> A\<rbrakk> \<Longrightarrow> quote_all p Fa \<turnstile> A; insert x Fa \<subseteq> Vs; {ConstP (F i) |i. i \<in> insert x Fa} \<turnstile> A\<rbrakk> \<Longrightarrow> quote_all p (insert x Fa) \<turnstile> A
[PROOF STEP]
case (insert v Us)
[PROOF STATE]
proof (state)
this:
finite Us
v \<notin> Us
\<lbrakk>Us \<subseteq> Vs; {ConstP (F i) |i. i \<in> Us} \<turnstile> ?A\<rbrakk> \<Longrightarrow> quote_all p Us \<turnstile> ?A
insert v Us \<subseteq> Vs
{ConstP (F i) |i. i \<in> insert v Us} \<turnstile> A

goal (1 subgoal):
 1. \<And>x Fa A. \<lbrakk>finite Fa; x \<notin> Fa; \<And>A. \<lbrakk>Fa \<subseteq> Vs; {ConstP (F i) |i. i \<in> Fa} \<turnstile> A\<rbrakk> \<Longrightarrow> quote_all p Fa \<turnstile> A; insert x Fa \<subseteq> Vs; {ConstP (F i) |i. i \<in> insert x Fa} \<turnstile> A\<rbrakk> \<Longrightarrow> quote_all p (insert x Fa) \<turnstile> A
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
finite Us
v \<notin> Us
\<lbrakk>Us \<subseteq> Vs; {ConstP (F i) |i. i \<in> Us} \<turnstile> ?A\<rbrakk> \<Longrightarrow> quote_all p Us \<turnstile> ?A
insert v Us \<subseteq> Vs
{ConstP (F i) |i. i \<in> insert v Us} \<turnstile> A

goal (1 subgoal):
 1. quote_all p (insert v Us) \<turnstile> A
[PROOF STEP]
by (auto simp: Collect_disj_Un)
         (metis (lifting) anti_deduction Imp_cut [OF _ QuoteP_imp_ConstP] Disj_I2 F_unfold)
[PROOF STATE]
proof (state)
this:
quote_all p (insert v Us) \<turnstile> A

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
quote_all p Us \<turnstile> A

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem quote_all_PfP_ssubst:
  assumes \<beta>: "{} \<turnstile> \<beta>"
      and V: "V \<subseteq> Vs"
      and s: "supp \<beta> \<subseteq> atom ` Vs"
    shows    "quote_all p V \<turnstile> PfP (ssubst \<lfloor>\<beta>\<rfloor>V V F)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. quote_all p V \<turnstile> PfP (ssubst \<lfloor>\<beta>\<rfloor>V V F)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. quote_all p V \<turnstile> PfP (ssubst \<lfloor>\<beta>\<rfloor>V V F)
[PROOF STEP]
have "{} \<turnstile> PfP \<guillemotleft>\<beta>\<guillemotright>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {} \<turnstile> PfP \<guillemotleft>\<beta>\<guillemotright>
[PROOF STEP]
by (metis \<beta> proved_iff_proved_PfP)
[PROOF STATE]
proof (state)
this:
{} \<turnstile> PfP \<guillemotleft>\<beta>\<guillemotright>

goal (1 subgoal):
 1. quote_all p V \<turnstile> PfP (ssubst \<lfloor>\<beta>\<rfloor>V V F)
[PROOF STEP]
hence "{ConstP (F i) | i. i \<in> V} \<turnstile> PfP (ssubst \<lfloor>\<beta>\<rfloor>V V F)"
[PROOF STATE]
proof (prove)
using this:
{} \<turnstile> PfP \<guillemotleft>\<beta>\<guillemotright>

goal (1 subgoal):
 1. {ConstP (F i) |i. i \<in> V} \<turnstile> PfP (ssubst \<lfloor>\<beta>\<rfloor>V V F)
[PROOF STEP]
by (simp add: PfP_implies_PfP_ssubst V s)
[PROOF STATE]
proof (state)
this:
{ConstP (F i) |i. i \<in> V} \<turnstile> PfP (ssubst \<lfloor>\<beta>\<rfloor>V V F)

goal (1 subgoal):
 1. quote_all p V \<turnstile> PfP (ssubst \<lfloor>\<beta>\<rfloor>V V F)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
{ConstP (F i) |i. i \<in> V} \<turnstile> PfP (ssubst \<lfloor>\<beta>\<rfloor>V V F)

goal (1 subgoal):
 1. quote_all p V \<turnstile> PfP (ssubst \<lfloor>\<beta>\<rfloor>V V F)
[PROOF STEP]
by (rule QuoteP_imp_ConstP_F_hyps [OF V])
[PROOF STATE]
proof (state)
this:
quote_all p V \<turnstile> PfP (ssubst \<lfloor>\<beta>\<rfloor>V V F)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma quote_all_Disj_I1_PfP_ssubst:
  assumes "V \<subseteq> Vs" "supp \<alpha> \<subseteq> atom ` Vs" "supp \<beta> \<subseteq> atom ` Vs"
      and prems: "H \<turnstile> PfP (ssubst \<lfloor>\<alpha>\<rfloor>V V F)" "quote_all p V \<subseteq> H"
    shows "H \<turnstile> PfP (ssubst \<lfloor>\<alpha> OR \<beta>\<rfloor>V V F)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. H \<turnstile> PfP (ssubst \<lfloor>\<alpha> OR \<beta>\<rfloor>V V F)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. H \<turnstile> PfP (ssubst \<lfloor>\<alpha> OR \<beta>\<rfloor>V V F)
[PROOF STEP]
have "{} \<turnstile> \<alpha> IMP (\<alpha> OR \<beta>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {} \<turnstile> \<alpha> IMP \<alpha> OR \<beta>
[PROOF STEP]
by (blast intro: Disj_I1)
[PROOF STATE]
proof (state)
this:
{} \<turnstile> \<alpha> IMP \<alpha> OR \<beta>

goal (1 subgoal):
 1. H \<turnstile> PfP (ssubst \<lfloor>\<alpha> OR \<beta>\<rfloor>V V F)
[PROOF STEP]
hence "quote_all p V \<turnstile> PfP (ssubst \<lfloor>\<alpha>\<rfloor>V V F) IMP PfP (ssubst \<lfloor>\<alpha> OR \<beta>\<rfloor>V V F)"
[PROOF STATE]
proof (prove)
using this:
{} \<turnstile> \<alpha> IMP \<alpha> OR \<beta>

goal (1 subgoal):
 1. quote_all p V \<turnstile> PfP (ssubst \<lfloor>\<alpha>\<rfloor>V V F) IMP PfP (ssubst \<lfloor>\<alpha> OR \<beta>\<rfloor>V V F)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
{} \<turnstile> \<alpha> IMP \<alpha> OR \<beta>
V \<subseteq> Vs
supp \<alpha> \<subseteq> atom ` Vs
supp \<beta> \<subseteq> atom ` Vs
H \<turnstile> PfP (ssubst \<lfloor>\<alpha>\<rfloor>V V F)
quote_all p V \<subseteq> H

goal (1 subgoal):
 1. quote_all p V \<turnstile> PfP (ssubst \<lfloor>\<alpha>\<rfloor>V V F) IMP PfP (ssubst \<lfloor>\<alpha> OR \<beta>\<rfloor>V V F)
[PROOF STEP]
by (auto simp: quote_all_MonPon_PfP_ssubst)
[PROOF STATE]
proof (state)
this:
quote_all p V \<turnstile> PfP (ssubst \<lfloor>\<alpha>\<rfloor>V V F) IMP PfP (ssubst \<lfloor>\<alpha> OR \<beta>\<rfloor>V V F)

goal (1 subgoal):
 1. H \<turnstile> PfP (ssubst \<lfloor>\<alpha> OR \<beta>\<rfloor>V V F)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
quote_all p V \<turnstile> PfP (ssubst \<lfloor>\<alpha>\<rfloor>V V F) IMP PfP (ssubst \<lfloor>\<alpha> OR \<beta>\<rfloor>V V F)

goal (1 subgoal):
 1. H \<turnstile> PfP (ssubst \<lfloor>\<alpha> OR \<beta>\<rfloor>V V F)
[PROOF STEP]
by (metis MP_same prems thin)
[PROOF STATE]
proof (state)
this:
H \<turnstile> PfP (ssubst \<lfloor>\<alpha> OR \<beta>\<rfloor>V V F)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma quote_all_Disj_I2_PfP_ssubst:
  assumes "V \<subseteq> Vs" "supp \<alpha> \<subseteq> atom ` Vs" "supp \<beta> \<subseteq> atom ` Vs"
      and prems: "H \<turnstile> PfP (ssubst \<lfloor>\<beta>\<rfloor>V V F)" "quote_all p V \<subseteq> H"
    shows "H \<turnstile> PfP (ssubst \<lfloor>\<alpha> OR \<beta>\<rfloor>V V F)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. H \<turnstile> PfP (ssubst \<lfloor>\<alpha> OR \<beta>\<rfloor>V V F)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. H \<turnstile> PfP (ssubst \<lfloor>\<alpha> OR \<beta>\<rfloor>V V F)
[PROOF STEP]
have "{} \<turnstile> \<beta> IMP (\<alpha> OR \<beta>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {} \<turnstile> \<beta> IMP \<alpha> OR \<beta>
[PROOF STEP]
by (blast intro: Disj_I2)
[PROOF STATE]
proof (state)
this:
{} \<turnstile> \<beta> IMP \<alpha> OR \<beta>

goal (1 subgoal):
 1. H \<turnstile> PfP (ssubst \<lfloor>\<alpha> OR \<beta>\<rfloor>V V F)
[PROOF STEP]
hence "quote_all p V \<turnstile> PfP (ssubst \<lfloor>\<beta>\<rfloor>V V F) IMP PfP (ssubst \<lfloor>\<alpha> OR \<beta>\<rfloor>V V F)"
[PROOF STATE]
proof (prove)
using this:
{} \<turnstile> \<beta> IMP \<alpha> OR \<beta>

goal (1 subgoal):
 1. quote_all p V \<turnstile> PfP (ssubst \<lfloor>\<beta>\<rfloor>V V F) IMP PfP (ssubst \<lfloor>\<alpha> OR \<beta>\<rfloor>V V F)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
{} \<turnstile> \<beta> IMP \<alpha> OR \<beta>
V \<subseteq> Vs
supp \<alpha> \<subseteq> atom ` Vs
supp \<beta> \<subseteq> atom ` Vs
H \<turnstile> PfP (ssubst \<lfloor>\<beta>\<rfloor>V V F)
quote_all p V \<subseteq> H

goal (1 subgoal):
 1. quote_all p V \<turnstile> PfP (ssubst \<lfloor>\<beta>\<rfloor>V V F) IMP PfP (ssubst \<lfloor>\<alpha> OR \<beta>\<rfloor>V V F)
[PROOF STEP]
by (auto simp: quote_all_MonPon_PfP_ssubst)
[PROOF STATE]
proof (state)
this:
quote_all p V \<turnstile> PfP (ssubst \<lfloor>\<beta>\<rfloor>V V F) IMP PfP (ssubst \<lfloor>\<alpha> OR \<beta>\<rfloor>V V F)

goal (1 subgoal):
 1. H \<turnstile> PfP (ssubst \<lfloor>\<alpha> OR \<beta>\<rfloor>V V F)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
quote_all p V \<turnstile> PfP (ssubst \<lfloor>\<beta>\<rfloor>V V F) IMP PfP (ssubst \<lfloor>\<alpha> OR \<beta>\<rfloor>V V F)

goal (1 subgoal):
 1. H \<turnstile> PfP (ssubst \<lfloor>\<alpha> OR \<beta>\<rfloor>V V F)
[PROOF STEP]
by (metis MP_same prems thin)
[PROOF STATE]
proof (state)
this:
H \<turnstile> PfP (ssubst \<lfloor>\<alpha> OR \<beta>\<rfloor>V V F)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma quote_all_Conj_I_PfP_ssubst:
  assumes "V \<subseteq> Vs" "supp \<alpha> \<subseteq> atom ` Vs" "supp \<beta> \<subseteq> atom ` Vs"
      and prems: "H \<turnstile> PfP (ssubst \<lfloor>\<alpha>\<rfloor>V V F)" "H \<turnstile> PfP (ssubst \<lfloor>\<beta>\<rfloor>V V F)" "quote_all p V \<subseteq> H"
    shows "H \<turnstile> PfP (ssubst \<lfloor>\<alpha> AND \<beta>\<rfloor>V V F)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. H \<turnstile> PfP (ssubst \<lfloor>\<alpha> AND \<beta>\<rfloor>V V F)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. H \<turnstile> PfP (ssubst \<lfloor>\<alpha> AND \<beta>\<rfloor>V V F)
[PROOF STEP]
have "{} \<turnstile> \<alpha> IMP \<beta> IMP (\<alpha> AND \<beta>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {} \<turnstile> \<alpha> IMP \<beta> IMP \<alpha> AND \<beta>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
{} \<turnstile> \<alpha> IMP \<beta> IMP \<alpha> AND \<beta>

goal (1 subgoal):
 1. H \<turnstile> PfP (ssubst \<lfloor>\<alpha> AND \<beta>\<rfloor>V V F)
[PROOF STEP]
hence "quote_all p V
         \<turnstile> PfP (ssubst \<lfloor>\<alpha>\<rfloor>V V F) IMP PfP (ssubst \<lfloor>\<beta>\<rfloor>V V F) IMP PfP (ssubst \<lfloor>\<alpha> AND \<beta>\<rfloor>V V F)"
[PROOF STATE]
proof (prove)
using this:
{} \<turnstile> \<alpha> IMP \<beta> IMP \<alpha> AND \<beta>

goal (1 subgoal):
 1. quote_all p V \<turnstile> PfP (ssubst \<lfloor>\<alpha>\<rfloor>V V F) IMP PfP (ssubst \<lfloor>\<beta>\<rfloor>V V F) IMP PfP (ssubst \<lfloor>\<alpha> AND \<beta>\<rfloor>V V F)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
{} \<turnstile> \<alpha> IMP \<beta> IMP \<alpha> AND \<beta>
V \<subseteq> Vs
supp \<alpha> \<subseteq> atom ` Vs
supp \<beta> \<subseteq> atom ` Vs
H \<turnstile> PfP (ssubst \<lfloor>\<alpha>\<rfloor>V V F)
H \<turnstile> PfP (ssubst \<lfloor>\<beta>\<rfloor>V V F)
quote_all p V \<subseteq> H

goal (1 subgoal):
 1. quote_all p V \<turnstile> PfP (ssubst \<lfloor>\<alpha>\<rfloor>V V F) IMP PfP (ssubst \<lfloor>\<beta>\<rfloor>V V F) IMP PfP (ssubst \<lfloor>\<alpha> AND \<beta>\<rfloor>V V F)
[PROOF STEP]
by (auto simp: quote_all_MonPon2_PfP_ssubst)
[PROOF STATE]
proof (state)
this:
quote_all p V \<turnstile> PfP (ssubst \<lfloor>\<alpha>\<rfloor>V V F) IMP PfP (ssubst \<lfloor>\<beta>\<rfloor>V V F) IMP PfP (ssubst \<lfloor>\<alpha> AND \<beta>\<rfloor>V V F)

goal (1 subgoal):
 1. H \<turnstile> PfP (ssubst \<lfloor>\<alpha> AND \<beta>\<rfloor>V V F)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
quote_all p V \<turnstile> PfP (ssubst \<lfloor>\<alpha>\<rfloor>V V F) IMP PfP (ssubst \<lfloor>\<beta>\<rfloor>V V F) IMP PfP (ssubst \<lfloor>\<alpha> AND \<beta>\<rfloor>V V F)

goal (1 subgoal):
 1. H \<turnstile> PfP (ssubst \<lfloor>\<alpha> AND \<beta>\<rfloor>V V F)
[PROOF STEP]
by (metis MP_same prems thin)
[PROOF STATE]
proof (state)
this:
H \<turnstile> PfP (ssubst \<lfloor>\<alpha> AND \<beta>\<rfloor>V V F)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma quote_all_Contra_PfP_ssubst:
  assumes "V \<subseteq> Vs" "supp \<alpha> \<subseteq> atom ` Vs"
  shows "quote_all p V
         \<turnstile> PfP (ssubst \<lfloor>\<alpha>\<rfloor>V V F) IMP PfP (ssubst \<lfloor>Neg \<alpha>\<rfloor>V V F) IMP PfP (ssubst \<lfloor>Fls\<rfloor>V V F)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. quote_all p V \<turnstile> PfP (ssubst \<lfloor>\<alpha>\<rfloor>V V F) IMP PfP (ssubst \<lfloor>Neg \<alpha>\<rfloor>V V F) IMP PfP (ssubst \<lfloor>Fls\<rfloor>V V F)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. quote_all p V \<turnstile> PfP (ssubst \<lfloor>\<alpha>\<rfloor>V V F) IMP PfP (ssubst \<lfloor>Neg \<alpha>\<rfloor>V V F) IMP PfP (ssubst \<lfloor>Fls\<rfloor>V V F)
[PROOF STEP]
have "{} \<turnstile> \<alpha> IMP Neg \<alpha> IMP Fls"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {} \<turnstile> \<alpha> IMP Neg \<alpha> IMP Fls
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
{} \<turnstile> \<alpha> IMP Neg \<alpha> IMP Fls

goal (1 subgoal):
 1. quote_all p V \<turnstile> PfP (ssubst \<lfloor>\<alpha>\<rfloor>V V F) IMP PfP (ssubst \<lfloor>Neg \<alpha>\<rfloor>V V F) IMP PfP (ssubst \<lfloor>Fls\<rfloor>V V F)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
{} \<turnstile> \<alpha> IMP Neg \<alpha> IMP Fls

goal (1 subgoal):
 1. quote_all p V \<turnstile> PfP (ssubst \<lfloor>\<alpha>\<rfloor>V V F) IMP PfP (ssubst \<lfloor>Neg \<alpha>\<rfloor>V V F) IMP PfP (ssubst \<lfloor>Fls\<rfloor>V V F)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
{} \<turnstile> \<alpha> IMP Neg \<alpha> IMP Fls
V \<subseteq> Vs
supp \<alpha> \<subseteq> atom ` Vs

goal (1 subgoal):
 1. quote_all p V \<turnstile> PfP (ssubst \<lfloor>\<alpha>\<rfloor>V V F) IMP PfP (ssubst \<lfloor>Neg \<alpha>\<rfloor>V V F) IMP PfP (ssubst \<lfloor>Fls\<rfloor>V V F)
[PROOF STEP]
by (auto simp: quote_all_MonPon2_PfP_ssubst supp_conv_fresh)
[PROOF STATE]
proof (state)
this:
quote_all p V \<turnstile> PfP (ssubst \<lfloor>\<alpha>\<rfloor>V V F) IMP PfP (ssubst \<lfloor>Neg \<alpha>\<rfloor>V V F) IMP PfP (ssubst \<lfloor>Fls\<rfloor>V V F)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma fresh_ssubst_dbtm: "\<lbrakk>atom i \<sharp> p\<bullet>V; V \<subseteq> Vs\<rbrakk> \<Longrightarrow> atom i \<sharp> ssubst (vquot_dbtm V t) V F"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>atom i \<sharp> p \<bullet> V; V \<subseteq> Vs\<rbrakk> \<Longrightarrow> atom i \<sharp> ssubst (vquot_dbtm V t) V F
[PROOF STEP]
by (induct t rule: dbtm.induct) (auto simp: F_unfold fresh_image permute_set_eq_image)


[STATEMENT]
lemma fresh_ssubst_dbfm: "\<lbrakk>atom i \<sharp> p\<bullet>V; V \<subseteq> Vs\<rbrakk> \<Longrightarrow> atom i \<sharp> ssubst (vquot_dbfm V A) V F"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>atom i \<sharp> p \<bullet> V; V \<subseteq> Vs\<rbrakk> \<Longrightarrow> atom i \<sharp> ssubst (vquot_dbfm V A) V F
[PROOF STEP]
by (nominal_induct A rule: dbfm.strong_induct) (auto simp: fresh_ssubst_dbtm)


[STATEMENT]
lemma fresh_ssubst_fm:
  fixes A::fm shows "\<lbrakk>atom i \<sharp> p\<bullet>V; V \<subseteq> Vs\<rbrakk> \<Longrightarrow> atom i \<sharp> ssubst (\<lfloor>A\<rfloor>V) V F"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>atom i \<sharp> p \<bullet> V; V \<subseteq> Vs\<rbrakk> \<Longrightarrow> atom i \<sharp> ssubst \<lfloor>A\<rfloor>V V F
[PROOF STEP]
by (simp add: fresh_ssubst_dbfm vquot_fm_def)