[STATEMENT]
lemma std\<^sub>1_falsifies: "falsifies\<^sub>c G C\<^sub>1 \<longleftrightarrow> falsifies\<^sub>c G (std\<^sub>1 C\<^sub>1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. falsifies\<^sub>c G C\<^sub>1 = falsifies\<^sub>c G (C\<^sub>1 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''1'' @ x)))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. falsifies\<^sub>c G C\<^sub>1 \<Longrightarrow> falsifies\<^sub>c G (C\<^sub>1 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''1'' @ x)))
 2. falsifies\<^sub>c G (C\<^sub>1 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''1'' @ x))) \<Longrightarrow> falsifies\<^sub>c G C\<^sub>1
[PROOF STEP]
assume asm: "falsifies\<^sub>c G C\<^sub>1"
[PROOF STATE]
proof (state)
this:
falsifies\<^sub>c G C\<^sub>1

goal (2 subgoals):
 1. falsifies\<^sub>c G C\<^sub>1 \<Longrightarrow> falsifies\<^sub>c G (C\<^sub>1 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''1'' @ x)))
 2. falsifies\<^sub>c G (C\<^sub>1 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''1'' @ x))) \<Longrightarrow> falsifies\<^sub>c G C\<^sub>1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
falsifies\<^sub>c G C\<^sub>1
[PROOF STEP]
obtain Cg where "instance_of\<^sub>l\<^sub>s Cg C\<^sub>1  \<and> falsifies\<^sub>g G Cg"
[PROOF STATE]
proof (prove)
using this:
falsifies\<^sub>c G C\<^sub>1

goal (1 subgoal):
 1. (\<And>Cg. instance_of\<^sub>l\<^sub>s Cg C\<^sub>1 \<and> falsifies\<^sub>g G Cg \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
instance_of\<^sub>l\<^sub>s Cg C\<^sub>1 \<and> falsifies\<^sub>g G Cg

goal (2 subgoals):
 1. falsifies\<^sub>c G C\<^sub>1 \<Longrightarrow> falsifies\<^sub>c G (C\<^sub>1 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''1'' @ x)))
 2. falsifies\<^sub>c G (C\<^sub>1 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''1'' @ x))) \<Longrightarrow> falsifies\<^sub>c G C\<^sub>1
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
instance_of\<^sub>l\<^sub>s Cg C\<^sub>1 \<and> falsifies\<^sub>g G Cg

goal (2 subgoals):
 1. falsifies\<^sub>c G C\<^sub>1 \<Longrightarrow> falsifies\<^sub>c G (C\<^sub>1 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''1'' @ x)))
 2. falsifies\<^sub>c G (C\<^sub>1 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''1'' @ x))) \<Longrightarrow> falsifies\<^sub>c G C\<^sub>1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
instance_of\<^sub>l\<^sub>s Cg C\<^sub>1 \<and> falsifies\<^sub>g G Cg
[PROOF STEP]
have "instance_of\<^sub>l\<^sub>s Cg (std\<^sub>1 C\<^sub>1)"
[PROOF STATE]
proof (prove)
using this:
instance_of\<^sub>l\<^sub>s Cg C\<^sub>1 \<and> falsifies\<^sub>g G Cg

goal (1 subgoal):
 1. instance_of\<^sub>l\<^sub>s Cg (C\<^sub>1 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''1'' @ x)))
[PROOF STEP]
using std_apart_instance_of\<^sub>l\<^sub>s1 instance_of\<^sub>l\<^sub>s_trans
[PROOF STATE]
proof (prove)
using this:
instance_of\<^sub>l\<^sub>s Cg C\<^sub>1 \<and> falsifies\<^sub>g G Cg
instance_of\<^sub>l\<^sub>s ?C\<^sub>1 (?C\<^sub>1 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''1'' @ x)))
\<lbrakk>instance_of\<^sub>l\<^sub>s ?L\<^sub>1 ?L\<^sub>2; instance_of\<^sub>l\<^sub>s ?L\<^sub>2 ?L\<^sub>3\<rbrakk> \<Longrightarrow> instance_of\<^sub>l\<^sub>s ?L\<^sub>1 ?L\<^sub>3

goal (1 subgoal):
 1. instance_of\<^sub>l\<^sub>s Cg (C\<^sub>1 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''1'' @ x)))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
instance_of\<^sub>l\<^sub>s Cg (C\<^sub>1 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''1'' @ x)))

goal (2 subgoals):
 1. falsifies\<^sub>c G C\<^sub>1 \<Longrightarrow> falsifies\<^sub>c G (C\<^sub>1 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''1'' @ x)))
 2. falsifies\<^sub>c G (C\<^sub>1 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''1'' @ x))) \<Longrightarrow> falsifies\<^sub>c G C\<^sub>1
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
instance_of\<^sub>l\<^sub>s Cg C\<^sub>1 \<and> falsifies\<^sub>g G Cg
instance_of\<^sub>l\<^sub>s Cg (C\<^sub>1 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''1'' @ x)))
[PROOF STEP]
show "falsifies\<^sub>c G (std\<^sub>1 C\<^sub>1)"
[PROOF STATE]
proof (prove)
using this:
instance_of\<^sub>l\<^sub>s Cg C\<^sub>1 \<and> falsifies\<^sub>g G Cg
instance_of\<^sub>l\<^sub>s Cg (C\<^sub>1 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''1'' @ x)))

goal (1 subgoal):
 1. falsifies\<^sub>c G (C\<^sub>1 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''1'' @ x)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
falsifies\<^sub>c G (C\<^sub>1 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''1'' @ x)))

goal (1 subgoal):
 1. falsifies\<^sub>c G (C\<^sub>1 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''1'' @ x))) \<Longrightarrow> falsifies\<^sub>c G C\<^sub>1
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. falsifies\<^sub>c G (C\<^sub>1 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''1'' @ x))) \<Longrightarrow> falsifies\<^sub>c G C\<^sub>1
[PROOF STEP]
assume asm: "falsifies\<^sub>c G (std\<^sub>1 C\<^sub>1)"
[PROOF STATE]
proof (state)
this:
falsifies\<^sub>c G (C\<^sub>1 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''1'' @ x)))

goal (1 subgoal):
 1. falsifies\<^sub>c G (C\<^sub>1 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''1'' @ x))) \<Longrightarrow> falsifies\<^sub>c G C\<^sub>1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
falsifies\<^sub>c G (C\<^sub>1 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''1'' @ x)))
[PROOF STEP]
have inst: "instance_of\<^sub>l\<^sub>s (std\<^sub>1 C\<^sub>1) C\<^sub>1"
[PROOF STATE]
proof (prove)
using this:
falsifies\<^sub>c G (C\<^sub>1 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''1'' @ x)))

goal (1 subgoal):
 1. instance_of\<^sub>l\<^sub>s (C\<^sub>1 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''1'' @ x))) C\<^sub>1
[PROOF STEP]
unfolding instance_of\<^sub>l\<^sub>s_def
[PROOF STATE]
proof (prove)
using this:
\<exists>C'. (\<exists>\<sigma>. C' = C\<^sub>1 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''1'' @ x)) \<cdot>\<^sub>l\<^sub>s \<sigma>) \<and> falsifies\<^sub>g G C'

goal (1 subgoal):
 1. \<exists>\<sigma>. C\<^sub>1 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''1'' @ x)) = C\<^sub>1 \<cdot>\<^sub>l\<^sub>s \<sigma>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
instance_of\<^sub>l\<^sub>s (C\<^sub>1 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''1'' @ x))) C\<^sub>1

goal (1 subgoal):
 1. falsifies\<^sub>c G (C\<^sub>1 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''1'' @ x))) \<Longrightarrow> falsifies\<^sub>c G C\<^sub>1
[PROOF STEP]
from asm
[PROOF STATE]
proof (chain)
picking this:
falsifies\<^sub>c G (C\<^sub>1 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''1'' @ x)))
[PROOF STEP]
obtain Cg where "instance_of\<^sub>l\<^sub>s Cg (std\<^sub>1 C\<^sub>1)  \<and> falsifies\<^sub>g G Cg"
[PROOF STATE]
proof (prove)
using this:
falsifies\<^sub>c G (C\<^sub>1 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''1'' @ x)))

goal (1 subgoal):
 1. (\<And>Cg. instance_of\<^sub>l\<^sub>s Cg (C\<^sub>1 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''1'' @ x))) \<and> falsifies\<^sub>g G Cg \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
instance_of\<^sub>l\<^sub>s Cg (C\<^sub>1 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''1'' @ x))) \<and> falsifies\<^sub>g G Cg

goal (1 subgoal):
 1. falsifies\<^sub>c G (C\<^sub>1 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''1'' @ x))) \<Longrightarrow> falsifies\<^sub>c G C\<^sub>1
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
instance_of\<^sub>l\<^sub>s Cg (C\<^sub>1 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''1'' @ x))) \<and> falsifies\<^sub>g G Cg

goal (1 subgoal):
 1. falsifies\<^sub>c G (C\<^sub>1 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''1'' @ x))) \<Longrightarrow> falsifies\<^sub>c G C\<^sub>1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
instance_of\<^sub>l\<^sub>s Cg (C\<^sub>1 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''1'' @ x))) \<and> falsifies\<^sub>g G Cg
[PROOF STEP]
have "instance_of\<^sub>l\<^sub>s Cg C\<^sub>1"
[PROOF STATE]
proof (prove)
using this:
instance_of\<^sub>l\<^sub>s Cg (C\<^sub>1 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''1'' @ x))) \<and> falsifies\<^sub>g G Cg

goal (1 subgoal):
 1. instance_of\<^sub>l\<^sub>s Cg C\<^sub>1
[PROOF STEP]
using inst instance_of\<^sub>l\<^sub>s_trans
[PROOF STATE]
proof (prove)
using this:
instance_of\<^sub>l\<^sub>s Cg (C\<^sub>1 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''1'' @ x))) \<and> falsifies\<^sub>g G Cg
instance_of\<^sub>l\<^sub>s (C\<^sub>1 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''1'' @ x))) C\<^sub>1
\<lbrakk>instance_of\<^sub>l\<^sub>s ?L\<^sub>1 ?L\<^sub>2; instance_of\<^sub>l\<^sub>s ?L\<^sub>2 ?L\<^sub>3\<rbrakk> \<Longrightarrow> instance_of\<^sub>l\<^sub>s ?L\<^sub>1 ?L\<^sub>3

goal (1 subgoal):
 1. instance_of\<^sub>l\<^sub>s Cg C\<^sub>1
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
instance_of\<^sub>l\<^sub>s Cg C\<^sub>1

goal (1 subgoal):
 1. falsifies\<^sub>c G (C\<^sub>1 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''1'' @ x))) \<Longrightarrow> falsifies\<^sub>c G C\<^sub>1
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
instance_of\<^sub>l\<^sub>s Cg (C\<^sub>1 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''1'' @ x))) \<and> falsifies\<^sub>g G Cg
instance_of\<^sub>l\<^sub>s Cg C\<^sub>1
[PROOF STEP]
show "falsifies\<^sub>c G C\<^sub>1"
[PROOF STATE]
proof (prove)
using this:
instance_of\<^sub>l\<^sub>s Cg (C\<^sub>1 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''1'' @ x))) \<and> falsifies\<^sub>g G Cg
instance_of\<^sub>l\<^sub>s Cg C\<^sub>1

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma std\<^sub>2_falsifies: "falsifies\<^sub>c G C\<^sub>2 \<longleftrightarrow> falsifies\<^sub>c G (std\<^sub>2 C\<^sub>2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. falsifies\<^sub>c G C\<^sub>2 = falsifies\<^sub>c G (C\<^sub>2 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''2'' @ x)))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. falsifies\<^sub>c G C\<^sub>2 \<Longrightarrow> falsifies\<^sub>c G (C\<^sub>2 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''2'' @ x)))
 2. falsifies\<^sub>c G (C\<^sub>2 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''2'' @ x))) \<Longrightarrow> falsifies\<^sub>c G C\<^sub>2
[PROOF STEP]
assume asm: "falsifies\<^sub>c G C\<^sub>2"
[PROOF STATE]
proof (state)
this:
falsifies\<^sub>c G C\<^sub>2

goal (2 subgoals):
 1. falsifies\<^sub>c G C\<^sub>2 \<Longrightarrow> falsifies\<^sub>c G (C\<^sub>2 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''2'' @ x)))
 2. falsifies\<^sub>c G (C\<^sub>2 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''2'' @ x))) \<Longrightarrow> falsifies\<^sub>c G C\<^sub>2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
falsifies\<^sub>c G C\<^sub>2
[PROOF STEP]
obtain Cg where "instance_of\<^sub>l\<^sub>s Cg C\<^sub>2  \<and> falsifies\<^sub>g G Cg"
[PROOF STATE]
proof (prove)
using this:
falsifies\<^sub>c G C\<^sub>2

goal (1 subgoal):
 1. (\<And>Cg. instance_of\<^sub>l\<^sub>s Cg C\<^sub>2 \<and> falsifies\<^sub>g G Cg \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
instance_of\<^sub>l\<^sub>s Cg C\<^sub>2 \<and> falsifies\<^sub>g G Cg

goal (2 subgoals):
 1. falsifies\<^sub>c G C\<^sub>2 \<Longrightarrow> falsifies\<^sub>c G (C\<^sub>2 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''2'' @ x)))
 2. falsifies\<^sub>c G (C\<^sub>2 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''2'' @ x))) \<Longrightarrow> falsifies\<^sub>c G C\<^sub>2
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
instance_of\<^sub>l\<^sub>s Cg C\<^sub>2 \<and> falsifies\<^sub>g G Cg

goal (2 subgoals):
 1. falsifies\<^sub>c G C\<^sub>2 \<Longrightarrow> falsifies\<^sub>c G (C\<^sub>2 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''2'' @ x)))
 2. falsifies\<^sub>c G (C\<^sub>2 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''2'' @ x))) \<Longrightarrow> falsifies\<^sub>c G C\<^sub>2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
instance_of\<^sub>l\<^sub>s Cg C\<^sub>2 \<and> falsifies\<^sub>g G Cg
[PROOF STEP]
have "instance_of\<^sub>l\<^sub>s Cg (std\<^sub>2 C\<^sub>2)"
[PROOF STATE]
proof (prove)
using this:
instance_of\<^sub>l\<^sub>s Cg C\<^sub>2 \<and> falsifies\<^sub>g G Cg

