[STATEMENT]
lemma SeqAppendP_fresh_iff [simp]:
  "a \<sharp> SeqAppendP f1 k1 f2 k2 g \<longleftrightarrow> a \<sharp> f1 \<and> a \<sharp> k1 \<and> a \<sharp> f2 \<and> a \<sharp> k2 \<and> a \<sharp> g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<sharp> SeqAppendP f1 k1 f2 k2 g = (a \<sharp> f1 \<and> a \<sharp> k1 \<and> a \<sharp> f2 \<and> a \<sharp> k2 \<and> a \<sharp> g)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a \<sharp> SeqAppendP f1 k1 f2 k2 g = (a \<sharp> f1 \<and> a \<sharp> k1 \<and> a \<sharp> f2 \<and> a \<sharp> k2 \<and> a \<sharp> g)
[PROOF STEP]
obtain g1::name and g2::name
    where "atom g1 \<sharp> (g2,f1,k1,f2,k2,g)" "atom g2 \<sharp> (f1,k1,f2,k2,g)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>g1 g2. \<lbrakk>atom g1 \<sharp> (g2, f1, k1, f2, k2, g); atom g2 \<sharp> (f1, k1, f2, k2, g)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis obtain_fresh)
[PROOF STATE]
proof (state)
this:
atom g1 \<sharp> (g2, f1, k1, f2, k2, g)
atom g2 \<sharp> (f1, k1, f2, k2, g)

goal (1 subgoal):
 1. a \<sharp> SeqAppendP f1 k1 f2 k2 g = (a \<sharp> f1 \<and> a \<sharp> k1 \<and> a \<sharp> f2 \<and> a \<sharp> k2 \<and> a \<sharp> g)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
atom g1 \<sharp> (g2, f1, k1, f2, k2, g)
atom g2 \<sharp> (f1, k1, f2, k2, g)

goal (1 subgoal):
 1. a \<sharp> SeqAppendP f1 k1 f2 k2 g = (a \<sharp> f1 \<and> a \<sharp> k1 \<and> a \<sharp> f2 \<and> a \<sharp> k2 \<and> a \<sharp> g)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a \<sharp> SeqAppendP f1 k1 f2 k2 g = (a \<sharp> f1 \<and> a \<sharp> k1 \<and> a \<sharp> f2 \<and> a \<sharp> k2 \<and> a \<sharp> g)

goal:
No subgoals!
[PROOF STEP]
qed