[STATEMENT]
lemma
  assumes "atom i \<sharp> (j,j',i')" "atom i' \<sharp> (j,j')" "atom j \<sharp> (j')"
  shows QuoteP_Mem_imp_QMem:
        "{QuoteP (Var i) (Var i'), QuoteP (Var j) (Var j'), Var i IN Var j}
         \<turnstile> PfP (Q_Mem (Var i') (Var j'))"     (is ?thesis1)
    and QuoteP_Mem_imp_QSubset:
        "{QuoteP (Var i) (Var i'), QuoteP (Var j) (Var j'), Var i SUBS Var j}
         \<turnstile> PfP (Q_Subset (Var i') (Var j'))"  (is ?thesis2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {QuoteP (Var i) (Var i'), QuoteP (Var j) (Var j'), Var i IN Var j} \<turnstile> PfP (Q_Mem (Var i') (Var j')) &&& {QuoteP (Var i) (Var i'), QuoteP (Var j) (Var j'), Var i SUBS Var j} \<turnstile> PfP (Q_Subset (Var i') (Var j'))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. {QuoteP (Var i) (Var i'), QuoteP (Var j) (Var j'), Var i IN Var j} \<turnstile> PfP (Q_Mem (Var i') (Var j'))
 2. {QuoteP (Var i) (Var i'), QuoteP (Var j) (Var j'), Var i SUBS Var j} \<turnstile> PfP (Q_Subset (Var i') (Var j'))
[PROOF STEP]
obtain si::name and ki::name and sj::name and kj::name
    where atoms: "atom si \<sharp> (ki,sj,kj,i,j,j',i')"  "atom ki \<sharp> (sj,kj,i,j,j',i')"
                 "atom sj \<sharp> (kj,i,j,j',i')"  "atom kj \<sharp> (i,j,j',i')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>si ki sj kj. \<lbrakk>atom si \<sharp> (ki, sj, kj, i, j, j', i'); atom ki \<sharp> (sj, kj, i, j, j', i'); atom sj \<sharp> (kj, i, j, j', i'); atom kj \<sharp> (i, j, j', i')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis obtain_fresh)
[PROOF STATE]
proof (state)
this:
atom si \<sharp> (ki, sj, kj, i, j, j', i')
atom ki \<sharp> (sj, kj, i, j, j', i')
atom sj \<sharp> (kj, i, j, j', i')
atom kj \<sharp> (i, j, j', i')

goal (2 subgoals):
 1. {QuoteP (Var i) (Var i'), QuoteP (Var j) (Var j'), Var i IN Var j} \<turnstile> PfP (Q_Mem (Var i') (Var j'))
 2. {QuoteP (Var i) (Var i'), QuoteP (Var j) (Var j'), Var i SUBS Var j} \<turnstile> PfP (Q_Subset (Var i') (Var j'))
[PROOF STEP]
hence C:  "{QuoteP (Var i) (Var i'), QuoteP (Var j) (Var j')}
             \<turnstile> (Var i IN Var j IMP PfP (Q_Mem (Var i') (Var j')))  AND
               (Var i SUBS Var j IMP PfP (Q_Subset (Var i') (Var j')))"
[PROOF STATE]
proof (prove)
using this:
atom si \<sharp> (ki, sj, kj, i, j, j', i')
atom ki \<sharp> (sj, kj, i, j, j', i')
atom sj \<sharp> (kj, i, j, j', i')
atom kj \<sharp> (i, j, j', i')

goal (1 subgoal):
 1. {QuoteP (Var i) (Var i'), QuoteP (Var j) (Var j')} \<turnstile> (Var i IN Var j IMP PfP (Q_Mem (Var i') (Var j'))) AND (Var i SUBS Var j IMP PfP (Q_Subset (Var i') (Var j')))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
atom si \<sharp> (ki, sj, kj, i, j, j', i')
atom ki \<sharp> (sj, kj, i, j, j', i')
atom sj \<sharp> (kj, i, j, j', i')
atom kj \<sharp> (i, j, j', i')
atom i \<sharp> (j, j', i')
atom i' \<sharp> (j, j')
atom j \<sharp> j'

goal (1 subgoal):
 1. {QuoteP (Var i) (Var i'), QuoteP (Var j) (Var j')} \<turnstile> (Var i IN Var j IMP PfP (Q_Mem (Var i') (Var j'))) AND (Var i SUBS Var j IMP PfP (Q_Subset (Var i') (Var j')))
[PROOF STEP]
by (auto simp: QuoteP.simps [of si "Var i" _ ki] QuoteP.simps [of sj "Var j" _ kj]
             intro!: SeqQuoteP_Mem_imp_QMem_and_Subset del: Conj_I)
[PROOF STATE]
proof (state)
this:
{QuoteP (Var i) (Var i'), QuoteP (Var j) (Var j')} \<turnstile> (Var i IN Var j IMP PfP (Q_Mem (Var i') (Var j'))) AND (Var i SUBS Var j IMP PfP (Q_Subset (Var i') (Var j')))

goal (2 subgoals):
 1. {QuoteP (Var i) (Var i'), QuoteP (Var j) (Var j'), Var i IN Var j} \<turnstile> PfP (Q_Mem (Var i') (Var j'))
 2. {QuoteP (Var i) (Var i'), QuoteP (Var j) (Var j'), Var i SUBS Var j} \<turnstile> PfP (Q_Subset (Var i') (Var j'))
[PROOF STEP]
show ?thesis1
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {QuoteP (Var i) (Var i'), QuoteP (Var j) (Var j'), Var i IN Var j} \<turnstile> PfP (Q_Mem (Var i') (Var j'))
[PROOF STEP]
by (best intro: Conj_E1 [OF C, THEN MP_thin])
[PROOF STATE]
proof (state)
this:
{QuoteP (Var i) (Var i'), QuoteP (Var j) (Var j'), Var i IN Var j} \<turnstile> PfP (Q_Mem (Var i') (Var j'))

goal (1 subgoal):
 1. {QuoteP (Var i) (Var i'), QuoteP (Var j) (Var j'), Var i SUBS Var j} \<turnstile> PfP (Q_Subset (Var i') (Var j'))
[PROOF STEP]
show ?thesis2
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {QuoteP (Var i) (Var i'), QuoteP (Var j) (Var j'), Var i SUBS Var j} \<turnstile> PfP (Q_Subset (Var i') (Var j'))
[PROOF STEP]
by (best intro: Conj_E2 [OF C, THEN MP_thin])
[PROOF STATE]
proof (state)
this:
{QuoteP (Var i) (Var i'), QuoteP (Var j) (Var j'), Var i SUBS Var j} \<turnstile> PfP (Q_Subset (Var i') (Var j'))

goal:
No subgoals!
[PROOF STEP]
qed