[STATEMENT]
theorem AbstFormP_Neg: "{AbstFormP v i x x'} \<turnstile> AbstFormP v i (Q_Neg x) (Q_Neg x')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {AbstFormP v i x x'} \<turnstile> AbstFormP v i (Q_Neg x) (Q_Neg x')
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. {AbstFormP v i x x'} \<turnstile> AbstFormP v i (Q_Neg x) (Q_Neg x')
[PROOF STEP]
obtain k1::name and s1::name and k::name and s::name
    where "atom s1 \<sharp> (v,i,x,x')"        "atom k1 \<sharp> (v,i,x,x',s1)"
      "atom s  \<sharp> (v,i,x,x',k1,s1)"  "atom k  \<sharp> (v,i,x,x',s,k1,s1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>s1 k1 s k. \<lbrakk>atom s1 \<sharp> (v, i, x, x'); atom k1 \<sharp> (v, i, x, x', s1); atom s \<sharp> (v, i, x, x', k1, s1); atom k \<sharp> (v, i, x, x', s, k1, s1)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis obtain_fresh)
[PROOF STATE]
proof (state)
this:
atom s1 \<sharp> (v, i, x, x')
atom k1 \<sharp> (v, i, x, x', s1)
atom s \<sharp> (v, i, x, x', k1, s1)
atom k \<sharp> (v, i, x, x', s, k1, s1)

goal (1 subgoal):
 1. {AbstFormP v i x x'} \<turnstile> AbstFormP v i (Q_Neg x) (Q_Neg x')
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
atom s1 \<sharp> (v, i, x, x')
atom k1 \<sharp> (v, i, x, x', s1)
atom s \<sharp> (v, i, x, x', k1, s1)
atom k \<sharp> (v, i, x, x', s, k1, s1)

goal (1 subgoal):
 1. {AbstFormP v i x x'} \<turnstile> AbstFormP v i (Q_Neg x) (Q_Neg x')
[PROOF STEP]
by (force simp: AbstFormP.simps [of s v i "Q_Neg x" _ k] AbstFormP.simps [of s1 v i x x' k1]
        intro: SeqAbstFormP_Neg [THEN cut3])
[PROOF STATE]
proof (state)
this:
{AbstFormP v i x x'} \<turnstile> AbstFormP v i (Q_Neg x) (Q_Neg x')

goal:
No subgoals!
[PROOF STEP]
qed