[STATEMENT]
lemma Exists_in_extend:
  assumes \<open>extend S C f n \<union> {f n} \<in> C\<close> (is \<open>?S' \<in> C\<close>)
    and \<open>Exists P = f n\<close>
  shows \<open>P[(App (SOME k. k \<notin> (\<Union>p \<in> extend S C f n \<union> {f n}. params p)) [])/0] \<in>
          extend S C f (Suc n)\<close>
    (is \<open>subst P ?t 0 \<in> extend S C f (Suc n)\<close>)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P[App (SOME k. k \<notin> \<Union> (params ` (extend S C f n \<union> {f n}))) []/0] \<in> extend S C f (Suc n)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P[App (SOME k. k \<notin> \<Union> (params ` (extend S C f n \<union> {f n}))) []/0] \<in> extend S C f (Suc n)
[PROOF STEP]
have \<open>\<exists>p. f n = Exists p\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>p. f n = Exists p
[PROOF STEP]
using \<open>Exists P = f n\<close>
[PROOF STATE]
proof (prove)
using this:
Exists P = f n

goal (1 subgoal):
 1. \<exists>p. f n = Exists p
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<exists>p. f n = Exists p

goal (1 subgoal):
 1. P[App (SOME k. k \<notin> \<Union> (params ` (extend S C f n \<union> {f n}))) []/0] \<in> extend S C f (Suc n)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>p. f n = Exists p
[PROOF STEP]
have \<open>extend S C f (Suc n) = (?S' \<union> {(dest_Exists (f n))[?t/0]})\<close>
[PROOF STATE]
proof (prove)
using this:
\<exists>p. f n = Exists p

goal (1 subgoal):
 1. extend S C f (Suc n) = extend S C f n \<union> {f n} \<union> {dest_Exists (f n)[App (SOME k. k \<notin> \<Union> (params ` (extend S C f n \<union> {f n}))) []/0]}
[PROOF STEP]
using \<open>?S' \<in> C\<close>
[PROOF STATE]
proof (prove)
using this:
\<exists>p. f n = Exists p
extend S C f n \<union> {f n} \<in> C

goal (1 subgoal):
 1. extend S C f (Suc n) = extend S C f n \<union> {f n} \<union> {dest_Exists (f n)[App (SOME k. k \<notin> \<Union> (params ` (extend S C f n \<union> {f n}))) []/0]}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
extend S C f (Suc n) = extend S C f n \<union> {f n} \<union> {dest_Exists (f n)[App (SOME k. k \<notin> \<Union> (params ` (extend S C f n \<union> {f n}))) []/0]}

goal (1 subgoal):
 1. P[App (SOME k. k \<notin> \<Union> (params ` (extend S C f n \<union> {f n}))) []/0] \<in> extend S C f (Suc n)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
extend S C f (Suc n) = extend S C f n \<union> {f n} \<union> {dest_Exists (f n)[App (SOME k. k \<notin> \<Union> (params ` (extend S C f n \<union> {f n}))) []/0]}

