[STATEMENT]
lemma weaken_assumptions:
  fixes p :: \<open>('a, 'b) form\<close>
  assumes inf_params: \<open>infinite (UNIV :: 'a set)\<close>
  shows \<open>z \<turnstile> p \<Longrightarrow> set z \<subseteq> set z' \<Longrightarrow> z' \<turnstile> p\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>z \<turnstile> p; set z \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> p
[PROOF STEP]
proof (induct z p arbitrary: z' rule: deriv.induct)
[PROOF STATE]
proof (state)
goal (18 subgoals):
 1. \<And>a G z'. \<lbrakk>a \<in> set G; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> a
 2. \<And>G z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> TT
 3. \<And>G a z'. \<lbrakk>G \<turnstile> FF; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> FF; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> a
 4. \<And>a G z'. \<lbrakk>a # G \<turnstile> FF; \<And>z'. set (a # G) \<subseteq> set z' \<Longrightarrow> z' \<turnstile> FF; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Neg a
 5. \<And>G a z'. \<lbrakk>G \<turnstile> Neg a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> Neg a; G \<turnstile> a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> FF
 6. \<And>a G z'. \<lbrakk>Neg a # G \<turnstile> FF; \<And>z'. set (Neg a # G) \<subseteq> set z' \<Longrightarrow> z' \<turnstile> FF; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> a
 7. \<And>G a b z'. \<lbrakk>G \<turnstile> a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a; G \<turnstile> b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> And a b
 8. \<And>G a b z'. \<lbrakk>G \<turnstile> And a b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> And a b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> a
 9. \<And>G a b z'. \<lbrakk>G \<turnstile> And a b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> And a b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> b
 10. \<And>G a b z'. \<lbrakk>G \<turnstile> a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Or a b
A total of 18 subgoals...
[PROOF STEP]
case (Assum p z)
[PROOF STATE]
proof (state)
this:
p \<in> set z
set z \<subseteq> set z'

goal (18 subgoals):
 1. \<And>a G z'. \<lbrakk>a \<in> set G; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> a
 2. \<And>G z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> TT
 3. \<And>G a z'. \<lbrakk>G \<turnstile> FF; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> FF; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> a
 4. \<And>a G z'. \<lbrakk>a # G \<turnstile> FF; \<And>z'. set (a # G) \<subseteq> set z' \<Longrightarrow> z' \<turnstile> FF; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Neg a
 5. \<And>G a z'. \<lbrakk>G \<turnstile> Neg a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> Neg a; G \<turnstile> a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> FF
 6. \<And>a G z'. \<lbrakk>Neg a # G \<turnstile> FF; \<And>z'. set (Neg a # G) \<subseteq> set z' \<Longrightarrow> z' \<turnstile> FF; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> a
 7. \<And>G a b z'. \<lbrakk>G \<turnstile> a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a; G \<turnstile> b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> And a b
 8. \<And>G a b z'. \<lbrakk>G \<turnstile> And a b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> And a b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> a
 9. \<And>G a b z'. \<lbrakk>G \<turnstile> And a b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> And a b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> b
 10. \<And>G a b z'. \<lbrakk>G \<turnstile> a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Or a b
A total of 18 subgoals...
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p \<in> set z
set z \<subseteq> set z'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
p \<in> set z
set z \<subseteq> set z'

goal (1 subgoal):
 1. z' \<turnstile> p
[PROOF STEP]
using deriv.Assum
[PROOF STATE]
proof (prove)
using this:
p \<in> set z
set z \<subseteq> set z'
?a \<in> set ?G \<Longrightarrow> ?G \<turnstile> ?a

goal (1 subgoal):
 1. z' \<turnstile> p
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
z' \<turnstile> p

goal (17 subgoals):
 1. \<And>G z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> TT
 2. \<And>G a z'. \<lbrakk>G \<turnstile> FF; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> FF; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> a
 3. \<And>a G z'. \<lbrakk>a # G \<turnstile> FF; \<And>z'. set (a # G) \<subseteq> set z' \<Longrightarrow> z' \<turnstile> FF; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Neg a
 4. \<And>G a z'. \<lbrakk>G \<turnstile> Neg a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> Neg a; G \<turnstile> a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> FF
 5. \<And>a G z'. \<lbrakk>Neg a # G \<turnstile> FF; \<And>z'. set (Neg a # G) \<subseteq> set z' \<Longrightarrow> z' \<turnstile> FF; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> a
 6. \<And>G a b z'. \<lbrakk>G \<turnstile> a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a; G \<turnstile> b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> And a b
 7. \<And>G a b z'. \<lbrakk>G \<turnstile> And a b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> And a b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> a
 8. \<And>G a b z'. \<lbrakk>G \<turnstile> And a b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> And a b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> b
 9. \<And>G a b z'. \<lbrakk>G \<turnstile> a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Or a b
 10. \<And>G b a z'. \<lbrakk>G \<turnstile> b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Or a b
A total of 17 subgoals...
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (17 subgoals):
 1. \<And>G z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> TT
 2. \<And>G a z'. \<lbrakk>G \<turnstile> FF; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> FF; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> a
 3. \<And>a G z'. \<lbrakk>a # G \<turnstile> FF; \<And>z'. set (a # G) \<subseteq> set z' \<Longrightarrow> z' \<turnstile> FF; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Neg a
 4. \<And>G a z'. \<lbrakk>G \<turnstile> Neg a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> Neg a; G \<turnstile> a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> FF
 5. \<And>a G z'. \<lbrakk>Neg a # G \<turnstile> FF; \<And>z'. set (Neg a # G) \<subseteq> set z' \<Longrightarrow> z' \<turnstile> FF; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> a
 6. \<And>G a b z'. \<lbrakk>G \<turnstile> a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a; G \<turnstile> b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> And a b
 7. \<And>G a b z'. \<lbrakk>G \<turnstile> And a b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> And a b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> a
 8. \<And>G a b z'. \<lbrakk>G \<turnstile> And a b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> And a b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> b
 9. \<And>G a b z'. \<lbrakk>G \<turnstile> a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Or a b
 10. \<And>G b a z'. \<lbrakk>G \<turnstile> b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Or a b
A total of 17 subgoals...
[PROOF STEP]
case TTI
[PROOF STATE]
proof (state)
this:
set G_ \<subseteq> set z'

goal (17 subgoals):
 1. \<And>G z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> TT
 2. \<And>G a z'. \<lbrakk>G \<turnstile> FF; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> FF; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> a
 3. \<And>a G z'. \<lbrakk>a # G \<turnstile> FF; \<And>z'. set (a # G) \<subseteq> set z' \<Longrightarrow> z' \<turnstile> FF; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Neg a
 4. \<And>G a z'. \<lbrakk>G \<turnstile> Neg a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> Neg a; G \<turnstile> a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> FF
 5. \<And>a G z'. \<lbrakk>Neg a # G \<turnstile> FF; \<And>z'. set (Neg a # G) \<subseteq> set z' \<Longrightarrow> z' \<turnstile> FF; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> a
 6. \<And>G a b z'. \<lbrakk>G \<turnstile> a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a; G \<turnstile> b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> And a b
 7. \<And>G a b z'. \<lbrakk>G \<turnstile> And a b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> And a b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> a
 8. \<And>G a b z'. \<lbrakk>G \<turnstile> And a b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> And a b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> b
 9. \<And>G a b z'. \<lbrakk>G \<turnstile> a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Or a b
 10. \<And>G b a z'. \<lbrakk>G \<turnstile> b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Or a b
A total of 17 subgoals...
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
set G_ \<subseteq> set z'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
set G_ \<subseteq> set z'

goal (1 subgoal):
 1. z' \<turnstile> TT
[PROOF STEP]
using deriv.TTI
[PROOF STATE]
proof (prove)
using this:
set G_ \<subseteq> set z'
?G \<turnstile> TT

goal (1 subgoal):
 1. z' \<turnstile> TT
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
z' \<turnstile> TT

goal (16 subgoals):
 1. \<And>G a z'. \<lbrakk>G \<turnstile> FF; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> FF; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> a
 2. \<And>a G z'. \<lbrakk>a # G \<turnstile> FF; \<And>z'. set (a # G) \<subseteq> set z' \<Longrightarrow> z' \<turnstile> FF; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Neg a
 3. \<And>G a z'. \<lbrakk>G \<turnstile> Neg a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> Neg a; G \<turnstile> a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> FF
 4. \<And>a G z'. \<lbrakk>Neg a # G \<turnstile> FF; \<And>z'. set (Neg a # G) \<subseteq> set z' \<Longrightarrow> z' \<turnstile> FF; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> a
 5. \<And>G a b z'. \<lbrakk>G \<turnstile> a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a; G \<turnstile> b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> And a b
 6. \<And>G a b z'. \<lbrakk>G \<turnstile> And a b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> And a b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> a
 7. \<And>G a b z'. \<lbrakk>G \<turnstile> And a b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> And a b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> b
 8. \<And>G a b z'. \<lbrakk>G \<turnstile> a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Or a b
 9. \<And>G b a z'. \<lbrakk>G \<turnstile> b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Or a b
 10. \<And>G a b c z'. \<lbrakk>G \<turnstile> Or a b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> Or a b; a # G \<turnstile> c; \<And>z'. set (a # G) \<subseteq> set z' \<Longrightarrow> z' \<turnstile> c; b # G \<turnstile> c; \<And>z'. set (b # G) \<subseteq> set z' \<Longrightarrow> z' \<turnstile> c; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> c
A total of 16 subgoals...
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (16 subgoals):
 1. \<And>G a z'. \<lbrakk>G \<turnstile> FF; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> FF; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> a
 2. \<And>a G z'. \<lbrakk>a # G \<turnstile> FF; \<And>z'. set (a # G) \<subseteq> set z' \<Longrightarrow> z' \<turnstile> FF; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Neg a
 3. \<And>G a z'. \<lbrakk>G \<turnstile> Neg a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> Neg a; G \<turnstile> a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> FF
 4. \<And>a G z'. \<lbrakk>Neg a # G \<turnstile> FF; \<And>z'. set (Neg a # G) \<subseteq> set z' \<Longrightarrow> z' \<turnstile> FF; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> a
 5. \<And>G a b z'. \<lbrakk>G \<turnstile> a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a; G \<turnstile> b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> And a b
 6. \<And>G a b z'. \<lbrakk>G \<turnstile> And a b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> And a b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> a
 7. \<And>G a b z'. \<lbrakk>G \<turnstile> And a b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> And a b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> b
 8. \<And>G a b z'. \<lbrakk>G \<turnstile> a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Or a b
 9. \<And>G b a z'. \<lbrakk>G \<turnstile> b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Or a b
 10. \<And>G a b c z'. \<lbrakk>G \<turnstile> Or a b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> Or a b; a # G \<turnstile> c; \<And>z'. set (a # G) \<subseteq> set z' \<Longrightarrow> z' \<turnstile> c; b # G \<turnstile> c; \<And>z'. set (b # G) \<subseteq> set z' \<Longrightarrow> z' \<turnstile> c; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> c
A total of 16 subgoals...
[PROOF STEP]
case FFE
[PROOF STATE]
proof (state)
this:
G_ \<turnstile> FF
set G_ \<subseteq> set ?z' \<Longrightarrow> ?z' \<turnstile> FF
set G_ \<subseteq> set z'

goal (16 subgoals):
 1. \<And>G a z'. \<lbrakk>G \<turnstile> FF; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> FF; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> a
 2. \<And>a G z'. \<lbrakk>a # G \<turnstile> FF; \<And>z'. set (a # G) \<subseteq> set z' \<Longrightarrow> z' \<turnstile> FF; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Neg a
 3. \<And>G a z'. \<lbrakk>G \<turnstile> Neg a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> Neg a; G \<turnstile> a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> FF
 4. \<And>a G z'. \<lbrakk>Neg a # G \<turnstile> FF; \<And>z'. set (Neg a # G) \<subseteq> set z' \<Longrightarrow> z' \<turnstile> FF; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> a
 5. \<And>G a b z'. \<lbrakk>G \<turnstile> a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a; G \<turnstile> b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> And a b
 6. \<And>G a b z'. \<lbrakk>G \<turnstile> And a b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> And a b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> a
 7. \<And>G a b z'. \<lbrakk>G \<turnstile> And a b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> And a b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> b
 8. \<And>G a b z'. \<lbrakk>G \<turnstile> a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Or a b
 9. \<And>G b a z'. \<lbrakk>G \<turnstile> b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Or a b
 10. \<And>G a b c z'. \<lbrakk>G \<turnstile> Or a b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> Or a b; a # G \<turnstile> c; \<And>z'. set (a # G) \<subseteq> set z' \<Longrightarrow> z' \<turnstile> c; b # G \<turnstile> c; \<And>z'. set (b # G) \<subseteq> set z' \<Longrightarrow> z' \<turnstile> c; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> c
A total of 16 subgoals...
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
G_ \<turnstile> FF
set G_ \<subseteq> set ?z' \<Longrightarrow> ?z' \<turnstile> FF
set G_ \<subseteq> set z'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
G_ \<turnstile> FF
set G_ \<subseteq> set ?z' \<Longrightarrow> ?z' \<turnstile> FF
set G_ \<subseteq> set z'

goal (1 subgoal):
 1. z' \<turnstile> a_
[PROOF STEP]
using deriv.FFE
[PROOF STATE]
proof (prove)
using this:
G_ \<turnstile> FF
set G_ \<subseteq> set ?z' \<Longrightarrow> ?z' \<turnstile> FF
set G_ \<subseteq> set z'
?G \<turnstile> FF \<Longrightarrow> ?G \<turnstile> ?a

goal (1 subgoal):
 1. z' \<turnstile> a_
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
z' \<turnstile> a_

goal (15 subgoals):
 1. \<And>a G z'. \<lbrakk>a # G \<turnstile> FF; \<And>z'. set (a # G) \<subseteq> set z' \<Longrightarrow> z' \<turnstile> FF; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Neg a
 2. \<And>G a z'. \<lbrakk>G \<turnstile> Neg a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> Neg a; G \<turnstile> a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> FF
 3. \<And>a G z'. \<lbrakk>Neg a # G \<turnstile> FF; \<And>z'. set (Neg a # G) \<subseteq> set z' \<Longrightarrow> z' \<turnstile> FF; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> a
 4. \<And>G a b z'. \<lbrakk>G \<turnstile> a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a; G \<turnstile> b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> And a b
 5. \<And>G a b z'. \<lbrakk>G \<turnstile> And a b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> And a b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> a
 6. \<And>G a b z'. \<lbrakk>G \<turnstile> And a b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> And a b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> b
 7. \<And>G a b z'. \<lbrakk>G \<turnstile> a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Or a b
 8. \<And>G b a z'. \<lbrakk>G \<turnstile> b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Or a b
 9. \<And>G a b c z'. \<lbrakk>G \<turnstile> Or a b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> Or a b; a # G \<turnstile> c; \<And>z'. set (a # G) \<subseteq> set z' \<Longrightarrow> z' \<turnstile> c; b # G \<turnstile> c; \<And>z'. set (b # G) \<subseteq> set z' \<Longrightarrow> z' \<turnstile> c; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> c
 10. \<And>a G b z'. \<lbrakk>a # G \<turnstile> b; \<And>z'. set (a # G) \<subseteq> set z' \<Longrightarrow> z' \<turnstile> b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Impl a b
A total of 15 subgoals...
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (15 subgoals):
 1. \<And>a G z'. \<lbrakk>a # G \<turnstile> FF; \<And>z'. set (a # G) \<subseteq> set z' \<Longrightarrow> z' \<turnstile> FF; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Neg a
 2. \<And>G a z'. \<lbrakk>G \<turnstile> Neg a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> Neg a; G \<turnstile> a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> FF
 3. \<And>a G z'. \<lbrakk>Neg a # G \<turnstile> FF; \<And>z'. set (Neg a # G) \<subseteq> set z' \<Longrightarrow> z' \<turnstile> FF; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> a
 4. \<And>G a b z'. \<lbrakk>G \<turnstile> a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a; G \<turnstile> b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> And a b
 5. \<And>G a b z'. \<lbrakk>G \<turnstile> And a b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> And a b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> a
 6. \<And>G a b z'. \<lbrakk>G \<turnstile> And a b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> And a b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> b
 7. \<And>G a b z'. \<lbrakk>G \<turnstile> a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Or a b
 8. \<And>G b a z'. \<lbrakk>G \<turnstile> b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Or a b
 9. \<And>G a b c z'. \<lbrakk>G \<turnstile> Or a b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> Or a b; a # G \<turnstile> c; \<And>z'. set (a # G) \<subseteq> set z' \<Longrightarrow> z' \<turnstile> c; b # G \<turnstile> c; \<And>z'. set (b # G) \<subseteq> set z' \<Longrightarrow> z' \<turnstile> c; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> c
 10. \<And>a G b z'. \<lbrakk>a # G \<turnstile> b; \<And>z'. set (a # G) \<subseteq> set z' \<Longrightarrow> z' \<turnstile> b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Impl a b
A total of 15 subgoals...
[PROOF STEP]
case (NegI p z)
[PROOF STATE]
proof (state)
this:
p # z \<turnstile> FF
set (p # z) \<subseteq> set ?z' \<Longrightarrow> ?z' \<turnstile> FF
set z \<subseteq> set z'

goal (15 subgoals):
 1. \<And>a G z'. \<lbrakk>a # G \<turnstile> FF; \<And>z'. set (a # G) \<subseteq> set z' \<Longrightarrow> z' \<turnstile> FF; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Neg a
 2. \<And>G a z'. \<lbrakk>G \<turnstile> Neg a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> Neg a; G \<turnstile> a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> FF
 3. \<And>a G z'. \<lbrakk>Neg a # G \<turnstile> FF; \<And>z'. set (Neg a # G) \<subseteq> set z' \<Longrightarrow> z' \<turnstile> FF; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> a
 4. \<And>G a b z'. \<lbrakk>G \<turnstile> a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a; G \<turnstile> b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> And a b
 5. \<And>G a b z'. \<lbrakk>G \<turnstile> And a b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> And a b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> a
 6. \<And>G a b z'. \<lbrakk>G \<turnstile> And a b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> And a b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> b
 7. \<And>G a b z'. \<lbrakk>G \<turnstile> a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Or a b
 8. \<And>G b a z'. \<lbrakk>G \<turnstile> b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Or a b
 9. \<And>G a b c z'. \<lbrakk>G \<turnstile> Or a b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> Or a b; a # G \<turnstile> c; \<And>z'. set (a # G) \<subseteq> set z' \<Longrightarrow> z' \<turnstile> c; b # G \<turnstile> c; \<And>z'. set (b # G) \<subseteq> set z' \<Longrightarrow> z' \<turnstile> c; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> c
 10. \<And>a G b z'. \<lbrakk>a # G \<turnstile> b; \<And>z'. set (a # G) \<subseteq> set z' \<Longrightarrow> z' \<turnstile> b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Impl a b
A total of 15 subgoals...
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p # z \<turnstile> FF
set (p # z) \<subseteq> set ?z' \<Longrightarrow> ?z' \<turnstile> FF
set z \<subseteq> set z'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
p # z \<turnstile> FF
set (p # z) \<subseteq> set ?z' \<Longrightarrow> ?z' \<turnstile> FF
set z \<subseteq> set z'

goal (1 subgoal):
 1. z' \<turnstile> Neg p
[PROOF STEP]
using deriv.NegI subset_cons
[PROOF STATE]
proof (prove)
using this:
p # z \<turnstile> FF
set (p # z) \<subseteq> set ?z' \<Longrightarrow> ?z' \<turnstile> FF
set z \<subseteq> set z'
?a # ?G \<turnstile> FF \<Longrightarrow> ?G \<turnstile> Neg ?a
set ?z \<subseteq> set ?z' \<Longrightarrow> set (?p # ?z) \<subseteq> set (?p # ?z')

goal (1 subgoal):
 1. z' \<turnstile> Neg p
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
z' \<turnstile> Neg p

goal (14 subgoals):
 1. \<And>G a z'. \<lbrakk>G \<turnstile> Neg a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> Neg a; G \<turnstile> a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> FF
 2. \<And>a G z'. \<lbrakk>Neg a # G \<turnstile> FF; \<And>z'. set (Neg a # G) \<subseteq> set z' \<Longrightarrow> z' \<turnstile> FF; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> a
 3. \<And>G a b z'. \<lbrakk>G \<turnstile> a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a; G \<turnstile> b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> And a b
 4. \<And>G a b z'. \<lbrakk>G \<turnstile> And a b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> And a b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> a
 5. \<And>G a b z'. \<lbrakk>G \<turnstile> And a b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> And a b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> b
 6. \<And>G a b z'. \<lbrakk>G \<turnstile> a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Or a b
 7. \<And>G b a z'. \<lbrakk>G \<turnstile> b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Or a b
 8. \<And>G a b c z'. \<lbrakk>G \<turnstile> Or a b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> Or a b; a # G \<turnstile> c; \<And>z'. set (a # G) \<subseteq> set z' \<Longrightarrow> z' \<turnstile> c; b # G \<turnstile> c; \<And>z'. set (b # G) \<subseteq> set z' \<Longrightarrow> z' \<turnstile> c; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> c
 9. \<And>a G b z'. \<lbrakk>a # G \<turnstile> b; \<And>z'. set (a # G) \<subseteq> set z' \<Longrightarrow> z' \<turnstile> b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Impl a b
 10. \<And>G a b z'. \<lbrakk>G \<turnstile> Impl a b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> Impl a b; G \<turnstile> a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> b
A total of 14 subgoals...
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (14 subgoals):
 1. \<And>G a z'. \<lbrakk>G \<turnstile> Neg a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> Neg a; G \<turnstile> a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> FF
 2. \<And>a G z'. \<lbrakk>Neg a # G \<turnstile> FF; \<And>z'. set (Neg a # G) \<subseteq> set z' \<Longrightarrow> z' \<turnstile> FF; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> a
 3. \<And>G a b z'. \<lbrakk>G \<turnstile> a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a; G \<turnstile> b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> And a b
 4. \<And>G a b z'. \<lbrakk>G \<turnstile> And a b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> And a b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> a
 5. \<And>G a b z'. \<lbrakk>G \<turnstile> And a b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> And a b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> b
 6. \<And>G a b z'. \<lbrakk>G \<turnstile> a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Or a b
 7. \<And>G b a z'. \<lbrakk>G \<turnstile> b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Or a b
 8. \<And>G a b c z'. \<lbrakk>G \<turnstile> Or a b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> Or a b; a # G \<turnstile> c; \<And>z'. set (a # G) \<subseteq> set z' \<Longrightarrow> z' \<turnstile> c; b # G \<turnstile> c; \<And>z'. set (b # G) \<subseteq> set z' \<Longrightarrow> z' \<turnstile> c; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> c
 9. \<And>a G b z'. \<lbrakk>a # G \<turnstile> b; \<And>z'. set (a # G) \<subseteq> set z' \<Longrightarrow> z' \<turnstile> b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Impl a b
 10. \<And>G a b z'. \<lbrakk>G \<turnstile> Impl a b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> Impl a b; G \<turnstile> a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> b
A total of 14 subgoals...
[PROOF STEP]
case (NegE p z)
[PROOF STATE]
proof (state)
this:
p \<turnstile> Neg z
set p \<subseteq> set ?z' \<Longrightarrow> ?z' \<turnstile> Neg z
p \<turnstile> z
set p \<subseteq> set ?z' \<Longrightarrow> ?z' \<turnstile> z
set p \<subseteq> set z'

goal (14 subgoals):
 1. \<And>G a z'. \<lbrakk>G \<turnstile> Neg a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> Neg a; G \<turnstile> a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> FF
 2. \<And>a G z'. \<lbrakk>Neg a # G \<turnstile> FF; \<And>z'. set (Neg a # G) \<subseteq> set z' \<Longrightarrow> z' \<turnstile> FF; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> a
 3. \<And>G a b z'. \<lbrakk>G \<turnstile> a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a; G \<turnstile> b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> And a b
 4. \<And>G a b z'. \<lbrakk>G \<turnstile> And a b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> And a b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> a
 5. \<And>G a b z'. \<lbrakk>G \<turnstile> And a b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> And a b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> b
 6. \<And>G a b z'. \<lbrakk>G \<turnstile> a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Or a b
 7. \<And>G b a z'. \<lbrakk>G \<turnstile> b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Or a b
 8. \<And>G a b c z'. \<lbrakk>G \<turnstile> Or a b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> Or a b; a # G \<turnstile> c; \<And>z'. set (a # G) \<subseteq> set z' \<Longrightarrow> z' \<turnstile> c; b # G \<turnstile> c; \<And>z'. set (b # G) \<subseteq> set z' \<Longrightarrow> z' \<turnstile> c; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> c
 9. \<And>a G b z'. \<lbrakk>a # G \<turnstile> b; \<And>z'. set (a # G) \<subseteq> set z' \<Longrightarrow> z' \<turnstile> b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Impl a b
 10. \<And>G a b z'. \<lbrakk>G \<turnstile> Impl a b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> Impl a b; G \<turnstile> a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> b
A total of 14 subgoals...
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p \<turnstile> Neg z
set p \<subseteq> set ?z' \<Longrightarrow> ?z' \<turnstile> Neg z
p \<turnstile> z
set p \<subseteq> set ?z' \<Longrightarrow> ?z' \<turnstile> z
set p \<subseteq> set z'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
p \<turnstile> Neg z
set p \<subseteq> set ?z' \<Longrightarrow> ?z' \<turnstile> Neg z
p \<turnstile> z
set p \<subseteq> set ?z' \<Longrightarrow> ?z' \<turnstile> z
set p \<subseteq> set z'

goal (1 subgoal):
 1. z' \<turnstile> FF
[PROOF STEP]
using deriv.NegE
[PROOF STATE]
proof (prove)
using this:
p \<turnstile> Neg z
set p \<subseteq> set ?z' \<Longrightarrow> ?z' \<turnstile> Neg z
p \<turnstile> z
set p \<subseteq> set ?z' \<Longrightarrow> ?z' \<turnstile> z
set p \<subseteq> set z'
\<lbrakk>?G \<turnstile> Neg ?a; ?G \<turnstile> ?a\<rbrakk> \<Longrightarrow> ?G \<turnstile> FF

goal (1 subgoal):
 1. z' \<turnstile> FF
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
z' \<turnstile> FF

goal (13 subgoals):
 1. \<And>a G z'. \<lbrakk>Neg a # G \<turnstile> FF; \<And>z'. set (Neg a # G) \<subseteq> set z' \<Longrightarrow> z' \<turnstile> FF; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> a
 2. \<And>G a b z'. \<lbrakk>G \<turnstile> a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a; G \<turnstile> b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> And a b
 3. \<And>G a b z'. \<lbrakk>G \<turnstile> And a b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> And a b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> a
 4. \<And>G a b z'. \<lbrakk>G \<turnstile> And a b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> And a b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> b
 5. \<And>G a b z'. \<lbrakk>G \<turnstile> a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Or a b
 6. \<And>G b a z'. \<lbrakk>G \<turnstile> b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Or a b
 7. \<And>G a b c z'. \<lbrakk>G \<turnstile> Or a b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> Or a b; a # G \<turnstile> c; \<And>z'. set (a # G) \<subseteq> set z' \<Longrightarrow> z' \<turnstile> c; b # G \<turnstile> c; \<And>z'. set (b # G) \<subseteq> set z' \<Longrightarrow> z' \<turnstile> c; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> c
 8. \<And>a G b z'. \<lbrakk>a # G \<turnstile> b; \<And>z'. set (a # G) \<subseteq> set z' \<Longrightarrow> z' \<turnstile> b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Impl a b
 9. \<And>G a b z'. \<lbrakk>G \<turnstile> Impl a b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> Impl a b; G \<turnstile> a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> b
 10. \<And>G a n z'. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a[App n []/0]; news n G; new n a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Forall a
A total of 13 subgoals...
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (13 subgoals):
 1. \<And>a G z'. \<lbrakk>Neg a # G \<turnstile> FF; \<And>z'. set (Neg a # G) \<subseteq> set z' \<Longrightarrow> z' \<turnstile> FF; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> a
 2. \<And>G a b z'. \<lbrakk>G \<turnstile> a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a; G \<turnstile> b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> And a b
 3. \<And>G a b z'. \<lbrakk>G \<turnstile> And a b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> And a b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> a
 4. \<And>G a b z'. \<lbrakk>G \<turnstile> And a b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> And a b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> b
 5. \<And>G a b z'. \<lbrakk>G \<turnstile> a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Or a b
 6. \<And>G b a z'. \<lbrakk>G \<turnstile> b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Or a b
 7. \<And>G a b c z'. \<lbrakk>G \<turnstile> Or a b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> Or a b; a # G \<turnstile> c; \<And>z'. set (a # G) \<subseteq> set z' \<Longrightarrow> z' \<turnstile> c; b # G \<turnstile> c; \<And>z'. set (b # G) \<subseteq> set z' \<Longrightarrow> z' \<turnstile> c; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> c
 8. \<And>a G b z'. \<lbrakk>a # G \<turnstile> b; \<And>z'. set (a # G) \<subseteq> set z' \<Longrightarrow> z' \<turnstile> b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Impl a b
 9. \<And>G a b z'. \<lbrakk>G \<turnstile> Impl a b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> Impl a b; G \<turnstile> a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> b
 10. \<And>G a n z'. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a[App n []/0]; news n G; new n a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Forall a
A total of 13 subgoals...
[PROOF STEP]
case (Class z p)
[PROOF STATE]
proof (state)
this:
Neg z # p \<turnstile> FF
set (Neg z # p) \<subseteq> set ?z' \<Longrightarrow> ?z' \<turnstile> FF
set p \<subseteq> set z'

goal (13 subgoals):
 1. \<And>a G z'. \<lbrakk>Neg a # G \<turnstile> FF; \<And>z'. set (Neg a # G) \<subseteq> set z' \<Longrightarrow> z' \<turnstile> FF; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> a
 2. \<And>G a b z'. \<lbrakk>G \<turnstile> a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a; G \<turnstile> b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> And a b
 3. \<And>G a b z'. \<lbrakk>G \<turnstile> And a b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> And a b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> a
 4. \<And>G a b z'. \<lbrakk>G \<turnstile> And a b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> And a b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> b
 5. \<And>G a b z'. \<lbrakk>G \<turnstile> a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Or a b
 6. \<And>G b a z'. \<lbrakk>G \<turnstile> b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Or a b
 7. \<And>G a b c z'. \<lbrakk>G \<turnstile> Or a b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> Or a b; a # G \<turnstile> c; \<And>z'. set (a # G) \<subseteq> set z' \<Longrightarrow> z' \<turnstile> c; b # G \<turnstile> c; \<And>z'. set (b # G) \<subseteq> set z' \<Longrightarrow> z' \<turnstile> c; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> c
 8. \<And>a G b z'. \<lbrakk>a # G \<turnstile> b; \<And>z'. set (a # G) \<subseteq> set z' \<Longrightarrow> z' \<turnstile> b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Impl a b
 9. \<And>G a b z'. \<lbrakk>G \<turnstile> Impl a b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> Impl a b; G \<turnstile> a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> b
 10. \<And>G a n z'. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a[App n []/0]; news n G; new n a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Forall a
A total of 13 subgoals...
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Neg z # p \<turnstile> FF
set (Neg z # p) \<subseteq> set ?z' \<Longrightarrow> ?z' \<turnstile> FF
set p \<subseteq> set z'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
Neg z # p \<turnstile> FF
set (Neg z # p) \<subseteq> set ?z' \<Longrightarrow> ?z' \<turnstile> FF
set p \<subseteq> set z'

goal (1 subgoal):
 1. z' \<turnstile> z
[PROOF STEP]
using deriv.Class subset_cons
[PROOF STATE]
proof (prove)
using this:
Neg z # p \<turnstile> FF
set (Neg z # p) \<subseteq> set ?z' \<Longrightarrow> ?z' \<turnstile> FF
set p \<subseteq> set z'
Neg ?a # ?G \<turnstile> FF \<Longrightarrow> ?G \<turnstile> ?a
set ?z \<subseteq> set ?z' \<Longrightarrow> set (?p # ?z) \<subseteq> set (?p # ?z')

goal (1 subgoal):
 1. z' \<turnstile> z
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
z' \<turnstile> z

goal (12 subgoals):
 1. \<And>G a b z'. \<lbrakk>G \<turnstile> a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a; G \<turnstile> b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> And a b
 2. \<And>G a b z'. \<lbrakk>G \<turnstile> And a b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> And a b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> a
 3. \<And>G a b z'. \<lbrakk>G \<turnstile> And a b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> And a b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> b
 4. \<And>G a b z'. \<lbrakk>G \<turnstile> a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Or a b
 5. \<And>G b a z'. \<lbrakk>G \<turnstile> b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Or a b
 6. \<And>G a b c z'. \<lbrakk>G \<turnstile> Or a b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> Or a b; a # G \<turnstile> c; \<And>z'. set (a # G) \<subseteq> set z' \<Longrightarrow> z' \<turnstile> c; b # G \<turnstile> c; \<And>z'. set (b # G) \<subseteq> set z' \<Longrightarrow> z' \<turnstile> c; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> c
 7. \<And>a G b z'. \<lbrakk>a # G \<turnstile> b; \<And>z'. set (a # G) \<subseteq> set z' \<Longrightarrow> z' \<turnstile> b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Impl a b
 8. \<And>G a b z'. \<lbrakk>G \<turnstile> Impl a b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> Impl a b; G \<turnstile> a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> b
 9. \<And>G a n z'. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a[App n []/0]; news n G; new n a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Forall a
 10. \<And>G a t z'. \<lbrakk>G \<turnstile> Forall a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> Forall a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> a[t/0]
A total of 12 subgoals...
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (12 subgoals):
 1. \<And>G a b z'. \<lbrakk>G \<turnstile> a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a; G \<turnstile> b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> And a b
 2. \<And>G a b z'. \<lbrakk>G \<turnstile> And a b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> And a b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> a
 3. \<And>G a b z'. \<lbrakk>G \<turnstile> And a b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> And a b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> b
 4. \<And>G a b z'. \<lbrakk>G \<turnstile> a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Or a b
 5. \<And>G b a z'. \<lbrakk>G \<turnstile> b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Or a b
 6. \<And>G a b c z'. \<lbrakk>G \<turnstile> Or a b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> Or a b; a # G \<turnstile> c; \<And>z'. set (a # G) \<subseteq> set z' \<Longrightarrow> z' \<turnstile> c; b # G \<turnstile> c; \<And>z'. set (b # G) \<subseteq> set z' \<Longrightarrow> z' \<turnstile> c; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> c
 7. \<And>a G b z'. \<lbrakk>a # G \<turnstile> b; \<And>z'. set (a # G) \<subseteq> set z' \<Longrightarrow> z' \<turnstile> b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Impl a b
 8. \<And>G a b z'. \<lbrakk>G \<turnstile> Impl a b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> Impl a b; G \<turnstile> a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> b
 9. \<And>G a n z'. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a[App n []/0]; news n G; new n a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Forall a
 10. \<And>G a t z'. \<lbrakk>G \<turnstile> Forall a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> Forall a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> a[t/0]
A total of 12 subgoals...
[PROOF STEP]
case (ImplE z p q)
[PROOF STATE]
proof (state)
this:
z \<turnstile> Impl p q
set z \<subseteq> set ?z' \<Longrightarrow> ?z' \<turnstile> Impl p q
z \<turnstile> p
set z \<subseteq> set ?z' \<Longrightarrow> ?z' \<turnstile> p
set z \<subseteq> set z'

goal (12 subgoals):
 1. \<And>G a b z'. \<lbrakk>G \<turnstile> a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a; G \<turnstile> b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> And a b
 2. \<And>G a b z'. \<lbrakk>G \<turnstile> And a b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> And a b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> a
 3. \<And>G a b z'. \<lbrakk>G \<turnstile> And a b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> And a b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> b
 4. \<And>G a b z'. \<lbrakk>G \<turnstile> a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Or a b
 5. \<And>G b a z'. \<lbrakk>G \<turnstile> b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Or a b
 6. \<And>G a b c z'. \<lbrakk>G \<turnstile> Or a b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> Or a b; a # G \<turnstile> c; \<And>z'. set (a # G) \<subseteq> set z' \<Longrightarrow> z' \<turnstile> c; b # G \<turnstile> c; \<And>z'. set (b # G) \<subseteq> set z' \<Longrightarrow> z' \<turnstile> c; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> c
 7. \<And>a G b z'. \<lbrakk>a # G \<turnstile> b; \<And>z'. set (a # G) \<subseteq> set z' \<Longrightarrow> z' \<turnstile> b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Impl a b
 8. \<And>G a b z'. \<lbrakk>G \<turnstile> Impl a b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> Impl a b; G \<turnstile> a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> b
 9. \<And>G a n z'. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a[App n []/0]; news n G; new n a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Forall a
 10. \<And>G a t z'. \<lbrakk>G \<turnstile> Forall a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> Forall a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> a[t/0]
A total of 12 subgoals...
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
z \<turnstile> Impl p q
set z \<subseteq> set ?z' \<Longrightarrow> ?z' \<turnstile> Impl p q
z \<turnstile> p
set z \<subseteq> set ?z' \<Longrightarrow> ?z' \<turnstile> p
set z \<subseteq> set z'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
z \<turnstile> Impl p q
set z \<subseteq> set ?z' \<Longrightarrow> ?z' \<turnstile> Impl p q
z \<turnstile> p
set z \<subseteq> set ?z' \<Longrightarrow> ?z' \<turnstile> p
set z \<subseteq> set z'

goal (1 subgoal):
 1. z' \<turnstile> q
[PROOF STEP]
using deriv.ImplE
[PROOF STATE]
proof (prove)
using this:
z \<turnstile> Impl p q
set z \<subseteq> set ?z' \<Longrightarrow> ?z' \<turnstile> Impl p q
z \<turnstile> p
set z \<subseteq> set ?z' \<Longrightarrow> ?z' \<turnstile> p
set z \<subseteq> set z'
\<lbrakk>?G \<turnstile> Impl ?a ?b; ?G \<turnstile> ?a\<rbrakk> \<Longrightarrow> ?G \<turnstile> ?b

goal (1 subgoal):
 1. z' \<turnstile> q
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
z' \<turnstile> q

goal (11 subgoals):
 1. \<And>G a b z'. \<lbrakk>G \<turnstile> a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a; G \<turnstile> b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> And a b
 2. \<And>G a b z'. \<lbrakk>G \<turnstile> And a b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> And a b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> a
 3. \<And>G a b z'. \<lbrakk>G \<turnstile> And a b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> And a b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> b
 4. \<And>G a b z'. \<lbrakk>G \<turnstile> a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Or a b
 5. \<And>G b a z'. \<lbrakk>G \<turnstile> b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Or a b
 6. \<And>G a b c z'. \<lbrakk>G \<turnstile> Or a b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> Or a b; a # G \<turnstile> c; \<And>z'. set (a # G) \<subseteq> set z' \<Longrightarrow> z' \<turnstile> c; b # G \<turnstile> c; \<And>z'. set (b # G) \<subseteq> set z' \<Longrightarrow> z' \<turnstile> c; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> c
 7. \<And>a G b z'. \<lbrakk>a # G \<turnstile> b; \<And>z'. set (a # G) \<subseteq> set z' \<Longrightarrow> z' \<turnstile> b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Impl a b
 8. \<And>G a n z'. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a[App n []/0]; news n G; new n a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Forall a
 9. \<And>G a t z'. \<lbrakk>G \<turnstile> Forall a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> Forall a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> a[t/0]
 10. \<And>G a t z'. \<lbrakk>G \<turnstile> a[t/0]; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a[t/0]; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Exists a
A total of 11 subgoals...
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (11 subgoals):
 1. \<And>G a b z'. \<lbrakk>G \<turnstile> a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a; G \<turnstile> b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> And a b
 2. \<And>G a b z'. \<lbrakk>G \<turnstile> And a b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> And a b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> a
 3. \<And>G a b z'. \<lbrakk>G \<turnstile> And a b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> And a b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> b
 4. \<And>G a b z'. \<lbrakk>G \<turnstile> a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Or a b
 5. \<And>G b a z'. \<lbrakk>G \<turnstile> b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Or a b
 6. \<And>G a b c z'. \<lbrakk>G \<turnstile> Or a b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> Or a b; a # G \<turnstile> c; \<And>z'. set (a # G) \<subseteq> set z' \<Longrightarrow> z' \<turnstile> c; b # G \<turnstile> c; \<And>z'. set (b # G) \<subseteq> set z' \<Longrightarrow> z' \<turnstile> c; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> c
 7. \<And>a G b z'. \<lbrakk>a # G \<turnstile> b; \<And>z'. set (a # G) \<subseteq> set z' \<Longrightarrow> z' \<turnstile> b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Impl a b
 8. \<And>G a n z'. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a[App n []/0]; news n G; new n a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Forall a
 9. \<And>G a t z'. \<lbrakk>G \<turnstile> Forall a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> Forall a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> a[t/0]
 10. \<And>G a t z'. \<lbrakk>G \<turnstile> a[t/0]; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a[t/0]; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Exists a
A total of 11 subgoals...
[PROOF STEP]
case (ImplI z q p)
[PROOF STATE]
proof (state)
this:
z # q \<turnstile> p
set (z # q) \<subseteq> set ?z' \<Longrightarrow> ?z' \<turnstile> p
set q \<subseteq> set z'

goal (11 subgoals):
 1. \<And>G a b z'. \<lbrakk>G \<turnstile> a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a; G \<turnstile> b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> And a b
 2. \<And>G a b z'. \<lbrakk>G \<turnstile> And a b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> And a b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> a
 3. \<And>G a b z'. \<lbrakk>G \<turnstile> And a b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> And a b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> b
 4. \<And>G a b z'. \<lbrakk>G \<turnstile> a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Or a b
 5. \<And>G b a z'. \<lbrakk>G \<turnstile> b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Or a b
 6. \<And>G a b c z'. \<lbrakk>G \<turnstile> Or a b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> Or a b; a # G \<turnstile> c; \<And>z'. set (a # G) \<subseteq> set z' \<Longrightarrow> z' \<turnstile> c; b # G \<turnstile> c; \<And>z'. set (b # G) \<subseteq> set z' \<Longrightarrow> z' \<turnstile> c; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> c
 7. \<And>a G b z'. \<lbrakk>a # G \<turnstile> b; \<And>z'. set (a # G) \<subseteq> set z' \<Longrightarrow> z' \<turnstile> b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Impl a b
 8. \<And>G a n z'. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a[App n []/0]; news n G; new n a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Forall a
 9. \<And>G a t z'. \<lbrakk>G \<turnstile> Forall a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> Forall a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> a[t/0]
 10. \<And>G a t z'. \<lbrakk>G \<turnstile> a[t/0]; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a[t/0]; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Exists a
A total of 11 subgoals...
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
z # q \<turnstile> p
set (z # q) \<subseteq> set ?z' \<Longrightarrow> ?z' \<turnstile> p
set q \<subseteq> set z'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
z # q \<turnstile> p
set (z # q) \<subseteq> set ?z' \<Longrightarrow> ?z' \<turnstile> p
set q \<subseteq> set z'

goal (1 subgoal):
 1. z' \<turnstile> Impl z p
[PROOF STEP]
using deriv.ImplI subset_cons
[PROOF STATE]
proof (prove)
using this:
z # q \<turnstile> p
set (z # q) \<subseteq> set ?z' \<Longrightarrow> ?z' \<turnstile> p
set q \<subseteq> set z'
?a # ?G \<turnstile> ?b \<Longrightarrow> ?G \<turnstile> Impl ?a ?b
set ?z \<subseteq> set ?z' \<Longrightarrow> set (?p # ?z) \<subseteq> set (?p # ?z')

goal (1 subgoal):
 1. z' \<turnstile> Impl z p
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
z' \<turnstile> Impl z p

goal (10 subgoals):
 1. \<And>G a b z'. \<lbrakk>G \<turnstile> a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a; G \<turnstile> b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> And a b
 2. \<And>G a b z'. \<lbrakk>G \<turnstile> And a b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> And a b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> a
 3. \<And>G a b z'. \<lbrakk>G \<turnstile> And a b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> And a b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> b
 4. \<And>G a b z'. \<lbrakk>G \<turnstile> a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Or a b
 5. \<And>G b a z'. \<lbrakk>G \<turnstile> b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Or a b
 6. \<And>G a b c z'. \<lbrakk>G \<turnstile> Or a b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> Or a b; a # G \<turnstile> c; \<And>z'. set (a # G) \<subseteq> set z' \<Longrightarrow> z' \<turnstile> c; b # G \<turnstile> c; \<And>z'. set (b # G) \<subseteq> set z' \<Longrightarrow> z' \<turnstile> c; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> c
 7. \<And>G a n z'. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a[App n []/0]; news n G; new n a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Forall a
 8. \<And>G a t z'. \<lbrakk>G \<turnstile> Forall a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> Forall a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> a[t/0]
 9. \<And>G a t z'. \<lbrakk>G \<turnstile> a[t/0]; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a[t/0]; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Exists a
 10. \<And>G a n b z'. \<lbrakk>G \<turnstile> Exists a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> Exists a; a[App n []/0] # G \<turnstile> b; \<And>z'. set (a[App n []/0] # G) \<subseteq> set z' \<Longrightarrow> z' \<turnstile> b; news n G; new n a; new n b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> b
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (10 subgoals):
 1. \<And>G a b z'. \<lbrakk>G \<turnstile> a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a; G \<turnstile> b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> And a b
 2. \<And>G a b z'. \<lbrakk>G \<turnstile> And a b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> And a b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> a
 3. \<And>G a b z'. \<lbrakk>G \<turnstile> And a b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> And a b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> b
 4. \<And>G a b z'. \<lbrakk>G \<turnstile> a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Or a b
 5. \<And>G b a z'. \<lbrakk>G \<turnstile> b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Or a b
 6. \<And>G a b c z'. \<lbrakk>G \<turnstile> Or a b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> Or a b; a # G \<turnstile> c; \<And>z'. set (a # G) \<subseteq> set z' \<Longrightarrow> z' \<turnstile> c; b # G \<turnstile> c; \<And>z'. set (b # G) \<subseteq> set z' \<Longrightarrow> z' \<turnstile> c; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> c
 7. \<And>G a n z'. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a[App n []/0]; news n G; new n a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Forall a
 8. \<And>G a t z'. \<lbrakk>G \<turnstile> Forall a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> Forall a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> a[t/0]
 9. \<And>G a t z'. \<lbrakk>G \<turnstile> a[t/0]; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a[t/0]; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Exists a
 10. \<And>G a n b z'. \<lbrakk>G \<turnstile> Exists a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> Exists a; a[App n []/0] # G \<turnstile> b; \<And>z'. set (a[App n []/0] # G) \<subseteq> set z' \<Longrightarrow> z' \<turnstile> b; news n G; new n a; new n b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> b
[PROOF STEP]
case (OrE z p q z )
[PROOF STATE]
proof (state)
this:
za__ \<turnstile> Or p q
set za__ \<subseteq> set ?z' \<Longrightarrow> ?z' \<turnstile> Or p q
p # za__ \<turnstile> z
set (p # za__) \<subseteq> set ?z' \<Longrightarrow> ?z' \<turnstile> z
q # za__ \<turnstile> z
set (q # za__) \<subseteq> set ?z' \<Longrightarrow> ?z' \<turnstile> z
set za__ \<subseteq> set z'

goal (10 subgoals):
 1. \<And>G a b z'. \<lbrakk>G \<turnstile> a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a; G \<turnstile> b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> And a b
 2. \<And>G a b z'. \<lbrakk>G \<turnstile> And a b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> And a b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> a
 3. \<And>G a b z'. \<lbrakk>G \<turnstile> And a b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> And a b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> b
 4. \<And>G a b z'. \<lbrakk>G \<turnstile> a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Or a b
 5. \<And>G b a z'. \<lbrakk>G \<turnstile> b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Or a b
 6. \<And>G a b c z'. \<lbrakk>G \<turnstile> Or a b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> Or a b; a # G \<turnstile> c; \<And>z'. set (a # G) \<subseteq> set z' \<Longrightarrow> z' \<turnstile> c; b # G \<turnstile> c; \<And>z'. set (b # G) \<subseteq> set z' \<Longrightarrow> z' \<turnstile> c; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> c
 7. \<And>G a n z'. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a[App n []/0]; news n G; new n a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Forall a
 8. \<And>G a t z'. \<lbrakk>G \<turnstile> Forall a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> Forall a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> a[t/0]
 9. \<And>G a t z'. \<lbrakk>G \<turnstile> a[t/0]; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a[t/0]; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Exists a
 10. \<And>G a n b z'. \<lbrakk>G \<turnstile> Exists a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> Exists a; a[App n []/0] # G \<turnstile> b; \<And>z'. set (a[App n []/0] # G) \<subseteq> set z' \<Longrightarrow> z' \<turnstile> b; news n G; new n a; new n b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> b
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
za__ \<turnstile> Or p q
set za__ \<subseteq> set ?z' \<Longrightarrow> ?z' \<turnstile> Or p q
p # za__ \<turnstile> z
set (p # za__) \<subseteq> set ?z' \<Longrightarrow> ?z' \<turnstile> z
q # za__ \<turnstile> z
set (q # za__) \<subseteq> set ?z' \<Longrightarrow> ?z' \<turnstile> z
set za__ \<subseteq> set z'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
za__ \<turnstile> Or p q
set za__ \<subseteq> set ?z' \<Longrightarrow> ?z' \<turnstile> Or p q
p # za__ \<turnstile> z
set (p # za__) \<subseteq> set ?z' \<Longrightarrow> ?z' \<turnstile> z
q # za__ \<turnstile> z
set (q # za__) \<subseteq> set ?z' \<Longrightarrow> ?z' \<turnstile> z
set za__ \<subseteq> set z'

goal (1 subgoal):
 1. z' \<turnstile> z
[PROOF STEP]
using deriv.OrE subset_cons
[PROOF STATE]
proof (prove)
using this:
za__ \<turnstile> Or p q
set za__ \<subseteq> set ?z' \<Longrightarrow> ?z' \<turnstile> Or p q
p # za__ \<turnstile> z
set (p # za__) \<subseteq> set ?z' \<Longrightarrow> ?z' \<turnstile> z
q # za__ \<turnstile> z
set (q # za__) \<subseteq> set ?z' \<Longrightarrow> ?z' \<turnstile> z
set za__ \<subseteq> set z'
\<lbrakk>?G \<turnstile> Or ?a ?b; ?a # ?G \<turnstile> ?c; ?b # ?G \<turnstile> ?c\<rbrakk> \<Longrightarrow> ?G \<turnstile> ?c
set ?z \<subseteq> set ?z' \<Longrightarrow> set (?p # ?z) \<subseteq> set (?p # ?z')

goal (1 subgoal):
 1. z' \<turnstile> z
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
z' \<turnstile> z

goal (9 subgoals):
 1. \<And>G a b z'. \<lbrakk>G \<turnstile> a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a; G \<turnstile> b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> And a b
 2. \<And>G a b z'. \<lbrakk>G \<turnstile> And a b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> And a b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> a
 3. \<And>G a b z'. \<lbrakk>G \<turnstile> And a b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> And a b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> b
 4. \<And>G a b z'. \<lbrakk>G \<turnstile> a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Or a b
 5. \<And>G b a z'. \<lbrakk>G \<turnstile> b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Or a b
 6. \<And>G a n z'. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a[App n []/0]; news n G; new n a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Forall a
 7. \<And>G a t z'. \<lbrakk>G \<turnstile> Forall a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> Forall a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> a[t/0]
 8. \<And>G a t z'. \<lbrakk>G \<turnstile> a[t/0]; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a[t/0]; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Exists a
 9. \<And>G a n b z'. \<lbrakk>G \<turnstile> Exists a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> Exists a; a[App n []/0] # G \<turnstile> b; \<And>z'. set (a[App n []/0] # G) \<subseteq> set z' \<Longrightarrow> z' \<turnstile> b; news n G; new n a; new n b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> b
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (9 subgoals):
 1. \<And>G a b z'. \<lbrakk>G \<turnstile> a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a; G \<turnstile> b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> And a b
 2. \<And>G a b z'. \<lbrakk>G \<turnstile> And a b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> And a b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> a
 3. \<And>G a b z'. \<lbrakk>G \<turnstile> And a b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> And a b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> b
 4. \<And>G a b z'. \<lbrakk>G \<turnstile> a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Or a b
 5. \<And>G b a z'. \<lbrakk>G \<turnstile> b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Or a b
 6. \<And>G a n z'. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a[App n []/0]; news n G; new n a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Forall a
 7. \<And>G a t z'. \<lbrakk>G \<turnstile> Forall a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> Forall a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> a[t/0]
 8. \<And>G a t z'. \<lbrakk>G \<turnstile> a[t/0]; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a[t/0]; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Exists a
 9. \<And>G a n b z'. \<lbrakk>G \<turnstile> Exists a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> Exists a; a[App n []/0] # G \<turnstile> b; \<And>z'. set (a[App n []/0] # G) \<subseteq> set z' \<Longrightarrow> z' \<turnstile> b; news n G; new n a; new n b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> b
[PROOF STEP]
case (OrI1 z p q)
[PROOF STATE]
proof (state)
this:
z \<turnstile> p
set z \<subseteq> set ?z' \<Longrightarrow> ?z' \<turnstile> p
set z \<subseteq> set z'

goal (9 subgoals):
 1. \<And>G a b z'. \<lbrakk>G \<turnstile> a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a; G \<turnstile> b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> And a b
 2. \<And>G a b z'. \<lbrakk>G \<turnstile> And a b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> And a b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> a
 3. \<And>G a b z'. \<lbrakk>G \<turnstile> And a b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> And a b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> b
 4. \<And>G a b z'. \<lbrakk>G \<turnstile> a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Or a b
 5. \<And>G b a z'. \<lbrakk>G \<turnstile> b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Or a b
 6. \<And>G a n z'. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a[App n []/0]; news n G; new n a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Forall a
 7. \<And>G a t z'. \<lbrakk>G \<turnstile> Forall a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> Forall a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> a[t/0]
 8. \<And>G a t z'. \<lbrakk>G \<turnstile> a[t/0]; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a[t/0]; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Exists a
 9. \<And>G a n b z'. \<lbrakk>G \<turnstile> Exists a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> Exists a; a[App n []/0] # G \<turnstile> b; \<And>z'. set (a[App n []/0] # G) \<subseteq> set z' \<Longrightarrow> z' \<turnstile> b; news n G; new n a; new n b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> b
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
z \<turnstile> p
set z \<subseteq> set ?z' \<Longrightarrow> ?z' \<turnstile> p
set z \<subseteq> set z'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
z \<turnstile> p
set z \<subseteq> set ?z' \<Longrightarrow> ?z' \<turnstile> p
set z \<subseteq> set z'

goal (1 subgoal):
 1. z' \<turnstile> Or p q
[PROOF STEP]
using deriv.OrI1
[PROOF STATE]
proof (prove)
using this:
z \<turnstile> p
set z \<subseteq> set ?z' \<Longrightarrow> ?z' \<turnstile> p
set z \<subseteq> set z'
?G \<turnstile> ?a \<Longrightarrow> ?G \<turnstile> Or ?a ?b

goal (1 subgoal):
 1. z' \<turnstile> Or p q
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
z' \<turnstile> Or p q

goal (8 subgoals):
 1. \<And>G a b z'. \<lbrakk>G \<turnstile> a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a; G \<turnstile> b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> And a b
 2. \<And>G a b z'. \<lbrakk>G \<turnstile> And a b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> And a b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> a
 3. \<And>G a b z'. \<lbrakk>G \<turnstile> And a b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> And a b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> b
 4. \<And>G b a z'. \<lbrakk>G \<turnstile> b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Or a b
 5. \<And>G a n z'. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a[App n []/0]; news n G; new n a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Forall a
 6. \<And>G a t z'. \<lbrakk>G \<turnstile> Forall a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> Forall a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> a[t/0]
 7. \<And>G a t z'. \<lbrakk>G \<turnstile> a[t/0]; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a[t/0]; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Exists a
 8. \<And>G a n b z'. \<lbrakk>G \<turnstile> Exists a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> Exists a; a[App n []/0] # G \<turnstile> b; \<And>z'. set (a[App n []/0] # G) \<subseteq> set z' \<Longrightarrow> z' \<turnstile> b; news n G; new n a; new n b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> b
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (8 subgoals):
 1. \<And>G a b z'. \<lbrakk>G \<turnstile> a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a; G \<turnstile> b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> And a b
 2. \<And>G a b z'. \<lbrakk>G \<turnstile> And a b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> And a b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> a
 3. \<And>G a b z'. \<lbrakk>G \<turnstile> And a b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> And a b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> b
 4. \<And>G b a z'. \<lbrakk>G \<turnstile> b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Or a b
 5. \<And>G a n z'. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a[App n []/0]; news n G; new n a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Forall a
 6. \<And>G a t z'. \<lbrakk>G \<turnstile> Forall a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> Forall a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> a[t/0]
 7. \<And>G a t z'. \<lbrakk>G \<turnstile> a[t/0]; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a[t/0]; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Exists a
 8. \<And>G a n b z'. \<lbrakk>G \<turnstile> Exists a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> Exists a; a[App n []/0] # G \<turnstile> b; \<And>z'. set (a[App n []/0] # G) \<subseteq> set z' \<Longrightarrow> z' \<turnstile> b; news n G; new n a; new n b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> b
[PROOF STEP]
case (OrI2 z q p)
[PROOF STATE]
proof (state)
this:
z \<turnstile> q
set z \<subseteq> set ?z' \<Longrightarrow> ?z' \<turnstile> q
set z \<subseteq> set z'

goal (8 subgoals):
 1. \<And>G a b z'. \<lbrakk>G \<turnstile> a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a; G \<turnstile> b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> And a b
 2. \<And>G a b z'. \<lbrakk>G \<turnstile> And a b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> And a b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> a
 3. \<And>G a b z'. \<lbrakk>G \<turnstile> And a b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> And a b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> b
 4. \<And>G b a z'. \<lbrakk>G \<turnstile> b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Or a b
 5. \<And>G a n z'. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a[App n []/0]; news n G; new n a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Forall a
 6. \<And>G a t z'. \<lbrakk>G \<turnstile> Forall a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> Forall a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> a[t/0]
 7. \<And>G a t z'. \<lbrakk>G \<turnstile> a[t/0]; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a[t/0]; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Exists a
 8. \<And>G a n b z'. \<lbrakk>G \<turnstile> Exists a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> Exists a; a[App n []/0] # G \<turnstile> b; \<And>z'. set (a[App n []/0] # G) \<subseteq> set z' \<Longrightarrow> z' \<turnstile> b; news n G; new n a; new n b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> b
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
z \<turnstile> q
set z \<subseteq> set ?z' \<Longrightarrow> ?z' \<turnstile> q
set z \<subseteq> set z'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
z \<turnstile> q
set z \<subseteq> set ?z' \<Longrightarrow> ?z' \<turnstile> q
set z \<subseteq> set z'

goal (1 subgoal):
 1. z' \<turnstile> Or p q
[PROOF STEP]
using deriv.OrI2
[PROOF STATE]
proof (prove)
using this:
z \<turnstile> q
set z \<subseteq> set ?z' \<Longrightarrow> ?z' \<turnstile> q
set z \<subseteq> set z'
?G \<turnstile> ?b \<Longrightarrow> ?G \<turnstile> Or ?a ?b

goal (1 subgoal):
 1. z' \<turnstile> Or p q
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
z' \<turnstile> Or p q

goal (7 subgoals):
 1. \<And>G a b z'. \<lbrakk>G \<turnstile> a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a; G \<turnstile> b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> And a b
 2. \<And>G a b z'. \<lbrakk>G \<turnstile> And a b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> And a b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> a
 3. \<And>G a b z'. \<lbrakk>G \<turnstile> And a b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> And a b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> b
 4. \<And>G a n z'. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a[App n []/0]; news n G; new n a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Forall a
 5. \<And>G a t z'. \<lbrakk>G \<turnstile> Forall a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> Forall a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> a[t/0]
 6. \<And>G a t z'. \<lbrakk>G \<turnstile> a[t/0]; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a[t/0]; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Exists a
 7. \<And>G a n b z'. \<lbrakk>G \<turnstile> Exists a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> Exists a; a[App n []/0] # G \<turnstile> b; \<And>z'. set (a[App n []/0] # G) \<subseteq> set z' \<Longrightarrow> z' \<turnstile> b; news n G; new n a; new n b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> b
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. \<And>G a b z'. \<lbrakk>G \<turnstile> a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a; G \<turnstile> b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> And a b
 2. \<And>G a b z'. \<lbrakk>G \<turnstile> And a b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> And a b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> a
 3. \<And>G a b z'. \<lbrakk>G \<turnstile> And a b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> And a b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> b
 4. \<And>G a n z'. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a[App n []/0]; news n G; new n a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Forall a
 5. \<And>G a t z'. \<lbrakk>G \<turnstile> Forall a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> Forall a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> a[t/0]
 6. \<And>G a t z'. \<lbrakk>G \<turnstile> a[t/0]; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a[t/0]; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Exists a
 7. \<And>G a n b z'. \<lbrakk>G \<turnstile> Exists a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> Exists a; a[App n []/0] # G \<turnstile> b; \<And>z'. set (a[App n []/0] # G) \<subseteq> set z' \<Longrightarrow> z' \<turnstile> b; news n G; new n a; new n b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> b
[PROOF STEP]
case (AndE1 z p q)
[PROOF STATE]
proof (state)
this:
z \<turnstile> And p q
set z \<subseteq> set ?z' \<Longrightarrow> ?z' \<turnstile> And p q
set z \<subseteq> set z'

goal (7 subgoals):
 1. \<And>G a b z'. \<lbrakk>G \<turnstile> a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a; G \<turnstile> b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> And a b
 2. \<And>G a b z'. \<lbrakk>G \<turnstile> And a b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> And a b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> a
 3. \<And>G a b z'. \<lbrakk>G \<turnstile> And a b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> And a b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> b
 4. \<And>G a n z'. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a[App n []/0]; news n G; new n a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Forall a
 5. \<And>G a t z'. \<lbrakk>G \<turnstile> Forall a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> Forall a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> a[t/0]
 6. \<And>G a t z'. \<lbrakk>G \<turnstile> a[t/0]; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a[t/0]; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Exists a
 7. \<And>G a n b z'. \<lbrakk>G \<turnstile> Exists a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> Exists a; a[App n []/0] # G \<turnstile> b; \<And>z'. set (a[App n []/0] # G) \<subseteq> set z' \<Longrightarrow> z' \<turnstile> b; news n G; new n a; new n b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> b
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
z \<turnstile> And p q
set z \<subseteq> set ?z' \<Longrightarrow> ?z' \<turnstile> And p q
set z \<subseteq> set z'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
z \<turnstile> And p q
set z \<subseteq> set ?z' \<Longrightarrow> ?z' \<turnstile> And p q
set z \<subseteq> set z'

goal (1 subgoal):
 1. z' \<turnstile> p
[PROOF STEP]
using deriv.AndE1
[PROOF STATE]
proof (prove)
using this:
z \<turnstile> And p q
set z \<subseteq> set ?z' \<Longrightarrow> ?z' \<turnstile> And p q
set z \<subseteq> set z'
?G \<turnstile> And ?a ?b \<Longrightarrow> ?G \<turnstile> ?a

goal (1 subgoal):
 1. z' \<turnstile> p
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
z' \<turnstile> p

goal (6 subgoals):
 1. \<And>G a b z'. \<lbrakk>G \<turnstile> a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a; G \<turnstile> b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> And a b
 2. \<And>G a b z'. \<lbrakk>G \<turnstile> And a b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> And a b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> b
 3. \<And>G a n z'. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a[App n []/0]; news n G; new n a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Forall a
 4. \<And>G a t z'. \<lbrakk>G \<turnstile> Forall a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> Forall a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> a[t/0]
 5. \<And>G a t z'. \<lbrakk>G \<turnstile> a[t/0]; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a[t/0]; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Exists a
 6. \<And>G a n b z'. \<lbrakk>G \<turnstile> Exists a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> Exists a; a[App n []/0] # G \<turnstile> b; \<And>z'. set (a[App n []/0] # G) \<subseteq> set z' \<Longrightarrow> z' \<turnstile> b; news n G; new n a; new n b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> b
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<And>G a b z'. \<lbrakk>G \<turnstile> a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a; G \<turnstile> b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> And a b
 2. \<And>G a b z'. \<lbrakk>G \<turnstile> And a b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> And a b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> b
 3. \<And>G a n z'. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a[App n []/0]; news n G; new n a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Forall a
 4. \<And>G a t z'. \<lbrakk>G \<turnstile> Forall a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> Forall a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> a[t/0]
 5. \<And>G a t z'. \<lbrakk>G \<turnstile> a[t/0]; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a[t/0]; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Exists a
 6. \<And>G a n b z'. \<lbrakk>G \<turnstile> Exists a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> Exists a; a[App n []/0] # G \<turnstile> b; \<And>z'. set (a[App n []/0] # G) \<subseteq> set z' \<Longrightarrow> z' \<turnstile> b; news n G; new n a; new n b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> b
[PROOF STEP]
case (AndE2 z p q)
[PROOF STATE]
proof (state)
this:
z \<turnstile> And p q
set z \<subseteq> set ?z' \<Longrightarrow> ?z' \<turnstile> And p q
set z \<subseteq> set z'

goal (6 subgoals):
 1. \<And>G a b z'. \<lbrakk>G \<turnstile> a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a; G \<turnstile> b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> And a b
 2. \<And>G a b z'. \<lbrakk>G \<turnstile> And a b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> And a b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> b
 3. \<And>G a n z'. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a[App n []/0]; news n G; new n a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Forall a
 4. \<And>G a t z'. \<lbrakk>G \<turnstile> Forall a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> Forall a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> a[t/0]
 5. \<And>G a t z'. \<lbrakk>G \<turnstile> a[t/0]; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a[t/0]; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Exists a
 6. \<And>G a n b z'. \<lbrakk>G \<turnstile> Exists a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> Exists a; a[App n []/0] # G \<turnstile> b; \<And>z'. set (a[App n []/0] # G) \<subseteq> set z' \<Longrightarrow> z' \<turnstile> b; news n G; new n a; new n b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> b
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
z \<turnstile> And p q
set z \<subseteq> set ?z' \<Longrightarrow> ?z' \<turnstile> And p q
set z \<subseteq> set z'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
z \<turnstile> And p q
set z \<subseteq> set ?z' \<Longrightarrow> ?z' \<turnstile> And p q
set z \<subseteq> set z'

goal (1 subgoal):
 1. z' \<turnstile> q
[PROOF STEP]
using deriv.AndE2
[PROOF STATE]
proof (prove)
using this:
z \<turnstile> And p q
set z \<subseteq> set ?z' \<Longrightarrow> ?z' \<turnstile> And p q
set z \<subseteq> set z'
?G \<turnstile> And ?a ?b \<Longrightarrow> ?G \<turnstile> ?b

goal (1 subgoal):
 1. z' \<turnstile> q
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
z' \<turnstile> q

goal (5 subgoals):
 1. \<And>G a b z'. \<lbrakk>G \<turnstile> a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a; G \<turnstile> b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> And a b
 2. \<And>G a n z'. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a[App n []/0]; news n G; new n a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Forall a
 3. \<And>G a t z'. \<lbrakk>G \<turnstile> Forall a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> Forall a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> a[t/0]
 4. \<And>G a t z'. \<lbrakk>G \<turnstile> a[t/0]; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a[t/0]; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Exists a
 5. \<And>G a n b z'. \<lbrakk>G \<turnstile> Exists a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> Exists a; a[App n []/0] # G \<turnstile> b; \<And>z'. set (a[App n []/0] # G) \<subseteq> set z' \<Longrightarrow> z' \<turnstile> b; news n G; new n a; new n b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> b
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>G a b z'. \<lbrakk>G \<turnstile> a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a; G \<turnstile> b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> And a b
 2. \<And>G a n z'. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a[App n []/0]; news n G; new n a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Forall a
 3. \<And>G a t z'. \<lbrakk>G \<turnstile> Forall a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> Forall a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> a[t/0]
 4. \<And>G a t z'. \<lbrakk>G \<turnstile> a[t/0]; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a[t/0]; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Exists a
 5. \<And>G a n b z'. \<lbrakk>G \<turnstile> Exists a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> Exists a; a[App n []/0] # G \<turnstile> b; \<And>z'. set (a[App n []/0] # G) \<subseteq> set z' \<Longrightarrow> z' \<turnstile> b; news n G; new n a; new n b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> b
[PROOF STEP]
case (AndI z p q)
[PROOF STATE]
proof (state)
this:
z \<turnstile> p
set z \<subseteq> set ?z' \<Longrightarrow> ?z' \<turnstile> p
z \<turnstile> q
set z \<subseteq> set ?z' \<Longrightarrow> ?z' \<turnstile> q
set z \<subseteq> set z'

goal (5 subgoals):
 1. \<And>G a b z'. \<lbrakk>G \<turnstile> a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a; G \<turnstile> b; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> And a b
 2. \<And>G a n z'. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a[App n []/0]; news n G; new n a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Forall a
 3. \<And>G a t z'. \<lbrakk>G \<turnstile> Forall a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> Forall a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> a[t/0]
 4. \<And>G a t z'. \<lbrakk>G \<turnstile> a[t/0]; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a[t/0]; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Exists a
 5. \<And>G a n b z'. \<lbrakk>G \<turnstile> Exists a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> Exists a; a[App n []/0] # G \<turnstile> b; \<And>z'. set (a[App n []/0] # G) \<subseteq> set z' \<Longrightarrow> z' \<turnstile> b; news n G; new n a; new n b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> b
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
z \<turnstile> p
set z \<subseteq> set ?z' \<Longrightarrow> ?z' \<turnstile> p
z \<turnstile> q
set z \<subseteq> set ?z' \<Longrightarrow> ?z' \<turnstile> q
set z \<subseteq> set z'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
z \<turnstile> p
set z \<subseteq> set ?z' \<Longrightarrow> ?z' \<turnstile> p
z \<turnstile> q
set z \<subseteq> set ?z' \<Longrightarrow> ?z' \<turnstile> q
set z \<subseteq> set z'

goal (1 subgoal):
 1. z' \<turnstile> And p q
[PROOF STEP]
using deriv.AndI
[PROOF STATE]
proof (prove)
using this:
z \<turnstile> p
set z \<subseteq> set ?z' \<Longrightarrow> ?z' \<turnstile> p
z \<turnstile> q
set z \<subseteq> set ?z' \<Longrightarrow> ?z' \<turnstile> q
set z \<subseteq> set z'
\<lbrakk>?G \<turnstile> ?a; ?G \<turnstile> ?b\<rbrakk> \<Longrightarrow> ?G \<turnstile> And ?a ?b

goal (1 subgoal):
 1. z' \<turnstile> And p q
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
z' \<turnstile> And p q

goal (4 subgoals):
 1. \<And>G a n z'. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a[App n []/0]; news n G; new n a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Forall a
 2. \<And>G a t z'. \<lbrakk>G \<turnstile> Forall a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> Forall a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> a[t/0]
 3. \<And>G a t z'. \<lbrakk>G \<turnstile> a[t/0]; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a[t/0]; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Exists a
 4. \<And>G a n b z'. \<lbrakk>G \<turnstile> Exists a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> Exists a; a[App n []/0] # G \<turnstile> b; \<And>z'. set (a[App n []/0] # G) \<subseteq> set z' \<Longrightarrow> z' \<turnstile> b; news n G; new n a; new n b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> b
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>G a n z'. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a[App n []/0]; news n G; new n a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Forall a
 2. \<And>G a t z'. \<lbrakk>G \<turnstile> Forall a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> Forall a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> a[t/0]
 3. \<And>G a t z'. \<lbrakk>G \<turnstile> a[t/0]; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a[t/0]; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Exists a
 4. \<And>G a n b z'. \<lbrakk>G \<turnstile> Exists a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> Exists a; a[App n []/0] # G \<turnstile> b; \<And>z'. set (a[App n []/0] # G) \<subseteq> set z' \<Longrightarrow> z' \<turnstile> b; news n G; new n a; new n b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> b
[PROOF STEP]
case (ExistsE z p c q)
[PROOF STATE]
proof (state)
this:
z \<turnstile> Exists p
set z \<subseteq> set ?z' \<Longrightarrow> ?z' \<turnstile> Exists p
p[App c []/0] # z \<turnstile> q
set (p[App c []/0] # z) \<subseteq> set ?z' \<Longrightarrow> ?z' \<turnstile> q
news c z
new c p
new c q
set z \<subseteq> set z'

goal (4 subgoals):
 1. \<And>G a n z'. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a[App n []/0]; news n G; new n a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Forall a
 2. \<And>G a t z'. \<lbrakk>G \<turnstile> Forall a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> Forall a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> a[t/0]
 3. \<And>G a t z'. \<lbrakk>G \<turnstile> a[t/0]; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a[t/0]; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Exists a
 4. \<And>G a n b z'. \<lbrakk>G \<turnstile> Exists a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> Exists a; a[App n []/0] # G \<turnstile> b; \<And>z'. set (a[App n []/0] # G) \<subseteq> set z' \<Longrightarrow> z' \<turnstile> b; news n G; new n a; new n b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> b
[PROOF STEP]
let ?params = \<open>params p \<union> params q \<union> (\<Union>p \<in> set z'. params p) \<union> {c}\<close>
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>G a n z'. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a[App n []/0]; news n G; new n a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Forall a
 2. \<And>G a t z'. \<lbrakk>G \<turnstile> Forall a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> Forall a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> a[t/0]
 3. \<And>G a t z'. \<lbrakk>G \<turnstile> a[t/0]; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a[t/0]; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Exists a
 4. \<And>G a n b z'. \<lbrakk>G \<turnstile> Exists a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> Exists a; a[App n []/0] # G \<turnstile> b; \<And>z'. set (a[App n []/0] # G) \<subseteq> set z' \<Longrightarrow> z' \<turnstile> b; news n G; new n a; new n b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> b
[PROOF STEP]
have \<open>finite ?params\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (params p \<union> params q \<union> \<Union> (params ` set z') \<union> {c})
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
finite (params p \<union> params q \<union> \<Union> (params ` set z') \<union> {c})

goal (4 subgoals):
 1. \<And>G a n z'. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a[App n []/0]; news n G; new n a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Forall a
 2. \<And>G a t z'. \<lbrakk>G \<turnstile> Forall a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> Forall a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> a[t/0]
 3. \<And>G a t z'. \<lbrakk>G \<turnstile> a[t/0]; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a[t/0]; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Exists a
 4. \<And>G a n b z'. \<lbrakk>G \<turnstile> Exists a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> Exists a; a[App n []/0] # G \<turnstile> b; \<And>z'. set (a[App n []/0] # G) \<subseteq> set z' \<Longrightarrow> z' \<turnstile> b; news n G; new n a; new n b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> b
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
finite (params p \<union> params q \<union> \<Union> (params ` set z') \<union> {c})
[PROOF STEP]
obtain fresh where fresh: \<open>fresh \<notin> ?params\<close>
[PROOF STATE]
proof (prove)
using this:
finite (params p \<union> params q \<union> \<Union> (params ` set z') \<union> {c})

goal (1 subgoal):
 1. (\<And>fresh. fresh \<notin> params p \<union> params q \<union> \<Union> (params ` set z') \<union> {c} \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using inf_params
[PROOF STATE]
proof (prove)
using this:
finite (params p \<union> params q \<union> \<Union> (params ` set z') \<union> {c})
infinite UNIV

goal (1 subgoal):
 1. (\<And>fresh. fresh \<notin> params p \<union> params q \<union> \<Union> (params ` set z') \<union> {c} \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (meson ex_new_if_finite List.finite_set infinite_UNIV_listI)
[PROOF STATE]
proof (state)
this:
fresh \<notin> params p \<union> params q \<union> \<Union> (params ` set z') \<union> {c}

goal (4 subgoals):
 1. \<And>G a n z'. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a[App n []/0]; news n G; new n a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Forall a
 2. \<And>G a t z'. \<lbrakk>G \<turnstile> Forall a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> Forall a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> a[t/0]
 3. \<And>G a t z'. \<lbrakk>G \<turnstile> a[t/0]; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a[t/0]; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Exists a
 4. \<And>G a n b z'. \<lbrakk>G \<turnstile> Exists a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> Exists a; a[App n []/0] # G \<turnstile> b; \<And>z'. set (a[App n []/0] # G) \<subseteq> set z' \<Longrightarrow> z' \<turnstile> b; news n G; new n a; new n b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> b
[PROOF STEP]
let ?z' = \<open>map (psubst (id(c := fresh))) z'\<close>
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>G a n z'. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a[App n []/0]; news n G; new n a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Forall a
 2. \<And>G a t z'. \<lbrakk>G \<turnstile> Forall a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> Forall a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> a[t/0]
 3. \<And>G a t z'. \<lbrakk>G \<turnstile> a[t/0]; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a[t/0]; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Exists a
 4. \<And>G a n b z'. \<lbrakk>G \<turnstile> Exists a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> Exists a; a[App n []/0] # G \<turnstile> b; \<And>z'. set (a[App n []/0] # G) \<subseteq> set z' \<Longrightarrow> z' \<turnstile> b; news n G; new n a; new n b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> b
[PROOF STEP]
have \<open>news c z\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. news c z
[PROOF STEP]
using ExistsE
[PROOF STATE]
proof (prove)
using this:
z \<turnstile> Exists p
set z \<subseteq> set ?z' \<Longrightarrow> ?z' \<turnstile> Exists p
p[App c []/0] # z \<turnstile> q
set (p[App c []/0] # z) \<subseteq> set ?z' \<Longrightarrow> ?z' \<turnstile> q
news c z
new c p
new c q
set z \<subseteq> set z'

goal (1 subgoal):
 1. news c z
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
news c z

goal (4 subgoals):
 1. \<And>G a n z'. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a[App n []/0]; news n G; new n a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Forall a
 2. \<And>G a t z'. \<lbrakk>G \<turnstile> Forall a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> Forall a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> a[t/0]
 3. \<And>G a t z'. \<lbrakk>G \<turnstile> a[t/0]; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a[t/0]; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Exists a
 4. \<And>G a n b z'. \<lbrakk>G \<turnstile> Exists a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> Exists a; a[App n []/0] # G \<turnstile> b; \<And>z'. set (a[App n []/0] # G) \<subseteq> set z' \<Longrightarrow> z' \<turnstile> b; news n G; new n a; new n b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> b
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
news c z
[PROOF STEP]
have \<open>set z \<subseteq> set ?z'\<close>
[PROOF STATE]
proof (prove)
using this:
news c z

goal (1 subgoal):
 1. set z \<subseteq> set (map (psubst (id(c := fresh))) z')
[PROOF STEP]
using ExistsE psubst_new_subset
[PROOF STATE]
proof (prove)
using this:
news c z
z \<turnstile> Exists p
set z \<subseteq> set ?z' \<Longrightarrow> ?z' \<turnstile> Exists p
p[App c []/0] # z \<turnstile> q
set (p[App c []/0] # z) \<subseteq> set ?z' \<Longrightarrow> ?z' \<turnstile> q
news c z
new c p
new c q
set z \<subseteq> set z'
\<lbrakk>set ?z \<subseteq> set ?z'; ?c \<notin> \<Union> (params ` set ?z)\<rbrakk> \<Longrightarrow> set ?z \<subseteq> set (map (psubst (id(?c := ?n))) ?z')

goal (1 subgoal):
 1. set z \<subseteq> set (map (psubst (id(c := fresh))) z')
[PROOF STEP]
by (simp add: Ball_set)
[PROOF STATE]
proof (state)
this:
set z \<subseteq> set (map (psubst (id(c := fresh))) z')

goal (4 subgoals):
 1. \<And>G a n z'. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a[App n []/0]; news n G; new n a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Forall a
 2. \<And>G a t z'. \<lbrakk>G \<turnstile> Forall a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> Forall a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> a[t/0]
 3. \<And>G a t z'. \<lbrakk>G \<turnstile> a[t/0]; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a[t/0]; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Exists a
 4. \<And>G a n b z'. \<lbrakk>G \<turnstile> Exists a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> Exists a; a[App n []/0] # G \<turnstile> b; \<And>z'. set (a[App n []/0] # G) \<subseteq> set z' \<Longrightarrow> z' \<turnstile> b; news n G; new n a; new n b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> b
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
set z \<subseteq> set (map (psubst (id(c := fresh))) z')
[PROOF STEP]
have \<open>?z' \<turnstile> Exists p\<close>
[PROOF STATE]
proof (prove)
using this:
set z \<subseteq> set (map (psubst (id(c := fresh))) z')

goal (1 subgoal):
 1. map (psubst (id(c := fresh))) z' \<turnstile> Exists p
[PROOF STEP]
using ExistsE
[PROOF STATE]
proof (prove)
using this:
set z \<subseteq> set (map (psubst (id(c := fresh))) z')
z \<turnstile> Exists p
set z \<subseteq> set ?z' \<Longrightarrow> ?z' \<turnstile> Exists p
p[App c []/0] # z \<turnstile> q
set (p[App c []/0] # z) \<subseteq> set ?z' \<Longrightarrow> ?z' \<turnstile> q
news c z
new c p
new c q
set z \<subseteq> set z'

goal (1 subgoal):
 1. map (psubst (id(c := fresh))) z' \<turnstile> Exists p
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
map (psubst (id(c := fresh))) z' \<turnstile> Exists p

goal (4 subgoals):
 1. \<And>G a n z'. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a[App n []/0]; news n G; new n a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Forall a
 2. \<And>G a t z'. \<lbrakk>G \<turnstile> Forall a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> Forall a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> a[t/0]
 3. \<And>G a t z'. \<lbrakk>G \<turnstile> a[t/0]; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a[t/0]; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Exists a
 4. \<And>G a n b z'. \<lbrakk>G \<turnstile> Exists a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> Exists a; a[App n []/0] # G \<turnstile> b; \<And>z'. set (a[App n []/0] # G) \<subseteq> set z' \<Longrightarrow> z' \<turnstile> b; news n G; new n a; new n b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> b
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
map (psubst (id(c := fresh))) z' \<turnstile> Exists p

goal (4 subgoals):
 1. \<And>G a n z'. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a[App n []/0]; news n G; new n a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Forall a
 2. \<And>G a t z'. \<lbrakk>G \<turnstile> Forall a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> Forall a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> a[t/0]
 3. \<And>G a t z'. \<lbrakk>G \<turnstile> a[t/0]; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a[t/0]; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Exists a
 4. \<And>G a n b z'. \<lbrakk>G \<turnstile> Exists a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> Exists a; a[App n []/0] # G \<turnstile> b; \<And>z'. set (a[App n []/0] # G) \<subseteq> set z' \<Longrightarrow> z' \<turnstile> b; news n G; new n a; new n b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> b
[PROOF STEP]
have \<open>set (subst p (App c []) 0 # z) \<subseteq> set (subst p (App c []) 0 # ?z')\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (p[App c []/0] # z) \<subseteq> set (p[App c []/0] # map (psubst (id(c := fresh))) z')
[PROOF STEP]
using \<open>set z \<subseteq> set ?z'\<close>
[PROOF STATE]
proof (prove)
using this:
set z \<subseteq> set (map (psubst (id(c := fresh))) z')

goal (1 subgoal):
 1. set (p[App c []/0] # z) \<subseteq> set (p[App c []/0] # map (psubst (id(c := fresh))) z')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set (p[App c []/0] # z) \<subseteq> set (p[App c []/0] # map (psubst (id(c := fresh))) z')

goal (4 subgoals):
 1. \<And>G a n z'. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a[App n []/0]; news n G; new n a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Forall a
 2. \<And>G a t z'. \<lbrakk>G \<turnstile> Forall a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> Forall a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> a[t/0]
 3. \<And>G a t z'. \<lbrakk>G \<turnstile> a[t/0]; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a[t/0]; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Exists a
 4. \<And>G a n b z'. \<lbrakk>G \<turnstile> Exists a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> Exists a; a[App n []/0] # G \<turnstile> b; \<And>z'. set (a[App n []/0] # G) \<subseteq> set z' \<Longrightarrow> z' \<turnstile> b; news n G; new n a; new n b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> b
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
set (p[App c []/0] # z) \<subseteq> set (p[App c []/0] # map (psubst (id(c := fresh))) z')
[PROOF STEP]
have \<open>subst p (App c []) 0 # ?z' \<turnstile> q\<close>
[PROOF STATE]
proof (prove)
using this:
set (p[App c []/0] # z) \<subseteq> set (p[App c []/0] # map (psubst (id(c := fresh))) z')

goal (1 subgoal):
 1. p[App c []/0] # map (psubst (id(c := fresh))) z' \<turnstile> q
[PROOF STEP]
using ExistsE
[PROOF STATE]
proof (prove)
using this:
set (p[App c []/0] # z) \<subseteq> set (p[App c []/0] # map (psubst (id(c := fresh))) z')
z \<turnstile> Exists p
set z \<subseteq> set ?z' \<Longrightarrow> ?z' \<turnstile> Exists p
p[App c []/0] # z \<turnstile> q
set (p[App c []/0] # z) \<subseteq> set ?z' \<Longrightarrow> ?z' \<turnstile> q
news c z
new c p
new c q
set z \<subseteq> set z'

goal (1 subgoal):
 1. p[App c []/0] # map (psubst (id(c := fresh))) z' \<turnstile> q
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
p[App c []/0] # map (psubst (id(c := fresh))) z' \<turnstile> q

goal (4 subgoals):
 1. \<And>G a n z'. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a[App n []/0]; news n G; new n a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Forall a
 2. \<And>G a t z'. \<lbrakk>G \<turnstile> Forall a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> Forall a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> a[t/0]
 3. \<And>G a t z'. \<lbrakk>G \<turnstile> a[t/0]; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a[t/0]; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Exists a
 4. \<And>G a n b z'. \<lbrakk>G \<turnstile> Exists a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> Exists a; a[App n []/0] # G \<turnstile> b; \<And>z'. set (a[App n []/0] # G) \<subseteq> set z' \<Longrightarrow> z' \<turnstile> b; news n G; new n a; new n b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> b
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
p[App c []/0] # map (psubst (id(c := fresh))) z' \<turnstile> q

goal (4 subgoals):
 1. \<And>G a n z'. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a[App n []/0]; news n G; new n a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Forall a
 2. \<And>G a t z'. \<lbrakk>G \<turnstile> Forall a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> Forall a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> a[t/0]
 3. \<And>G a t z'. \<lbrakk>G \<turnstile> a[t/0]; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a[t/0]; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Exists a
 4. \<And>G a n b z'. \<lbrakk>G \<turnstile> Exists a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> Exists a; a[App n []/0] # G \<turnstile> b; \<And>z'. set (a[App n []/0] # G) \<subseteq> set z' \<Longrightarrow> z' \<turnstile> b; news n G; new n a; new n b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> b
[PROOF STEP]
have \<open>news c ?z'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. news c (map (psubst (id(c := fresh))) z')
[PROOF STEP]
using fresh
[PROOF STATE]
proof (prove)
using this:
fresh \<notin> params p \<union> params q \<union> \<Union> (params ` set z') \<union> {c}

goal (1 subgoal):
 1. news c (map (psubst (id(c := fresh))) z')
[PROOF STEP]
by (simp add: map_psubst_new_free)
[PROOF STATE]
proof (state)
this:
news c (map (psubst (id(c := fresh))) z')

goal (4 subgoals):
 1. \<And>G a n z'. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a[App n []/0]; news n G; new n a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Forall a
 2. \<And>G a t z'. \<lbrakk>G \<turnstile> Forall a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> Forall a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> a[t/0]
 3. \<And>G a t z'. \<lbrakk>G \<turnstile> a[t/0]; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a[t/0]; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Exists a
 4. \<And>G a n b z'. \<lbrakk>G \<turnstile> Exists a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> Exists a; a[App n []/0] # G \<turnstile> b; \<And>z'. set (a[App n []/0] # G) \<subseteq> set z' \<Longrightarrow> z' \<turnstile> b; news n G; new n a; new n b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> b
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
news c (map (psubst (id(c := fresh))) z')
[PROOF STEP]
have \<open>new c p\<close> \<open>new c q\<close> \<open>news c ?z'\<close>
[PROOF STATE]
proof (prove)
using this:
news c (map (psubst (id(c := fresh))) z')

goal (1 subgoal):
 1. new c p &&& new c q &&& news c (map (psubst (id(c := fresh))) z')
[PROOF STEP]
using ExistsE
[PROOF STATE]
proof (prove)
using this:
news c (map (psubst (id(c := fresh))) z')
z \<turnstile> Exists p
set z \<subseteq> set ?z' \<Longrightarrow> ?z' \<turnstile> Exists p
p[App c []/0] # z \<turnstile> q
set (p[App c []/0] # z) \<subseteq> set ?z' \<Longrightarrow> ?z' \<turnstile> q
news c z
new c p
new c q
set z \<subseteq> set z'

goal (1 subgoal):
 1. new c p &&& new c q &&& news c (map (psubst (id(c := fresh))) z')
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
new c p
new c q
news c (map (psubst (id(c := fresh))) z')

goal (4 subgoals):
 1. \<And>G a n z'. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a[App n []/0]; news n G; new n a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Forall a
 2. \<And>G a t z'. \<lbrakk>G \<turnstile> Forall a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> Forall a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> a[t/0]
 3. \<And>G a t z'. \<lbrakk>G \<turnstile> a[t/0]; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a[t/0]; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Exists a
 4. \<And>G a n b z'. \<lbrakk>G \<turnstile> Exists a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> Exists a; a[App n []/0] # G \<turnstile> b; \<And>z'. set (a[App n []/0] # G) \<subseteq> set z' \<Longrightarrow> z' \<turnstile> b; news n G; new n a; new n b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> b
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
map (psubst (id(c := fresh))) z' \<turnstile> Exists p
p[App c []/0] # map (psubst (id(c := fresh))) z' \<turnstile> q
new c p
new c q
news c (map (psubst (id(c := fresh))) z')
[PROOF STEP]
have \<open>?z' \<turnstile> q\<close>
[PROOF STATE]
proof (prove)
using this:
map (psubst (id(c := fresh))) z' \<turnstile> Exists p
p[App c []/0] # map (psubst (id(c := fresh))) z' \<turnstile> q
new c p
new c q
news c (map (psubst (id(c := fresh))) z')

goal (1 subgoal):
 1. map (psubst (id(c := fresh))) z' \<turnstile> q
[PROOF STEP]
using ExistsE deriv.ExistsE
[PROOF STATE]
proof (prove)
using this:
map (psubst (id(c := fresh))) z' \<turnstile> Exists p
p[App c []/0] # map (psubst (id(c := fresh))) z' \<turnstile> q
new c p
new c q
news c (map (psubst (id(c := fresh))) z')
z \<turnstile> Exists p
set z \<subseteq> set ?z' \<Longrightarrow> ?z' \<turnstile> Exists p
p[App c []/0] # z \<turnstile> q
set (p[App c []/0] # z) \<subseteq> set ?z' \<Longrightarrow> ?z' \<turnstile> q
news c z
new c p
new c q
set z \<subseteq> set z'
\<lbrakk>?G \<turnstile> Exists ?a; ?a[App ?n []/0] # ?G \<turnstile> ?b; news ?n ?G; new ?n ?a; new ?n ?b\<rbrakk> \<Longrightarrow> ?G \<turnstile> ?b

goal (1 subgoal):
 1. map (psubst (id(c := fresh))) z' \<turnstile> q
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
map (psubst (id(c := fresh))) z' \<turnstile> q

goal (4 subgoals):
 1. \<And>G a n z'. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a[App n []/0]; news n G; new n a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Forall a
 2. \<And>G a t z'. \<lbrakk>G \<turnstile> Forall a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> Forall a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> a[t/0]
 3. \<And>G a t z'. \<lbrakk>G \<turnstile> a[t/0]; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a[t/0]; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Exists a
 4. \<And>G a n b z'. \<lbrakk>G \<turnstile> Exists a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> Exists a; a[App n []/0] # G \<turnstile> b; \<And>z'. set (a[App n []/0] # G) \<subseteq> set z' \<Longrightarrow> z' \<turnstile> b; news n G; new n a; new n b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> b
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
map (psubst (id(c := fresh))) z' \<turnstile> q
[PROOF STEP]
have \<open>map (psubst (id(fresh := c))) ?z' \<turnstile> psubst (id(fresh := c)) q\<close>
[PROOF STATE]
proof (prove)
using this:
map (psubst (id(c := fresh))) z' \<turnstile> q

goal (1 subgoal):
 1. map (psubst (id(fresh := c))) (map (psubst (id(c := fresh))) z') \<turnstile> psubst (id(fresh := c)) q
[PROOF STEP]
using deriv_psubst inf_params
[PROOF STATE]
proof (prove)
using this:
map (psubst (id(c := fresh))) z' \<turnstile> q
\<lbrakk>infinite UNIV; ?z \<turnstile> ?p\<rbrakk> \<Longrightarrow> map (psubst ?f) ?z \<turnstile> psubst ?f ?p
infinite UNIV

goal (1 subgoal):
 1. map (psubst (id(fresh := c))) (map (psubst (id(c := fresh))) z') \<turnstile> psubst (id(fresh := c)) q
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
map (psubst (id(fresh := c))) (map (psubst (id(c := fresh))) z') \<turnstile> psubst (id(fresh := c)) q

goal (4 subgoals):
 1. \<And>G a n z'. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a[App n []/0]; news n G; new n a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Forall a
 2. \<And>G a t z'. \<lbrakk>G \<turnstile> Forall a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> Forall a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> a[t/0]
 3. \<And>G a t z'. \<lbrakk>G \<turnstile> a[t/0]; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a[t/0]; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Exists a
 4. \<And>G a n b z'. \<lbrakk>G \<turnstile> Exists a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> Exists a; a[App n []/0] # G \<turnstile> b; \<And>z'. set (a[App n []/0] # G) \<subseteq> set z' \<Longrightarrow> z' \<turnstile> b; news n G; new n a; new n b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> b
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
map (psubst (id(fresh := c))) (map (psubst (id(c := fresh))) z') \<turnstile> psubst (id(fresh := c)) q

goal (4 subgoals):
 1. \<And>G a n z'. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a[App n []/0]; news n G; new n a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Forall a
 2. \<And>G a t z'. \<lbrakk>G \<turnstile> Forall a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> Forall a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> a[t/0]
 3. \<And>G a t z'. \<lbrakk>G \<turnstile> a[t/0]; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a[t/0]; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Exists a
 4. \<And>G a n b z'. \<lbrakk>G \<turnstile> Exists a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> Exists a; a[App n []/0] # G \<turnstile> b; \<And>z'. set (a[App n []/0] # G) \<subseteq> set z' \<Longrightarrow> z' \<turnstile> b; news n G; new n a; new n b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> b
[PROOF STEP]
have \<open>map (psubst (id(fresh := c))) ?z' = z'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map (psubst (id(fresh := c))) (map (psubst (id(c := fresh))) z') = z'
[PROOF STEP]
using fresh map_psubst_new_away Ball_set
[PROOF STATE]
proof (prove)
using this:
fresh \<notin> params p \<union> params q \<union> \<Union> (params ` set z') \<union> {c}
news ?fresh ?z \<Longrightarrow> map (psubst (id(?fresh := ?c))) (map (psubst (id(?c := ?fresh))) ?z) = ?z
Ball (set ?xs) ?P = list_all ?P ?xs

goal (1 subgoal):
 1. map (psubst (id(fresh := c))) (map (psubst (id(c := fresh))) z') = z'
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
map (psubst (id(fresh := c))) (map (psubst (id(c := fresh))) z') = z'

goal (4 subgoals):
 1. \<And>G a n z'. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a[App n []/0]; news n G; new n a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Forall a
 2. \<And>G a t z'. \<lbrakk>G \<turnstile> Forall a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> Forall a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> a[t/0]
 3. \<And>G a t z'. \<lbrakk>G \<turnstile> a[t/0]; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a[t/0]; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Exists a
 4. \<And>G a n b z'. \<lbrakk>G \<turnstile> Exists a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> Exists a; a[App n []/0] # G \<turnstile> b; \<And>z'. set (a[App n []/0] # G) \<subseteq> set z' \<Longrightarrow> z' \<turnstile> b; news n G; new n a; new n b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> b
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
map (psubst (id(fresh := c))) (map (psubst (id(c := fresh))) z') = z'

goal (4 subgoals):
 1. \<And>G a n z'. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a[App n []/0]; news n G; new n a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Forall a
 2. \<And>G a t z'. \<lbrakk>G \<turnstile> Forall a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> Forall a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> a[t/0]
 3. \<And>G a t z'. \<lbrakk>G \<turnstile> a[t/0]; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a[t/0]; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Exists a
 4. \<And>G a n b z'. \<lbrakk>G \<turnstile> Exists a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> Exists a; a[App n []/0] # G \<turnstile> b; \<And>z'. set (a[App n []/0] # G) \<subseteq> set z' \<Longrightarrow> z' \<turnstile> b; news n G; new n a; new n b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> b
[PROOF STEP]
have \<open>psubst (id(fresh := c)) q = q\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. psubst (id(fresh := c)) q = q
[PROOF STEP]
using fresh
[PROOF STATE]
proof (prove)
using this:
fresh \<notin> params p \<union> params q \<union> \<Union> (params ` set z') \<union> {c}

goal (1 subgoal):
 1. psubst (id(fresh := c)) q = q
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
psubst (id(fresh := c)) q = q

goal (4 subgoals):
 1. \<And>G a n z'. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a[App n []/0]; news n G; new n a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Forall a
 2. \<And>G a t z'. \<lbrakk>G \<turnstile> Forall a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> Forall a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> a[t/0]
 3. \<And>G a t z'. \<lbrakk>G \<turnstile> a[t/0]; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a[t/0]; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Exists a
 4. \<And>G a n b z'. \<lbrakk>G \<turnstile> Exists a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> Exists a; a[App n []/0] # G \<turnstile> b; \<And>z'. set (a[App n []/0] # G) \<subseteq> set z' \<Longrightarrow> z' \<turnstile> b; news n G; new n a; new n b; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> b
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
map (psubst (id(fresh := c))) (map (psubst (id(c := fresh))) z') \<turnstile> psubst (id(fresh := c)) q
map (psubst (id(fresh := c))) (map (psubst (id(c := fresh))) z') = z'
psubst (id(fresh := c)) q = q
[PROOF STEP]
show \<open>z' \<turnstile> q\<close>
[PROOF STATE]
proof (prove)
using this:
map (psubst (id(fresh := c))) (map (psubst (id(c := fresh))) z') \<turnstile> psubst (id(fresh := c)) q
map (psubst (id(fresh := c))) (map (psubst (id(c := fresh))) z') = z'
psubst (id(fresh := c)) q = q

goal (1 subgoal):
 1. z' \<turnstile> q
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
z' \<turnstile> q

goal (3 subgoals):
 1. \<And>G a n z'. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a[App n []/0]; news n G; new n a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Forall a
 2. \<And>G a t z'. \<lbrakk>G \<turnstile> Forall a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> Forall a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> a[t/0]
 3. \<And>G a t z'. \<lbrakk>G \<turnstile> a[t/0]; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a[t/0]; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Exists a
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>G a n z'. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a[App n []/0]; news n G; new n a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Forall a
 2. \<And>G a t z'. \<lbrakk>G \<turnstile> Forall a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> Forall a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> a[t/0]
 3. \<And>G a t z'. \<lbrakk>G \<turnstile> a[t/0]; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a[t/0]; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Exists a
[PROOF STEP]
case (ExistsI z p t)
[PROOF STATE]
proof (state)
this:
z \<turnstile> p[t/0]
set z \<subseteq> set ?z' \<Longrightarrow> ?z' \<turnstile> p[t/0]
set z \<subseteq> set z'

goal (3 subgoals):
 1. \<And>G a n z'. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a[App n []/0]; news n G; new n a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Forall a
 2. \<And>G a t z'. \<lbrakk>G \<turnstile> Forall a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> Forall a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> a[t/0]
 3. \<And>G a t z'. \<lbrakk>G \<turnstile> a[t/0]; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a[t/0]; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Exists a
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
z \<turnstile> p[t/0]
set z \<subseteq> set ?z' \<Longrightarrow> ?z' \<turnstile> p[t/0]
set z \<subseteq> set z'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
z \<turnstile> p[t/0]
set z \<subseteq> set ?z' \<Longrightarrow> ?z' \<turnstile> p[t/0]
set z \<subseteq> set z'

goal (1 subgoal):
 1. z' \<turnstile> Exists p
[PROOF STEP]
using deriv.ExistsI
[PROOF STATE]
proof (prove)
using this:
z \<turnstile> p[t/0]
set z \<subseteq> set ?z' \<Longrightarrow> ?z' \<turnstile> p[t/0]
set z \<subseteq> set z'
?G \<turnstile> ?a[?t/0] \<Longrightarrow> ?G \<turnstile> Exists ?a

goal (1 subgoal):
 1. z' \<turnstile> Exists p
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
z' \<turnstile> Exists p

goal (2 subgoals):
 1. \<And>G a n z'. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a[App n []/0]; news n G; new n a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Forall a
 2. \<And>G a t z'. \<lbrakk>G \<turnstile> Forall a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> Forall a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> a[t/0]
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>G a n z'. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a[App n []/0]; news n G; new n a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Forall a
 2. \<And>G a t z'. \<lbrakk>G \<turnstile> Forall a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> Forall a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> a[t/0]
[PROOF STEP]
case (ForallE p z t)
[PROOF STATE]
proof (state)
this:
p \<turnstile> Forall z
set p \<subseteq> set ?z' \<Longrightarrow> ?z' \<turnstile> Forall z
set p \<subseteq> set z'

goal (2 subgoals):
 1. \<And>G a n z'. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a[App n []/0]; news n G; new n a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Forall a
 2. \<And>G a t z'. \<lbrakk>G \<turnstile> Forall a; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> Forall a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> a[t/0]
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p \<turnstile> Forall z
set p \<subseteq> set ?z' \<Longrightarrow> ?z' \<turnstile> Forall z
set p \<subseteq> set z'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
p \<turnstile> Forall z
set p \<subseteq> set ?z' \<Longrightarrow> ?z' \<turnstile> Forall z
set p \<subseteq> set z'

goal (1 subgoal):
 1. z' \<turnstile> z[t/0]
[PROOF STEP]
using deriv.ForallE
[PROOF STATE]
proof (prove)
using this:
p \<turnstile> Forall z
set p \<subseteq> set ?z' \<Longrightarrow> ?z' \<turnstile> Forall z
set p \<subseteq> set z'
?G \<turnstile> Forall ?a \<Longrightarrow> ?G \<turnstile> ?a[?t/0]

goal (1 subgoal):
 1. z' \<turnstile> z[t/0]
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
z' \<turnstile> z[t/0]

goal (1 subgoal):
 1. \<And>G a n z'. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a[App n []/0]; news n G; new n a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Forall a
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>G a n z'. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a[App n []/0]; news n G; new n a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Forall a
[PROOF STEP]
case (ForallI z p c)
[PROOF STATE]
proof (state)
this:
z \<turnstile> p[App c []/0]
set z \<subseteq> set ?z' \<Longrightarrow> ?z' \<turnstile> p[App c []/0]
news c z
new c p
set z \<subseteq> set z'

goal (1 subgoal):
 1. \<And>G a n z'. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a[App n []/0]; news n G; new n a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Forall a
[PROOF STEP]
let ?params = \<open>params p \<union> (\<Union>p \<in> set z'. params p) \<union> {c}\<close>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>G a n z'. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a[App n []/0]; news n G; new n a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Forall a
[PROOF STEP]
have \<open>finite ?params\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (params p \<union> \<Union> (params ` set z') \<union> {c})
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
finite (params p \<union> \<Union> (params ` set z') \<union> {c})

goal (1 subgoal):
 1. \<And>G a n z'. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a[App n []/0]; news n G; new n a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Forall a
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
finite (params p \<union> \<Union> (params ` set z') \<union> {c})
[PROOF STEP]
obtain fresh where fresh: \<open>fresh \<notin> ?params\<close>
[PROOF STATE]
proof (prove)
using this:
finite (params p \<union> \<Union> (params ` set z') \<union> {c})

goal (1 subgoal):
 1. (\<And>fresh. fresh \<notin> params p \<union> \<Union> (params ` set z') \<union> {c} \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using inf_params
[PROOF STATE]
proof (prove)
using this:
finite (params p \<union> \<Union> (params ` set z') \<union> {c})
infinite UNIV

goal (1 subgoal):
 1. (\<And>fresh. fresh \<notin> params p \<union> \<Union> (params ` set z') \<union> {c} \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (meson ex_new_if_finite List.finite_set infinite_UNIV_listI)
[PROOF STATE]
proof (state)
this:
fresh \<notin> params p \<union> \<Union> (params ` set z') \<union> {c}

goal (1 subgoal):
 1. \<And>G a n z'. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a[App n []/0]; news n G; new n a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Forall a
[PROOF STEP]
let ?z' = \<open>map (psubst (id(c := fresh))) z'\<close>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>G a n z'. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a[App n []/0]; news n G; new n a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Forall a
[PROOF STEP]
have \<open>news c z\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. news c z
[PROOF STEP]
using ForallI
[PROOF STATE]
proof (prove)
using this:
z \<turnstile> p[App c []/0]
set z \<subseteq> set ?z' \<Longrightarrow> ?z' \<turnstile> p[App c []/0]
news c z
new c p
set z \<subseteq> set z'

goal (1 subgoal):
 1. news c z
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
news c z

goal (1 subgoal):
 1. \<And>G a n z'. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a[App n []/0]; news n G; new n a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Forall a
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
news c z
[PROOF STEP]
have \<open>set z \<subseteq> set ?z'\<close>
[PROOF STATE]
proof (prove)
using this:
news c z

goal (1 subgoal):
 1. set z \<subseteq> set (map (psubst (id(c := fresh))) z')
[PROOF STEP]
using ForallI psubst_new_subset
[PROOF STATE]
proof (prove)
using this:
news c z
z \<turnstile> p[App c []/0]
set z \<subseteq> set ?z' \<Longrightarrow> ?z' \<turnstile> p[App c []/0]
news c z
new c p
set z \<subseteq> set z'
\<lbrakk>set ?z \<subseteq> set ?z'; ?c \<notin> \<Union> (params ` set ?z)\<rbrakk> \<Longrightarrow> set ?z \<subseteq> set (map (psubst (id(?c := ?n))) ?z')

goal (1 subgoal):
 1. set z \<subseteq> set (map (psubst (id(c := fresh))) z')
[PROOF STEP]
by (metis (no_types, lifting) Ball_set UN_iff)
[PROOF STATE]
proof (state)
this:
set z \<subseteq> set (map (psubst (id(c := fresh))) z')

goal (1 subgoal):
 1. \<And>G a n z'. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a[App n []/0]; news n G; new n a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Forall a
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
set z \<subseteq> set (map (psubst (id(c := fresh))) z')
[PROOF STEP]
have \<open>?z' \<turnstile> subst p (App c []) 0\<close>
[PROOF STATE]
proof (prove)
using this:
set z \<subseteq> set (map (psubst (id(c := fresh))) z')

goal (1 subgoal):
 1. map (psubst (id(c := fresh))) z' \<turnstile> p[App c []/0]
[PROOF STEP]
using ForallI
[PROOF STATE]
proof (prove)
using this:
set z \<subseteq> set (map (psubst (id(c := fresh))) z')
z \<turnstile> p[App c []/0]
set z \<subseteq> set ?z' \<Longrightarrow> ?z' \<turnstile> p[App c []/0]
news c z
new c p
set z \<subseteq> set z'

goal (1 subgoal):
 1. map (psubst (id(c := fresh))) z' \<turnstile> p[App c []/0]
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
map (psubst (id(c := fresh))) z' \<turnstile> p[App c []/0]

goal (1 subgoal):
 1. \<And>G a n z'. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a[App n []/0]; news n G; new n a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Forall a
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
map (psubst (id(c := fresh))) z' \<turnstile> p[App c []/0]

goal (1 subgoal):
 1. \<And>G a n z'. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a[App n []/0]; news n G; new n a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Forall a
[PROOF STEP]
have \<open>\<forall>p \<in> set ?z'. c \<notin> params p\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>p\<in>set (map (psubst (id(c := fresh))) z'). new c p
[PROOF STEP]
using fresh psubst_new_free
[PROOF STATE]
proof (prove)
using this:
fresh \<notin> params p \<union> \<Union> (params ` set z') \<union> {c}
?c \<noteq> ?n \<Longrightarrow> new ?n (psubst (id(?n := ?c)) ?p)

goal (1 subgoal):
 1. \<forall>p\<in>set (map (psubst (id(c := fresh))) z'). new c p
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<forall>p\<in>set (map (psubst (id(c := fresh))) z'). new c p

goal (1 subgoal):
 1. \<And>G a n z'. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a[App n []/0]; news n G; new n a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Forall a
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>p\<in>set (map (psubst (id(c := fresh))) z'). new c p
[PROOF STEP]
have \<open>list_all (\<lambda>p. c \<notin> params p) (p # ?z')\<close>
[PROOF STATE]
proof (prove)
using this:
\<forall>p\<in>set (map (psubst (id(c := fresh))) z'). new c p

goal (1 subgoal):
 1. news c (p # map (psubst (id(c := fresh))) z')
[PROOF STEP]
using ForallI
[PROOF STATE]
proof (prove)
using this:
\<forall>p\<in>set (map (psubst (id(c := fresh))) z'). new c p
z \<turnstile> p[App c []/0]
set z \<subseteq> set ?z' \<Longrightarrow> ?z' \<turnstile> p[App c []/0]
news c z
new c p
set z \<subseteq> set z'

goal (1 subgoal):
 1. news c (p # map (psubst (id(c := fresh))) z')
[PROOF STEP]
by (simp add: list_all_iff)
[PROOF STATE]
proof (state)
this:
news c (p # map (psubst (id(c := fresh))) z')

goal (1 subgoal):
 1. \<And>G a n z'. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a[App n []/0]; news n G; new n a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Forall a
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
news c (p # map (psubst (id(c := fresh))) z')
[PROOF STEP]
have \<open>new c p\<close> \<open>news c ?z'\<close>
[PROOF STATE]
proof (prove)
using this:
news c (p # map (psubst (id(c := fresh))) z')

goal (1 subgoal):
 1. new c p &&& news c (map (psubst (id(c := fresh))) z')
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
new c p
news c (map (psubst (id(c := fresh))) z')

goal (1 subgoal):
 1. \<And>G a n z'. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a[App n []/0]; news n G; new n a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Forall a
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
map (psubst (id(c := fresh))) z' \<turnstile> p[App c []/0]
new c p
news c (map (psubst (id(c := fresh))) z')
[PROOF STEP]
have \<open>?z' \<turnstile> Forall p\<close>
[PROOF STATE]
proof (prove)
using this:
map (psubst (id(c := fresh))) z' \<turnstile> p[App c []/0]
new c p
news c (map (psubst (id(c := fresh))) z')

goal (1 subgoal):
 1. map (psubst (id(c := fresh))) z' \<turnstile> Forall p
[PROOF STEP]
using ForallI deriv.ForallI
[PROOF STATE]
proof (prove)
using this:
map (psubst (id(c := fresh))) z' \<turnstile> p[App c []/0]
new c p
news c (map (psubst (id(c := fresh))) z')
z \<turnstile> p[App c []/0]
set z \<subseteq> set ?z' \<Longrightarrow> ?z' \<turnstile> p[App c []/0]
news c z
new c p
set z \<subseteq> set z'
\<lbrakk>?G \<turnstile> ?a[App ?n []/0]; news ?n ?G; new ?n ?a\<rbrakk> \<Longrightarrow> ?G \<turnstile> Forall ?a

goal (1 subgoal):
 1. map (psubst (id(c := fresh))) z' \<turnstile> Forall p
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
map (psubst (id(c := fresh))) z' \<turnstile> Forall p

goal (1 subgoal):
 1. \<And>G a n z'. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a[App n []/0]; news n G; new n a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Forall a
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
map (psubst (id(c := fresh))) z' \<turnstile> Forall p
[PROOF STEP]
have \<open>map (psubst (id(fresh := c))) ?z' \<turnstile> psubst (id(fresh := c)) (Forall p)\<close>
[PROOF STATE]
proof (prove)
using this:
map (psubst (id(c := fresh))) z' \<turnstile> Forall p

goal (1 subgoal):
 1. map (psubst (id(fresh := c))) (map (psubst (id(c := fresh))) z') \<turnstile> psubst (id(fresh := c)) (Forall p)
[PROOF STEP]
using deriv_psubst inf_params
[PROOF STATE]
proof (prove)
using this:
map (psubst (id(c := fresh))) z' \<turnstile> Forall p
\<lbrakk>infinite UNIV; ?z \<turnstile> ?p\<rbrakk> \<Longrightarrow> map (psubst ?f) ?z \<turnstile> psubst ?f ?p
infinite UNIV

goal (1 subgoal):
 1. map (psubst (id(fresh := c))) (map (psubst (id(c := fresh))) z') \<turnstile> psubst (id(fresh := c)) (Forall p)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
map (psubst (id(fresh := c))) (map (psubst (id(c := fresh))) z') \<turnstile> psubst (id(fresh := c)) (Forall p)

goal (1 subgoal):
 1. \<And>G a n z'. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a[App n []/0]; news n G; new n a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Forall a
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
map (psubst (id(fresh := c))) (map (psubst (id(c := fresh))) z') \<turnstile> psubst (id(fresh := c)) (Forall p)

goal (1 subgoal):
 1. \<And>G a n z'. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a[App n []/0]; news n G; new n a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Forall a
[PROOF STEP]
have \<open>map (psubst (id(fresh := c))) ?z' = z'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map (psubst (id(fresh := c))) (map (psubst (id(c := fresh))) z') = z'
[PROOF STEP]
using fresh map_psubst_new_away Ball_set
[PROOF STATE]
proof (prove)
using this:
fresh \<notin> params p \<union> \<Union> (params ` set z') \<union> {c}
news ?fresh ?z \<Longrightarrow> map (psubst (id(?fresh := ?c))) (map (psubst (id(?c := ?fresh))) ?z) = ?z
Ball (set ?xs) ?P = list_all ?P ?xs

goal (1 subgoal):
 1. map (psubst (id(fresh := c))) (map (psubst (id(c := fresh))) z') = z'
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
map (psubst (id(fresh := c))) (map (psubst (id(c := fresh))) z') = z'

goal (1 subgoal):
 1. \<And>G a n z'. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a[App n []/0]; news n G; new n a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Forall a
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
map (psubst (id(fresh := c))) (map (psubst (id(c := fresh))) z') = z'

goal (1 subgoal):
 1. \<And>G a n z'. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a[App n []/0]; news n G; new n a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Forall a
[PROOF STEP]
have \<open>psubst (id(fresh := c)) (Forall p) = Forall p\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. psubst (id(fresh := c)) (Forall p) = Forall p
[PROOF STEP]
using fresh ForallI
[PROOF STATE]
proof (prove)
using this:
fresh \<notin> params p \<union> \<Union> (params ` set z') \<union> {c}
z \<turnstile> p[App c []/0]
set z \<subseteq> set ?z' \<Longrightarrow> ?z' \<turnstile> p[App c []/0]
news c z
new c p
set z \<subseteq> set z'

goal (1 subgoal):
 1. psubst (id(fresh := c)) (Forall p) = Forall p
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
psubst (id(fresh := c)) (Forall p) = Forall p

goal (1 subgoal):
 1. \<And>G a n z'. \<lbrakk>G \<turnstile> a[App n []/0]; \<And>z'. set G \<subseteq> set z' \<Longrightarrow> z' \<turnstile> a[App n []/0]; news n G; new n a; set G \<subseteq> set z'\<rbrakk> \<Longrightarrow> z' \<turnstile> Forall a
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
map (psubst (id(fresh := c))) (map (psubst (id(c := fresh))) z') \<turnstile> psubst (id(fresh := c)) (Forall p)
map (psubst (id(fresh := c))) (map (psubst (id(c := fresh))) z') = z'
psubst (id(fresh := c)) (Forall p) = Forall p
[PROOF STEP]
show \<open>z' \<turnstile> Forall p\<close>
[PROOF STATE]
proof (prove)
using this:
map (psubst (id(fresh := c))) (map (psubst (id(c := fresh))) z') \<turnstile> psubst (id(fresh := c)) (Forall p)
map (psubst (id(fresh := c))) (map (psubst (id(c := fresh))) z') = z'
psubst (id(fresh := c)) (Forall p) = Forall p

goal (1 subgoal):
 1. z' \<turnstile> Forall p
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
z' \<turnstile> Forall p

goal:
No subgoals!
[PROOF STEP]
qed