[STATEMENT]
lemma falsifies\<^sub>g_empty:
  assumes "falsifies\<^sub>g [] C"
  shows "C = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C = {}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. C = {}
[PROOF STEP]
have "\<forall>l \<in> C. False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>l\<in>C. False
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>l. l \<in> C \<Longrightarrow> False
[PROOF STEP]
fix l
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>l. l \<in> C \<Longrightarrow> False
[PROOF STEP]
assume "l\<in>C"
[PROOF STATE]
proof (state)
this:
l \<in> C

goal (1 subgoal):
 1. \<And>l. l \<in> C \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
l \<in> C
[PROOF STEP]
have "falsifies\<^sub>l [] l"
[PROOF STATE]
proof (prove)
using this:
l \<in> C

goal (1 subgoal):
 1. falsifies\<^sub>l [] l
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
l \<in> C
falsifies\<^sub>g [] C

goal (1 subgoal):
 1. falsifies\<^sub>l [] l
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
falsifies\<^sub>l [] l

goal (1 subgoal):
 1. \<And>l. l \<in> C \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
falsifies\<^sub>l [] l
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
falsifies\<^sub>l [] l

goal (1 subgoal):
 1. False
[PROOF STEP]
unfolding falsifies\<^sub>l_def
[PROOF STATE]
proof (prove)
using this:
ground\<^sub>l l \<and> (let i = nat_of_fatom (get_atom l) in i < length [] \<and> [] ! i = (\<not> sign l))

goal (1 subgoal):
 1. False
[PROOF STEP]
by (cases l) auto
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>l\<in>C. False

goal (1 subgoal):
 1. C = {}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>l\<in>C. False
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>l\<in>C. False

goal (1 subgoal):
 1. C = {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
C = {}

goal:
No subgoals!
[PROOF STEP]
qed