goal (1 subgoal):
 1. P[App (SOME k. k \<notin> \<Union> (params ` (extend S C f n \<union> {f n}))) []/0] \<in> extend S C f (Suc n)
[PROOF STEP]
have \<open>\<dots> = (?S' \<union> {(dest_Exists (Exists P))[?t/0]})\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. extend S C f n \<union> {f n} \<union> {dest_Exists (f n)[App (SOME k. k \<notin> \<Union> (params ` (extend S C f n \<union> {f n}))) []/0]} = extend S C f n \<union> {f n} \<union> {dest_Exists (Exists P)[App (SOME k. k \<notin> \<Union> (params ` (extend S C f n \<union> {f n}))) []/0]}
[PROOF STEP]
using \<open>Exists P = f n\<close>
[PROOF STATE]
proof (prove)
using this:
Exists P = f n

goal (1 subgoal):
 1. extend S C f n \<union> {f n} \<union> {dest_Exists (f n)[App (SOME k. k \<notin> \<Union> (params ` (extend S C f n \<union> {f n}))) []/0]} = extend S C f n \<union> {f n} \<union> {dest_Exists (Exists P)[App (SOME k. k \<notin> \<Union> (params ` (extend S C f n \<union> {f n}))) []/0]}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
extend S C f n \<union> {f n} \<union> {dest_Exists (f n)[App (SOME k. k \<notin> \<Union> (params ` (extend S C f n \<union> {f n}))) []/0]} = extend S C f n \<union> {f n} \<union> {dest_Exists (Exists P)[App (SOME k. k \<notin> \<Union> (params ` (extend S C f n \<union> {f n}))) []/0]}

goal (1 subgoal):
 1. P[App (SOME k. k \<notin> \<Union> (params ` (extend S C f n \<union> {f n}))) []/0] \<in> extend S C f (Suc n)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
extend S C f n \<union> {f n} \<union> {dest_Exists (f n)[App (SOME k. k \<notin> \<Union> (params ` (extend S C f n \<union> {f n}))) []/0]} = extend S C f n \<union> {f n} \<union> {dest_Exists (Exists P)[App (SOME k. k \<notin> \<Union> (params ` (extend S C f n \<union> {f n}))) []/0]}

goal (1 subgoal):
 1. P[App (SOME k. k \<notin> \<Union> (params ` (extend S C f n \<union> {f n}))) []/0] \<in> extend S C f (Suc n)
[PROOF STEP]
have \<open>\<dots> = (?S' \<union> {P[?t/0]})\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. extend S C f n \<union> {f n} \<union> {dest_Exists (Exists P)[App (SOME k. k \<notin> \<Union> (params ` (extend S C f n \<union> {f n}))) []/0]} = extend S C f n \<union> {f n} \<union> {P[App (SOME k. k \<notin> \<Union> (params ` (extend S C f n \<union> {f n}))) []/0]}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
extend S C f n \<union> {f n} \<union> {dest_Exists (Exists P)[App (SOME k. k \<notin> \<Union> (params ` (extend S C f n \<union> {f n}))) []/0]} = extend S C f n \<union> {f n} \<union> {P[App (SOME k. k \<notin> \<Union> (params ` (extend S C f n \<union> {f n}))) []/0]}

goal (1 subgoal):
 1. P[App (SOME k. k \<notin> \<Union> (params ` (extend S C f n \<union> {f n}))) []/0] \<in> extend S C f (Suc n)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
extend S C f (Suc n) = extend S C f n \<union> {f n} \<union> {P[App (SOME k. k \<notin> \<Union> (params ` (extend S C f n \<union> {f n}))) []/0]}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
extend S C f (Suc n) = extend S C f n \<union> {f n} \<union> {P[App (SOME k. k \<notin> \<Union> (params ` (extend S C f n \<union> {f n}))) []/0]}

goal (1 subgoal):
 1. P[App (SOME k. k \<notin> \<Union> (params ` (extend S C f n \<union> {f n}))) []/0] \<in> extend S C f (Suc n)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
P[App (SOME k. k \<notin> \<Union> (params ` (extend S C f n \<union> {f n}))) []/0] \<in> extend S C f (Suc n)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Neg_Forall_in_extend:
  assumes \<open>extend S C f n \<union> {f n} \<in> C\<close> (is \<open>?S' \<in> C\<close>)
    and \<open>Neg (Forall P) = f n\<close>
  shows \<open>Neg (P[(App (SOME k. k \<notin> (\<Union>p \<in> extend S C f n \<union> {f n}. params p)) [])/0])  \<in>
          extend S C f (Suc n)\<close>
    (is \<open>Neg (subst P ?t 0) \<in> extend S C f (Suc n)\<close>)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Neg (P[App (SOME k. k \<notin> \<Union> (params ` (extend S C f n \<union> {f n}))) []/0]) \<in> extend S C f (Suc n)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Neg (P[App (SOME k. k \<notin> \<Union> (params ` (extend S C f n \<union> {f n}))) []/0]) \<in> extend S C f (Suc n)
[PROOF STEP]
have \<open>f n \<noteq> Exists P\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f n \<noteq> Exists P
[PROOF STEP]
using \<open>Neg (Forall P) = f n\<close>
[PROOF STATE]
proof (prove)
using this:
Neg (Forall P) = f n

goal (1 subgoal):
 1. f n \<noteq> Exists P
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f n \<noteq> Exists P

goal (1 subgoal):
 1. Neg (P[App (SOME k. k \<notin> \<Union> (params ` (extend S C f n \<union> {f n}))) []/0]) \<in> extend S C f (Suc n)
[PROOF STEP]
have \<open>\<exists>p. f n = Neg (Forall p)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>p. f n = Neg (Forall p)
[PROOF STEP]
using \<open>Neg (Forall P) = f n\<close>
[PROOF STATE]
proof (prove)
using this:
Neg (Forall P) = f n

goal (1 subgoal):
 1. \<exists>p. f n = Neg (Forall p)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<exists>p. f n = Neg (Forall p)

goal (1 subgoal):
 1. Neg (P[App (SOME k. k \<notin> \<Union> (params ` (extend S C f n \<union> {f n}))) []/0]) \<in> extend S C f (Suc n)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>p. f n = Neg (Forall p)
[PROOF STEP]
have \<open>extend S C f (Suc n) = (?S' \<union> {Neg (dest_Forall (dest_Neg (f n))[?t/0])})\<close>
[PROOF STATE]
proof (prove)
using this:
\<exists>p. f n = Neg (Forall p)

goal (1 subgoal):
 1. extend S C f (Suc n) = extend S C f n \<union> {f n} \<union> {Neg (dest_Forall (dest_Neg (f n))[App (SOME k. k \<notin> \<Union> (params ` (extend S C f n \<union> {f n}))) []/0])}
[PROOF STEP]
using \<open>?S' \<in> C\<close> \<open>f n \<noteq> Exists P\<close>
[PROOF STATE]
proof (prove)
using this:
\<exists>p. f n = Neg (Forall p)
extend S C f n \<union> {f n} \<in> C
f n \<noteq> Exists P

goal (1 subgoal):
 1. extend S C f (Suc n) = extend S C f n \<union> {f n} \<union> {Neg (dest_Forall (dest_Neg (f n))[App (SOME k. k \<notin> \<Union> (params ` (extend S C f n \<union> {f n}))) []/0])}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
extend S C f (Suc n) = extend S C f n \<union> {f n} \<union> {Neg (dest_Forall (dest_Neg (f n))[App (SOME k. k \<notin> \<Union> (params ` (extend S C f n \<union> {f n}))) []/0])}

goal (1 subgoal):
 1. Neg (P[App (SOME k. k \<notin> \<Union> (params ` (extend S C f n \<union> {f n}))) []/0]) \<in> extend S C f (Suc n)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
extend S C f (Suc n) = extend S C f n \<union> {f n} \<union> {Neg (dest_Forall (dest_Neg (f n))[App (SOME k. k \<notin> \<Union> (params ` (extend S C f n \<union> {f n}))) []/0])}

goal (1 subgoal):
 1. Neg (P[App (SOME k. k \<notin> \<Union> (params ` (extend S C f n \<union> {f n}))) []/0]) \<in> extend S C f (Suc n)
[PROOF STEP]
have \<open>\<dots> = (?S' \<union> {Neg (dest_Forall (dest_Neg (Neg (Forall P)))[?t/0])})\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. extend S C f n \<union> {f n} \<union> {Neg (dest_Forall (dest_Neg (f n))[App (SOME k. k \<notin> \<Union> (params ` (extend S C f n \<union> {f n}))) []/0])} = extend S C f n \<union> {f n} \<union> {Neg (dest_Forall (dest_Neg (Neg (Forall P)))[App (SOME k. k \<notin> \<Union> (params ` (extend S C f n \<union> {f n}))) []/0])}
[PROOF STEP]
using \<open>Neg (Forall P) = f n\<close>
[PROOF STATE]
proof (prove)
using this:
Neg (Forall P) = f n

goal (1 subgoal):
 1. extend S C f n \<union> {f n} \<union> {Neg (dest_Forall (dest_Neg (f n))[App (SOME k. k \<notin> \<Union> (params ` (extend S C f n \<union> {f n}))) []/0])} = extend S C f n \<union> {f n} \<union> {Neg (dest_Forall (dest_Neg (Neg (Forall P)))[App (SOME k. k \<notin> \<Union> (params ` (extend S C f n \<union> {f n}))) []/0])}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
extend S C f n \<union> {f n} \<union> {Neg (dest_Forall (dest_Neg (f n))[App (SOME k. k \<notin> \<Union> (params ` (extend S C f n \<union> {f n}))) []/0])} = extend S C f n \<union> {f n} \<union> {Neg (dest_Forall (dest_Neg (Neg (Forall P)))[App (SOME k. k \<notin> \<Union> (params ` (extend S C f n \<union> {f n}))) []/0])}

goal (1 subgoal):
 1. Neg (P[App (SOME k. k \<notin> \<Union> (params ` (extend S C f n \<union> {f n}))) []/0]) \<in> extend S C f (Suc n)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
extend S C f n \<union> {f n} \<union> {Neg (dest_Forall (dest_Neg (f n))[App (SOME k. k \<notin> \<Union> (params ` (extend S C f n \<union> {f n}))) []/0])} = extend S C f n \<union> {f n} \<union> {Neg (dest_Forall (dest_Neg (Neg (Forall P)))[App (SOME k. k \<notin> \<Union> (params ` (extend S C f n \<union> {f n}))) []/0])}

goal (1 subgoal):
 1. Neg (P[App (SOME k. k \<notin> \<Union> (params ` (extend S C f n \<union> {f n}))) []/0]) \<in> extend S C f (Suc n)
[PROOF STEP]
have \<open>\<dots> = (?S' \<union> {Neg (P[?t/0])})\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. extend S C f n \<union> {f n} \<union> {Neg (dest_Forall (dest_Neg (Neg (Forall P)))[App (SOME k. k \<notin> \<Union> (params ` (extend S C f n \<union> {f n}))) []/0])} = extend S C f n \<union> {f n} \<union> {Neg (P[App (SOME k. k \<notin> \<Union> (params ` (extend S C f n \<union> {f n}))) []/0])}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
extend S C f n \<union> {f n} \<union> {Neg (dest_Forall (dest_Neg (Neg (Forall P)))[App (SOME k. k \<notin> \<Union> (params ` (extend S C f n \<union> {f n}))) []/0])} = extend S C f n \<union> {f n} \<union> {Neg (P[App (SOME k. k \<notin> \<Union> (params ` (extend S C f n \<union> {f n}))) []/0])}

goal (1 subgoal):
 1. Neg (P[App (SOME k. k \<notin> \<Union> (params ` (extend S C f n \<union> {f n}))) []/0]) \<in> extend S C f (Suc n)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
extend S C f (Suc n) = extend S C f n \<union> {f n} \<union> {Neg (P[App (SOME k. k \<notin> \<Union> (params ` (extend S C f n \<union> {f n}))) []/0])}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
extend S C f (Suc n) = extend S C f n \<union> {f n} \<union> {Neg (P[App (SOME k. k \<notin> \<Union> (params ` (extend S C f n \<union> {f n}))) []/0])}

goal (1 subgoal):
 1. Neg (P[App (SOME k. k \<notin> \<Union> (params ` (extend S C f n \<union> {f n}))) []/0]) \<in> extend S C f (Suc n)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Neg (P[App (SOME k. k \<notin> \<Union> (params ` (extend S C f n \<union> {f n}))) []/0]) \<in> extend S C f (Suc n)

goal:
No subgoals!
[PROOF STEP]
qed