goal (1 subgoal):
 1. instance_of\<^sub>l\<^sub>s Cg (C\<^sub>2 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''2'' @ x)))
[PROOF STEP]
using std_apart_instance_of\<^sub>l\<^sub>s2 instance_of\<^sub>l\<^sub>s_trans
[PROOF STATE]
proof (prove)
using this:
instance_of\<^sub>l\<^sub>s Cg C\<^sub>2 \<and> falsifies\<^sub>g G Cg
instance_of\<^sub>l\<^sub>s ?C2.0 (?C2.0 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''2'' @ x)))
\<lbrakk>instance_of\<^sub>l\<^sub>s ?L\<^sub>1 ?L\<^sub>2; instance_of\<^sub>l\<^sub>s ?L\<^sub>2 ?L\<^sub>3\<rbrakk> \<Longrightarrow> instance_of\<^sub>l\<^sub>s ?L\<^sub>1 ?L\<^sub>3

goal (1 subgoal):
 1. instance_of\<^sub>l\<^sub>s Cg (C\<^sub>2 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''2'' @ x)))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
instance_of\<^sub>l\<^sub>s Cg (C\<^sub>2 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''2'' @ x)))

goal (2 subgoals):
 1. falsifies\<^sub>c G C\<^sub>2 \<Longrightarrow> falsifies\<^sub>c G (C\<^sub>2 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''2'' @ x)))
 2. falsifies\<^sub>c G (C\<^sub>2 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''2'' @ x))) \<Longrightarrow> falsifies\<^sub>c G C\<^sub>2
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
instance_of\<^sub>l\<^sub>s Cg C\<^sub>2 \<and> falsifies\<^sub>g G Cg
instance_of\<^sub>l\<^sub>s Cg (C\<^sub>2 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''2'' @ x)))
[PROOF STEP]
show "falsifies\<^sub>c G (std\<^sub>2 C\<^sub>2)"
[PROOF STATE]
proof (prove)
using this:
instance_of\<^sub>l\<^sub>s Cg C\<^sub>2 \<and> falsifies\<^sub>g G Cg
instance_of\<^sub>l\<^sub>s Cg (C\<^sub>2 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''2'' @ x)))

goal (1 subgoal):
 1. falsifies\<^sub>c G (C\<^sub>2 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''2'' @ x)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
falsifies\<^sub>c G (C\<^sub>2 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''2'' @ x)))

goal (1 subgoal):
 1. falsifies\<^sub>c G (C\<^sub>2 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''2'' @ x))) \<Longrightarrow> falsifies\<^sub>c G C\<^sub>2
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. falsifies\<^sub>c G (C\<^sub>2 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''2'' @ x))) \<Longrightarrow> falsifies\<^sub>c G C\<^sub>2
[PROOF STEP]
assume asm: "falsifies\<^sub>c G (std\<^sub>2 C\<^sub>2)"
[PROOF STATE]
proof (state)
this:
falsifies\<^sub>c G (C\<^sub>2 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''2'' @ x)))

goal (1 subgoal):
 1. falsifies\<^sub>c G (C\<^sub>2 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''2'' @ x))) \<Longrightarrow> falsifies\<^sub>c G C\<^sub>2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
falsifies\<^sub>c G (C\<^sub>2 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''2'' @ x)))
[PROOF STEP]
have inst: "instance_of\<^sub>l\<^sub>s (std\<^sub>2 C\<^sub>2) C\<^sub>2"
[PROOF STATE]
proof (prove)
using this:
falsifies\<^sub>c G (C\<^sub>2 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''2'' @ x)))

goal (1 subgoal):
 1. instance_of\<^sub>l\<^sub>s (C\<^sub>2 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''2'' @ x))) C\<^sub>2
[PROOF STEP]
unfolding instance_of\<^sub>l\<^sub>s_def
[PROOF STATE]
proof (prove)
using this:
\<exists>C'. (\<exists>\<sigma>. C' = C\<^sub>2 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''2'' @ x)) \<cdot>\<^sub>l\<^sub>s \<sigma>) \<and> falsifies\<^sub>g G C'

goal (1 subgoal):
 1. \<exists>\<sigma>. C\<^sub>2 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''2'' @ x)) = C\<^sub>2 \<cdot>\<^sub>l\<^sub>s \<sigma>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
instance_of\<^sub>l\<^sub>s (C\<^sub>2 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''2'' @ x))) C\<^sub>2

goal (1 subgoal):
 1. falsifies\<^sub>c G (C\<^sub>2 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''2'' @ x))) \<Longrightarrow> falsifies\<^sub>c G C\<^sub>2
[PROOF STEP]
from asm
[PROOF STATE]
proof (chain)
picking this:
falsifies\<^sub>c G (C\<^sub>2 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''2'' @ x)))
[PROOF STEP]
obtain Cg where "instance_of\<^sub>l\<^sub>s Cg (std\<^sub>2 C\<^sub>2)  \<and> falsifies\<^sub>g G Cg"
[PROOF STATE]
proof (prove)
using this:
falsifies\<^sub>c G (C\<^sub>2 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''2'' @ x)))

goal (1 subgoal):
 1. (\<And>Cg. instance_of\<^sub>l\<^sub>s Cg (C\<^sub>2 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''2'' @ x))) \<and> falsifies\<^sub>g G Cg \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
instance_of\<^sub>l\<^sub>s Cg (C\<^sub>2 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''2'' @ x))) \<and> falsifies\<^sub>g G Cg

goal (1 subgoal):
 1. falsifies\<^sub>c G (C\<^sub>2 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''2'' @ x))) \<Longrightarrow> falsifies\<^sub>c G C\<^sub>2
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
instance_of\<^sub>l\<^sub>s Cg (C\<^sub>2 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''2'' @ x))) \<and> falsifies\<^sub>g G Cg

goal (1 subgoal):
 1. falsifies\<^sub>c G (C\<^sub>2 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''2'' @ x))) \<Longrightarrow> falsifies\<^sub>c G C\<^sub>2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
instance_of\<^sub>l\<^sub>s Cg (C\<^sub>2 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''2'' @ x))) \<and> falsifies\<^sub>g G Cg
[PROOF STEP]
have "instance_of\<^sub>l\<^sub>s Cg C\<^sub>2"
[PROOF STATE]
proof (prove)
using this:
instance_of\<^sub>l\<^sub>s Cg (C\<^sub>2 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''2'' @ x))) \<and> falsifies\<^sub>g G Cg

goal (1 subgoal):
 1. instance_of\<^sub>l\<^sub>s Cg C\<^sub>2
[PROOF STEP]
using inst instance_of\<^sub>l\<^sub>s_trans
[PROOF STATE]
proof (prove)
using this:
instance_of\<^sub>l\<^sub>s Cg (C\<^sub>2 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''2'' @ x))) \<and> falsifies\<^sub>g G Cg
instance_of\<^sub>l\<^sub>s (C\<^sub>2 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''2'' @ x))) C\<^sub>2
\<lbrakk>instance_of\<^sub>l\<^sub>s ?L\<^sub>1 ?L\<^sub>2; instance_of\<^sub>l\<^sub>s ?L\<^sub>2 ?L\<^sub>3\<rbrakk> \<Longrightarrow> instance_of\<^sub>l\<^sub>s ?L\<^sub>1 ?L\<^sub>3

goal (1 subgoal):
 1. instance_of\<^sub>l\<^sub>s Cg C\<^sub>2
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
instance_of\<^sub>l\<^sub>s Cg C\<^sub>2

goal (1 subgoal):
 1. falsifies\<^sub>c G (C\<^sub>2 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''2'' @ x))) \<Longrightarrow> falsifies\<^sub>c G C\<^sub>2
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
instance_of\<^sub>l\<^sub>s Cg (C\<^sub>2 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''2'' @ x))) \<and> falsifies\<^sub>g G Cg
instance_of\<^sub>l\<^sub>s Cg C\<^sub>2
[PROOF STEP]
show "falsifies\<^sub>c G C\<^sub>2"
[PROOF STATE]
proof (prove)
using this:
instance_of\<^sub>l\<^sub>s Cg (C\<^sub>2 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''2'' @ x))) \<and> falsifies\<^sub>g G Cg
instance_of\<^sub>l\<^sub>s Cg C\<^sub>2

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma std\<^sub>1_renames: "var_renaming_of C\<^sub>1 (std\<^sub>1 C\<^sub>1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. var_renaming_of C\<^sub>1 (C\<^sub>1 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''1'' @ x)))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. var_renaming_of C\<^sub>1 (C\<^sub>1 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''1'' @ x)))
[PROOF STEP]
have "instance_of\<^sub>l\<^sub>s C\<^sub>1 (std\<^sub>1 C\<^sub>1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. instance_of\<^sub>l\<^sub>s C\<^sub>1 (C\<^sub>1 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''1'' @ x)))
[PROOF STEP]
using std_apart_instance_of\<^sub>l\<^sub>s1
[PROOF STATE]
proof (prove)
using this:
instance_of\<^sub>l\<^sub>s ?C\<^sub>1 (?C\<^sub>1 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''1'' @ x)))

goal (1 subgoal):
 1. instance_of\<^sub>l\<^sub>s C\<^sub>1 (C\<^sub>1 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''1'' @ x)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
instance_of\<^sub>l\<^sub>s C\<^sub>1 (C\<^sub>1 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''1'' @ x)))

goal (1 subgoal):
 1. var_renaming_of C\<^sub>1 (C\<^sub>1 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''1'' @ x)))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
instance_of\<^sub>l\<^sub>s C\<^sub>1 (C\<^sub>1 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''1'' @ x)))

goal (1 subgoal):
 1. var_renaming_of C\<^sub>1 (C\<^sub>1 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''1'' @ x)))
[PROOF STEP]
have "instance_of\<^sub>l\<^sub>s (std\<^sub>1 C\<^sub>1) C\<^sub>1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. instance_of\<^sub>l\<^sub>s (C\<^sub>1 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''1'' @ x))) C\<^sub>1
[PROOF STEP]
unfolding instance_of\<^sub>l\<^sub>s_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>\<sigma>. C\<^sub>1 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''1'' @ x)) = C\<^sub>1 \<cdot>\<^sub>l\<^sub>s \<sigma>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
instance_of\<^sub>l\<^sub>s (C\<^sub>1 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''1'' @ x))) C\<^sub>1

goal (1 subgoal):
 1. var_renaming_of C\<^sub>1 (C\<^sub>1 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''1'' @ x)))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
instance_of\<^sub>l\<^sub>s C\<^sub>1 (C\<^sub>1 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''1'' @ x)))
instance_of\<^sub>l\<^sub>s (C\<^sub>1 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''1'' @ x))) C\<^sub>1
[PROOF STEP]
show "var_renaming_of C\<^sub>1 (std\<^sub>1 C\<^sub>1)"
[PROOF STATE]
proof (prove)
using this:
instance_of\<^sub>l\<^sub>s C\<^sub>1 (C\<^sub>1 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''1'' @ x)))
instance_of\<^sub>l\<^sub>s (C\<^sub>1 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''1'' @ x))) C\<^sub>1

goal (1 subgoal):
 1. var_renaming_of C\<^sub>1 (C\<^sub>1 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''1'' @ x)))
[PROOF STEP]
unfolding var_renaming_of_def
[PROOF STATE]
proof (prove)
using this:
instance_of\<^sub>l\<^sub>s C\<^sub>1 (C\<^sub>1 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''1'' @ x)))
instance_of\<^sub>l\<^sub>s (C\<^sub>1 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''1'' @ x))) C\<^sub>1

goal (1 subgoal):
 1. instance_of\<^sub>l\<^sub>s C\<^sub>1 (C\<^sub>1 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''1'' @ x))) \<and> instance_of\<^sub>l\<^sub>s (C\<^sub>1 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''1'' @ x))) C\<^sub>1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
var_renaming_of C\<^sub>1 (C\<^sub>1 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''1'' @ x)))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma std\<^sub>2_renames: "var_renaming_of C\<^sub>2 (std\<^sub>2 C\<^sub>2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. var_renaming_of C\<^sub>2 (C\<^sub>2 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''2'' @ x)))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. var_renaming_of C\<^sub>2 (C\<^sub>2 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''2'' @ x)))
[PROOF STEP]
have "instance_of\<^sub>l\<^sub>s C\<^sub>2 (std\<^sub>2 C\<^sub>2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. instance_of\<^sub>l\<^sub>s C\<^sub>2 (C\<^sub>2 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''2'' @ x)))
[PROOF STEP]
using std_apart_instance_of\<^sub>l\<^sub>s2
[PROOF STATE]
proof (prove)
using this:
instance_of\<^sub>l\<^sub>s ?C2.0 (?C2.0 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''2'' @ x)))

goal (1 subgoal):
 1. instance_of\<^sub>l\<^sub>s C\<^sub>2 (C\<^sub>2 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''2'' @ x)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
instance_of\<^sub>l\<^sub>s C\<^sub>2 (C\<^sub>2 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''2'' @ x)))

goal (1 subgoal):
 1. var_renaming_of C\<^sub>2 (C\<^sub>2 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''2'' @ x)))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
instance_of\<^sub>l\<^sub>s C\<^sub>2 (C\<^sub>2 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''2'' @ x)))

goal (1 subgoal):
 1. var_renaming_of C\<^sub>2 (C\<^sub>2 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''2'' @ x)))
[PROOF STEP]
have "instance_of\<^sub>l\<^sub>s (std\<^sub>2 C\<^sub>2) C\<^sub>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. instance_of\<^sub>l\<^sub>s (C\<^sub>2 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''2'' @ x))) C\<^sub>2
[PROOF STEP]
unfolding instance_of\<^sub>l\<^sub>s_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>\<sigma>. C\<^sub>2 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''2'' @ x)) = C\<^sub>2 \<cdot>\<^sub>l\<^sub>s \<sigma>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
instance_of\<^sub>l\<^sub>s (C\<^sub>2 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''2'' @ x))) C\<^sub>2

goal (1 subgoal):
 1. var_renaming_of C\<^sub>2 (C\<^sub>2 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''2'' @ x)))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
instance_of\<^sub>l\<^sub>s C\<^sub>2 (C\<^sub>2 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''2'' @ x)))
instance_of\<^sub>l\<^sub>s (C\<^sub>2 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''2'' @ x))) C\<^sub>2
[PROOF STEP]
show "var_renaming_of C\<^sub>2 (std\<^sub>2 C\<^sub>2)"
[PROOF STATE]
proof (prove)
using this:
instance_of\<^sub>l\<^sub>s C\<^sub>2 (C\<^sub>2 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''2'' @ x)))
instance_of\<^sub>l\<^sub>s (C\<^sub>2 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''2'' @ x))) C\<^sub>2

