[STATEMENT]
lemma HaddP_SUCC_Ex1:
  assumes "atom i \<sharp> (x,y,z)"
    shows "insert (HaddP (SUCC x) y z) (insert (OrdP x) H)
           \<turnstile> Ex i (HaddP x y (Var i) AND z EQ SUCC (Var i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert (HaddP (SUCC x) y z) (insert (OrdP x) H) \<turnstile> SyntaxN.Ex i (HaddP x y (Var i) AND z EQ SUCC (Var i))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. insert (HaddP (SUCC x) y z) (insert (OrdP x) H) \<turnstile> SyntaxN.Ex i (HaddP x y (Var i) AND z EQ SUCC (Var i))
[PROOF STEP]
have "{ HaddP (SUCC x) y z, OrdP x } \<turnstile> Ex i (HaddP x y (Var i) AND z EQ SUCC (Var i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {HaddP (SUCC x) y z, OrdP x} \<turnstile> SyntaxN.Ex i (HaddP x y (Var i) AND z EQ SUCC (Var i))
[PROOF STEP]
apply (rule cut_same [OF HaddP_commute [THEN cut2]])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. {HaddP (SUCC x) y z, OrdP x} \<turnstile> HaddP ?x2 ?y2 ?z2
 2. {HaddP (SUCC x) y z, OrdP x} \<turnstile> OrdP ?x2
 3. {HaddP ?y2 ?x2 ?z2, HaddP (SUCC x) y z, OrdP x} \<turnstile> SyntaxN.Ex i (HaddP x y (Var i) AND z EQ SUCC (Var i))
[PROOF STEP]
apply (blast intro: OrdP_SUCC_I)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {HaddP y (SUCC x) z, HaddP (SUCC x) y z, OrdP x} \<turnstile> SyntaxN.Ex i (HaddP x y (Var i) AND z EQ SUCC (Var i))
[PROOF STEP]
apply (rule cut_same [OF HaddP_SUCC_Ex2 [where z'=i]], blast)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. atom i \<sharp> (y, x, z)
 2. {SyntaxN.Ex i (HaddP y x (Var i) AND z EQ SUCC (Var i)), HaddP y (SUCC x) z, HaddP (SUCC x) y z, OrdP x} \<turnstile> SyntaxN.Ex i (HaddP x y (Var i) AND z EQ SUCC (Var i))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
atom i \<sharp> (x, y, z)

goal (2 subgoals):
 1. atom i \<sharp> (y, x, z)
 2. {SyntaxN.Ex i (HaddP y x (Var i) AND z EQ SUCC (Var i)), HaddP y (SUCC x) z, HaddP (SUCC x) y z, OrdP x} \<turnstile> SyntaxN.Ex i (HaddP x y (Var i) AND z EQ SUCC (Var i))
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. atom i \<sharp> (x, y, z) \<Longrightarrow> {HaddP y x (Var i), z EQ SUCC (Var i), HaddP y (SUCC x) z, HaddP (SUCC x) y z, OrdP x} \<turnstile> SyntaxN.Ex i (HaddP x y (Var i) AND z EQ SUCC (Var i))
[PROOF STEP]
apply (auto intro!: Ex_I [where x="Var i"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. atom i \<sharp> (x, y, z) \<Longrightarrow> {HaddP y x (Var i), z EQ SUCC (Var i), HaddP y (SUCC x) z, HaddP (SUCC x) y z, OrdP x} \<turnstile> HaddP x y (Var i)
[PROOF STEP]
by (metis AssumeH(2) HaddP_commute [THEN cut2] HaddP_imp_OrdP rotate2 thin1)
[PROOF STATE]
proof (state)
this:
{HaddP (SUCC x) y z, OrdP x} \<turnstile> SyntaxN.Ex i (HaddP x y (Var i) AND z EQ SUCC (Var i))

goal (1 subgoal):
 1. insert (HaddP (SUCC x) y z) (insert (OrdP x) H) \<turnstile> SyntaxN.Ex i (HaddP x y (Var i) AND z EQ SUCC (Var i))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
{HaddP (SUCC x) y z, OrdP x} \<turnstile> SyntaxN.Ex i (HaddP x y (Var i) AND z EQ SUCC (Var i))

goal (1 subgoal):
 1. insert (HaddP (SUCC x) y z) (insert (OrdP x) H) \<turnstile> SyntaxN.Ex i (HaddP x y (Var i) AND z EQ SUCC (Var i))
[PROOF STEP]
by (metis Assume AssumeH(2) cut2)
[PROOF STATE]
proof (state)
this:
insert (HaddP (SUCC x) y z) (insert (OrdP x) H) \<turnstile> SyntaxN.Ex i (HaddP x y (Var i) AND z EQ SUCC (Var i))

goal:
No subgoals!
[PROOF STEP]
qed