goal (1 subgoal):
 1. var_renaming_of C\<^sub>2 (C\<^sub>2 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''2'' @ x)))
[PROOF STEP]
unfolding var_renaming_of_def
[PROOF STATE]
proof (prove)
using this:
instance_of\<^sub>l\<^sub>s C\<^sub>2 (C\<^sub>2 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''2'' @ x)))
instance_of\<^sub>l\<^sub>s (C\<^sub>2 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''2'' @ x))) C\<^sub>2

goal (1 subgoal):
 1. instance_of\<^sub>l\<^sub>s C\<^sub>2 (C\<^sub>2 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''2'' @ x))) \<and> instance_of\<^sub>l\<^sub>s (C\<^sub>2 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''2'' @ x))) C\<^sub>2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
var_renaming_of C\<^sub>2 (C\<^sub>2 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''2'' @ x)))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma maximum:
  assumes asm: "finite C"
  shows "\<exists>n :: nat. \<forall>l \<in> C. f l \<le> n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>n. \<forall>l\<in>C. f l \<le> n
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>l\<in>C. f l \<le> ?n
[PROOF STEP]
from asm
[PROOF STATE]
proof (chain)
picking this:
finite C
[PROOF STEP]
show "\<forall>l\<in>C. f l \<le> (Max (f ` C))"
[PROOF STATE]
proof (prove)
using this:
finite C

goal (1 subgoal):
 1. \<forall>l\<in>C. f l \<le> Max (f ` C)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>l\<in>C. f l \<le> Max (f ` C)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma extend_preserves_model: (* only for ground *)
  assumes f_infpath: "wf_infpath (f :: nat \<Rightarrow> partial_pred_denot)"
  assumes C_ground: "ground\<^sub>l\<^sub>s C"
  assumes C_sat: "\<not>falsifies\<^sub>c (f (Suc n)) C"
  assumes n_max: "\<forall>l\<in>C. nat_of_fatom (get_atom l) \<le> n"
  shows "eval\<^sub>c HFun (extend f) C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval\<^sub>c HFun (extend f) C
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. eval\<^sub>c HFun (extend f) C
[PROOF STEP]
let ?F = "HFun"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. eval\<^sub>c HFun (extend f) C
[PROOF STEP]
let ?G = "extend f"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. eval\<^sub>c HFun (extend f) C
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. eval\<^sub>c HFun (extend f) C
[PROOF STEP]
fix E
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. eval\<^sub>c HFun (extend f) C
[PROOF STEP]
from C_sat
[PROOF STATE]
proof (chain)
picking this:
\<not> falsifies\<^sub>c (f (Suc n)) C
[PROOF STEP]
have "\<forall>C'. (\<not>instance_of\<^sub>l\<^sub>s C' C \<or> \<not>falsifies\<^sub>g (f (Suc n)) C')"
[PROOF STATE]
proof (prove)
using this:
\<not> falsifies\<^sub>c (f (Suc n)) C

goal (1 subgoal):
 1. \<forall>C'. \<not> instance_of\<^sub>l\<^sub>s C' C \<or> \<not> falsifies\<^sub>g (f (Suc n)) C'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>C'. \<not> instance_of\<^sub>l\<^sub>s C' C \<or> \<not> falsifies\<^sub>g (f (Suc n)) C'

goal (1 subgoal):
 1. eval\<^sub>c HFun (extend f) C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>C'. \<not> instance_of\<^sub>l\<^sub>s C' C \<or> \<not> falsifies\<^sub>g (f (Suc n)) C'
[PROOF STEP]
have "\<not>falsifies\<^sub>g (f (Suc n)) C"
[PROOF STATE]
proof (prove)
using this:
\<forall>C'. \<not> instance_of\<^sub>l\<^sub>s C' C \<or> \<not> falsifies\<^sub>g (f (Suc n)) C'

goal (1 subgoal):
 1. \<not> falsifies\<^sub>g (f (Suc n)) C
[PROOF STEP]
using instance_of\<^sub>l\<^sub>s_self
[PROOF STATE]
proof (prove)
using this:
\<forall>C'. \<not> instance_of\<^sub>l\<^sub>s C' C \<or> \<not> falsifies\<^sub>g (f (Suc n)) C'
instance_of\<^sub>l\<^sub>s ?L ?L

goal (1 subgoal):
 1. \<not> falsifies\<^sub>g (f (Suc n)) C
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<not> falsifies\<^sub>g (f (Suc n)) C

goal (1 subgoal):
 1. eval\<^sub>c HFun (extend f) C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> falsifies\<^sub>g (f (Suc n)) C
[PROOF STEP]
obtain l where l_p: "l\<in>C \<and> \<not>falsifies\<^sub>l (f (Suc n)) l"
[PROOF STATE]
proof (prove)
using this:
\<not> falsifies\<^sub>g (f (Suc n)) C

goal (1 subgoal):
 1. (\<And>l. l \<in> C \<and> \<not> falsifies\<^sub>l (f (Suc n)) l \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using C_ground
[PROOF STATE]
proof (prove)
using this:
\<not> falsifies\<^sub>g (f (Suc n)) C
ground\<^sub>l\<^sub>s C

goal (1 subgoal):
 1. (\<And>l. l \<in> C \<and> \<not> falsifies\<^sub>l (f (Suc n)) l \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
l \<in> C \<and> \<not> falsifies\<^sub>l (f (Suc n)) l

goal (1 subgoal):
 1. eval\<^sub>c HFun (extend f) C
[PROOF STEP]
let ?i = "nat_of_fatom (get_atom l)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. eval\<^sub>c HFun (extend f) C
[PROOF STEP]
from l_p
[PROOF STATE]
proof (chain)
picking this:
l \<in> C \<and> \<not> falsifies\<^sub>l (f (Suc n)) l
[PROOF STEP]
have i_n: "?i \<le> n"
[PROOF STATE]
proof (prove)
using this:
l \<in> C \<and> \<not> falsifies\<^sub>l (f (Suc n)) l

goal (1 subgoal):
 1. nat_of_fatom (get_atom l) \<le> n
[PROOF STEP]
using n_max
[PROOF STATE]
proof (prove)
using this:
l \<in> C \<and> \<not> falsifies\<^sub>l (f (Suc n)) l
\<forall>l\<in>C. nat_of_fatom (get_atom l) \<le> n

goal (1 subgoal):
 1. nat_of_fatom (get_atom l) \<le> n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nat_of_fatom (get_atom l) \<le> n

goal (1 subgoal):
 1. eval\<^sub>c HFun (extend f) C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
nat_of_fatom (get_atom l) \<le> n
[PROOF STEP]
have j_n: "?i < length (f (Suc n))"
[PROOF STATE]
proof (prove)
using this:
nat_of_fatom (get_atom l) \<le> n

goal (1 subgoal):
 1. nat_of_fatom (get_atom l) < length (f (Suc n))
[PROOF STEP]
using f_infpath infpath_length[of f]
[PROOF STATE]
proof (prove)
using this:
nat_of_fatom (get_atom l) \<le> n
wf_infpath f
wf_infpath f \<Longrightarrow> length (f ?n) = ?n

goal (1 subgoal):
 1. nat_of_fatom (get_atom l) < length (f (Suc n))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nat_of_fatom (get_atom l) < length (f (Suc n))

goal (1 subgoal):
 1. eval\<^sub>c HFun (extend f) C
[PROOF STEP]
have "eval\<^sub>l E HFun (extend f) l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval\<^sub>l E HFun (extend f) l
[PROOF STEP]
proof (cases l)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x11 x12. l = Pos x11 x12 \<Longrightarrow> eval\<^sub>l E HFun (extend f) l
 2. \<And>x21 x22. l = Neg x21 x22 \<Longrightarrow> eval\<^sub>l E HFun (extend f) l
[PROOF STEP]
case (Pos P ts)
[PROOF STATE]
proof (state)
this:
l = Pos P ts

goal (2 subgoals):
 1. \<And>x11 x12. l = Pos x11 x12 \<Longrightarrow> eval\<^sub>l E HFun (extend f) l
 2. \<And>x21 x22. l = Neg x21 x22 \<Longrightarrow> eval\<^sub>l E HFun (extend f) l
[PROOF STEP]
from Pos l_p C_ground
[PROOF STATE]
proof (chain)
picking this:
l = Pos P ts
l \<in> C \<and> \<not> falsifies\<^sub>l (f (Suc n)) l
ground\<^sub>l\<^sub>s C
[PROOF STEP]
have ts_ground: "ground\<^sub>t\<^sub>s ts"
[PROOF STATE]
proof (prove)
using this:
l = Pos P ts
l \<in> C \<and> \<not> falsifies\<^sub>l (f (Suc n)) l
ground\<^sub>l\<^sub>s C

goal (1 subgoal):
 1. ground\<^sub>t\<^sub>s ts
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ground\<^sub>t\<^sub>s ts

goal (2 subgoals):
 1. \<And>x11 x12. l = Pos x11 x12 \<Longrightarrow> eval\<^sub>l E HFun (extend f) l
 2. \<And>x21 x22. l = Neg x21 x22 \<Longrightarrow> eval\<^sub>l E HFun (extend f) l
[PROOF STEP]
have "\<not>falsifies\<^sub>l (f (Suc n)) l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> falsifies\<^sub>l (f (Suc n)) l
[PROOF STEP]
using l_p
[PROOF STATE]
proof (prove)
using this:
l \<in> C \<and> \<not> falsifies\<^sub>l (f (Suc n)) l

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

goal (2 subgoals):
 1. \<And>x11 x12. l = Pos x11 x12 \<Longrightarrow> eval\<^sub>l E HFun (extend f) l
 2. \<And>x21 x22. l = Neg x21 x22 \<Longrightarrow> eval\<^sub>l E HFun (extend f) l
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> falsifies\<^sub>l (f (Suc n)) l
[PROOF STEP]
have "f (Suc n) ! ?i = True"
[PROOF STATE]
proof (prove)
using this:
\<not> falsifies\<^sub>l (f (Suc n)) l

goal (1 subgoal):
 1. f (Suc n) ! nat_of_fatom (get_atom l) = True
[PROOF STEP]
using j_n Pos ts_ground empty_subts[of ts]
[PROOF STATE]
proof (prove)
using this:
\<not> falsifies\<^sub>l (f (Suc n)) l
nat_of_fatom (get_atom l) < length (f (Suc n))
l = Pos P ts
ground\<^sub>t\<^sub>s ts
ts \<cdot>\<^sub>t\<^sub>s \<epsilon> = ts

goal (1 subgoal):
 1. f (Suc n) ! nat_of_fatom (get_atom l) = True
[PROOF STEP]
unfolding falsifies\<^sub>l_def
[PROOF STATE]
proof (prove)
using this:
\<not> (ground\<^sub>l l \<and> (let i = nat_of_fatom (get_atom l) in i < length (f (Suc n)) \<and> f (Suc n) ! i = (\<not> sign l)))
nat_of_fatom (get_atom l) < length (f (Suc n))
l = Pos P ts
ground\<^sub>t\<^sub>s ts
ts \<cdot>\<^sub>t\<^sub>s \<epsilon> = ts

goal (1 subgoal):
 1. f (Suc n) ! nat_of_fatom (get_atom l) = True
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f (Suc n) ! nat_of_fatom (get_atom l) = True

goal (2 subgoals):
 1. \<And>x11 x12. l = Pos x11 x12 \<Longrightarrow> eval\<^sub>l E HFun (extend f) l
 2. \<And>x21 x22. l = Neg x21 x22 \<Longrightarrow> eval\<^sub>l E HFun (extend f) l
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
f (Suc n) ! nat_of_fatom (get_atom l) = True

goal (2 subgoals):
 1. \<And>x11 x12. l = Pos x11 x12 \<Longrightarrow> eval\<^sub>l E HFun (extend f) l
 2. \<And>x21 x22. l = Neg x21 x22 \<Longrightarrow> eval\<^sub>l E HFun (extend f) l
[PROOF STEP]
have "f (Suc ?i) ! ?i = f (Suc n) ! ?i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f (Suc (nat_of_fatom (get_atom l))) ! nat_of_fatom (get_atom l) = f (Suc n) ! nat_of_fatom (get_atom l)
[PROOF STEP]
using f_infpath i_n j_n infpath_length[of f] ith_in_extension[of f]
[PROOF STATE]
proof (prove)
using this:
wf_infpath f
nat_of_fatom (get_atom l) \<le> n
nat_of_fatom (get_atom l) < length (f (Suc n))
wf_infpath f \<Longrightarrow> length (f ?n) = ?n
\<lbrakk>wf_infpath f; ?i < length (f ?n\<^sub>1); ?n\<^sub>1 \<le> ?n\<^sub>2\<rbrakk> \<Longrightarrow> f ?n\<^sub>1 ! ?i = f ?n\<^sub>2 ! ?i

goal (1 subgoal):
 1. f (Suc (nat_of_fatom (get_atom l))) ! nat_of_fatom (get_atom l) = f (Suc n) ! nat_of_fatom (get_atom l)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
f (Suc (nat_of_fatom (get_atom l))) ! nat_of_fatom (get_atom l) = f (Suc n) ! nat_of_fatom (get_atom l)

goal (2 subgoals):
 1. \<And>x11 x12. l = Pos x11 x12 \<Longrightarrow> eval\<^sub>l E HFun (extend f) l
 2. \<And>x21 x22. l = Neg x21 x22 \<Longrightarrow> eval\<^sub>l E HFun (extend f) l
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
f (Suc n) ! nat_of_fatom (get_atom l) = True
f (Suc (nat_of_fatom (get_atom l))) ! nat_of_fatom (get_atom l) = f (Suc n) ! nat_of_fatom (get_atom l)
[PROOF STEP]
have "f (Suc ?i) ! ?i = True"
[PROOF STATE]
proof (prove)
using this:
f (Suc n) ! nat_of_fatom (get_atom l) = True
f (Suc (nat_of_fatom (get_atom l))) ! nat_of_fatom (get_atom l) = f (Suc n) ! nat_of_fatom (get_atom l)

goal (1 subgoal):
 1. f (Suc (nat_of_fatom (get_atom l))) ! nat_of_fatom (get_atom l) = True
[PROOF STEP]
using Pos
[PROOF STATE]
proof (prove)
using this:
f (Suc n) ! nat_of_fatom (get_atom l) = True
f (Suc (nat_of_fatom (get_atom l))) ! nat_of_fatom (get_atom l) = f (Suc n) ! nat_of_fatom (get_atom l)
l = Pos P ts

goal (1 subgoal):
 1. f (Suc (nat_of_fatom (get_atom l))) ! nat_of_fatom (get_atom l) = True
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f (Suc (nat_of_fatom (get_atom l))) ! nat_of_fatom (get_atom l) = True

goal (2 subgoals):
 1. \<And>x11 x12. l = Pos x11 x12 \<Longrightarrow> eval\<^sub>l E HFun (extend f) l
 2. \<And>x21 x22. l = Neg x21 x22 \<Longrightarrow> eval\<^sub>l E HFun (extend f) l
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
f (Suc (nat_of_fatom (get_atom l))) ! nat_of_fatom (get_atom l) = True
[PROOF STEP]
have "?G P (hterms_of_fterms ts)"
[PROOF STATE]
proof (prove)
using this:
f (Suc (nat_of_fatom (get_atom l))) ! nat_of_fatom (get_atom l) = True

goal (1 subgoal):
 1. extend f P (hterms_of_fterms ts)
[PROOF STEP]
using Pos
[PROOF STATE]
proof (prove)
using this:
f (Suc (nat_of_fatom (get_atom l))) ! nat_of_fatom (get_atom l) = True
l = Pos P ts

goal (1 subgoal):
 1. extend f P (hterms_of_fterms ts)
[PROOF STEP]
by (simp add: nat_of_fatom_def)
[PROOF STATE]
proof (state)
this:
extend f P (hterms_of_fterms ts)

goal (2 subgoals):
 1. \<And>x11 x12. l = Pos x11 x12 \<Longrightarrow> eval\<^sub>l E HFun (extend f) l
 2. \<And>x21 x22. l = Neg x21 x22 \<Longrightarrow> eval\<^sub>l E HFun (extend f) l
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
extend f P (hterms_of_fterms ts)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
extend f P (hterms_of_fterms ts)

goal (1 subgoal):
 1. eval\<^sub>l E HFun (extend f) l
[PROOF STEP]
using eval\<^sub>l_ground\<^sub>t\<^sub>s[of ts _ ?G P] ts_ground Pos
[PROOF STATE]
proof (prove)
using this:
extend f P (hterms_of_fterms ts)
ground\<^sub>t\<^sub>s ts \<Longrightarrow> eval\<^sub>l ?E HFun (extend f) (Pos P ts) = extend f P (hterms_of_fterms ts)
ground\<^sub>t\<^sub>s ts
l = Pos P ts

goal (1 subgoal):
 1. eval\<^sub>l E HFun (extend f) l
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
eval\<^sub>l E HFun (extend f) l

goal (1 subgoal):
 1. \<And>x21 x22. l = Neg x21 x22 \<Longrightarrow> eval\<^sub>l E HFun (extend f) l
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x21 x22. l = Neg x21 x22 \<Longrightarrow> eval\<^sub>l E HFun (extend f) l
[PROOF STEP]
case (Neg P ts)
[PROOF STATE]
proof (state)
this:
l = Neg P ts

goal (1 subgoal):
 1. \<And>x21 x22. l = Neg x21 x22 \<Longrightarrow> eval\<^sub>l E HFun (extend f) l
[PROOF STEP]
(* Symmetric *)
[PROOF STATE]
proof (state)
this:
l = Neg P ts

goal (1 subgoal):
 1. \<And>x21 x22. l = Neg x21 x22 \<Longrightarrow> eval\<^sub>l E HFun (extend f) l
[PROOF STEP]
from Neg l_p C_ground
[PROOF STATE]
proof (chain)
picking this:
l = Neg P ts
l \<in> C \<and> \<not> falsifies\<^sub>l (f (Suc n)) l
ground\<^sub>l\<^sub>s C
[PROOF STEP]
have ts_ground: "ground\<^sub>t\<^sub>s ts"
[PROOF STATE]
proof (prove)
using this:
l = Neg P ts
l \<in> C \<and> \<not> falsifies\<^sub>l (f (Suc n)) l
ground\<^sub>l\<^sub>s C

goal (1 subgoal):
 1. ground\<^sub>t\<^sub>s ts
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ground\<^sub>t\<^sub>s ts

goal (1 subgoal):
 1. \<And>x21 x22. l = Neg x21 x22 \<Longrightarrow> eval\<^sub>l E HFun (extend f) l
[PROOF STEP]
have "\<not>falsifies\<^sub>l (f (Suc n)) l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> falsifies\<^sub>l (f (Suc n)) l
[PROOF STEP]
using l_p
[PROOF STATE]
proof (prove)
using this:
l \<in> C \<and> \<not> falsifies\<^sub>l (f (Suc n)) l

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

goal (1 subgoal):
 1. \<And>x21 x22. l = Neg x21 x22 \<Longrightarrow> eval\<^sub>l E HFun (extend f) l
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> falsifies\<^sub>l (f (Suc n)) l
[PROOF STEP]
have "f (Suc n) ! ?i = False"
[PROOF STATE]
proof (prove)
using this:
\<not> falsifies\<^sub>l (f (Suc n)) l

goal (1 subgoal):
 1. f (Suc n) ! nat_of_fatom (get_atom l) = False
[PROOF STEP]
using j_n Neg ts_ground empty_subts[of ts]
[PROOF STATE]
proof (prove)
using this:
\<not> falsifies\<^sub>l (f (Suc n)) l
nat_of_fatom (get_atom l) < length (f (Suc n))
l = Neg P ts
ground\<^sub>t\<^sub>s ts
ts \<cdot>\<^sub>t\<^sub>s \<epsilon> = ts

goal (1 subgoal):
 1. f (Suc n) ! nat_of_fatom (get_atom l) = False
[PROOF STEP]
unfolding falsifies\<^sub>l_def
[PROOF STATE]
proof (prove)
using this:
\<not> (ground\<^sub>l l \<and> (let i = nat_of_fatom (get_atom l) in i < length (f (Suc n)) \<and> f (Suc n) ! i = (\<not> sign l)))
nat_of_fatom (get_atom l) < length (f (Suc n))
l = Neg P ts
ground\<^sub>t\<^sub>s ts
ts \<cdot>\<^sub>t\<^sub>s \<epsilon> = ts

goal (1 subgoal):
 1. f (Suc n) ! nat_of_fatom (get_atom l) = False
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f (Suc n) ! nat_of_fatom (get_atom l) = False

goal (1 subgoal):
 1. \<And>x21 x22. l = Neg x21 x22 \<Longrightarrow> eval\<^sub>l E HFun (extend f) l
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
f (Suc n) ! nat_of_fatom (get_atom l) = False

goal (1 subgoal):
 1. \<And>x21 x22. l = Neg x21 x22 \<Longrightarrow> eval\<^sub>l E HFun (extend f) l
[PROOF STEP]
have "f (Suc ?i) ! ?i = f (Suc n) ! ?i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f (Suc (nat_of_fatom (get_atom l))) ! nat_of_fatom (get_atom l) = f (Suc n) ! nat_of_fatom (get_atom l)
[PROOF STEP]
using f_infpath i_n j_n infpath_length[of f] ith_in_extension[of f]
[PROOF STATE]
proof (prove)
using this:
wf_infpath f
nat_of_fatom (get_atom l) \<le> n
nat_of_fatom (get_atom l) < length (f (Suc n))
wf_infpath f \<Longrightarrow> length (f ?n) = ?n
\<lbrakk>wf_infpath f; ?i < length (f ?n\<^sub>1); ?n\<^sub>1 \<le> ?n\<^sub>2\<rbrakk> \<Longrightarrow> f ?n\<^sub>1 ! ?i = f ?n\<^sub>2 ! ?i

goal (1 subgoal):
 1. f (Suc (nat_of_fatom (get_atom l))) ! nat_of_fatom (get_atom l) = f (Suc n) ! nat_of_fatom (get_atom l)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
f (Suc (nat_of_fatom (get_atom l))) ! nat_of_fatom (get_atom l) = f (Suc n) ! nat_of_fatom (get_atom l)

goal (1 subgoal):
 1. \<And>x21 x22. l = Neg x21 x22 \<Longrightarrow> eval\<^sub>l E HFun (extend f) l
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
f (Suc n) ! nat_of_fatom (get_atom l) = False
f (Suc (nat_of_fatom (get_atom l))) ! nat_of_fatom (get_atom l) = f (Suc n) ! nat_of_fatom (get_atom l)
[PROOF STEP]
have "f (Suc ?i) ! ?i = False"
[PROOF STATE]
proof (prove)
using this:
f (Suc n) ! nat_of_fatom (get_atom l) = False
f (Suc (nat_of_fatom (get_atom l))) ! nat_of_fatom (get_atom l) = f (Suc n) ! nat_of_fatom (get_atom l)

goal (1 subgoal):
 1. f (Suc (nat_of_fatom (get_atom l))) ! nat_of_fatom (get_atom l) = False
[PROOF STEP]
using Neg
[PROOF STATE]
proof (prove)
using this:
f (Suc n) ! nat_of_fatom (get_atom l) = False
f (Suc (nat_of_fatom (get_atom l))) ! nat_of_fatom (get_atom l) = f (Suc n) ! nat_of_fatom (get_atom l)
l = Neg P ts

goal (1 subgoal):
 1. f (Suc (nat_of_fatom (get_atom l))) ! nat_of_fatom (get_atom l) = False
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f (Suc (nat_of_fatom (get_atom l))) ! nat_of_fatom (get_atom l) = False

goal (1 subgoal):
 1. \<And>x21 x22. l = Neg x21 x22 \<Longrightarrow> eval\<^sub>l E HFun (extend f) l
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
f (Suc (nat_of_fatom (get_atom l))) ! nat_of_fatom (get_atom l) = False
[PROOF STEP]
have "\<not>?G P (hterms_of_fterms ts)"
[PROOF STATE]
proof (prove)
using this:
f (Suc (nat_of_fatom (get_atom l))) ! nat_of_fatom (get_atom l) = False

goal (1 subgoal):
 1. \<not> extend f P (hterms_of_fterms ts)
[PROOF STEP]
using Neg
[PROOF STATE]
proof (prove)
using this:
f (Suc (nat_of_fatom (get_atom l))) ! nat_of_fatom (get_atom l) = False
l = Neg P ts

goal (1 subgoal):
 1. \<not> extend f P (hterms_of_fterms ts)
[PROOF STEP]
by (simp add: nat_of_fatom_def)
[PROOF STATE]
proof (state)
this:
\<not> extend f P (hterms_of_fterms ts)

goal (1 subgoal):
 1. \<And>x21 x22. l = Neg x21 x22 \<Longrightarrow> eval\<^sub>l E HFun (extend f) l
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> extend f P (hterms_of_fterms ts)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> extend f P (hterms_of_fterms ts)

goal (1 subgoal):
 1. eval\<^sub>l E HFun (extend f) l
[PROOF STEP]
using Neg eval\<^sub>l_ground\<^sub>t\<^sub>s[of ts _ ?G P] ts_ground
[PROOF STATE]
proof (prove)
using this:
\<not> extend f P (hterms_of_fterms ts)
l = Neg P ts
ground\<^sub>t\<^sub>s ts \<Longrightarrow> eval\<^sub>l ?E HFun (extend f) (Pos P ts) = extend f P (hterms_of_fterms ts)
ground\<^sub>t\<^sub>s ts

goal (1 subgoal):
 1. eval\<^sub>l E HFun (extend f) l
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
eval\<^sub>l E HFun (extend f) l

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
eval\<^sub>l E HFun (extend f) l

goal (1 subgoal):
 1. eval\<^sub>c HFun (extend f) C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
eval\<^sub>l E HFun (extend f) l
[PROOF STEP]
have "\<exists>l \<in> C. eval\<^sub>l E HFun (extend f) l"
[PROOF STATE]
proof (prove)
using this:
eval\<^sub>l E HFun (extend f) l

goal (1 subgoal):
 1. \<exists>l\<in>C. eval\<^sub>l E HFun (extend f) l
[PROOF STEP]
using l_p
[PROOF STATE]
proof (prove)
using this:
eval\<^sub>l E HFun (extend f) l
l \<in> C \<and> \<not> falsifies\<^sub>l (f (Suc n)) l

goal (1 subgoal):
 1. \<exists>l\<in>C. eval\<^sub>l E HFun (extend f) l
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>l\<in>C. eval\<^sub>l E HFun (extend f) l

goal (1 subgoal):
 1. eval\<^sub>c HFun (extend f) C
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<exists>l\<in>C. eval\<^sub>l ?E2 HFun (extend f) l

goal (1 subgoal):
 1. eval\<^sub>c HFun (extend f) C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>l\<in>C. eval\<^sub>l ?E2 HFun (extend f) l
[PROOF STEP]
have "eval\<^sub>c HFun (extend f) C"
[PROOF STATE]
proof (prove)
using this:
\<exists>l\<in>C. eval\<^sub>l ?E2 HFun (extend f) l

goal (1 subgoal):
 1. eval\<^sub>c HFun (extend f) C
[PROOF STEP]
unfolding eval\<^sub>c_def
[PROOF STATE]
proof (prove)
using this:
\<exists>l\<in>C. eval\<^sub>l ?E2 HFun (extend f) l

goal (1 subgoal):
 1. \<forall>E. Bex C (eval\<^sub>l E HFun (extend f))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
eval\<^sub>c HFun (extend f) C

goal (1 subgoal):
 1. eval\<^sub>c HFun (extend f) C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
eval\<^sub>c HFun (extend f) C
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
eval\<^sub>c HFun (extend f) C

goal (1 subgoal):
 1. eval\<^sub>c HFun (extend f) C
[PROOF STEP]
using instance_of\<^sub>l\<^sub>s_self
[PROOF STATE]
proof (prove)
using this:
eval\<^sub>c HFun (extend f) C
instance_of\<^sub>l\<^sub>s ?L ?L

goal (1 subgoal):
 1. eval\<^sub>c HFun (extend f) C
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
eval\<^sub>c HFun (extend f) C

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma extend_preserves_model2: (* only for ground *)
  assumes f_infpath: "wf_infpath (f :: nat \<Rightarrow> partial_pred_denot)"
  assumes C_ground: "ground\<^sub>l\<^sub>s C"
  assumes fin_c: "finite C"
  assumes model_C: "\<forall>n. \<not>falsifies\<^sub>c (f n) C"
  shows C_false: "eval\<^sub>c HFun (extend f) C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval\<^sub>c HFun (extend f) C
[PROOF STEP]
proof -
  \<comment> \<open>Since C is finite, C has a largest index of a literal.\<close>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. eval\<^sub>c HFun (extend f) C
[PROOF STEP]
obtain n where largest: "\<forall>l \<in> C. nat_of_fatom (get_atom l) \<le> n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>n. \<forall>l\<in>C. nat_of_fatom (get_atom l) \<le> n \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using fin_c maximum[of C "\<lambda>l. nat_of_fatom (get_atom l)"]
[PROOF STATE]
proof (prove)
using this:
finite C
finite C \<Longrightarrow> \<exists>n. \<forall>l\<in>C. nat_of_fatom (get_atom l) \<le> n

goal (1 subgoal):
 1. (\<And>n. \<forall>l\<in>C. nat_of_fatom (get_atom l) \<le> n \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>l\<in>C. nat_of_fatom (get_atom l) \<le> n

goal (1 subgoal):
 1. eval\<^sub>c HFun (extend f) C
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>l\<in>C. nat_of_fatom (get_atom l) \<le> n

goal (1 subgoal):
 1. eval\<^sub>c HFun (extend f) C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>l\<in>C. nat_of_fatom (get_atom l) \<le> n
[PROOF STEP]
have "\<not>falsifies\<^sub>c (f (Suc n)) C"
[PROOF STATE]
proof (prove)
using this:
\<forall>l\<in>C. nat_of_fatom (get_atom l) \<le> n

goal (1 subgoal):
 1. \<not> falsifies\<^sub>c (f (Suc n)) C
[PROOF STEP]
using model_C
[PROOF STATE]
proof (prove)
using this:
\<forall>l\<in>C. nat_of_fatom (get_atom l) \<le> n
\<forall>n. \<not> falsifies\<^sub>c (f n) C

goal (1 subgoal):
 1. \<not> falsifies\<^sub>c (f (Suc n)) C
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<not> falsifies\<^sub>c (f (Suc n)) C

goal (1 subgoal):
 1. eval\<^sub>c HFun (extend f) C
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<forall>l\<in>C. nat_of_fatom (get_atom l) \<le> n
\<not> falsifies\<^sub>c (f (Suc n)) C
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>l\<in>C. nat_of_fatom (get_atom l) \<le> n
\<not> falsifies\<^sub>c (f (Suc n)) C

goal (1 subgoal):
 1. eval\<^sub>c HFun (extend f) C
[PROOF STEP]
using model_C f_infpath C_ground extend_preserves_model[of f C n ]
[PROOF STATE]
proof (prove)
using this:
\<forall>l\<in>C. nat_of_fatom (get_atom l) \<le> n
\<not> falsifies\<^sub>c (f (Suc n)) C
\<forall>n. \<not> falsifies\<^sub>c (f n) C
wf_infpath f
ground\<^sub>l\<^sub>s C
\<lbrakk>wf_infpath f; ground\<^sub>l\<^sub>s C; \<not> falsifies\<^sub>c (f (Suc n)) C; \<forall>l\<in>C. nat_of_fatom (get_atom l) \<le> n\<rbrakk> \<Longrightarrow> eval\<^sub>c HFun (extend f) C

goal (1 subgoal):
 1. eval\<^sub>c HFun (extend f) C
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
eval\<^sub>c HFun (extend f) C

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma extend_infpath:
  assumes f_infpath: "wf_infpath (f :: nat \<Rightarrow> partial_pred_denot)"
  assumes model_c: "\<forall>n. \<not>falsifies\<^sub>c (f n) C"
  assumes fin_c: "finite C"
  shows "eval\<^sub>c HFun (extend f) C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval\<^sub>c HFun (extend f) C
[PROOF STEP]
unfolding eval\<^sub>c_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>E. Bex C (eval\<^sub>l E HFun (extend f))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>E. Bex C (eval\<^sub>l E HFun (extend f))
[PROOF STEP]
fix E
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>E. Bex C (eval\<^sub>l E HFun (extend f))
[PROOF STEP]
let ?G = "extend f"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>E. Bex C (eval\<^sub>l E HFun (extend f))
[PROOF STEP]
let ?\<sigma> = "sub_of_denot E"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>E. Bex C (eval\<^sub>l E HFun (extend f))
[PROOF STEP]
from fin_c
[PROOF STATE]
proof (chain)
picking this:
finite C
[PROOF STEP]
have fin_c\<sigma>: "finite (C \<cdot>\<^sub>l\<^sub>s sub_of_denot E)"
[PROOF STATE]
proof (prove)
using this:
finite C

goal (1 subgoal):
 1. finite (C \<cdot>\<^sub>l\<^sub>s sub_of_denot E)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite (C \<cdot>\<^sub>l\<^sub>s sub_of_denot E)

goal (1 subgoal):
 1. \<And>E. Bex C (eval\<^sub>l E HFun (extend f))
[PROOF STEP]
have groundc\<sigma>: "ground\<^sub>l\<^sub>s (C \<cdot>\<^sub>l\<^sub>s sub_of_denot E)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ground\<^sub>l\<^sub>s (C \<cdot>\<^sub>l\<^sub>s sub_of_denot E)
[PROOF STEP]
using sub_of_denot_equiv_ground
[PROOF STATE]
proof (prove)
using this:
(\<exists>l\<in>?C. eval\<^sub>l ?E HFun ?G l) = (\<exists>l\<in>?C \<cdot>\<^sub>l\<^sub>s sub_of_denot ?E. eval\<^sub>l ?E HFun ?G l) \<and> ground\<^sub>l\<^sub>s (?C \<cdot>\<^sub>l\<^sub>s sub_of_denot ?E)

goal (1 subgoal):
 1. ground\<^sub>l\<^sub>s (C \<cdot>\<^sub>l\<^sub>s sub_of_denot E)
[PROOF STEP]
by auto

  \<comment> \<open>Here starts the proof\<close>
  \<comment> \<open>We go from syntactic FO world to syntactic ground world:\<close>
[PROOF STATE]
proof (state)
this:
ground\<^sub>l\<^sub>s (C \<cdot>\<^sub>l\<^sub>s sub_of_denot E)

goal (1 subgoal):
 1. \<And>E. Bex C (eval\<^sub>l E HFun (extend f))
[PROOF STEP]
from model_c
[PROOF STATE]
proof (chain)
picking this:
\<forall>n. \<not> falsifies\<^sub>c (f n) C
[PROOF STEP]
have "\<forall>n. \<not>falsifies\<^sub>c (f n) (C \<cdot>\<^sub>l\<^sub>s ?\<sigma>)"
[PROOF STATE]
proof (prove)
using this:
\<forall>n. \<not> falsifies\<^sub>c (f n) C

goal (1 subgoal):
 1. \<forall>n. \<not> falsifies\<^sub>c (f n) (C \<cdot>\<^sub>l\<^sub>s sub_of_denot E)
[PROOF STEP]
using partial_equiv_subst
[PROOF STATE]
proof (prove)
using this:
\<forall>n. \<not> falsifies\<^sub>c (f n) C
falsifies\<^sub>c ?G (?C \<cdot>\<^sub>l\<^sub>s ?\<tau>) \<Longrightarrow> falsifies\<^sub>c ?G ?C

goal (1 subgoal):
 1. \<forall>n. \<not> falsifies\<^sub>c (f n) (C \<cdot>\<^sub>l\<^sub>s sub_of_denot E)
[PROOF STEP]
by blast
  \<comment> \<open>Then from syntactic ground world to semantic ground world:\<close>
[PROOF STATE]
proof (state)
this:
\<forall>n. \<not> falsifies\<^sub>c (f n) (C \<cdot>\<^sub>l\<^sub>s sub_of_denot E)

goal (1 subgoal):
 1. \<And>E. Bex C (eval\<^sub>l E HFun (extend f))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>n. \<not> falsifies\<^sub>c (f n) (C \<cdot>\<^sub>l\<^sub>s sub_of_denot E)
[PROOF STEP]
have "eval\<^sub>c HFun ?G (C \<cdot>\<^sub>l\<^sub>s ?\<sigma>)"
[PROOF STATE]
proof (prove)
using this:
\<forall>n. \<not> falsifies\<^sub>c (f n) (C \<cdot>\<^sub>l\<^sub>s sub_of_denot E)

goal (1 subgoal):
 1. eval\<^sub>c HFun (extend f) (C \<cdot>\<^sub>l\<^sub>s sub_of_denot E)
[PROOF STEP]
using groundc\<sigma> f_infpath fin_c\<sigma> extend_preserves_model2[of f "C \<cdot>\<^sub>l\<^sub>s ?\<sigma>"]
[PROOF STATE]
proof (prove)
using this:
\<forall>n. \<not> falsifies\<^sub>c (f n) (C \<cdot>\<^sub>l\<^sub>s sub_of_denot E)
ground\<^sub>l\<^sub>s (C \<cdot>\<^sub>l\<^sub>s sub_of_denot E)
wf_infpath f
finite (C \<cdot>\<^sub>l\<^sub>s sub_of_denot E)
\<lbrakk>wf_infpath f; ground\<^sub>l\<^sub>s (C \<cdot>\<^sub>l\<^sub>s sub_of_denot E); finite (C \<cdot>\<^sub>l\<^sub>s sub_of_denot E); \<forall>n. \<not> falsifies\<^sub>c (f n) (C \<cdot>\<^sub>l\<^sub>s sub_of_denot E)\<rbrakk> \<Longrightarrow> eval\<^sub>c HFun (extend f) (C \<cdot>\<^sub>l\<^sub>s sub_of_denot E)

goal (1 subgoal):
 1. eval\<^sub>c HFun (extend f) (C \<cdot>\<^sub>l\<^sub>s sub_of_denot E)
[PROOF STEP]
by blast
  \<comment> \<open>Then from semantic ground world to semantic FO world:\<close>
[PROOF STATE]
proof (state)
this:
eval\<^sub>c HFun (extend f) (C \<cdot>\<^sub>l\<^sub>s sub_of_denot E)

goal (1 subgoal):
 1. \<And>E. Bex C (eval\<^sub>l E HFun (extend f))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
eval\<^sub>c HFun (extend f) (C \<cdot>\<^sub>l\<^sub>s sub_of_denot E)
[PROOF STEP]
have "\<forall>E. \<exists>l \<in> (C \<cdot>\<^sub>l\<^sub>s ?\<sigma>). eval\<^sub>l E HFun ?G l"
[PROOF STATE]
proof (prove)
using this:
eval\<^sub>c HFun (extend f) (C \<cdot>\<^sub>l\<^sub>s sub_of_denot E)

goal (1 subgoal):
 1. \<forall>Ea. \<exists>l\<in>C \<cdot>\<^sub>l\<^sub>s sub_of_denot E. eval\<^sub>l Ea HFun (extend f) l
[PROOF STEP]
unfolding eval\<^sub>c_def
[PROOF STATE]
proof (prove)
using this:
\<forall>Ea. Bex (C \<cdot>\<^sub>l\<^sub>s sub_of_denot E) (eval\<^sub>l Ea HFun (extend f))

goal (1 subgoal):
 1. \<forall>Ea. \<exists>l\<in>C \<cdot>\<^sub>l\<^sub>s sub_of_denot E. eval\<^sub>l Ea HFun (extend f) l
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>Ea. \<exists>l\<in>C \<cdot>\<^sub>l\<^sub>s sub_of_denot E. eval\<^sub>l Ea HFun (extend f) l

goal (1 subgoal):
 1. \<And>E. Bex C (eval\<^sub>l E HFun (extend f))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>Ea. \<exists>l\<in>C \<cdot>\<^sub>l\<^sub>s sub_of_denot E. eval\<^sub>l Ea HFun (extend f) l
[PROOF STEP]
have "\<exists>l \<in> (C \<cdot>\<^sub>l\<^sub>s ?\<sigma>). eval\<^sub>l E HFun ?G l"
[PROOF STATE]
proof (prove)
using this:
\<forall>Ea. \<exists>l\<in>C \<cdot>\<^sub>l\<^sub>s sub_of_denot E. eval\<^sub>l Ea HFun (extend f) l

goal (1 subgoal):
 1. \<exists>l\<in>C \<cdot>\<^sub>l\<^sub>s sub_of_denot E. eval\<^sub>l E HFun (extend f) l
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>l\<in>C \<cdot>\<^sub>l\<^sub>s sub_of_denot E. eval\<^sub>l E HFun (extend f) l

goal (1 subgoal):
 1. \<And>E. Bex C (eval\<^sub>l E HFun (extend f))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>l\<in>C \<cdot>\<^sub>l\<^sub>s sub_of_denot E. eval\<^sub>l E HFun (extend f) l
[PROOF STEP]
show "\<exists>l \<in> C. eval\<^sub>l E HFun ?G l"
[PROOF STATE]
proof (prove)
using this:
\<exists>l\<in>C \<cdot>\<^sub>l\<^sub>s sub_of_denot E. eval\<^sub>l E HFun (extend f) l

goal (1 subgoal):
 1. \<exists>l\<in>C. eval\<^sub>l E HFun (extend f) l
[PROOF STEP]
using sub_of_denot_equiv_ground[of C E "extend f"]
[PROOF STATE]
proof (prove)
using this:
\<exists>l\<in>C \<cdot>\<^sub>l\<^sub>s sub_of_denot E. eval\<^sub>l E HFun (extend f) l
(\<exists>l\<in>C. eval\<^sub>l E HFun (extend f) l) = (\<exists>l\<in>C \<cdot>\<^sub>l\<^sub>s sub_of_denot E. eval\<^sub>l E HFun (extend f) l) \<and> ground\<^sub>l\<^sub>s (C \<cdot>\<^sub>l\<^sub>s sub_of_denot E)

goal (1 subgoal):
 1. \<exists>l\<in>C. eval\<^sub>l E HFun (extend f) l
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>l\<in>C. eval\<^sub>l E HFun (extend f) l

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma infpath_model:
  assumes f_infpath: "wf_infpath (f :: nat \<Rightarrow> partial_pred_denot)"
  assumes model_cs: "\<forall>n. \<not>falsifies\<^sub>c\<^sub>s (f n) Cs"
  assumes fin_cs: "finite Cs"
  assumes fin_c: "\<forall>C \<in> Cs. finite C"
  shows "eval\<^sub>c\<^sub>s HFun (extend f) Cs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval\<^sub>c\<^sub>s HFun (extend f) Cs
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. eval\<^sub>c\<^sub>s HFun (extend f) Cs
[PROOF STEP]
let ?F = "HFun"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. eval\<^sub>c\<^sub>s HFun (extend f) Cs
[PROOF STEP]
have "\<forall>C \<in> Cs. eval\<^sub>c ?F (extend f) C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>C\<in>Cs. eval\<^sub>c HFun (extend f) C
[PROOF STEP]
proof (rule ballI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>C. C \<in> Cs \<Longrightarrow> eval\<^sub>c HFun (extend f) C
[PROOF STEP]
fix C
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>C. C \<in> Cs \<Longrightarrow> eval\<^sub>c HFun (extend f) C
[PROOF STEP]
assume asm: "C \<in> Cs"
[PROOF STATE]
proof (state)
this:
C \<in> Cs

goal (1 subgoal):
 1. \<And>C. C \<in> Cs \<Longrightarrow> eval\<^sub>c HFun (extend f) C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
C \<in> Cs
[PROOF STEP]
have "\<forall>n. \<not>falsifies\<^sub>c (f n) C"
[PROOF STATE]
proof (prove)
using this:
C \<in> Cs

goal (1 subgoal):
 1. \<forall>n. \<not> falsifies\<^sub>c (f n) C
[PROOF STEP]
using model_cs
[PROOF STATE]
proof (prove)
using this:
C \<in> Cs
\<forall>n. \<not> falsifies\<^sub>c\<^sub>s (f n) Cs

goal (1 subgoal):
 1. \<forall>n. \<not> falsifies\<^sub>c (f n) C
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>n. \<not> falsifies\<^sub>c (f n) C

goal (1 subgoal):
 1. \<And>C. C \<in> Cs \<Longrightarrow> eval\<^sub>c HFun (extend f) C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>n. \<not> falsifies\<^sub>c (f n) C
[PROOF STEP]
show "eval\<^sub>c ?F (extend f) C"
[PROOF STATE]
proof (prove)
using this:
\<forall>n. \<not> falsifies\<^sub>c (f n) C

goal (1 subgoal):
 1. eval\<^sub>c HFun (extend f) C
[PROOF STEP]
using fin_c asm f_infpath extend_infpath[of f C]
[PROOF STATE]
proof (prove)
using this:
\<forall>n. \<not> falsifies\<^sub>c (f n) C
\<forall>C\<in>Cs. finite C
C \<in> Cs
wf_infpath f
\<lbrakk>wf_infpath f; \<forall>n. \<not> falsifies\<^sub>c (f n) C; finite C\<rbrakk> \<Longrightarrow> eval\<^sub>c HFun (extend f) C

goal (1 subgoal):
 1. eval\<^sub>c HFun (extend f) C
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
eval\<^sub>c HFun (extend f) C

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>C\<in>Cs. eval\<^sub>c HFun (extend f) C

goal (1 subgoal):
 1. eval\<^sub>c\<^sub>s HFun (extend f) Cs
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>C\<in>Cs. eval\<^sub>c HFun (extend f) C
[PROOF STEP]
show "eval\<^sub>c\<^sub>s ?F (extend f) Cs"
[PROOF STATE]
proof (prove)
using this:
\<forall>C\<in>Cs. eval\<^sub>c HFun (extend f) C

goal (1 subgoal):
 1. eval\<^sub>c\<^sub>s HFun (extend f) Cs
[PROOF STEP]
unfolding eval\<^sub>c\<^sub>s_def
[PROOF STATE]
proof (prove)
using this:
\<forall>C\<in>Cs. eval\<^sub>c HFun (extend f) C

goal (1 subgoal):
 1. Ball Cs (eval\<^sub>c HFun (extend f))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
eval\<^sub>c\<^sub>s HFun (extend f) Cs

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma branch_length:
  assumes "branch b (deeptree n)"
  shows "length b = n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length b = n
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
branch b (deeptree n)

goal (1 subgoal):
 1. length b = n
[PROOF STEP]
proof (induction n arbitrary: b)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>b. branch b (deeptree 0) \<Longrightarrow> length b = 0
 2. \<And>n b. \<lbrakk>\<And>b. branch b (deeptree n) \<Longrightarrow> length b = n; branch b (deeptree (Suc n))\<rbrakk> \<Longrightarrow> length b = Suc n
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
branch b (deeptree 0)

goal (2 subgoals):
 1. \<And>b. branch b (deeptree 0) \<Longrightarrow> length b = 0
 2. \<And>n b. \<lbrakk>\<And>b. branch b (deeptree n) \<Longrightarrow> length b = n; branch b (deeptree (Suc n))\<rbrakk> \<Longrightarrow> length b = Suc n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
branch b (deeptree 0)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
branch b (deeptree 0)

goal (1 subgoal):
 1. length b = 0
[PROOF STEP]
using branch_inv_Leaf
[PROOF STATE]
proof (prove)
using this:
branch b (deeptree 0)
branch ?b Leaf = (?b = [])

goal (1 subgoal):
 1. length b = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length b = 0

goal (1 subgoal):
 1. \<And>n b. \<lbrakk>\<And>b. branch b (deeptree n) \<Longrightarrow> length b = n; branch b (deeptree (Suc n))\<rbrakk> \<Longrightarrow> length b = Suc n
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n b. \<lbrakk>\<And>b. branch b (deeptree n) \<Longrightarrow> length b = n; branch b (deeptree (Suc n))\<rbrakk> \<Longrightarrow> length b = Suc n
[PROOF STEP]
case (Suc n)
[PROOF STATE]
proof (state)
this:
branch ?b (deeptree n) \<Longrightarrow> length ?b = n
branch b (deeptree (Suc n))

goal (1 subgoal):
 1. \<And>n b. \<lbrakk>\<And>b. branch b (deeptree n) \<Longrightarrow> length b = n; branch b (deeptree (Suc n))\<rbrakk> \<Longrightarrow> length b = Suc n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
branch ?b (deeptree n) \<Longrightarrow> length ?b = n
branch b (deeptree (Suc n))
[PROOF STEP]
have "branch b (Branching (deeptree n) (deeptree n))"
[PROOF STATE]
proof (prove)
using this:
branch ?b (deeptree n) \<Longrightarrow> length ?b = n
branch b (deeptree (Suc n))

goal (1 subgoal):
 1. branch b (Branching (deeptree n) (deeptree n))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
branch b (Branching (deeptree n) (deeptree n))

goal (1 subgoal):
 1. \<And>n b. \<lbrakk>\<And>b. branch b (deeptree n) \<Longrightarrow> length b = n; branch b (deeptree (Suc n))\<rbrakk> \<Longrightarrow> length b = Suc n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
branch b (Branching (deeptree n) (deeptree n))
[PROOF STEP]
obtain a b' where p: "b = a#b'\<and> branch b' (deeptree n)"
[PROOF STATE]
proof (prove)
using this:
branch b (Branching (deeptree n) (deeptree n))

goal (1 subgoal):
 1. (\<And>a b'. b = a # b' \<and> branch b' (deeptree n) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using branch_inv_Branching[of b]
[PROOF STATE]
proof (prove)
using this:
branch b (Branching (deeptree n) (deeptree n))
branch b (Branching ?l ?r) = (\<exists>a b'. b = a # b' \<and> (a \<longrightarrow> branch b' ?l) \<and> (\<not> a \<longrightarrow> branch b' ?r))

goal (1 subgoal):
 1. (\<And>a b'. b = a # b' \<and> branch b' (deeptree n) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
b = a # b' \<and> branch b' (deeptree n)

goal (1 subgoal):
 1. \<And>n b. \<lbrakk>\<And>b. branch b (deeptree n) \<Longrightarrow> length b = n; branch b (deeptree (Suc n))\<rbrakk> \<Longrightarrow> length b = Suc n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
b = a # b' \<and> branch b' (deeptree n)
[PROOF STEP]
have "length b' = n"
[PROOF STATE]
proof (prove)
using this:
b = a # b' \<and> branch b' (deeptree n)

goal (1 subgoal):
 1. length b' = n
[PROOF STEP]
using Suc
[PROOF STATE]
proof (prove)
using this:
b = a # b' \<and> branch b' (deeptree n)
branch ?b (deeptree n) \<Longrightarrow> length ?b = n
branch b (deeptree (Suc n))

goal (1 subgoal):
 1. length b' = n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length b' = n

goal (1 subgoal):
 1. \<And>n b. \<lbrakk>\<And>b. branch b (deeptree n) \<Longrightarrow> length b = n; branch b (deeptree (Suc n))\<rbrakk> \<Longrightarrow> length b = Suc n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length b' = n
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
length b' = n

goal (1 subgoal):
 1. length b = Suc n
[PROOF STEP]
using p
[PROOF STATE]
proof (prove)
using this:
length b' = n
b = a # b' \<and> branch b' (deeptree n)

goal (1 subgoal):
 1. length b = Suc n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length b = Suc n

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma infinity:
  assumes inj: "\<forall>n :: nat. undiago (diago n) = n"
  assumes all_tree: "\<forall>n :: nat. (diago n) \<in> tree"
  shows "\<not>finite tree"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. infinite tree
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. infinite tree
[PROOF STEP]
from inj all_tree
[PROOF STATE]
proof (chain)
picking this:
\<forall>n. undiago (diago n) = n
\<forall>n. diago n \<in> tree
[PROOF STEP]
have "\<forall>n. n = undiago (diago n) \<and> (diago n) \<in> tree"
[PROOF STATE]
proof (prove)
using this:
\<forall>n. undiago (diago n) = n
\<forall>n. diago n \<in> tree

goal (1 subgoal):
 1. \<forall>n. n = undiago (diago n) \<and> diago n \<in> tree
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>n. n = undiago (diago n) \<and> diago n \<in> tree

goal (1 subgoal):
 1. infinite tree
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>n. n = undiago (diago n) \<and> diago n \<in> tree
[PROOF STEP]
have "\<forall>n. \<exists>ds. n = undiago ds \<and> ds \<in> tree"
[PROOF STATE]
proof (prove)
using this:
\<forall>n. n = undiago (diago n) \<and> diago n \<in> tree

goal (1 subgoal):
 1. \<forall>n. \<exists>ds. n = undiago ds \<and> ds \<in> tree
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>n. \<exists>ds. n = undiago ds \<and> ds \<in> tree

goal (1 subgoal):
 1. infinite tree
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>n. \<exists>ds. n = undiago ds \<and> ds \<in> tree
[PROOF STEP]
have "undiago ` tree = (UNIV :: nat set)"
[PROOF STATE]
proof (prove)
using this:
\<forall>n. \<exists>ds. n = undiago ds \<and> ds \<in> tree

goal (1 subgoal):
 1. undiago ` tree = UNIV
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
undiago ` tree = UNIV

goal (1 subgoal):
 1. infinite tree
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
undiago ` tree = UNIV
[PROOF STEP]
have "\<not>finite tree"
[PROOF STATE]
proof (prove)
using this:
undiago ` tree = UNIV

goal (1 subgoal):
 1. infinite tree
[PROOF STEP]
by (metis finite_imageI infinite_UNIV_nat)
[PROOF STATE]
proof (state)
this:
infinite tree

goal (1 subgoal):
 1. infinite tree
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
infinite tree
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
infinite tree

goal (1 subgoal):
 1. infinite tree
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
infinite tree

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma longer_falsifies\<^sub>l:
  assumes "falsifies\<^sub>l ds l"
  shows "falsifies\<^sub>l (ds@d) l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. falsifies\<^sub>l (ds @ d) l
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. falsifies\<^sub>l (ds @ d) l
[PROOF STEP]
let ?i = "nat_of_fatom (get_atom l)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. falsifies\<^sub>l (ds @ d) l
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
falsifies\<^sub>l ds l
[PROOF STEP]
have i_p: "ground\<^sub>l l \<and>  ?i < length ds \<and> ds ! ?i = (\<not>sign l)"
[PROOF STATE]
proof (prove)
using this:
falsifies\<^sub>l ds l

goal (1 subgoal):
 1. ground\<^sub>l l \<and> nat_of_fatom (get_atom l) < length ds \<and> ds ! nat_of_fatom (get_atom l) = (\<not> sign l)
[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 ds \<and> ds ! i = (\<not> sign l))

goal (1 subgoal):
 1. ground\<^sub>l l \<and> nat_of_fatom (get_atom l) < length ds \<and> ds ! nat_of_fatom (get_atom l) = (\<not> sign l)
[PROOF STEP]
by meson
[PROOF STATE]
proof (state)
this:
ground\<^sub>l l \<and> nat_of_fatom (get_atom l) < length ds \<and> ds ! nat_of_fatom (get_atom l) = (\<not> sign l)

goal (1 subgoal):
 1. falsifies\<^sub>l (ds @ d) l
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
ground\<^sub>l l \<and> nat_of_fatom (get_atom l) < length ds \<and> ds ! nat_of_fatom (get_atom l) = (\<not> sign l)

goal (1 subgoal):
 1. falsifies\<^sub>l (ds @ d) l
[PROOF STEP]
from i_p
[PROOF STATE]
proof (chain)
picking this:
ground\<^sub>l l \<and> nat_of_fatom (get_atom l) < length ds \<and> ds ! nat_of_fatom (get_atom l) = (\<not> sign l)
[PROOF STEP]
have "?i < length (ds@d)"
[PROOF STATE]
proof (prove)
using this:
ground\<^sub>l l \<and> nat_of_fatom (get_atom l) < length ds \<and> ds ! nat_of_fatom (get_atom l) = (\<not> sign l)

goal (1 subgoal):
 1. nat_of_fatom (get_atom l) < length (ds @ d)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nat_of_fatom (get_atom l) < length (ds @ d)

goal (1 subgoal):
 1. falsifies\<^sub>l (ds @ d) l
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
nat_of_fatom (get_atom l) < length (ds @ d)

goal (1 subgoal):
 1. falsifies\<^sub>l (ds @ d) l
[PROOF STEP]
from i_p
[PROOF STATE]
proof (chain)
picking this:
ground\<^sub>l l \<and> nat_of_fatom (get_atom l) < length ds \<and> ds ! nat_of_fatom (get_atom l) = (\<not> sign l)
[PROOF STEP]
have "(ds@d) ! ?i = (\<not>sign l)"
[PROOF STATE]
proof (prove)
using this:
ground\<^sub>l l \<and> nat_of_fatom (get_atom l) < length ds \<and> ds ! nat_of_fatom (get_atom l) = (\<not> sign l)

goal (1 subgoal):
 1. (ds @ d) ! nat_of_fatom (get_atom l) = (\<not> sign l)
[PROOF STEP]
by (simp add: nth_append)
[PROOF STATE]
proof (state)
this:
(ds @ d) ! nat_of_fatom (get_atom l) = (\<not> sign l)

goal (1 subgoal):
 1. falsifies\<^sub>l (ds @ d) l
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
ground\<^sub>l l \<and> nat_of_fatom (get_atom l) < length ds \<and> ds ! nat_of_fatom (get_atom l) = (\<not> sign l)
nat_of_fatom (get_atom l) < length (ds @ d)
(ds @ d) ! nat_of_fatom (get_atom l) = (\<not> sign l)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
ground\<^sub>l l \<and> nat_of_fatom (get_atom l) < length ds \<and> ds ! nat_of_fatom (get_atom l) = (\<not> sign l)
nat_of_fatom (get_atom l) < length (ds @ d)
(ds @ d) ! nat_of_fatom (get_atom l) = (\<not> sign l)

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

goal (1 subgoal):
 1. ground\<^sub>l l \<and> (let i = nat_of_fatom (get_atom l) in i < length (ds @ d) \<and> (ds @ d) ! i = (\<not> sign l))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
falsifies\<^sub>l (ds @ d) l

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma longer_falsifies\<^sub>g:
  assumes "falsifies\<^sub>g ds C"
  shows "falsifies\<^sub>g (ds @ d) C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. falsifies\<^sub>g (ds @ d) C
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. falsifies\<^sub>g (ds @ d) C
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. falsifies\<^sub>g (ds @ d) C
[PROOF STEP]
fix l
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. falsifies\<^sub>g (ds @ d) C
[PROOF STEP]
assume "l\<in>C"
[PROOF STATE]
proof (state)
this:
l \<in> C

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

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

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

goal (1 subgoal):
 1. falsifies\<^sub>g (ds @ d) C
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?l2 \<in> C \<Longrightarrow> falsifies\<^sub>l (ds @ d) ?l2

goal (1 subgoal):
 1. falsifies\<^sub>g (ds @ d) C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?l2 \<in> C \<Longrightarrow> falsifies\<^sub>l (ds @ d) ?l2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
?l2 \<in> C \<Longrightarrow> falsifies\<^sub>l (ds @ d) ?l2

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

goal (1 subgoal):
 1. falsifies\<^sub>g (ds @ d) C
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
falsifies\<^sub>g (ds @ d) C

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma longer_falsifies\<^sub>c:
  assumes "falsifies\<^sub>c ds C"
  shows "falsifies\<^sub>c (ds @ d) C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. falsifies\<^sub>c (ds @ d) C
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. falsifies\<^sub>c (ds @ d) C
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
falsifies\<^sub>c ds C
[PROOF STEP]
obtain C' where "instance_of\<^sub>l\<^sub>s C' C \<and> falsifies\<^sub>g ds C'"
[PROOF STATE]
proof (prove)
using this:
falsifies\<^sub>c ds C

goal (1 subgoal):
 1. (\<And>C'. instance_of\<^sub>l\<^sub>s C' C \<and> falsifies\<^sub>g ds C' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
instance_of\<^sub>l\<^sub>s C' C \<and> falsifies\<^sub>g ds C'

goal (1 subgoal):
 1. falsifies\<^sub>c (ds @ d) C
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
instance_of\<^sub>l\<^sub>s C' C \<and> falsifies\<^sub>g ds C'

goal (1 subgoal):
 1. falsifies\<^sub>c (ds @ d) C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
instance_of\<^sub>l\<^sub>s C' C \<and> falsifies\<^sub>g ds C'
[PROOF STEP]
have "falsifies\<^sub>g (ds @ d) C'"
[PROOF STATE]
proof (prove)
using this:
instance_of\<^sub>l\<^sub>s C' C \<and> falsifies\<^sub>g ds C'

goal (1 subgoal):
 1. falsifies\<^sub>g (ds @ d) C'
[PROOF STEP]
using longer_falsifies\<^sub>g
[PROOF STATE]
proof (prove)
using this:
instance_of\<^sub>l\<^sub>s C' C \<and> falsifies\<^sub>g ds C'
falsifies\<^sub>g ?ds ?C \<Longrightarrow> falsifies\<^sub>g (?ds @ ?d) ?C

goal (1 subgoal):
 1. falsifies\<^sub>g (ds @ d) C'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
falsifies\<^sub>g (ds @ d) C'

goal (1 subgoal):
 1. falsifies\<^sub>c (ds @ d) C
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
instance_of\<^sub>l\<^sub>s C' C \<and> falsifies\<^sub>g ds C'
falsifies\<^sub>g (ds @ d) C'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
instance_of\<^sub>l\<^sub>s C' C \<and> falsifies\<^sub>g ds C'
falsifies\<^sub>g (ds @ d) C'

goal (1 subgoal):
 1. falsifies\<^sub>c (ds @ d) C
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
falsifies\<^sub>c (ds @ d) C

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma longer_falsifies:
  assumes "falsifies\<^sub>c\<^sub>s ds Cs"
  shows "falsifies\<^sub>c\<^sub>s (ds @ d) Cs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. falsifies\<^sub>c\<^sub>s (ds @ d) Cs
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. falsifies\<^sub>c\<^sub>s (ds @ d) Cs
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
falsifies\<^sub>c\<^sub>s ds Cs
[PROOF STEP]
obtain C where "C \<in> Cs \<and> falsifies\<^sub>c ds C"
[PROOF STATE]
proof (prove)
using this:
falsifies\<^sub>c\<^sub>s ds Cs

goal (1 subgoal):
 1. (\<And>C. C \<in> Cs \<and> falsifies\<^sub>c ds C \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
C \<in> Cs \<and> falsifies\<^sub>c ds C

goal (1 subgoal):
 1. falsifies\<^sub>c\<^sub>s (ds @ d) Cs
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
C \<in> Cs \<and> falsifies\<^sub>c ds C

goal (1 subgoal):
 1. falsifies\<^sub>c\<^sub>s (ds @ d) Cs
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
C \<in> Cs \<and> falsifies\<^sub>c ds C
[PROOF STEP]
have "falsifies\<^sub>c (ds @ d) C"
[PROOF STATE]
proof (prove)
using this:
C \<in> Cs \<and> falsifies\<^sub>c ds C

goal (1 subgoal):
 1. falsifies\<^sub>c (ds @ d) C
[PROOF STEP]
using longer_falsifies\<^sub>c[of C ds d]
[PROOF STATE]
proof (prove)
using this:
C \<in> Cs \<and> falsifies\<^sub>c ds C
falsifies\<^sub>c ds C \<Longrightarrow> falsifies\<^sub>c (ds @ d) C

goal (1 subgoal):
 1. falsifies\<^sub>c (ds @ d) C
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
falsifies\<^sub>c (ds @ d) C

goal (1 subgoal):
 1. falsifies\<^sub>c\<^sub>s (ds @ d) Cs
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
C \<in> Cs \<and> falsifies\<^sub>c ds C
falsifies\<^sub>c (ds @ d) C
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
C \<in> Cs \<and> falsifies\<^sub>c ds C
falsifies\<^sub>c (ds @ d) C

goal (1 subgoal):
 1. falsifies\<^sub>c\<^sub>s (ds @ d) Cs
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
falsifies\<^sub>c\<^sub>s (ds @ d) Cs

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem herbrand':
  assumes openb: "\<forall>T. \<exists>G. open_branch G T Cs"
  assumes finite_cs: "finite Cs" "\<forall>C\<in>Cs. finite C"
  shows "\<exists>G. eval\<^sub>c\<^sub>s HFun G Cs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>G. eval\<^sub>c\<^sub>s HFun G Cs
[PROOF STEP]
proof -
  \<comment> \<open>Show T infinite:\<close>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>G. eval\<^sub>c\<^sub>s HFun G Cs
[PROOF STEP]
let ?tree = "{G. \<not>falsifies\<^sub>c\<^sub>s G Cs}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>G. eval\<^sub>c\<^sub>s HFun G Cs
[PROOF STEP]
let ?undiag = length
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>G. eval\<^sub>c\<^sub>s HFun G Cs
[PROOF STEP]
let ?diag = "(\<lambda>l. SOME b. open_branch b (deeptree l) Cs) :: nat \<Rightarrow> partial_pred_denot"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>G. eval\<^sub>c\<^sub>s HFun G Cs
[PROOF STEP]
from openb
[PROOF STATE]
proof (chain)
picking this:
\<forall>T. \<exists>G. branch G T \<and> \<not> falsifies\<^sub>c\<^sub>s G Cs
[PROOF STEP]
have diag_open: "\<forall>l. open_branch (?diag l) (deeptree l) Cs"
[PROOF STATE]
proof (prove)
using this:
\<forall>T. \<exists>G. branch G T \<and> \<not> falsifies\<^sub>c\<^sub>s G Cs

goal (1 subgoal):
 1. \<forall>l. branch (SOME b. branch b (deeptree l) \<and> \<not> falsifies\<^sub>c\<^sub>s b Cs) (deeptree l) \<and> \<not> falsifies\<^sub>c\<^sub>s (SOME b. branch b (deeptree l) \<and> \<not> falsifies\<^sub>c\<^sub>s b Cs) Cs
[PROOF STEP]
using someI_ex[of "\<lambda>b. open_branch b (deeptree _) Cs"]
[PROOF STATE]
proof (prove)
using this:
\<forall>T. \<exists>G. branch G T \<and> \<not> falsifies\<^sub>c\<^sub>s G Cs
\<exists>x. branch x (deeptree ?uu4) \<and> \<not> falsifies\<^sub>c\<^sub>s x Cs \<Longrightarrow> branch (SOME x. branch x (deeptree ?uu4) \<and> \<not> falsifies\<^sub>c\<^sub>s x Cs) (deeptree ?uu4) \<and> \<not> falsifies\<^sub>c\<^sub>s (SOME x. branch x (deeptree ?uu4) \<and> \<not> falsifies\<^sub>c\<^sub>s x Cs) Cs

goal (1 subgoal):
 1. \<forall>l. branch (SOME b. branch b (deeptree l) \<and> \<not> falsifies\<^sub>c\<^sub>s b Cs) (deeptree l) \<and> \<not> falsifies\<^sub>c\<^sub>s (SOME b. branch b (deeptree l) \<and> \<not> falsifies\<^sub>c\<^sub>s b Cs) Cs
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>l. branch (SOME b. branch b (deeptree l) \<and> \<not> falsifies\<^sub>c\<^sub>s b Cs) (deeptree l) \<and> \<not> falsifies\<^sub>c\<^sub>s (SOME b. branch b (deeptree l) \<and> \<not> falsifies\<^sub>c\<^sub>s b Cs) Cs

goal (1 subgoal):
 1. \<exists>G. eval\<^sub>c\<^sub>s HFun G Cs
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>l. branch (SOME b. branch b (deeptree l) \<and> \<not> falsifies\<^sub>c\<^sub>s b Cs) (deeptree l) \<and> \<not> falsifies\<^sub>c\<^sub>s (SOME b. branch b (deeptree l) \<and> \<not> falsifies\<^sub>c\<^sub>s b Cs) Cs
[PROOF STEP]
have "\<forall>n. ?undiag (?diag n) = n"
[PROOF STATE]
proof (prove)
using this:
\<forall>l. branch (SOME b. branch b (deeptree l) \<and> \<not> falsifies\<^sub>c\<^sub>s b Cs) (deeptree l) \<and> \<not> falsifies\<^sub>c\<^sub>s (SOME b. branch b (deeptree l) \<and> \<not> falsifies\<^sub>c\<^sub>s b Cs) Cs

goal (1 subgoal):
 1. \<forall>n. length (SOME b. branch b (deeptree n) \<and> \<not> falsifies\<^sub>c\<^sub>s b Cs) = n
[PROOF STEP]
using branch_length
[PROOF STATE]
proof (prove)
using this:
\<forall>l. branch (SOME b. branch b (deeptree l) \<and> \<not> falsifies\<^sub>c\<^sub>s b Cs) (deeptree l) \<and> \<not> falsifies\<^sub>c\<^sub>s (SOME b. branch b (deeptree l) \<and> \<not> falsifies\<^sub>c\<^sub>s b Cs) Cs
branch ?b (deeptree ?n) \<Longrightarrow> length ?b = ?n

goal (1 subgoal):
 1. \<forall>n. length (SOME b. branch b (deeptree n) \<and> \<not> falsifies\<^sub>c\<^sub>s b Cs) = n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>n. length (SOME b. branch b (deeptree n) \<and> \<not> falsifies\<^sub>c\<^sub>s b Cs) = n

goal (1 subgoal):
 1. \<exists>G. eval\<^sub>c\<^sub>s HFun G Cs
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>n. length (SOME b. branch b (deeptree n) \<and> \<not> falsifies\<^sub>c\<^sub>s b Cs) = n

goal (1 subgoal):
 1. \<exists>G. eval\<^sub>c\<^sub>s HFun G Cs
[PROOF STEP]
have "\<forall>n. (?diag n) \<in> ?tree"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>n. (SOME b. branch b (deeptree n) \<and> \<not> falsifies\<^sub>c\<^sub>s b Cs) \<in> {G. \<not> falsifies\<^sub>c\<^sub>s G Cs}
[PROOF STEP]
using diag_open
[PROOF STATE]
proof (prove)
using this:
\<forall>l. branch (SOME b. branch b (deeptree l) \<and> \<not> falsifies\<^sub>c\<^sub>s b Cs) (deeptree l) \<and> \<not> falsifies\<^sub>c\<^sub>s (SOME b. branch b (deeptree l) \<and> \<not> falsifies\<^sub>c\<^sub>s b Cs) Cs

goal (1 subgoal):
 1. \<forall>n. (SOME b. branch b (deeptree n) \<and> \<not> falsifies\<^sub>c\<^sub>s b Cs) \<in> {G. \<not> falsifies\<^sub>c\<^sub>s G Cs}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>n. (SOME b. branch b (deeptree n) \<and> \<not> falsifies\<^sub>c\<^sub>s b Cs) \<in> {G. \<not> falsifies\<^sub>c\<^sub>s G Cs}

goal (1 subgoal):
 1. \<exists>G. eval\<^sub>c\<^sub>s HFun G Cs
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<forall>n. length (SOME b. branch b (deeptree n) \<and> \<not> falsifies\<^sub>c\<^sub>s b Cs) = n
\<forall>n. (SOME b. branch b (deeptree n) \<and> \<not> falsifies\<^sub>c\<^sub>s b Cs) \<in> {G. \<not> falsifies\<^sub>c\<^sub>s G Cs}
[PROOF STEP]
have "\<not>finite ?tree"
[PROOF STATE]
proof (prove)
using this:
\<forall>n. length (SOME b. branch b (deeptree n) \<and> \<not> falsifies\<^sub>c\<^sub>s b Cs) = n
\<forall>n. (SOME b. branch b (deeptree n) \<and> \<not> falsifies\<^sub>c\<^sub>s b Cs) \<in> {G. \<not> falsifies\<^sub>c\<^sub>s G Cs}

goal (1 subgoal):
 1. infinite {G. \<not> falsifies\<^sub>c\<^sub>s G Cs}
[PROOF STEP]
using infinity[of _ "\<lambda>n. SOME b. open_branch b (_ n) Cs"]
[PROOF STATE]
proof (prove)
using this:
\<forall>n. length (SOME b. branch b (deeptree n) \<and> \<not> falsifies\<^sub>c\<^sub>s b Cs) = n
\<forall>n. (SOME b. branch b (deeptree n) \<and> \<not> falsifies\<^sub>c\<^sub>s b Cs) \<in> {G. \<not> falsifies\<^sub>c\<^sub>s G Cs}
\<lbrakk>\<forall>n. ?undiago (SOME b. branch b (?uu4 n) \<and> \<not> falsifies\<^sub>c\<^sub>s b Cs) = n; \<forall>n. (SOME b. branch b (?uu4 n) \<and> \<not> falsifies\<^sub>c\<^sub>s b Cs) \<in> ?tree\<rbrakk> \<Longrightarrow> infinite ?tree

goal (1 subgoal):
 1. infinite {G. \<not> falsifies\<^sub>c\<^sub>s G Cs}
[PROOF STEP]
by simp
  \<comment> \<open>Get infinite path:\<close>
[PROOF STATE]
proof (state)
this:
infinite {G. \<not> falsifies\<^sub>c\<^sub>s G Cs}

goal (1 subgoal):
 1. \<exists>G. eval\<^sub>c\<^sub>s HFun G Cs
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
infinite {G. \<not> falsifies\<^sub>c\<^sub>s G Cs}

goal (1 subgoal):
 1. \<exists>G. eval\<^sub>c\<^sub>s HFun G Cs
[PROOF STEP]
have "\<forall>ds d. \<not>falsifies\<^sub>c\<^sub>s (ds @ d) Cs \<longrightarrow> \<not>falsifies\<^sub>c\<^sub>s ds Cs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>ds d. \<not> falsifies\<^sub>c\<^sub>s (ds @ d) Cs \<longrightarrow> \<not> falsifies\<^sub>c\<^sub>s ds Cs
[PROOF STEP]
using longer_falsifies[of Cs]
[PROOF STATE]
proof (prove)
using this:
falsifies\<^sub>c\<^sub>s ?ds Cs \<Longrightarrow> falsifies\<^sub>c\<^sub>s (?ds @ ?d) Cs

goal (1 subgoal):
 1. \<forall>ds d. \<not> falsifies\<^sub>c\<^sub>s (ds @ d) Cs \<longrightarrow> \<not> falsifies\<^sub>c\<^sub>s ds Cs
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>ds d. \<not> falsifies\<^sub>c\<^sub>s (ds @ d) Cs \<longrightarrow> \<not> falsifies\<^sub>c\<^sub>s ds Cs

goal (1 subgoal):
 1. \<exists>G. eval\<^sub>c\<^sub>s HFun G Cs
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>ds d. \<not> falsifies\<^sub>c\<^sub>s (ds @ d) Cs \<longrightarrow> \<not> falsifies\<^sub>c\<^sub>s ds Cs
[PROOF STEP]
have "(\<forall>ds d. ds @ d \<in> ?tree \<longrightarrow> ds \<in> ?tree)"
[PROOF STATE]
proof (prove)
using this:
\<forall>ds d. \<not> falsifies\<^sub>c\<^sub>s (ds @ d) Cs \<longrightarrow> \<not> falsifies\<^sub>c\<^sub>s ds Cs

goal (1 subgoal):
 1. wf_tree {G. \<not> falsifies\<^sub>c\<^sub>s G Cs}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
wf_tree {G. \<not> falsifies\<^sub>c\<^sub>s G Cs}

goal (1 subgoal):
 1. \<exists>G. eval\<^sub>c\<^sub>s HFun G Cs
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
infinite {G. \<not> falsifies\<^sub>c\<^sub>s G Cs}
wf_tree {G. \<not> falsifies\<^sub>c\<^sub>s G Cs}
[PROOF STEP]
have "\<exists>c. wf_infpath c \<and> (\<forall>n. c n \<in> ?tree)"
[PROOF STATE]
proof (prove)
using this:
infinite {G. \<not> falsifies\<^sub>c\<^sub>s G Cs}
wf_tree {G. \<not> falsifies\<^sub>c\<^sub>s G Cs}

goal (1 subgoal):
 1. \<exists>c. wf_infpath c \<and> (\<forall>n. c n \<in> {G. \<not> falsifies\<^sub>c\<^sub>s G Cs})
[PROOF STEP]
using konig[of ?tree]
[PROOF STATE]
proof (prove)
using this:
infinite {G. \<not> falsifies\<^sub>c\<^sub>s G Cs}
wf_tree {G. \<not> falsifies\<^sub>c\<^sub>s G Cs}
\<lbrakk>infinite {G. \<not> falsifies\<^sub>c\<^sub>s G Cs}; wf_tree {G. \<not> falsifies\<^sub>c\<^sub>s G Cs}\<rbrakk> \<Longrightarrow> \<exists>c. wf_infpath c \<and> (\<forall>n. c n \<in> {G. \<not> falsifies\<^sub>c\<^sub>s G Cs})

goal (1 subgoal):
 1. \<exists>c. wf_infpath c \<and> (\<forall>n. c n \<in> {G. \<not> falsifies\<^sub>c\<^sub>s G Cs})
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>c. wf_infpath c \<and> (\<forall>n. c n \<in> {G. \<not> falsifies\<^sub>c\<^sub>s G Cs})

goal (1 subgoal):
 1. \<exists>G. eval\<^sub>c\<^sub>s HFun G Cs
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>c. wf_infpath c \<and> (\<forall>n. c n \<in> {G. \<not> falsifies\<^sub>c\<^sub>s G Cs})
[PROOF STEP]
have "\<exists>G. wf_infpath G \<and> (\<forall>n. \<not> falsifies\<^sub>c\<^sub>s (G n) Cs)"
[PROOF STATE]
proof (prove)
using this:
\<exists>c. wf_infpath c \<and> (\<forall>n. c n \<in> {G. \<not> falsifies\<^sub>c\<^sub>s G Cs})

goal (1 subgoal):
 1. \<exists>G. wf_infpath G \<and> (\<forall>n. \<not> falsifies\<^sub>c\<^sub>s (G n) Cs)
[PROOF STEP]
by auto
  \<comment> \<open>Apply above infpath lemma:\<close>
[PROOF STATE]
proof (state)
this:
\<exists>G. wf_infpath G \<and> (\<forall>n. \<not> falsifies\<^sub>c\<^sub>s (G n) Cs)

goal (1 subgoal):
 1. \<exists>G. eval\<^sub>c\<^sub>s HFun G Cs
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>G. wf_infpath G \<and> (\<forall>n. \<not> falsifies\<^sub>c\<^sub>s (G n) Cs)
[PROOF STEP]
show "\<exists>G. eval\<^sub>c\<^sub>s HFun G Cs"
[PROOF STATE]
proof (prove)
using this:
\<exists>G. wf_infpath G \<and> (\<forall>n. \<not> falsifies\<^sub>c\<^sub>s (G n) Cs)

goal (1 subgoal):
 1. \<exists>G. eval\<^sub>c\<^sub>s HFun G Cs
[PROOF STEP]
using infpath_model finite_cs
[PROOF STATE]
proof (prove)
using this:
\<exists>G. wf_infpath G \<and> (\<forall>n. \<not> falsifies\<^sub>c\<^sub>s (G n) Cs)
\<lbrakk>wf_infpath ?f; \<forall>n. \<not> falsifies\<^sub>c\<^sub>s (?f n) ?Cs; finite ?Cs; \<forall>C\<in>?Cs. finite C\<rbrakk> \<Longrightarrow> eval\<^sub>c\<^sub>s HFun (extend ?f) ?Cs
finite Cs
\<forall>C\<in>Cs. finite C

goal (1 subgoal):
 1. \<exists>G. eval\<^sub>c\<^sub>s HFun G Cs
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>G. eval\<^sub>c\<^sub>s HFun G Cs

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma shorter_falsifies\<^sub>l:
  assumes "falsifies\<^sub>l (ds@d) l"
  assumes "nat_of_fatom (get_atom l) < length ds"
  shows "falsifies\<^sub>l ds l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. falsifies\<^sub>l ds l
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. falsifies\<^sub>l ds l
[PROOF STEP]
let ?i = "nat_of_fatom (get_atom l)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. falsifies\<^sub>l ds l
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
falsifies\<^sub>l (ds @ d) l
nat_of_fatom (get_atom l) < length ds
[PROOF STEP]
have i_p: "ground\<^sub>l l \<and>  ?i < length (ds@d) \<and> (ds@d) ! ?i = (\<not>sign l)"
[PROOF STATE]
proof (prove)
using this:
falsifies\<^sub>l (ds @ d) l
nat_of_fatom (get_atom l) < length ds

goal (1 subgoal):
 1. ground\<^sub>l l \<and> nat_of_fatom (get_atom l) < length (ds @ d) \<and> (ds @ d) ! nat_of_fatom (get_atom l) = (\<not> sign l)
[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 (ds @ d) \<and> (ds @ d) ! i = (\<not> sign l))
nat_of_fatom (get_atom l) < length ds

goal (1 subgoal):
 1. ground\<^sub>l l \<and> nat_of_fatom (get_atom l) < length (ds @ d) \<and> (ds @ d) ! nat_of_fatom (get_atom l) = (\<not> sign l)
[PROOF STEP]
by meson
[PROOF STATE]
proof (state)
this:
ground\<^sub>l l \<and> nat_of_fatom (get_atom l) < length (ds @ d) \<and> (ds @ d) ! nat_of_fatom (get_atom l) = (\<not> sign l)

goal (1 subgoal):
 1. falsifies\<^sub>l ds l
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
ground\<^sub>l l \<and> nat_of_fatom (get_atom l) < length (ds @ d) \<and> (ds @ d) ! nat_of_fatom (get_atom l) = (\<not> sign l)

goal (1 subgoal):
 1. falsifies\<^sub>l ds l
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ground\<^sub>l l \<and> nat_of_fatom (get_atom l) < length (ds @ d) \<and> (ds @ d) ! nat_of_fatom (get_atom l) = (\<not> sign l)
[PROOF STEP]
have "?i < length ds"
[PROOF STATE]
proof (prove)
using this:
ground\<^sub>l l \<and> nat_of_fatom (get_atom l) < length (ds @ d) \<and> (ds @ d) ! nat_of_fatom (get_atom l) = (\<not> sign l)

goal (1 subgoal):
 1. nat_of_fatom (get_atom l) < length ds
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
ground\<^sub>l l \<and> nat_of_fatom (get_atom l) < length (ds @ d) \<and> (ds @ d) ! nat_of_fatom (get_atom l) = (\<not> sign l)
falsifies\<^sub>l (ds @ d) l
nat_of_fatom (get_atom l) < length ds

goal (1 subgoal):
 1. nat_of_fatom (get_atom l) < length ds
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nat_of_fatom (get_atom l) < length ds

goal (1 subgoal):
 1. falsifies\<^sub>l ds l
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
nat_of_fatom (get_atom l) < length ds

goal (1 subgoal):
 1. falsifies\<^sub>l ds l
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
nat_of_fatom (get_atom l) < length ds
[PROOF STEP]
have "ds ! ?i = (\<not>sign l)"
[PROOF STATE]
proof (prove)
using this:
nat_of_fatom (get_atom l) < length ds

goal (1 subgoal):
 1. ds ! nat_of_fatom (get_atom l) = (\<not> sign l)
[PROOF STEP]
using i_p nth_append[of ds d ?i]
[PROOF STATE]
proof (prove)
using this:
nat_of_fatom (get_atom l) < length ds
ground\<^sub>l l \<and> nat_of_fatom (get_atom l) < length (ds @ d) \<and> (ds @ d) ! nat_of_fatom (get_atom l) = (\<not> sign l)
(ds @ d) ! nat_of_fatom (get_atom l) = (if nat_of_fatom (get_atom l) < length ds then ds ! nat_of_fatom (get_atom l) else d ! (nat_of_fatom (get_atom l) - length ds))

goal (1 subgoal):
 1. ds ! nat_of_fatom (get_atom l) = (\<not> sign l)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ds ! nat_of_fatom (get_atom l) = (\<not> sign l)

goal (1 subgoal):
 1. falsifies\<^sub>l ds l
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
ground\<^sub>l l \<and> nat_of_fatom (get_atom l) < length (ds @ d) \<and> (ds @ d) ! nat_of_fatom (get_atom l) = (\<not> sign l)
nat_of_fatom (get_atom l) < length ds
ds ! nat_of_fatom (get_atom l) = (\<not> sign l)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
ground\<^sub>l l \<and> nat_of_fatom (get_atom l) < length (ds @ d) \<and> (ds @ d) ! nat_of_fatom (get_atom l) = (\<not> sign l)
nat_of_fatom (get_atom l) < length ds
ds ! nat_of_fatom (get_atom l) = (\<not> sign l)

goal (1 subgoal):
 1. falsifies\<^sub>l ds l
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
ground\<^sub>l l \<and> nat_of_fatom (get_atom l) < length (ds @ d) \<and> (ds @ d) ! nat_of_fatom (get_atom l) = (\<not> sign l)
nat_of_fatom (get_atom l) < length ds
ds ! nat_of_fatom (get_atom l) = (\<not> sign l)
falsifies\<^sub>l (ds @ d) l
nat_of_fatom (get_atom l) < length ds

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

goal (1 subgoal):
 1. ground\<^sub>l l \<and> (let i = nat_of_fatom (get_atom l) in i < length ds \<and> ds ! i = (\<not> sign l))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
falsifies\<^sub>l ds l

goal:
No subgoals!
[PROOF STEP]
qed