[STATEMENT]
lemma simple_resolution_sound:
  assumes C\<^sub>1sat:  "eval\<^sub>c F G C\<^sub>1"
  assumes C\<^sub>2sat:  "eval\<^sub>c F G C\<^sub>2"
  assumes l\<^sub>1inc\<^sub>1: "l\<^sub>1 \<in> C\<^sub>1"
  assumes l\<^sub>2inc\<^sub>2: "l\<^sub>2 \<in> C\<^sub>2"
  assumes comp: "l\<^sub>1\<^sup>c = l\<^sub>2"
  shows "eval\<^sub>c F G ((C\<^sub>1 - {l\<^sub>1}) \<union> (C\<^sub>2 - {l\<^sub>2}))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval\<^sub>c F G (C\<^sub>1 - {l\<^sub>1} \<union> (C\<^sub>2 - {l\<^sub>2}))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. eval\<^sub>c F G (C\<^sub>1 - {l\<^sub>1} \<union> (C\<^sub>2 - {l\<^sub>2}))
[PROOF STEP]
have "\<forall>E. \<exists>l \<in> (((C\<^sub>1 - {l\<^sub>1}) \<union> (C\<^sub>2 - {l\<^sub>2}))). eval\<^sub>l E F G l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>E. \<exists>l\<in>C\<^sub>1 - {l\<^sub>1} \<union> (C\<^sub>2 - {l\<^sub>2}). eval\<^sub>l E F G l
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>E. \<exists>l\<in>C\<^sub>1 - {l\<^sub>1} \<union> (C\<^sub>2 - {l\<^sub>2}). eval\<^sub>l E F G l
[PROOF STEP]
fix E
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>E. \<exists>l\<in>C\<^sub>1 - {l\<^sub>1} \<union> (C\<^sub>2 - {l\<^sub>2}). eval\<^sub>l E F G l
[PROOF STEP]
have "eval\<^sub>l E F G l\<^sub>1 \<or> eval\<^sub>l E F G l\<^sub>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval\<^sub>l E F G l\<^sub>1 \<or> eval\<^sub>l E F G l\<^sub>2
[PROOF STEP]
using comp
[PROOF STATE]
proof (prove)
using this:
l\<^sub>1\<^sup>c = l\<^sub>2

goal (1 subgoal):
 1. eval\<^sub>l E F G l\<^sub>1 \<or> eval\<^sub>l E F G l\<^sub>2
[PROOF STEP]
by (cases l\<^sub>1) auto
[PROOF STATE]
proof (state)
this:
eval\<^sub>l E F G l\<^sub>1 \<or> eval\<^sub>l E F G l\<^sub>2

goal (1 subgoal):
 1. \<And>E. \<exists>l\<in>C\<^sub>1 - {l\<^sub>1} \<union> (C\<^sub>2 - {l\<^sub>2}). eval\<^sub>l E F G l
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
eval\<^sub>l E F G l\<^sub>1 \<or> eval\<^sub>l E F G l\<^sub>2
[PROOF STEP]
show "\<exists>l \<in> (((C\<^sub>1 - {l\<^sub>1}) \<union> (C\<^sub>2 - {l\<^sub>2}))). eval\<^sub>l E F G l"
[PROOF STATE]
proof (prove)
using this:
eval\<^sub>l E F G l\<^sub>1 \<or> eval\<^sub>l E F G l\<^sub>2

goal (1 subgoal):
 1. \<exists>l\<in>C\<^sub>1 - {l\<^sub>1} \<union> (C\<^sub>2 - {l\<^sub>2}). eval\<^sub>l E F G l
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. eval\<^sub>l E F G l\<^sub>1 \<Longrightarrow> \<exists>l\<in>C\<^sub>1 - {l\<^sub>1} \<union> (C\<^sub>2 - {l\<^sub>2}). eval\<^sub>l E F G l
 2. eval\<^sub>l E F G l\<^sub>2 \<Longrightarrow> \<exists>l\<in>C\<^sub>1 - {l\<^sub>1} \<union> (C\<^sub>2 - {l\<^sub>2}). eval\<^sub>l E F G l
[PROOF STEP]
assume "eval\<^sub>l E F G l\<^sub>1"
[PROOF STATE]
proof (state)
this:
eval\<^sub>l E F G l\<^sub>1

goal (2 subgoals):
 1. eval\<^sub>l E F G l\<^sub>1 \<Longrightarrow> \<exists>l\<in>C\<^sub>1 - {l\<^sub>1} \<union> (C\<^sub>2 - {l\<^sub>2}). eval\<^sub>l E F G l
 2. eval\<^sub>l E F G l\<^sub>2 \<Longrightarrow> \<exists>l\<in>C\<^sub>1 - {l\<^sub>1} \<union> (C\<^sub>2 - {l\<^sub>2}). eval\<^sub>l E F G l
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
eval\<^sub>l E F G l\<^sub>1
[PROOF STEP]
have "\<not>eval\<^sub>l E F G l\<^sub>2"
[PROOF STATE]
proof (prove)
using this:
eval\<^sub>l E F G l\<^sub>1

goal (1 subgoal):
 1. \<not> eval\<^sub>l E F G l\<^sub>2
[PROOF STEP]
using comp
[PROOF STATE]
proof (prove)
using this:
eval\<^sub>l E F G l\<^sub>1
l\<^sub>1\<^sup>c = l\<^sub>2

goal (1 subgoal):
 1. \<not> eval\<^sub>l E F G l\<^sub>2
[PROOF STEP]
by (cases l\<^sub>1) auto
[PROOF STATE]
proof (state)
this:
\<not> eval\<^sub>l E F G l\<^sub>2

goal (2 subgoals):
 1. eval\<^sub>l E F G l\<^sub>1 \<Longrightarrow> \<exists>l\<in>C\<^sub>1 - {l\<^sub>1} \<union> (C\<^sub>2 - {l\<^sub>2}). eval\<^sub>l E F G l
 2. eval\<^sub>l E F G l\<^sub>2 \<Longrightarrow> \<exists>l\<in>C\<^sub>1 - {l\<^sub>1} \<union> (C\<^sub>2 - {l\<^sub>2}). eval\<^sub>l E F G l
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> eval\<^sub>l E F G l\<^sub>2
[PROOF STEP]
have "\<exists>l\<^sub>2'\<in> C\<^sub>2. l\<^sub>2' \<noteq> l\<^sub>2 \<and> eval\<^sub>l E F G l\<^sub>2'"
[PROOF STATE]
proof (prove)
using this:
\<not> eval\<^sub>l E F G l\<^sub>2

goal (1 subgoal):
 1. \<exists>l\<^sub>2'\<in>C\<^sub>2. l\<^sub>2' \<noteq> l\<^sub>2 \<and> eval\<^sub>l E F G l\<^sub>2'
[PROOF STEP]
using l\<^sub>2inc\<^sub>2 C\<^sub>2sat
[PROOF STATE]
proof (prove)
using this:
\<not> eval\<^sub>l E F G l\<^sub>2
l\<^sub>2 \<in> C\<^sub>2
eval\<^sub>c F G C\<^sub>2

goal (1 subgoal):
 1. \<exists>l\<^sub>2'\<in>C\<^sub>2. l\<^sub>2' \<noteq> l\<^sub>2 \<and> eval\<^sub>l E F G l\<^sub>2'
[PROOF STEP]
unfolding eval\<^sub>c_def
[PROOF STATE]
proof (prove)
using this:
\<not> eval\<^sub>l E F G l\<^sub>2
l\<^sub>2 \<in> C\<^sub>2
\<forall>E. Bex C\<^sub>2 (eval\<^sub>l E F G)

goal (1 subgoal):
 1. \<exists>l\<^sub>2'\<in>C\<^sub>2. l\<^sub>2' \<noteq> l\<^sub>2 \<and> eval\<^sub>l E F G l\<^sub>2'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>l\<^sub>2'\<in>C\<^sub>2. l\<^sub>2' \<noteq> l\<^sub>2 \<and> eval\<^sub>l E F G l\<^sub>2'

goal (2 subgoals):
 1. eval\<^sub>l E F G l\<^sub>1 \<Longrightarrow> \<exists>l\<in>C\<^sub>1 - {l\<^sub>1} \<union> (C\<^sub>2 - {l\<^sub>2}). eval\<^sub>l E F G l
 2. eval\<^sub>l E F G l\<^sub>2 \<Longrightarrow> \<exists>l\<in>C\<^sub>1 - {l\<^sub>1} \<union> (C\<^sub>2 - {l\<^sub>2}). eval\<^sub>l E F G l
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>l\<^sub>2'\<in>C\<^sub>2. l\<^sub>2' \<noteq> l\<^sub>2 \<and> eval\<^sub>l E F G l\<^sub>2'
[PROOF STEP]
show "\<exists>l\<in>(C\<^sub>1 - {l\<^sub>1}) \<union> (C\<^sub>2 - {l\<^sub>2}). eval\<^sub>l E F G l"
[PROOF STATE]
proof (prove)
using this:
\<exists>l\<^sub>2'\<in>C\<^sub>2. l\<^sub>2' \<noteq> l\<^sub>2 \<and> eval\<^sub>l E F G l\<^sub>2'

goal (1 subgoal):
 1. \<exists>l\<in>C\<^sub>1 - {l\<^sub>1} \<union> (C\<^sub>2 - {l\<^sub>2}). eval\<^sub>l E F G l
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>l\<in>C\<^sub>1 - {l\<^sub>1} \<union> (C\<^sub>2 - {l\<^sub>2}). eval\<^sub>l E F G l

goal (1 subgoal):
 1. eval\<^sub>l E F G l\<^sub>2 \<Longrightarrow> \<exists>l\<in>C\<^sub>1 - {l\<^sub>1} \<union> (C\<^sub>2 - {l\<^sub>2}). eval\<^sub>l E F G l
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. eval\<^sub>l E F G l\<^sub>2 \<Longrightarrow> \<exists>l\<in>C\<^sub>1 - {l\<^sub>1} \<union> (C\<^sub>2 - {l\<^sub>2}). eval\<^sub>l E F G l
[PROOF STEP]
assume "eval\<^sub>l E F G l\<^sub>2"
[PROOF STATE]
proof (state)
this:
eval\<^sub>l E F G l\<^sub>2

goal (1 subgoal):
 1. eval\<^sub>l E F G l\<^sub>2 \<Longrightarrow> \<exists>l\<in>C\<^sub>1 - {l\<^sub>1} \<union> (C\<^sub>2 - {l\<^sub>2}). eval\<^sub>l E F G l
[PROOF STEP]
(* Symmetric *)
[PROOF STATE]
proof (state)
this:
eval\<^sub>l E F G l\<^sub>2

goal (1 subgoal):
 1. eval\<^sub>l E F G l\<^sub>2 \<Longrightarrow> \<exists>l\<in>C\<^sub>1 - {l\<^sub>1} \<union> (C\<^sub>2 - {l\<^sub>2}). eval\<^sub>l E F G l
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
eval\<^sub>l E F G l\<^sub>2
[PROOF STEP]
have "\<not>eval\<^sub>l E F G l\<^sub>1"
[PROOF STATE]
proof (prove)
using this:
eval\<^sub>l E F G l\<^sub>2

goal (1 subgoal):
 1. \<not> eval\<^sub>l E F G l\<^sub>1
[PROOF STEP]
using comp
[PROOF STATE]
proof (prove)
using this:
eval\<^sub>l E F G l\<^sub>2
l\<^sub>1\<^sup>c = l\<^sub>2

goal (1 subgoal):
 1. \<not> eval\<^sub>l E F G l\<^sub>1
[PROOF STEP]
by (cases l\<^sub>1) auto
[PROOF STATE]
proof (state)
this:
\<not> eval\<^sub>l E F G l\<^sub>1

goal (1 subgoal):
 1. eval\<^sub>l E F G l\<^sub>2 \<Longrightarrow> \<exists>l\<in>C\<^sub>1 - {l\<^sub>1} \<union> (C\<^sub>2 - {l\<^sub>2}). eval\<^sub>l E F G l
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> eval\<^sub>l E F G l\<^sub>1
[PROOF STEP]
have "\<exists>l\<^sub>1'\<in> C\<^sub>1. l\<^sub>1' \<noteq> l\<^sub>1 \<and> eval\<^sub>l E F G l\<^sub>1'"
[PROOF STATE]
proof (prove)
using this:
\<not> eval\<^sub>l E F G l\<^sub>1

goal (1 subgoal):
 1. \<exists>l\<^sub>1'\<in>C\<^sub>1. l\<^sub>1' \<noteq> l\<^sub>1 \<and> eval\<^sub>l E F G l\<^sub>1'
[PROOF STEP]
using l\<^sub>1inc\<^sub>1 C\<^sub>1sat
[PROOF STATE]
proof (prove)
using this:
\<not> eval\<^sub>l E F G l\<^sub>1
l\<^sub>1 \<in> C\<^sub>1
eval\<^sub>c F G C\<^sub>1

goal (1 subgoal):
 1. \<exists>l\<^sub>1'\<in>C\<^sub>1. l\<^sub>1' \<noteq> l\<^sub>1 \<and> eval\<^sub>l E F G l\<^sub>1'
[PROOF STEP]
unfolding eval\<^sub>c_def
[PROOF STATE]
proof (prove)
using this:
\<not> eval\<^sub>l E F G l\<^sub>1
l\<^sub>1 \<in> C\<^sub>1
\<forall>E. Bex C\<^sub>1 (eval\<^sub>l E F G)

goal (1 subgoal):
 1. \<exists>l\<^sub>1'\<in>C\<^sub>1. l\<^sub>1' \<noteq> l\<^sub>1 \<and> eval\<^sub>l E F G l\<^sub>1'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>l\<^sub>1'\<in>C\<^sub>1. l\<^sub>1' \<noteq> l\<^sub>1 \<and> eval\<^sub>l E F G l\<^sub>1'

goal (1 subgoal):
 1. eval\<^sub>l E F G l\<^sub>2 \<Longrightarrow> \<exists>l\<in>C\<^sub>1 - {l\<^sub>1} \<union> (C\<^sub>2 - {l\<^sub>2}). eval\<^sub>l E F G l
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>l\<^sub>1'\<in>C\<^sub>1. l\<^sub>1' \<noteq> l\<^sub>1 \<and> eval\<^sub>l E F G l\<^sub>1'
[PROOF STEP]
show "\<exists>l\<in>(C\<^sub>1 - {l\<^sub>1}) \<union> (C\<^sub>2 - {l\<^sub>2}). eval\<^sub>l E F G l"
[PROOF STATE]
proof (prove)
using this:
\<exists>l\<^sub>1'\<in>C\<^sub>1. l\<^sub>1' \<noteq> l\<^sub>1 \<and> eval\<^sub>l E F G l\<^sub>1'

goal (1 subgoal):
 1. \<exists>l\<in>C\<^sub>1 - {l\<^sub>1} \<union> (C\<^sub>2 - {l\<^sub>2}). eval\<^sub>l E F G l
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>l\<in>C\<^sub>1 - {l\<^sub>1} \<union> (C\<^sub>2 - {l\<^sub>2}). eval\<^sub>l E F G l

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>l\<in>C\<^sub>1 - {l\<^sub>1} \<union> (C\<^sub>2 - {l\<^sub>2}). eval\<^sub>l E F G l

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>E. \<exists>l\<in>C\<^sub>1 - {l\<^sub>1} \<union> (C\<^sub>2 - {l\<^sub>2}). eval\<^sub>l E F G l

goal (1 subgoal):
 1. eval\<^sub>c F G (C\<^sub>1 - {l\<^sub>1} \<union> (C\<^sub>2 - {l\<^sub>2}))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>E. \<exists>l\<in>C\<^sub>1 - {l\<^sub>1} \<union> (C\<^sub>2 - {l\<^sub>2}). eval\<^sub>l E F G l
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>E. \<exists>l\<in>C\<^sub>1 - {l\<^sub>1} \<union> (C\<^sub>2 - {l\<^sub>2}). eval\<^sub>l E F G l

goal (1 subgoal):
 1. eval\<^sub>c F G (C\<^sub>1 - {l\<^sub>1} \<union> (C\<^sub>2 - {l\<^sub>2}))
[PROOF STEP]
unfolding eval\<^sub>c_def
[PROOF STATE]
proof (prove)
using this:
\<forall>E. \<exists>l\<in>C\<^sub>1 - {l\<^sub>1} \<union> (C\<^sub>2 - {l\<^sub>2}). eval\<^sub>l E F G l

goal (1 subgoal):
 1. \<forall>E. Bex (C\<^sub>1 - {l\<^sub>1} \<union> (C\<^sub>2 - {l\<^sub>2})) (eval\<^sub>l E F G)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
eval\<^sub>c F G (C\<^sub>1 - {l\<^sub>1} \<union> (C\<^sub>2 - {l\<^sub>2}))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mresolution_sound:
  assumes sat\<^sub>1: "eval\<^sub>c F G C\<^sub>1"
  assumes sat\<^sub>2: "eval\<^sub>c F G C\<^sub>2"
  assumes appl: "applicable C\<^sub>1 C\<^sub>2 L\<^sub>1 L\<^sub>2 \<sigma>"
  shows "eval\<^sub>c F G (mresolution C\<^sub>1 C\<^sub>2 L\<^sub>1 L\<^sub>2 \<sigma>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval\<^sub>c F G (mresolution C\<^sub>1 C\<^sub>2 L\<^sub>1 L\<^sub>2 \<sigma>)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. eval\<^sub>c F G (mresolution C\<^sub>1 C\<^sub>2 L\<^sub>1 L\<^sub>2 \<sigma>)
[PROOF STEP]
from sat\<^sub>1
[PROOF STATE]
proof (chain)
picking this:
eval\<^sub>c F G C\<^sub>1
[PROOF STEP]
have sat\<^sub>1\<sigma>: "eval\<^sub>c F G (C\<^sub>1 \<cdot>\<^sub>l\<^sub>s \<sigma>)"
[PROOF STATE]
proof (prove)
using this:
eval\<^sub>c F G C\<^sub>1

goal (1 subgoal):
 1. eval\<^sub>c F G (C\<^sub>1 \<cdot>\<^sub>l\<^sub>s \<sigma>)
[PROOF STEP]
using subst_sound
[PROOF STATE]
proof (prove)
using this:
eval\<^sub>c F G C\<^sub>1
eval\<^sub>c ?F ?G ?C \<Longrightarrow> eval\<^sub>c ?F ?G (?C \<cdot>\<^sub>l\<^sub>s ?\<sigma>)

goal (1 subgoal):
 1. eval\<^sub>c F G (C\<^sub>1 \<cdot>\<^sub>l\<^sub>s \<sigma>)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
eval\<^sub>c F G (C\<^sub>1 \<cdot>\<^sub>l\<^sub>s \<sigma>)

goal (1 subgoal):
 1. eval\<^sub>c F G (mresolution C\<^sub>1 C\<^sub>2 L\<^sub>1 L\<^sub>2 \<sigma>)
[PROOF STEP]
from sat\<^sub>2
[PROOF STATE]
proof (chain)
picking this:
eval\<^sub>c F G C\<^sub>2
[PROOF STEP]
have sat\<^sub>2\<sigma>: "eval\<^sub>c F G (C\<^sub>2 \<cdot>\<^sub>l\<^sub>s \<sigma>)"
[PROOF STATE]
proof (prove)
using this:
eval\<^sub>c F G C\<^sub>2

goal (1 subgoal):
 1. eval\<^sub>c F G (C\<^sub>2 \<cdot>\<^sub>l\<^sub>s \<sigma>)
[PROOF STEP]
using subst_sound
[PROOF STATE]
proof (prove)
using this:
eval\<^sub>c F G C\<^sub>2
eval\<^sub>c ?F ?G ?C \<Longrightarrow> eval\<^sub>c ?F ?G (?C \<cdot>\<^sub>l\<^sub>s ?\<sigma>)

goal (1 subgoal):
 1. eval\<^sub>c F G (C\<^sub>2 \<cdot>\<^sub>l\<^sub>s \<sigma>)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
eval\<^sub>c F G (C\<^sub>2 \<cdot>\<^sub>l\<^sub>s \<sigma>)

goal (1 subgoal):
 1. eval\<^sub>c F G (mresolution C\<^sub>1 C\<^sub>2 L\<^sub>1 L\<^sub>2 \<sigma>)
[PROOF STEP]
from appl
[PROOF STATE]
proof (chain)
picking this:
applicable C\<^sub>1 C\<^sub>2 L\<^sub>1 L\<^sub>2 \<sigma>
[PROOF STEP]
obtain l\<^sub>1 where l\<^sub>1_p: "l\<^sub>1 \<in> L\<^sub>1"
[PROOF STATE]
proof (prove)
using this:
applicable C\<^sub>1 C\<^sub>2 L\<^sub>1 L\<^sub>2 \<sigma>

goal (1 subgoal):
 1. (\<And>l\<^sub>1. l\<^sub>1 \<in> L\<^sub>1 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding applicable_def
[PROOF STATE]
proof (prove)
using this:
C\<^sub>1 \<noteq> {} \<and> C\<^sub>2 \<noteq> {} \<and> L\<^sub>1 \<noteq> {} \<and> L\<^sub>2 \<noteq> {} \<and> vars\<^sub>l\<^sub>s C\<^sub>1 \<inter> vars\<^sub>l\<^sub>s C\<^sub>2 = {} \<and> L\<^sub>1 \<subseteq> C\<^sub>1 \<and> L\<^sub>2 \<subseteq> C\<^sub>2 \<and> mgu\<^sub>l\<^sub>s \<sigma> (L\<^sub>1 \<union> L\<^sub>2\<^sup>C)

goal (1 subgoal):
 1. (\<And>l\<^sub>1. l\<^sub>1 \<in> L\<^sub>1 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
l\<^sub>1 \<in> L\<^sub>1

goal (1 subgoal):
 1. eval\<^sub>c F G (mresolution C\<^sub>1 C\<^sub>2 L\<^sub>1 L\<^sub>2 \<sigma>)
[PROOF STEP]
from l\<^sub>1_p appl
[PROOF STATE]
proof (chain)
picking this:
l\<^sub>1 \<in> L\<^sub>1
applicable C\<^sub>1 C\<^sub>2 L\<^sub>1 L\<^sub>2 \<sigma>
[PROOF STEP]
have "l\<^sub>1 \<in> C\<^sub>1"
[PROOF STATE]
proof (prove)
using this:
l\<^sub>1 \<in> L\<^sub>1
applicable C\<^sub>1 C\<^sub>2 L\<^sub>1 L\<^sub>2 \<sigma>

goal (1 subgoal):
 1. l\<^sub>1 \<in> C\<^sub>1
[PROOF STEP]
unfolding applicable_def
[PROOF STATE]
proof (prove)
using this:
l\<^sub>1 \<in> L\<^sub>1
C\<^sub>1 \<noteq> {} \<and> C\<^sub>2 \<noteq> {} \<and> L\<^sub>1 \<noteq> {} \<and> L\<^sub>2 \<noteq> {} \<and> vars\<^sub>l\<^sub>s C\<^sub>1 \<inter> vars\<^sub>l\<^sub>s C\<^sub>2 = {} \<and> L\<^sub>1 \<subseteq> C\<^sub>1 \<and> L\<^sub>2 \<subseteq> C\<^sub>2 \<and> mgu\<^sub>l\<^sub>s \<sigma> (L\<^sub>1 \<union> L\<^sub>2\<^sup>C)

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

goal (1 subgoal):
 1. eval\<^sub>c F G (mresolution C\<^sub>1 C\<^sub>2 L\<^sub>1 L\<^sub>2 \<sigma>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
l\<^sub>1 \<in> C\<^sub>1
[PROOF STEP]
have inc\<^sub>1\<sigma>: "l\<^sub>1 \<cdot>\<^sub>l \<sigma> \<in> C\<^sub>1 \<cdot>\<^sub>l\<^sub>s \<sigma>"
[PROOF STATE]
proof (prove)
using this:
l\<^sub>1 \<in> C\<^sub>1

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

goal (1 subgoal):
 1. eval\<^sub>c F G (mresolution C\<^sub>1 C\<^sub>2 L\<^sub>1 L\<^sub>2 \<sigma>)
[PROOF STEP]
from l\<^sub>1_p
[PROOF STATE]
proof (chain)
picking this:
l\<^sub>1 \<in> L\<^sub>1
[PROOF STEP]
have unified\<^sub>1: "l\<^sub>1 \<in> (L\<^sub>1 \<union> (L\<^sub>2\<^sup>C))"
[PROOF STATE]
proof (prove)
using this:
l\<^sub>1 \<in> L\<^sub>1

goal (1 subgoal):
 1. l\<^sub>1 \<in> L\<^sub>1 \<union> L\<^sub>2\<^sup>C
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
l\<^sub>1 \<in> L\<^sub>1 \<union> L\<^sub>2\<^sup>C

goal (1 subgoal):
 1. eval\<^sub>c F G (mresolution C\<^sub>1 C\<^sub>2 L\<^sub>1 L\<^sub>2 \<sigma>)
[PROOF STEP]
from l\<^sub>1_p appl
[PROOF STATE]
proof (chain)
picking this:
l\<^sub>1 \<in> L\<^sub>1
applicable C\<^sub>1 C\<^sub>2 L\<^sub>1 L\<^sub>2 \<sigma>
[PROOF STEP]
have l\<^sub>1\<sigma>isl\<^sub>1\<sigma>: "{l\<^sub>1 \<cdot>\<^sub>l \<sigma>} = L\<^sub>1 \<cdot>\<^sub>l\<^sub>s \<sigma>"
[PROOF STATE]
proof (prove)
using this:
l\<^sub>1 \<in> L\<^sub>1
applicable C\<^sub>1 C\<^sub>2 L\<^sub>1 L\<^sub>2 \<sigma>

goal (1 subgoal):
 1. {l\<^sub>1 \<cdot>\<^sub>l \<sigma>} = L\<^sub>1 \<cdot>\<^sub>l\<^sub>s \<sigma>
[PROOF STEP]
unfolding mgu\<^sub>l\<^sub>s_def unifier\<^sub>l\<^sub>s_def applicable_def
[PROOF STATE]
proof (prove)
using this:
l\<^sub>1 \<in> L\<^sub>1
C\<^sub>1 \<noteq> {} \<and> C\<^sub>2 \<noteq> {} \<and> L\<^sub>1 \<noteq> {} \<and> L\<^sub>2 \<noteq> {} \<and> vars\<^sub>l\<^sub>s C\<^sub>1 \<inter> vars\<^sub>l\<^sub>s C\<^sub>2 = {} \<and> L\<^sub>1 \<subseteq> C\<^sub>1 \<and> L\<^sub>2 \<subseteq> C\<^sub>2 \<and> (\<exists>l'. \<forall>l\<in>L\<^sub>1 \<union> L\<^sub>2\<^sup>C. l \<cdot>\<^sub>l \<sigma> = l') \<and> (\<forall>u. (\<exists>l'. \<forall>l\<in>L\<^sub>1 \<union> L\<^sub>2\<^sup>C. l \<cdot>\<^sub>l u = l') \<longrightarrow> (\<exists>i. u = \<sigma> \<cdot> i))

goal (1 subgoal):
 1. {l\<^sub>1 \<cdot>\<^sub>l \<sigma>} = L\<^sub>1 \<cdot>\<^sub>l\<^sub>s \<sigma>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{l\<^sub>1 \<cdot>\<^sub>l \<sigma>} = L\<^sub>1 \<cdot>\<^sub>l\<^sub>s \<sigma>

goal (1 subgoal):
 1. eval\<^sub>c F G (mresolution C\<^sub>1 C\<^sub>2 L\<^sub>1 L\<^sub>2 \<sigma>)
[PROOF STEP]
from appl
[PROOF STATE]
proof (chain)
picking this:
applicable C\<^sub>1 C\<^sub>2 L\<^sub>1 L\<^sub>2 \<sigma>
[PROOF STEP]
obtain l\<^sub>2 where l\<^sub>2_p: "l\<^sub>2 \<in> L\<^sub>2"
[PROOF STATE]
proof (prove)
using this:
applicable C\<^sub>1 C\<^sub>2 L\<^sub>1 L\<^sub>2 \<sigma>

goal (1 subgoal):
 1. (\<And>l\<^sub>2. l\<^sub>2 \<in> L\<^sub>2 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding applicable_def
[PROOF STATE]
proof (prove)
using this:
C\<^sub>1 \<noteq> {} \<and> C\<^sub>2 \<noteq> {} \<and> L\<^sub>1 \<noteq> {} \<and> L\<^sub>2 \<noteq> {} \<and> vars\<^sub>l\<^sub>s C\<^sub>1 \<inter> vars\<^sub>l\<^sub>s C\<^sub>2 = {} \<and> L\<^sub>1 \<subseteq> C\<^sub>1 \<and> L\<^sub>2 \<subseteq> C\<^sub>2 \<and> mgu\<^sub>l\<^sub>s \<sigma> (L\<^sub>1 \<union> L\<^sub>2\<^sup>C)

goal (1 subgoal):
 1. (\<And>l\<^sub>2. l\<^sub>2 \<in> L\<^sub>2 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
l\<^sub>2 \<in> L\<^sub>2

goal (1 subgoal):
 1. eval\<^sub>c F G (mresolution C\<^sub>1 C\<^sub>2 L\<^sub>1 L\<^sub>2 \<sigma>)
[PROOF STEP]
from l\<^sub>2_p appl
[PROOF STATE]
proof (chain)
picking this:
l\<^sub>2 \<in> L\<^sub>2
applicable C\<^sub>1 C\<^sub>2 L\<^sub>1 L\<^sub>2 \<sigma>
[PROOF STEP]
have "l\<^sub>2 \<in> C\<^sub>2"
[PROOF STATE]
proof (prove)
using this:
l\<^sub>2 \<in> L\<^sub>2
applicable C\<^sub>1 C\<^sub>2 L\<^sub>1 L\<^sub>2 \<sigma>

goal (1 subgoal):
 1. l\<^sub>2 \<in> C\<^sub>2
[PROOF STEP]
unfolding applicable_def
[PROOF STATE]
proof (prove)
using this:
l\<^sub>2 \<in> L\<^sub>2
C\<^sub>1 \<noteq> {} \<and> C\<^sub>2 \<noteq> {} \<and> L\<^sub>1 \<noteq> {} \<and> L\<^sub>2 \<noteq> {} \<and> vars\<^sub>l\<^sub>s C\<^sub>1 \<inter> vars\<^sub>l\<^sub>s C\<^sub>2 = {} \<and> L\<^sub>1 \<subseteq> C\<^sub>1 \<and> L\<^sub>2 \<subseteq> C\<^sub>2 \<and> mgu\<^sub>l\<^sub>s \<sigma> (L\<^sub>1 \<union> L\<^sub>2\<^sup>C)

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

goal (1 subgoal):
 1. eval\<^sub>c F G (mresolution C\<^sub>1 C\<^sub>2 L\<^sub>1 L\<^sub>2 \<sigma>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
l\<^sub>2 \<in> C\<^sub>2
[PROOF STEP]
have inc\<^sub>2\<sigma>: "l\<^sub>2 \<cdot>\<^sub>l \<sigma> \<in> C\<^sub>2 \<cdot>\<^sub>l\<^sub>s \<sigma>"
[PROOF STATE]
proof (prove)
using this:
l\<^sub>2 \<in> C\<^sub>2

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

goal (1 subgoal):
 1. eval\<^sub>c F G (mresolution C\<^sub>1 C\<^sub>2 L\<^sub>1 L\<^sub>2 \<sigma>)
[PROOF STEP]
from l\<^sub>2_p
[PROOF STATE]
proof (chain)
picking this:
l\<^sub>2 \<in> L\<^sub>2
[PROOF STEP]
have unified\<^sub>2: "l\<^sub>2\<^sup>c \<in> (L\<^sub>1 \<union> (L\<^sub>2\<^sup>C))"
[PROOF STATE]
proof (prove)
using this:
l\<^sub>2 \<in> L\<^sub>2

goal (1 subgoal):
 1. l\<^sub>2\<^sup>c \<in> L\<^sub>1 \<union> L\<^sub>2\<^sup>C
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
l\<^sub>2\<^sup>c \<in> L\<^sub>1 \<union> L\<^sub>2\<^sup>C

goal (1 subgoal):
 1. eval\<^sub>c F G (mresolution C\<^sub>1 C\<^sub>2 L\<^sub>1 L\<^sub>2 \<sigma>)
[PROOF STEP]
from unified\<^sub>1 unified\<^sub>2 appl
[PROOF STATE]
proof (chain)
picking this:
l\<^sub>1 \<in> L\<^sub>1 \<union> L\<^sub>2\<^sup>C
l\<^sub>2\<^sup>c \<in> L\<^sub>1 \<union> L\<^sub>2\<^sup>C
applicable C\<^sub>1 C\<^sub>2 L\<^sub>1 L\<^sub>2 \<sigma>
[PROOF STEP]
have "l\<^sub>1 \<cdot>\<^sub>l \<sigma> = (l\<^sub>2\<^sup>c) \<cdot>\<^sub>l \<sigma>"
[PROOF STATE]
proof (prove)
using this:
l\<^sub>1 \<in> L\<^sub>1 \<union> L\<^sub>2\<^sup>C
l\<^sub>2\<^sup>c \<in> L\<^sub>1 \<union> L\<^sub>2\<^sup>C
applicable C\<^sub>1 C\<^sub>2 L\<^sub>1 L\<^sub>2 \<sigma>

goal (1 subgoal):
 1. l\<^sub>1 \<cdot>\<^sub>l \<sigma> = l\<^sub>2\<^sup>c \<cdot>\<^sub>l \<sigma>
[PROOF STEP]
unfolding mgu\<^sub>l\<^sub>s_def unifier\<^sub>l\<^sub>s_def applicable_def
[PROOF STATE]
proof (prove)
using this:
l\<^sub>1 \<in> L\<^sub>1 \<union> L\<^sub>2\<^sup>C
l\<^sub>2\<^sup>c \<in> L\<^sub>1 \<union> L\<^sub>2\<^sup>C
C\<^sub>1 \<noteq> {} \<and> C\<^sub>2 \<noteq> {} \<and> L\<^sub>1 \<noteq> {} \<and> L\<^sub>2 \<noteq> {} \<and> vars\<^sub>l\<^sub>s C\<^sub>1 \<inter> vars\<^sub>l\<^sub>s C\<^sub>2 = {} \<and> L\<^sub>1 \<subseteq> C\<^sub>1 \<and> L\<^sub>2 \<subseteq> C\<^sub>2 \<and> (\<exists>l'. \<forall>l\<in>L\<^sub>1 \<union> L\<^sub>2\<^sup>C. l \<cdot>\<^sub>l \<sigma> = l') \<and> (\<forall>u. (\<exists>l'. \<forall>l\<in>L\<^sub>1 \<union> L\<^sub>2\<^sup>C. l \<cdot>\<^sub>l u = l') \<longrightarrow> (\<exists>i. u = \<sigma> \<cdot> i))

goal (1 subgoal):
 1. l\<^sub>1 \<cdot>\<^sub>l \<sigma> = l\<^sub>2\<^sup>c \<cdot>\<^sub>l \<sigma>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
l\<^sub>1 \<cdot>\<^sub>l \<sigma> = l\<^sub>2\<^sup>c \<cdot>\<^sub>l \<sigma>

goal (1 subgoal):
 1. eval\<^sub>c F G (mresolution C\<^sub>1 C\<^sub>2 L\<^sub>1 L\<^sub>2 \<sigma>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
l\<^sub>1 \<cdot>\<^sub>l \<sigma> = l\<^sub>2\<^sup>c \<cdot>\<^sub>l \<sigma>
[PROOF STEP]
have comp: "(l\<^sub>1 \<cdot>\<^sub>l \<sigma>)\<^sup>c = l\<^sub>2 \<cdot>\<^sub>l \<sigma>"
[PROOF STATE]
proof (prove)
using this:
l\<^sub>1 \<cdot>\<^sub>l \<sigma> = l\<^sub>2\<^sup>c \<cdot>\<^sub>l \<sigma>

goal (1 subgoal):
 1. (l\<^sub>1 \<cdot>\<^sub>l \<sigma>)\<^sup>c = l\<^sub>2 \<cdot>\<^sub>l \<sigma>
[PROOF STEP]
using comp_sub comp_swap
[PROOF STATE]
proof (prove)
using this:
l\<^sub>1 \<cdot>\<^sub>l \<sigma> = l\<^sub>2\<^sup>c \<cdot>\<^sub>l \<sigma>
?l\<^sup>c \<cdot>\<^sub>l ?\<sigma> = (?l \<cdot>\<^sub>l ?\<sigma>)\<^sup>c
(?l\<^sub>1\<^sup>c = ?l\<^sub>2) = (?l\<^sub>1 = ?l\<^sub>2\<^sup>c)

goal (1 subgoal):
 1. (l\<^sub>1 \<cdot>\<^sub>l \<sigma>)\<^sup>c = l\<^sub>2 \<cdot>\<^sub>l \<sigma>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(l\<^sub>1 \<cdot>\<^sub>l \<sigma>)\<^sup>c = l\<^sub>2 \<cdot>\<^sub>l \<sigma>

goal (1 subgoal):
 1. eval\<^sub>c F G (mresolution C\<^sub>1 C\<^sub>2 L\<^sub>1 L\<^sub>2 \<sigma>)
[PROOF STEP]
from appl
[PROOF STATE]
proof (chain)
picking this:
applicable C\<^sub>1 C\<^sub>2 L\<^sub>1 L\<^sub>2 \<sigma>
[PROOF STEP]
have "unifier\<^sub>l\<^sub>s \<sigma> (L\<^sub>2\<^sup>C)"
[PROOF STATE]
proof (prove)
using this:
applicable C\<^sub>1 C\<^sub>2 L\<^sub>1 L\<^sub>2 \<sigma>

goal (1 subgoal):
 1. unifier\<^sub>l\<^sub>s \<sigma> (L\<^sub>2\<^sup>C)
[PROOF STEP]
using unifier_sub2
[PROOF STATE]
proof (prove)
using this:
applicable C\<^sub>1 C\<^sub>2 L\<^sub>1 L\<^sub>2 \<sigma>
unifier\<^sub>l\<^sub>s ?\<sigma> (?L\<^sub>1 \<union> ?L\<^sub>2) \<Longrightarrow> unifier\<^sub>l\<^sub>s ?\<sigma> ?L\<^sub>1 \<and> unifier\<^sub>l\<^sub>s ?\<sigma> ?L\<^sub>2

goal (1 subgoal):
 1. unifier\<^sub>l\<^sub>s \<sigma> (L\<^sub>2\<^sup>C)
[PROOF STEP]
unfolding mgu\<^sub>l\<^sub>s_def applicable_def
[PROOF STATE]
proof (prove)
using this:
C\<^sub>1 \<noteq> {} \<and> C\<^sub>2 \<noteq> {} \<and> L\<^sub>1 \<noteq> {} \<and> L\<^sub>2 \<noteq> {} \<and> vars\<^sub>l\<^sub>s C\<^sub>1 \<inter> vars\<^sub>l\<^sub>s C\<^sub>2 = {} \<and> L\<^sub>1 \<subseteq> C\<^sub>1 \<and> L\<^sub>2 \<subseteq> C\<^sub>2 \<and> unifier\<^sub>l\<^sub>s \<sigma> (L\<^sub>1 \<union> L\<^sub>2\<^sup>C) \<and> (\<forall>u. unifier\<^sub>l\<^sub>s u (L\<^sub>1 \<union> L\<^sub>2\<^sup>C) \<longrightarrow> (\<exists>i. u = \<sigma> \<cdot> i))
unifier\<^sub>l\<^sub>s ?\<sigma> (?L\<^sub>1 \<union> ?L\<^sub>2) \<Longrightarrow> unifier\<^sub>l\<^sub>s ?\<sigma> ?L\<^sub>1 \<and> unifier\<^sub>l\<^sub>s ?\<sigma> ?L\<^sub>2

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

goal (1 subgoal):
 1. eval\<^sub>c F G (mresolution C\<^sub>1 C\<^sub>2 L\<^sub>1 L\<^sub>2 \<sigma>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
unifier\<^sub>l\<^sub>s \<sigma> (L\<^sub>2\<^sup>C)
[PROOF STEP]
have "unifier\<^sub>l\<^sub>s \<sigma> L\<^sub>2"
[PROOF STATE]
proof (prove)
using this:
unifier\<^sub>l\<^sub>s \<sigma> (L\<^sub>2\<^sup>C)

goal (1 subgoal):
 1. unifier\<^sub>l\<^sub>s \<sigma> L\<^sub>2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
unifier\<^sub>l\<^sub>s \<sigma> L\<^sub>2

goal (1 subgoal):
 1. eval\<^sub>c F G (mresolution C\<^sub>1 C\<^sub>2 L\<^sub>1 L\<^sub>2 \<sigma>)
[PROOF STEP]
from this l\<^sub>2_p
[PROOF STATE]
proof (chain)
picking this:
unifier\<^sub>l\<^sub>s \<sigma> L\<^sub>2
l\<^sub>2 \<in> L\<^sub>2
[PROOF STEP]
have l\<^sub>2\<sigma>isl\<^sub>2\<sigma>: "{l\<^sub>2 \<cdot>\<^sub>l \<sigma>} = L\<^sub>2 \<cdot>\<^sub>l\<^sub>s \<sigma>"
[PROOF STATE]
proof (prove)
using this:
unifier\<^sub>l\<^sub>s \<sigma> L\<^sub>2
l\<^sub>2 \<in> L\<^sub>2

goal (1 subgoal):
 1. {l\<^sub>2 \<cdot>\<^sub>l \<sigma>} = L\<^sub>2 \<cdot>\<^sub>l\<^sub>s \<sigma>
[PROOF STEP]
unfolding unifier\<^sub>l\<^sub>s_def
[PROOF STATE]
proof (prove)
using this:
\<exists>l'. \<forall>l\<in>L\<^sub>2. l \<cdot>\<^sub>l \<sigma> = l'
l\<^sub>2 \<in> L\<^sub>2

goal (1 subgoal):
 1. {l\<^sub>2 \<cdot>\<^sub>l \<sigma>} = L\<^sub>2 \<cdot>\<^sub>l\<^sub>s \<sigma>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{l\<^sub>2 \<cdot>\<^sub>l \<sigma>} = L\<^sub>2 \<cdot>\<^sub>l\<^sub>s \<sigma>

goal (1 subgoal):
 1. eval\<^sub>c F G (mresolution C\<^sub>1 C\<^sub>2 L\<^sub>1 L\<^sub>2 \<sigma>)
[PROOF STEP]
from sat\<^sub>1\<sigma> sat\<^sub>2\<sigma> inc\<^sub>1\<sigma> inc\<^sub>2\<sigma> comp
[PROOF STATE]
proof (chain)
picking this:
eval\<^sub>c F G (C\<^sub>1 \<cdot>\<^sub>l\<^sub>s \<sigma>)
eval\<^sub>c F G (C\<^sub>2 \<cdot>\<^sub>l\<^sub>s \<sigma>)
l\<^sub>1 \<cdot>\<^sub>l \<sigma> \<in> C\<^sub>1 \<cdot>\<^sub>l\<^sub>s \<sigma>
l\<^sub>2 \<cdot>\<^sub>l \<sigma> \<in> C\<^sub>2 \<cdot>\<^sub>l\<^sub>s \<sigma>
(l\<^sub>1 \<cdot>\<^sub>l \<sigma>)\<^sup>c = l\<^sub>2 \<cdot>\<^sub>l \<sigma>
[PROOF STEP]
have "eval\<^sub>c F G ((C\<^sub>1 \<cdot>\<^sub>l\<^sub>s \<sigma>) - {l\<^sub>1 \<cdot>\<^sub>l \<sigma>} \<union> ((C\<^sub>2 \<cdot>\<^sub>l\<^sub>s \<sigma>) - {l\<^sub>2 \<cdot>\<^sub>l \<sigma>}))"
[PROOF STATE]
proof (prove)
using this:
eval\<^sub>c F G (C\<^sub>1 \<cdot>\<^sub>l\<^sub>s \<sigma>)
eval\<^sub>c F G (C\<^sub>2 \<cdot>\<^sub>l\<^sub>s \<sigma>)
l\<^sub>1 \<cdot>\<^sub>l \<sigma> \<in> C\<^sub>1 \<cdot>\<^sub>l\<^sub>s \<sigma>
l\<^sub>2 \<cdot>\<^sub>l \<sigma> \<in> C\<^sub>2 \<cdot>\<^sub>l\<^sub>s \<sigma>
(l\<^sub>1 \<cdot>\<^sub>l \<sigma>)\<^sup>c = l\<^sub>2 \<cdot>\<^sub>l \<sigma>

goal (1 subgoal):
 1. eval\<^sub>c F G ((C\<^sub>1 \<cdot>\<^sub>l\<^sub>s \<sigma>) - {l\<^sub>1 \<cdot>\<^sub>l \<sigma>} \<union> ((C\<^sub>2 \<cdot>\<^sub>l\<^sub>s \<sigma>) - {l\<^sub>2 \<cdot>\<^sub>l \<sigma>}))
[PROOF STEP]
using simple_resolution_sound[of F G "C\<^sub>1 \<cdot>\<^sub>l\<^sub>s \<sigma>" "C\<^sub>2 \<cdot>\<^sub>l\<^sub>s \<sigma>" "l\<^sub>1 \<cdot>\<^sub>l \<sigma>" " l\<^sub>2 \<cdot>\<^sub>l \<sigma>"]
[PROOF STATE]
proof (prove)
using this:
eval\<^sub>c F G (C\<^sub>1 \<cdot>\<^sub>l\<^sub>s \<sigma>)
eval\<^sub>c F G (C\<^sub>2 \<cdot>\<^sub>l\<^sub>s \<sigma>)
l\<^sub>1 \<cdot>\<^sub>l \<sigma> \<in> C\<^sub>1 \<cdot>\<^sub>l\<^sub>s \<sigma>
l\<^sub>2 \<cdot>\<^sub>l \<sigma> \<in> C\<^sub>2 \<cdot>\<^sub>l\<^sub>s \<sigma>
(l\<^sub>1 \<cdot>\<^sub>l \<sigma>)\<^sup>c = l\<^sub>2 \<cdot>\<^sub>l \<sigma>
\<lbrakk>eval\<^sub>c F G (C\<^sub>1 \<cdot>\<^sub>l\<^sub>s \<sigma>); eval\<^sub>c F G (C\<^sub>2 \<cdot>\<^sub>l\<^sub>s \<sigma>); l\<^sub>1 \<cdot>\<^sub>l \<sigma> \<in> C\<^sub>1 \<cdot>\<^sub>l\<^sub>s \<sigma>; l\<^sub>2 \<cdot>\<^sub>l \<sigma> \<in> C\<^sub>2 \<cdot>\<^sub>l\<^sub>s \<sigma>; (l\<^sub>1 \<cdot>\<^sub>l \<sigma>)\<^sup>c = l\<^sub>2 \<cdot>\<^sub>l \<sigma>\<rbrakk> \<Longrightarrow> eval\<^sub>c F G ((C\<^sub>1 \<cdot>\<^sub>l\<^sub>s \<sigma>) - {l\<^sub>1 \<cdot>\<^sub>l \<sigma>} \<union> ((C\<^sub>2 \<cdot>\<^sub>l\<^sub>s \<sigma>) - {l\<^sub>2 \<cdot>\<^sub>l \<sigma>}))

goal (1 subgoal):
 1. eval\<^sub>c F G ((C\<^sub>1 \<cdot>\<^sub>l\<^sub>s \<sigma>) - {l\<^sub>1 \<cdot>\<^sub>l \<sigma>} \<union> ((C\<^sub>2 \<cdot>\<^sub>l\<^sub>s \<sigma>) - {l\<^sub>2 \<cdot>\<^sub>l \<sigma>}))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
eval\<^sub>c F G ((C\<^sub>1 \<cdot>\<^sub>l\<^sub>s \<sigma>) - {l\<^sub>1 \<cdot>\<^sub>l \<sigma>} \<union> ((C\<^sub>2 \<cdot>\<^sub>l\<^sub>s \<sigma>) - {l\<^sub>2 \<cdot>\<^sub>l \<sigma>}))

goal (1 subgoal):
 1. eval\<^sub>c F G (mresolution C\<^sub>1 C\<^sub>2 L\<^sub>1 L\<^sub>2 \<sigma>)
[PROOF STEP]
from this l\<^sub>1\<sigma>isl\<^sub>1\<sigma> l\<^sub>2\<sigma>isl\<^sub>2\<sigma>
[PROOF STATE]
proof (chain)
picking this:
eval\<^sub>c F G ((C\<^sub>1 \<cdot>\<^sub>l\<^sub>s \<sigma>) - {l\<^sub>1 \<cdot>\<^sub>l \<sigma>} \<union> ((C\<^sub>2 \<cdot>\<^sub>l\<^sub>s \<sigma>) - {l\<^sub>2 \<cdot>\<^sub>l \<sigma>}))
{l\<^sub>1 \<cdot>\<^sub>l \<sigma>} = L\<^sub>1 \<cdot>\<^sub>l\<^sub>s \<sigma>
{l\<^sub>2 \<cdot>\<^sub>l \<sigma>} = L\<^sub>2 \<cdot>\<^sub>l\<^sub>s \<sigma>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
eval\<^sub>c F G ((C\<^sub>1 \<cdot>\<^sub>l\<^sub>s \<sigma>) - {l\<^sub>1 \<cdot>\<^sub>l \<sigma>} \<union> ((C\<^sub>2 \<cdot>\<^sub>l\<^sub>s \<sigma>) - {l\<^sub>2 \<cdot>\<^sub>l \<sigma>}))
{l\<^sub>1 \<cdot>\<^sub>l \<sigma>} = L\<^sub>1 \<cdot>\<^sub>l\<^sub>s \<sigma>
{l\<^sub>2 \<cdot>\<^sub>l \<sigma>} = L\<^sub>2 \<cdot>\<^sub>l\<^sub>s \<sigma>

goal (1 subgoal):
 1. eval\<^sub>c F G (mresolution C\<^sub>1 C\<^sub>2 L\<^sub>1 L\<^sub>2 \<sigma>)
[PROOF STEP]
unfolding mresolution_def
[PROOF STATE]
proof (prove)
using this:
eval\<^sub>c F G ((C\<^sub>1 \<cdot>\<^sub>l\<^sub>s \<sigma>) - {l\<^sub>1 \<cdot>\<^sub>l \<sigma>} \<union> ((C\<^sub>2 \<cdot>\<^sub>l\<^sub>s \<sigma>) - {l\<^sub>2 \<cdot>\<^sub>l \<sigma>}))
{l\<^sub>1 \<cdot>\<^sub>l \<sigma>} = L\<^sub>1 \<cdot>\<^sub>l\<^sub>s \<sigma>
{l\<^sub>2 \<cdot>\<^sub>l \<sigma>} = L\<^sub>2 \<cdot>\<^sub>l\<^sub>s \<sigma>

goal (1 subgoal):
 1. eval\<^sub>c F G ((C\<^sub>1 \<cdot>\<^sub>l\<^sub>s \<sigma>) - (L\<^sub>1 \<cdot>\<^sub>l\<^sub>s \<sigma>) \<union> ((C\<^sub>2 \<cdot>\<^sub>l\<^sub>s \<sigma>) - (L\<^sub>2 \<cdot>\<^sub>l\<^sub>s \<sigma>)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
eval\<^sub>c F G (mresolution C\<^sub>1 C\<^sub>2 L\<^sub>1 L\<^sub>2 \<sigma>)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma resolution_superset: "mresolution C\<^sub>1 C\<^sub>2 L\<^sub>1 L\<^sub>2 \<sigma> \<subseteq> resolution C\<^sub>1 C\<^sub>2 L\<^sub>1 L\<^sub>2 \<sigma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mresolution C\<^sub>1 C\<^sub>2 L\<^sub>1 L\<^sub>2 \<sigma> \<subseteq> resolution C\<^sub>1 C\<^sub>2 L\<^sub>1 L\<^sub>2 \<sigma>
[PROOF STEP]
unfolding mresolution_def resolution_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (C\<^sub>1 \<cdot>\<^sub>l\<^sub>s \<sigma>) - (L\<^sub>1 \<cdot>\<^sub>l\<^sub>s \<sigma>) \<union> ((C\<^sub>2 \<cdot>\<^sub>l\<^sub>s \<sigma>) - (L\<^sub>2 \<cdot>\<^sub>l\<^sub>s \<sigma>)) \<subseteq> C\<^sub>1 - L\<^sub>1 \<union> (C\<^sub>2 - L\<^sub>2) \<cdot>\<^sub>l\<^sub>s \<sigma>
[PROOF STEP]
by auto


[STATEMENT]
lemma superset_sound:
  assumes sup: "C \<subseteq> C'"
  assumes sat: "eval\<^sub>c F G C"
  shows "eval\<^sub>c F G C'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval\<^sub>c F G C'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. eval\<^sub>c F G C'
[PROOF STEP]
have "\<forall>E. \<exists>l \<in> C'. eval\<^sub>l E F G l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>E. \<exists>l\<in>C'. eval\<^sub>l E F G l
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>E. \<exists>l\<in>C'. eval\<^sub>l E F G l
[PROOF STEP]
fix E
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>E. \<exists>l\<in>C'. eval\<^sub>l E F G l
[PROOF STEP]
from sat
[PROOF STATE]
proof (chain)
picking this:
eval\<^sub>c F G C
[PROOF STEP]
have "\<forall>E. \<exists>l \<in> C. eval\<^sub>l E F G l"
[PROOF STATE]
proof (prove)
using this:
eval\<^sub>c F G C

goal (1 subgoal):
 1. \<forall>E. \<exists>l\<in>C. eval\<^sub>l E F G l
[PROOF STEP]
unfolding eval\<^sub>c_def
[PROOF STATE]
proof (prove)
using this:
\<forall>E. Bex C (eval\<^sub>l E F G)

goal (1 subgoal):
 1. \<forall>E. \<exists>l\<in>C. eval\<^sub>l E F G l
[PROOF STEP]
by -
[PROOF STATE]
proof (state)
this:
\<forall>E. \<exists>l\<in>C. eval\<^sub>l E F G l

goal (1 subgoal):
 1. \<And>E. \<exists>l\<in>C'. eval\<^sub>l E F G l
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>E. \<exists>l\<in>C. eval\<^sub>l E F G l
[PROOF STEP]
have "\<exists>l \<in> C . eval\<^sub>l E F G l"
[PROOF STATE]
proof (prove)
using this:
\<forall>E. \<exists>l\<in>C. eval\<^sub>l E F G l

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

goal (1 subgoal):
 1. \<And>E. \<exists>l\<in>C'. eval\<^sub>l E F G l
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>l\<in>C. eval\<^sub>l E F G l
[PROOF STEP]
show "\<exists>l \<in> C'. eval\<^sub>l E F G l"
[PROOF STATE]
proof (prove)
using this:
\<exists>l\<in>C. eval\<^sub>l E F G l

goal (1 subgoal):
 1. \<exists>l\<in>C'. eval\<^sub>l E F G l
[PROOF STEP]
using sup
[PROOF STATE]
proof (prove)
using this:
\<exists>l\<in>C. eval\<^sub>l E F G l
C \<subseteq> C'

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>E. \<exists>l\<in>C'. eval\<^sub>l E F G l

goal (1 subgoal):
 1. eval\<^sub>c F G C'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>E. \<exists>l\<in>C'. eval\<^sub>l E F G l
[PROOF STEP]
show "eval\<^sub>c F G C'"
[PROOF STATE]
proof (prove)
using this:
\<forall>E. \<exists>l\<in>C'. eval\<^sub>l E F G l

goal (1 subgoal):
 1. eval\<^sub>c F G C'
[PROOF STEP]
unfolding eval\<^sub>c_def
[PROOF STATE]
proof (prove)
using this:
\<forall>E. \<exists>l\<in>C'. eval\<^sub>l E F G l

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem resolution_sound:
  assumes sat\<^sub>1: "eval\<^sub>c F G C\<^sub>1"
  assumes sat\<^sub>2: "eval\<^sub>c F G C\<^sub>2"
  assumes appl: "applicable C\<^sub>1 C\<^sub>2 L\<^sub>1 L\<^sub>2 \<sigma>"
  shows "eval\<^sub>c F G (resolution C\<^sub>1 C\<^sub>2 L\<^sub>1 L\<^sub>2 \<sigma>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval\<^sub>c F G (resolution C\<^sub>1 C\<^sub>2 L\<^sub>1 L\<^sub>2 \<sigma>)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. eval\<^sub>c F G (resolution C\<^sub>1 C\<^sub>2 L\<^sub>1 L\<^sub>2 \<sigma>)
[PROOF STEP]
from sat\<^sub>1 sat\<^sub>2 appl
[PROOF STATE]
proof (chain)
picking this:
eval\<^sub>c F G C\<^sub>1
eval\<^sub>c F G C\<^sub>2
applicable C\<^sub>1 C\<^sub>2 L\<^sub>1 L\<^sub>2 \<sigma>
[PROOF STEP]
have "eval\<^sub>c F G (mresolution C\<^sub>1 C\<^sub>2 L\<^sub>1 L\<^sub>2 \<sigma>)"
[PROOF STATE]
proof (prove)
using this:
eval\<^sub>c F G C\<^sub>1
eval\<^sub>c F G C\<^sub>2
applicable C\<^sub>1 C\<^sub>2 L\<^sub>1 L\<^sub>2 \<sigma>

goal (1 subgoal):
 1. eval\<^sub>c F G (mresolution C\<^sub>1 C\<^sub>2 L\<^sub>1 L\<^sub>2 \<sigma>)
[PROOF STEP]
using mresolution_sound
[PROOF STATE]
proof (prove)
using this:
eval\<^sub>c F G C\<^sub>1
eval\<^sub>c F G C\<^sub>2
applicable C\<^sub>1 C\<^sub>2 L\<^sub>1 L\<^sub>2 \<sigma>
\<lbrakk>eval\<^sub>c ?F ?G ?C\<^sub>1; eval\<^sub>c ?F ?G ?C\<^sub>2; applicable ?C\<^sub>1 ?C\<^sub>2 ?L\<^sub>1 ?L\<^sub>2 ?\<sigma>\<rbrakk> \<Longrightarrow> eval\<^sub>c ?F ?G (mresolution ?C\<^sub>1 ?C\<^sub>2 ?L\<^sub>1 ?L\<^sub>2 ?\<sigma>)

goal (1 subgoal):
 1. eval\<^sub>c F G (mresolution C\<^sub>1 C\<^sub>2 L\<^sub>1 L\<^sub>2 \<sigma>)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
eval\<^sub>c F G (mresolution C\<^sub>1 C\<^sub>2 L\<^sub>1 L\<^sub>2 \<sigma>)

goal (1 subgoal):
 1. eval\<^sub>c F G (resolution C\<^sub>1 C\<^sub>2 L\<^sub>1 L\<^sub>2 \<sigma>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
eval\<^sub>c F G (mresolution C\<^sub>1 C\<^sub>2 L\<^sub>1 L\<^sub>2 \<sigma>)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
eval\<^sub>c F G (mresolution C\<^sub>1 C\<^sub>2 L\<^sub>1 L\<^sub>2 \<sigma>)

goal (1 subgoal):
 1. eval\<^sub>c F G (resolution C\<^sub>1 C\<^sub>2 L\<^sub>1 L\<^sub>2 \<sigma>)
[PROOF STEP]
using superset_sound resolution_superset
[PROOF STATE]
proof (prove)
using this:
eval\<^sub>c F G (mresolution C\<^sub>1 C\<^sub>2 L\<^sub>1 L\<^sub>2 \<sigma>)
\<lbrakk>?C \<subseteq> ?C'; eval\<^sub>c ?F ?G ?C\<rbrakk> \<Longrightarrow> eval\<^sub>c ?F ?G ?C'
mresolution ?C\<^sub>1 ?C\<^sub>2 ?L\<^sub>1 ?L\<^sub>2 ?\<sigma> \<subseteq> resolution ?C\<^sub>1 ?C\<^sub>2 ?L\<^sub>1 ?L\<^sub>2 ?\<sigma>

goal (1 subgoal):
 1. eval\<^sub>c F G (resolution C\<^sub>1 C\<^sub>2 L\<^sub>1 L\<^sub>2 \<sigma>)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
eval\<^sub>c F G (resolution C\<^sub>1 C\<^sub>2 L\<^sub>1 L\<^sub>2 \<sigma>)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mstep_sound:
  assumes "mresolution_step Cs Cs'"
  assumes "eval\<^sub>c\<^sub>s F G Cs"
  shows "eval\<^sub>c\<^sub>s F G Cs'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval\<^sub>c\<^sub>s F G Cs'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
mresolution_step Cs Cs'
eval\<^sub>c\<^sub>s F G Cs

goal (1 subgoal):
 1. eval\<^sub>c\<^sub>s F G Cs'
[PROOF STEP]
proof (induction rule: mresolution_step.induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>C\<^sub>1 Cs C\<^sub>2 L\<^sub>1 L\<^sub>2 \<sigma>. \<lbrakk>C\<^sub>1 \<in> Cs; C\<^sub>2 \<in> Cs; applicable C\<^sub>1 C\<^sub>2 L\<^sub>1 L\<^sub>2 \<sigma>; eval\<^sub>c\<^sub>s F G Cs\<rbrakk> \<Longrightarrow> eval\<^sub>c\<^sub>s F G (Cs \<union> {mresolution C\<^sub>1 C\<^sub>2 L\<^sub>1 L\<^sub>2 \<sigma>})
 2. \<And>C Cs C'. \<lbrakk>C \<in> Cs; var_renaming_of C C'; eval\<^sub>c\<^sub>s F G Cs\<rbrakk> \<Longrightarrow> eval\<^sub>c\<^sub>s F G (Cs \<union> {C'})
[PROOF STEP]
case (mresolution_rule C\<^sub>1 Cs C\<^sub>2 l\<^sub>1 l\<^sub>2 \<sigma>)
[PROOF STATE]
proof (state)
this:
C\<^sub>1 \<in> Cs
C\<^sub>2 \<in> Cs
applicable C\<^sub>1 C\<^sub>2 l\<^sub>1 l\<^sub>2 \<sigma>
eval\<^sub>c\<^sub>s F G Cs

goal (2 subgoals):
 1. \<And>C\<^sub>1 Cs C\<^sub>2 L\<^sub>1 L\<^sub>2 \<sigma>. \<lbrakk>C\<^sub>1 \<in> Cs; C\<^sub>2 \<in> Cs; applicable C\<^sub>1 C\<^sub>2 L\<^sub>1 L\<^sub>2 \<sigma>; eval\<^sub>c\<^sub>s F G Cs\<rbrakk> \<Longrightarrow> eval\<^sub>c\<^sub>s F G (Cs \<union> {mresolution C\<^sub>1 C\<^sub>2 L\<^sub>1 L\<^sub>2 \<sigma>})
 2. \<And>C Cs C'. \<lbrakk>C \<in> Cs; var_renaming_of C C'; eval\<^sub>c\<^sub>s F G Cs\<rbrakk> \<Longrightarrow> eval\<^sub>c\<^sub>s F G (Cs \<union> {C'})
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
C\<^sub>1 \<in> Cs
C\<^sub>2 \<in> Cs
applicable C\<^sub>1 C\<^sub>2 l\<^sub>1 l\<^sub>2 \<sigma>
eval\<^sub>c\<^sub>s F G Cs
[PROOF STEP]
have "eval\<^sub>c F G C\<^sub>1 \<and> eval\<^sub>c F G C\<^sub>2"
[PROOF STATE]
proof (prove)
using this:
C\<^sub>1 \<in> Cs
C\<^sub>2 \<in> Cs
applicable C\<^sub>1 C\<^sub>2 l\<^sub>1 l\<^sub>2 \<sigma>
eval\<^sub>c\<^sub>s F G Cs

goal (1 subgoal):
 1. eval\<^sub>c F G C\<^sub>1 \<and> eval\<^sub>c F G C\<^sub>2
[PROOF STEP]
unfolding eval\<^sub>c\<^sub>s_def
[PROOF STATE]
proof (prove)
using this:
C\<^sub>1 \<in> Cs
C\<^sub>2 \<in> Cs
applicable C\<^sub>1 C\<^sub>2 l\<^sub>1 l\<^sub>2 \<sigma>
Ball Cs (eval\<^sub>c F G)

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

goal (2 subgoals):
 1. \<And>C\<^sub>1 Cs C\<^sub>2 L\<^sub>1 L\<^sub>2 \<sigma>. \<lbrakk>C\<^sub>1 \<in> Cs; C\<^sub>2 \<in> Cs; applicable C\<^sub>1 C\<^sub>2 L\<^sub>1 L\<^sub>2 \<sigma>; eval\<^sub>c\<^sub>s F G Cs\<rbrakk> \<Longrightarrow> eval\<^sub>c\<^sub>s F G (Cs \<union> {mresolution C\<^sub>1 C\<^sub>2 L\<^sub>1 L\<^sub>2 \<sigma>})
 2. \<And>C Cs C'. \<lbrakk>C \<in> Cs; var_renaming_of C C'; eval\<^sub>c\<^sub>s F G Cs\<rbrakk> \<Longrightarrow> eval\<^sub>c\<^sub>s F G (Cs \<union> {C'})
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
eval\<^sub>c F G C\<^sub>1 \<and> eval\<^sub>c F G C\<^sub>2
[PROOF STEP]
have "eval\<^sub>c F G (mresolution C\<^sub>1 C\<^sub>2 l\<^sub>1 l\<^sub>2 \<sigma>)"
[PROOF STATE]
proof (prove)
using this:
eval\<^sub>c F G C\<^sub>1 \<and> eval\<^sub>c F G C\<^sub>2

goal (1 subgoal):
 1. eval\<^sub>c F G (mresolution C\<^sub>1 C\<^sub>2 l\<^sub>1 l\<^sub>2 \<sigma>)
[PROOF STEP]
using mresolution_sound mresolution_rule
[PROOF STATE]
proof (prove)
using this:
eval\<^sub>c F G C\<^sub>1 \<and> eval\<^sub>c F G C\<^sub>2
\<lbrakk>eval\<^sub>c ?F ?G ?C\<^sub>1; eval\<^sub>c ?F ?G ?C\<^sub>2; applicable ?C\<^sub>1 ?C\<^sub>2 ?L\<^sub>1 ?L\<^sub>2 ?\<sigma>\<rbrakk> \<Longrightarrow> eval\<^sub>c ?F ?G (mresolution ?C\<^sub>1 ?C\<^sub>2 ?L\<^sub>1 ?L\<^sub>2 ?\<sigma>)
C\<^sub>1 \<in> Cs
C\<^sub>2 \<in> Cs
applicable C\<^sub>1 C\<^sub>2 l\<^sub>1 l\<^sub>2 \<sigma>
eval\<^sub>c\<^sub>s F G Cs

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

goal (2 subgoals):
 1. \<And>C\<^sub>1 Cs C\<^sub>2 L\<^sub>1 L\<^sub>2 \<sigma>. \<lbrakk>C\<^sub>1 \<in> Cs; C\<^sub>2 \<in> Cs; applicable C\<^sub>1 C\<^sub>2 L\<^sub>1 L\<^sub>2 \<sigma>; eval\<^sub>c\<^sub>s F G Cs\<rbrakk> \<Longrightarrow> eval\<^sub>c\<^sub>s F G (Cs \<union> {mresolution C\<^sub>1 C\<^sub>2 L\<^sub>1 L\<^sub>2 \<sigma>})
 2. \<And>C Cs C'. \<lbrakk>C \<in> Cs; var_renaming_of C C'; eval\<^sub>c\<^sub>s F G Cs\<rbrakk> \<Longrightarrow> eval\<^sub>c\<^sub>s F G (Cs \<union> {C'})
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
eval\<^sub>c F G (mresolution C\<^sub>1 C\<^sub>2 l\<^sub>1 l\<^sub>2 \<sigma>)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
eval\<^sub>c F G (mresolution C\<^sub>1 C\<^sub>2 l\<^sub>1 l\<^sub>2 \<sigma>)

goal (1 subgoal):
 1. eval\<^sub>c\<^sub>s F G (Cs \<union> {mresolution C\<^sub>1 C\<^sub>2 l\<^sub>1 l\<^sub>2 \<sigma>})
[PROOF STEP]
using mresolution_rule
[PROOF STATE]
proof (prove)
using this:
eval\<^sub>c F G (mresolution C\<^sub>1 C\<^sub>2 l\<^sub>1 l\<^sub>2 \<sigma>)
C\<^sub>1 \<in> Cs
C\<^sub>2 \<in> Cs
applicable C\<^sub>1 C\<^sub>2 l\<^sub>1 l\<^sub>2 \<sigma>
eval\<^sub>c\<^sub>s F G Cs

goal (1 subgoal):
 1. eval\<^sub>c\<^sub>s F G (Cs \<union> {mresolution C\<^sub>1 C\<^sub>2 l\<^sub>1 l\<^sub>2 \<sigma>})
[PROOF STEP]
unfolding eval\<^sub>c\<^sub>s_def
[PROOF STATE]
proof (prove)
using this:
eval\<^sub>c F G (mresolution C\<^sub>1 C\<^sub>2 l\<^sub>1 l\<^sub>2 \<sigma>)
C\<^sub>1 \<in> Cs
C\<^sub>2 \<in> Cs
applicable C\<^sub>1 C\<^sub>2 l\<^sub>1 l\<^sub>2 \<sigma>
Ball Cs (eval\<^sub>c F G)

goal (1 subgoal):
 1. Ball (Cs \<union> {mresolution C\<^sub>1 C\<^sub>2 l\<^sub>1 l\<^sub>2 \<sigma>}) (eval\<^sub>c F G)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
eval\<^sub>c\<^sub>s F G (Cs \<union> {mresolution C\<^sub>1 C\<^sub>2 l\<^sub>1 l\<^sub>2 \<sigma>})

goal (1 subgoal):
 1. \<And>C Cs C'. \<lbrakk>C \<in> Cs; var_renaming_of C C'; eval\<^sub>c\<^sub>s F G Cs\<rbrakk> \<Longrightarrow> eval\<^sub>c\<^sub>s F G (Cs \<union> {C'})
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>C Cs C'. \<lbrakk>C \<in> Cs; var_renaming_of C C'; eval\<^sub>c\<^sub>s F G Cs\<rbrakk> \<Longrightarrow> eval\<^sub>c\<^sub>s F G (Cs \<union> {C'})
[PROOF STEP]
case (standardize_apart C Cs C')
[PROOF STATE]
proof (state)
this:
C \<in> Cs
var_renaming_of C C'
eval\<^sub>c\<^sub>s F G Cs

goal (1 subgoal):
 1. \<And>C Cs C'. \<lbrakk>C \<in> Cs; var_renaming_of C C'; eval\<^sub>c\<^sub>s F G Cs\<rbrakk> \<Longrightarrow> eval\<^sub>c\<^sub>s F G (Cs \<union> {C'})
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
C \<in> Cs
var_renaming_of C C'
eval\<^sub>c\<^sub>s F G Cs
[PROOF STEP]
have "eval\<^sub>c F G C"
[PROOF STATE]
proof (prove)
using this:
C \<in> Cs
var_renaming_of C C'
eval\<^sub>c\<^sub>s F G Cs

goal (1 subgoal):
 1. eval\<^sub>c F G C
[PROOF STEP]
unfolding eval\<^sub>c\<^sub>s_def
[PROOF STATE]
proof (prove)
using this:
C \<in> Cs
var_renaming_of C C'
Ball Cs (eval\<^sub>c F G)

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

goal (1 subgoal):
 1. \<And>C Cs C'. \<lbrakk>C \<in> Cs; var_renaming_of C C'; eval\<^sub>c\<^sub>s F G Cs\<rbrakk> \<Longrightarrow> eval\<^sub>c\<^sub>s F G (Cs \<union> {C'})
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
eval\<^sub>c F G C
[PROOF STEP]
have "eval\<^sub>c F G C'"
[PROOF STATE]
proof (prove)
using this:
eval\<^sub>c F G C

goal (1 subgoal):
 1. eval\<^sub>c F G C'
[PROOF STEP]
using subst_sound standardize_apart
[PROOF STATE]
proof (prove)
using this:
eval\<^sub>c F G C
eval\<^sub>c ?F ?G ?C \<Longrightarrow> eval\<^sub>c ?F ?G (?C \<cdot>\<^sub>l\<^sub>s ?\<sigma>)
C \<in> Cs
var_renaming_of C C'
eval\<^sub>c\<^sub>s F G Cs

goal (1 subgoal):
 1. eval\<^sub>c F G C'
[PROOF STEP]
unfolding var_renaming_of_def instance_of\<^sub>l\<^sub>s_def
[PROOF STATE]
proof (prove)
using this:
eval\<^sub>c F G C
eval\<^sub>c ?F ?G ?C \<Longrightarrow> eval\<^sub>c ?F ?G (?C \<cdot>\<^sub>l\<^sub>s ?\<sigma>)
C \<in> Cs
(\<exists>\<sigma>. C = C' \<cdot>\<^sub>l\<^sub>s \<sigma>) \<and> (\<exists>\<sigma>. C' = C \<cdot>\<^sub>l\<^sub>s \<sigma>)
eval\<^sub>c\<^sub>s F G Cs

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

goal (1 subgoal):
 1. \<And>C Cs C'. \<lbrakk>C \<in> Cs; var_renaming_of C C'; eval\<^sub>c\<^sub>s F G Cs\<rbrakk> \<Longrightarrow> eval\<^sub>c\<^sub>s F G (Cs \<union> {C'})
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
eval\<^sub>c F G C'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
eval\<^sub>c F G C'

goal (1 subgoal):
 1. eval\<^sub>c\<^sub>s F G (Cs \<union> {C'})
[PROOF STEP]
using standardize_apart
[PROOF STATE]
proof (prove)
using this:
eval\<^sub>c F G C'
C \<in> Cs
var_renaming_of C C'
eval\<^sub>c\<^sub>s F G Cs

goal (1 subgoal):
 1. eval\<^sub>c\<^sub>s F G (Cs \<union> {C'})
[PROOF STEP]
unfolding eval\<^sub>c\<^sub>s_def
[PROOF STATE]
proof (prove)
using this:
eval\<^sub>c F G C'
C \<in> Cs
var_renaming_of C C'
Ball Cs (eval\<^sub>c F G)

goal (1 subgoal):
 1. Ball (Cs \<union> {C'}) (eval\<^sub>c F G)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
eval\<^sub>c\<^sub>s F G (Cs \<union> {C'})

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem step_sound:
  assumes "resolution_step Cs Cs'"
  assumes "eval\<^sub>c\<^sub>s F G Cs"
  shows "eval\<^sub>c\<^sub>s F G Cs'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval\<^sub>c\<^sub>s F G Cs'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
resolution_step Cs Cs'
eval\<^sub>c\<^sub>s F G Cs

goal (1 subgoal):
 1. eval\<^sub>c\<^sub>s F G Cs'
[PROOF STEP]
proof (induction rule: resolution_step.induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>C\<^sub>1 Cs C\<^sub>2 L\<^sub>1 L\<^sub>2 \<sigma>. \<lbrakk>C\<^sub>1 \<in> Cs; C\<^sub>2 \<in> Cs; applicable C\<^sub>1 C\<^sub>2 L\<^sub>1 L\<^sub>2 \<sigma>; eval\<^sub>c\<^sub>s F G Cs\<rbrakk> \<Longrightarrow> eval\<^sub>c\<^sub>s F G (Cs \<union> {resolution C\<^sub>1 C\<^sub>2 L\<^sub>1 L\<^sub>2 \<sigma>})
 2. \<And>C Cs C'. \<lbrakk>C \<in> Cs; var_renaming_of C C'; eval\<^sub>c\<^sub>s F G Cs\<rbrakk> \<Longrightarrow> eval\<^sub>c\<^sub>s F G (Cs \<union> {C'})
[PROOF STEP]
case (resolution_rule C\<^sub>1 Cs C\<^sub>2 l\<^sub>1 l\<^sub>2 \<sigma>)
[PROOF STATE]
proof (state)
this:
C\<^sub>1 \<in> Cs
C\<^sub>2 \<in> Cs
applicable C\<^sub>1 C\<^sub>2 l\<^sub>1 l\<^sub>2 \<sigma>
eval\<^sub>c\<^sub>s F G Cs

goal (2 subgoals):
 1. \<And>C\<^sub>1 Cs C\<^sub>2 L\<^sub>1 L\<^sub>2 \<sigma>. \<lbrakk>C\<^sub>1 \<in> Cs; C\<^sub>2 \<in> Cs; applicable C\<^sub>1 C\<^sub>2 L\<^sub>1 L\<^sub>2 \<sigma>; eval\<^sub>c\<^sub>s F G Cs\<rbrakk> \<Longrightarrow> eval\<^sub>c\<^sub>s F G (Cs \<union> {resolution C\<^sub>1 C\<^sub>2 L\<^sub>1 L\<^sub>2 \<sigma>})
 2. \<And>C Cs C'. \<lbrakk>C \<in> Cs; var_renaming_of C C'; eval\<^sub>c\<^sub>s F G Cs\<rbrakk> \<Longrightarrow> eval\<^sub>c\<^sub>s F G (Cs \<union> {C'})
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
C\<^sub>1 \<in> Cs
C\<^sub>2 \<in> Cs
applicable C\<^sub>1 C\<^sub>2 l\<^sub>1 l\<^sub>2 \<sigma>
eval\<^sub>c\<^sub>s F G Cs
[PROOF STEP]
have "eval\<^sub>c F G C\<^sub>1 \<and> eval\<^sub>c F G C\<^sub>2"
[PROOF STATE]
proof (prove)
using this:
C\<^sub>1 \<in> Cs
C\<^sub>2 \<in> Cs
applicable C\<^sub>1 C\<^sub>2 l\<^sub>1 l\<^sub>2 \<sigma>
eval\<^sub>c\<^sub>s F G Cs

goal (1 subgoal):
 1. eval\<^sub>c F G C\<^sub>1 \<and> eval\<^sub>c F G C\<^sub>2
[PROOF STEP]
unfolding eval\<^sub>c\<^sub>s_def
[PROOF STATE]
proof (prove)
using this:
C\<^sub>1 \<in> Cs
C\<^sub>2 \<in> Cs
applicable C\<^sub>1 C\<^sub>2 l\<^sub>1 l\<^sub>2 \<sigma>
Ball Cs (eval\<^sub>c F G)

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

goal (2 subgoals):
 1. \<And>C\<^sub>1 Cs C\<^sub>2 L\<^sub>1 L\<^sub>2 \<sigma>. \<lbrakk>C\<^sub>1 \<in> Cs; C\<^sub>2 \<in> Cs; applicable C\<^sub>1 C\<^sub>2 L\<^sub>1 L\<^sub>2 \<sigma>; eval\<^sub>c\<^sub>s F G Cs\<rbrakk> \<Longrightarrow> eval\<^sub>c\<^sub>s F G (Cs \<union> {resolution C\<^sub>1 C\<^sub>2 L\<^sub>1 L\<^sub>2 \<sigma>})
 2. \<And>C Cs C'. \<lbrakk>C \<in> Cs; var_renaming_of C C'; eval\<^sub>c\<^sub>s F G Cs\<rbrakk> \<Longrightarrow> eval\<^sub>c\<^sub>s F G (Cs \<union> {C'})
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
eval\<^sub>c F G C\<^sub>1 \<and> eval\<^sub>c F G C\<^sub>2
[PROOF STEP]
have "eval\<^sub>c F G (resolution C\<^sub>1 C\<^sub>2 l\<^sub>1 l\<^sub>2 \<sigma>)"
[PROOF STATE]
proof (prove)
using this:
eval\<^sub>c F G C\<^sub>1 \<and> eval\<^sub>c F G C\<^sub>2

goal (1 subgoal):
 1. eval\<^sub>c F G (resolution C\<^sub>1 C\<^sub>2 l\<^sub>1 l\<^sub>2 \<sigma>)
[PROOF STEP]
using resolution_sound resolution_rule
[PROOF STATE]
proof (prove)
using this:
eval\<^sub>c F G C\<^sub>1 \<and> eval\<^sub>c F G C\<^sub>2
\<lbrakk>eval\<^sub>c ?F ?G ?C\<^sub>1; eval\<^sub>c ?F ?G ?C\<^sub>2; applicable ?C\<^sub>1 ?C\<^sub>2 ?L\<^sub>1 ?L\<^sub>2 ?\<sigma>\<rbrakk> \<Longrightarrow> eval\<^sub>c ?F ?G (resolution ?C\<^sub>1 ?C\<^sub>2 ?L\<^sub>1 ?L\<^sub>2 ?\<sigma>)
C\<^sub>1 \<in> Cs
C\<^sub>2 \<in> Cs
applicable C\<^sub>1 C\<^sub>2 l\<^sub>1 l\<^sub>2 \<sigma>
eval\<^sub>c\<^sub>s F G Cs

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

goal (2 subgoals):
 1. \<And>C\<^sub>1 Cs C\<^sub>2 L\<^sub>1 L\<^sub>2 \<sigma>. \<lbrakk>C\<^sub>1 \<in> Cs; C\<^sub>2 \<in> Cs; applicable C\<^sub>1 C\<^sub>2 L\<^sub>1 L\<^sub>2 \<sigma>; eval\<^sub>c\<^sub>s F G Cs\<rbrakk> \<Longrightarrow> eval\<^sub>c\<^sub>s F G (Cs \<union> {resolution C\<^sub>1 C\<^sub>2 L\<^sub>1 L\<^sub>2 \<sigma>})
 2. \<And>C Cs C'. \<lbrakk>C \<in> Cs; var_renaming_of C C'; eval\<^sub>c\<^sub>s F G Cs\<rbrakk> \<Longrightarrow> eval\<^sub>c\<^sub>s F G (Cs \<union> {C'})
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
eval\<^sub>c F G (resolution C\<^sub>1 C\<^sub>2 l\<^sub>1 l\<^sub>2 \<sigma>)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
eval\<^sub>c F G (resolution C\<^sub>1 C\<^sub>2 l\<^sub>1 l\<^sub>2 \<sigma>)

goal (1 subgoal):
 1. eval\<^sub>c\<^sub>s F G (Cs \<union> {resolution C\<^sub>1 C\<^sub>2 l\<^sub>1 l\<^sub>2 \<sigma>})
[PROOF STEP]
using resolution_rule
[PROOF STATE]
proof (prove)
using this:
eval\<^sub>c F G (resolution C\<^sub>1 C\<^sub>2 l\<^sub>1 l\<^sub>2 \<sigma>)
C\<^sub>1 \<in> Cs
C\<^sub>2 \<in> Cs
applicable C\<^sub>1 C\<^sub>2 l\<^sub>1 l\<^sub>2 \<sigma>
eval\<^sub>c\<^sub>s F G Cs

goal (1 subgoal):
 1. eval\<^sub>c\<^sub>s F G (Cs \<union> {resolution C\<^sub>1 C\<^sub>2 l\<^sub>1 l\<^sub>2 \<sigma>})
[PROOF STEP]
unfolding eval\<^sub>c\<^sub>s_def
[PROOF STATE]
proof (prove)
using this:
eval\<^sub>c F G (resolution C\<^sub>1 C\<^sub>2 l\<^sub>1 l\<^sub>2 \<sigma>)
C\<^sub>1 \<in> Cs
C\<^sub>2 \<in> Cs
applicable C\<^sub>1 C\<^sub>2 l\<^sub>1 l\<^sub>2 \<sigma>
Ball Cs (eval\<^sub>c F G)

goal (1 subgoal):
 1. Ball (Cs \<union> {resolution C\<^sub>1 C\<^sub>2 l\<^sub>1 l\<^sub>2 \<sigma>}) (eval\<^sub>c F G)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
eval\<^sub>c\<^sub>s F G (Cs \<union> {resolution C\<^sub>1 C\<^sub>2 l\<^sub>1 l\<^sub>2 \<sigma>})

goal (1 subgoal):
 1. \<And>C Cs C'. \<lbrakk>C \<in> Cs; var_renaming_of C C'; eval\<^sub>c\<^sub>s F G Cs\<rbrakk> \<Longrightarrow> eval\<^sub>c\<^sub>s F G (Cs \<union> {C'})
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>C Cs C'. \<lbrakk>C \<in> Cs; var_renaming_of C C'; eval\<^sub>c\<^sub>s F G Cs\<rbrakk> \<Longrightarrow> eval\<^sub>c\<^sub>s F G (Cs \<union> {C'})
[PROOF STEP]
case (standardize_apart C Cs C')
[PROOF STATE]
proof (state)
this:
C \<in> Cs
var_renaming_of C C'
eval\<^sub>c\<^sub>s F G Cs

goal (1 subgoal):
 1. \<And>C Cs C'. \<lbrakk>C \<in> Cs; var_renaming_of C C'; eval\<^sub>c\<^sub>s F G Cs\<rbrakk> \<Longrightarrow> eval\<^sub>c\<^sub>s F G (Cs \<union> {C'})
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
C \<in> Cs
var_renaming_of C C'
eval\<^sub>c\<^sub>s F G Cs
[PROOF STEP]
have "eval\<^sub>c F G C"
[PROOF STATE]
proof (prove)
using this:
C \<in> Cs
var_renaming_of C C'
eval\<^sub>c\<^sub>s F G Cs

goal (1 subgoal):
 1. eval\<^sub>c F G C
[PROOF STEP]
unfolding eval\<^sub>c\<^sub>s_def
[PROOF STATE]
proof (prove)
using this:
C \<in> Cs
var_renaming_of C C'
Ball Cs (eval\<^sub>c F G)

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

goal (1 subgoal):
 1. \<And>C Cs C'. \<lbrakk>C \<in> Cs; var_renaming_of C C'; eval\<^sub>c\<^sub>s F G Cs\<rbrakk> \<Longrightarrow> eval\<^sub>c\<^sub>s F G (Cs \<union> {C'})
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
eval\<^sub>c F G C
[PROOF STEP]
have "eval\<^sub>c F G C'"
[PROOF STATE]
proof (prove)
using this:
eval\<^sub>c F G C

goal (1 subgoal):
 1. eval\<^sub>c F G C'
[PROOF STEP]
using subst_sound standardize_apart
[PROOF STATE]
proof (prove)
using this:
eval\<^sub>c F G C
eval\<^sub>c ?F ?G ?C \<Longrightarrow> eval\<^sub>c ?F ?G (?C \<cdot>\<^sub>l\<^sub>s ?\<sigma>)
C \<in> Cs
var_renaming_of C C'
eval\<^sub>c\<^sub>s F G Cs

goal (1 subgoal):
 1. eval\<^sub>c F G C'
[PROOF STEP]
unfolding var_renaming_of_def instance_of\<^sub>l\<^sub>s_def
[PROOF STATE]
proof (prove)
using this:
eval\<^sub>c F G C
eval\<^sub>c ?F ?G ?C \<Longrightarrow> eval\<^sub>c ?F ?G (?C \<cdot>\<^sub>l\<^sub>s ?\<sigma>)
C \<in> Cs
(\<exists>\<sigma>. C = C' \<cdot>\<^sub>l\<^sub>s \<sigma>) \<and> (\<exists>\<sigma>. C' = C \<cdot>\<^sub>l\<^sub>s \<sigma>)
eval\<^sub>c\<^sub>s F G Cs

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

goal (1 subgoal):
 1. \<And>C Cs C'. \<lbrakk>C \<in> Cs; var_renaming_of C C'; eval\<^sub>c\<^sub>s F G Cs\<rbrakk> \<Longrightarrow> eval\<^sub>c\<^sub>s F G (Cs \<union> {C'})
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
eval\<^sub>c F G C'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
eval\<^sub>c F G C'

goal (1 subgoal):
 1. eval\<^sub>c\<^sub>s F G (Cs \<union> {C'})
[PROOF STEP]
using standardize_apart
[PROOF STATE]
proof (prove)
using this:
eval\<^sub>c F G C'
C \<in> Cs
var_renaming_of C C'
eval\<^sub>c\<^sub>s F G Cs

goal (1 subgoal):
 1. eval\<^sub>c\<^sub>s F G (Cs \<union> {C'})
[PROOF STEP]
unfolding eval\<^sub>c\<^sub>s_def
[PROOF STATE]
proof (prove)
using this:
eval\<^sub>c F G C'
C \<in> Cs
var_renaming_of C C'
Ball Cs (eval\<^sub>c F G)

goal (1 subgoal):
 1. Ball (Cs \<union> {C'}) (eval\<^sub>c F G)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
eval\<^sub>c\<^sub>s F G (Cs \<union> {C'})

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mderivation_sound:
  assumes "mresolution_deriv Cs Cs'"
  assumes "eval\<^sub>c\<^sub>s F G Cs"
  shows "eval\<^sub>c\<^sub>s F G Cs'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval\<^sub>c\<^sub>s F G Cs'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
mresolution_deriv Cs Cs'
eval\<^sub>c\<^sub>s F G Cs

goal (1 subgoal):
 1. eval\<^sub>c\<^sub>s F G Cs'
[PROOF STEP]
unfolding mresolution_deriv_def
[PROOF STATE]
proof (prove)
using this:
mresolution_step\<^sup>*\<^sup>* Cs Cs'
eval\<^sub>c\<^sub>s F G Cs

goal (1 subgoal):
 1. eval\<^sub>c\<^sub>s F G Cs'
[PROOF STEP]
proof (induction rule: rtranclp.induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>a. eval\<^sub>c\<^sub>s F G a \<Longrightarrow> eval\<^sub>c\<^sub>s F G a
 2. \<And>a b c. \<lbrakk>mresolution_step\<^sup>*\<^sup>* a b; eval\<^sub>c\<^sub>s F G a \<Longrightarrow> eval\<^sub>c\<^sub>s F G b; mresolution_step b c; eval\<^sub>c\<^sub>s F G a\<rbrakk> \<Longrightarrow> eval\<^sub>c\<^sub>s F G c
[PROOF STEP]
case rtrancl_refl
[PROOF STATE]
proof (state)
this:
eval\<^sub>c\<^sub>s F G a_

goal (2 subgoals):
 1. \<And>a. eval\<^sub>c\<^sub>s F G a \<Longrightarrow> eval\<^sub>c\<^sub>s F G a
 2. \<And>a b c. \<lbrakk>mresolution_step\<^sup>*\<^sup>* a b; eval\<^sub>c\<^sub>s F G a \<Longrightarrow> eval\<^sub>c\<^sub>s F G b; mresolution_step b c; eval\<^sub>c\<^sub>s F G a\<rbrakk> \<Longrightarrow> eval\<^sub>c\<^sub>s F G c
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
eval\<^sub>c\<^sub>s F G a_
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
eval\<^sub>c\<^sub>s F G a_

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

goal (1 subgoal):
 1. \<And>a b c. \<lbrakk>mresolution_step\<^sup>*\<^sup>* a b; eval\<^sub>c\<^sub>s F G a \<Longrightarrow> eval\<^sub>c\<^sub>s F G b; mresolution_step b c; eval\<^sub>c\<^sub>s F G a\<rbrakk> \<Longrightarrow> eval\<^sub>c\<^sub>s F G c
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b c. \<lbrakk>mresolution_step\<^sup>*\<^sup>* a b; eval\<^sub>c\<^sub>s F G a \<Longrightarrow> eval\<^sub>c\<^sub>s F G b; mresolution_step b c; eval\<^sub>c\<^sub>s F G a\<rbrakk> \<Longrightarrow> eval\<^sub>c\<^sub>s F G c
[PROOF STEP]
case (rtrancl_into_rtrancl Cs\<^sub>1 Cs\<^sub>2 Cs\<^sub>3)
[PROOF STATE]
proof (state)
this:
mresolution_step\<^sup>*\<^sup>* Cs\<^sub>1 Cs\<^sub>2
mresolution_step Cs\<^sub>2 Cs\<^sub>3
eval\<^sub>c\<^sub>s F G Cs\<^sub>1 \<Longrightarrow> eval\<^sub>c\<^sub>s F G Cs\<^sub>2
eval\<^sub>c\<^sub>s F G Cs\<^sub>1

goal (1 subgoal):
 1. \<And>a b c. \<lbrakk>mresolution_step\<^sup>*\<^sup>* a b; eval\<^sub>c\<^sub>s F G a \<Longrightarrow> eval\<^sub>c\<^sub>s F G b; mresolution_step b c; eval\<^sub>c\<^sub>s F G a\<rbrakk> \<Longrightarrow> eval\<^sub>c\<^sub>s F G c
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
mresolution_step\<^sup>*\<^sup>* Cs\<^sub>1 Cs\<^sub>2
mresolution_step Cs\<^sub>2 Cs\<^sub>3
eval\<^sub>c\<^sub>s F G Cs\<^sub>1 \<Longrightarrow> eval\<^sub>c\<^sub>s F G Cs\<^sub>2
eval\<^sub>c\<^sub>s F G Cs\<^sub>1
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
mresolution_step\<^sup>*\<^sup>* Cs\<^sub>1 Cs\<^sub>2
mresolution_step Cs\<^sub>2 Cs\<^sub>3
eval\<^sub>c\<^sub>s F G Cs\<^sub>1 \<Longrightarrow> eval\<^sub>c\<^sub>s F G Cs\<^sub>2
eval\<^sub>c\<^sub>s F G Cs\<^sub>1

goal (1 subgoal):
 1. eval\<^sub>c\<^sub>s F G Cs\<^sub>3
[PROOF STEP]
using mstep_sound
[PROOF STATE]
proof (prove)
using this:
mresolution_step\<^sup>*\<^sup>* Cs\<^sub>1 Cs\<^sub>2
mresolution_step Cs\<^sub>2 Cs\<^sub>3
eval\<^sub>c\<^sub>s F G Cs\<^sub>1 \<Longrightarrow> eval\<^sub>c\<^sub>s F G Cs\<^sub>2
eval\<^sub>c\<^sub>s F G Cs\<^sub>1
\<lbrakk>mresolution_step ?Cs ?Cs'; eval\<^sub>c\<^sub>s ?F ?G ?Cs\<rbrakk> \<Longrightarrow> eval\<^sub>c\<^sub>s ?F ?G ?Cs'

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem derivation_sound:
  assumes "resolution_deriv Cs Cs'"
  assumes "eval\<^sub>c\<^sub>s F G Cs"
  shows"eval\<^sub>c\<^sub>s F G Cs'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval\<^sub>c\<^sub>s F G Cs'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
resolution_deriv Cs Cs'
eval\<^sub>c\<^sub>s F G Cs

goal (1 subgoal):
 1. eval\<^sub>c\<^sub>s F G Cs'
[PROOF STEP]
unfolding resolution_deriv_def
[PROOF STATE]
proof (prove)
using this:
resolution_step\<^sup>*\<^sup>* Cs Cs'
eval\<^sub>c\<^sub>s F G Cs

goal (1 subgoal):
 1. eval\<^sub>c\<^sub>s F G Cs'
[PROOF STEP]
proof (induction rule: rtranclp.induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>a. eval\<^sub>c\<^sub>s F G a \<Longrightarrow> eval\<^sub>c\<^sub>s F G a
 2. \<And>a b c. \<lbrakk>resolution_step\<^sup>*\<^sup>* a b; eval\<^sub>c\<^sub>s F G a \<Longrightarrow> eval\<^sub>c\<^sub>s F G b; resolution_step b c; eval\<^sub>c\<^sub>s F G a\<rbrakk> \<Longrightarrow> eval\<^sub>c\<^sub>s F G c
[PROOF STEP]
case rtrancl_refl
[PROOF STATE]
proof (state)
this:
eval\<^sub>c\<^sub>s F G a_

goal (2 subgoals):
 1. \<And>a. eval\<^sub>c\<^sub>s F G a \<Longrightarrow> eval\<^sub>c\<^sub>s F G a
 2. \<And>a b c. \<lbrakk>resolution_step\<^sup>*\<^sup>* a b; eval\<^sub>c\<^sub>s F G a \<Longrightarrow> eval\<^sub>c\<^sub>s F G b; resolution_step b c; eval\<^sub>c\<^sub>s F G a\<rbrakk> \<Longrightarrow> eval\<^sub>c\<^sub>s F G c
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
eval\<^sub>c\<^sub>s F G a_
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
eval\<^sub>c\<^sub>s F G a_

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

goal (1 subgoal):
 1. \<And>a b c. \<lbrakk>resolution_step\<^sup>*\<^sup>* a b; eval\<^sub>c\<^sub>s F G a \<Longrightarrow> eval\<^sub>c\<^sub>s F G b; resolution_step b c; eval\<^sub>c\<^sub>s F G a\<rbrakk> \<Longrightarrow> eval\<^sub>c\<^sub>s F G c
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b c. \<lbrakk>resolution_step\<^sup>*\<^sup>* a b; eval\<^sub>c\<^sub>s F G a \<Longrightarrow> eval\<^sub>c\<^sub>s F G b; resolution_step b c; eval\<^sub>c\<^sub>s F G a\<rbrakk> \<Longrightarrow> eval\<^sub>c\<^sub>s F G c
[PROOF STEP]
case (rtrancl_into_rtrancl Cs\<^sub>1 Cs\<^sub>2 Cs\<^sub>3)
[PROOF STATE]
proof (state)
this:
resolution_step\<^sup>*\<^sup>* Cs\<^sub>1 Cs\<^sub>2
resolution_step Cs\<^sub>2 Cs\<^sub>3
eval\<^sub>c\<^sub>s F G Cs\<^sub>1 \<Longrightarrow> eval\<^sub>c\<^sub>s F G Cs\<^sub>2
eval\<^sub>c\<^sub>s F G Cs\<^sub>1

goal (1 subgoal):
 1. \<And>a b c. \<lbrakk>resolution_step\<^sup>*\<^sup>* a b; eval\<^sub>c\<^sub>s F G a \<Longrightarrow> eval\<^sub>c\<^sub>s F G b; resolution_step b c; eval\<^sub>c\<^sub>s F G a\<rbrakk> \<Longrightarrow> eval\<^sub>c\<^sub>s F G c
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
resolution_step\<^sup>*\<^sup>* Cs\<^sub>1 Cs\<^sub>2
resolution_step Cs\<^sub>2 Cs\<^sub>3
eval\<^sub>c\<^sub>s F G Cs\<^sub>1 \<Longrightarrow> eval\<^sub>c\<^sub>s F G Cs\<^sub>2
eval\<^sub>c\<^sub>s F G Cs\<^sub>1
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
resolution_step\<^sup>*\<^sup>* Cs\<^sub>1 Cs\<^sub>2
resolution_step Cs\<^sub>2 Cs\<^sub>3
eval\<^sub>c\<^sub>s F G Cs\<^sub>1 \<Longrightarrow> eval\<^sub>c\<^sub>s F G Cs\<^sub>2
eval\<^sub>c\<^sub>s F G Cs\<^sub>1

goal (1 subgoal):
 1. eval\<^sub>c\<^sub>s F G Cs\<^sub>3
[PROOF STEP]
using step_sound
[PROOF STATE]
proof (prove)
using this:
resolution_step\<^sup>*\<^sup>* Cs\<^sub>1 Cs\<^sub>2
resolution_step Cs\<^sub>2 Cs\<^sub>3
eval\<^sub>c\<^sub>s F G Cs\<^sub>1 \<Longrightarrow> eval\<^sub>c\<^sub>s F G Cs\<^sub>2
eval\<^sub>c\<^sub>s F G Cs\<^sub>1
\<lbrakk>resolution_step ?Cs ?Cs'; eval\<^sub>c\<^sub>s ?F ?G ?Cs\<rbrakk> \<Longrightarrow> eval\<^sub>c\<^sub>s ?F ?G ?Cs'

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem derivation_sound_refute:
  assumes deriv: "resolution_deriv Cs Cs' \<and> {} \<in> Cs'"
  shows "\<not>eval\<^sub>c\<^sub>s F G Cs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> eval\<^sub>c\<^sub>s F G Cs
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> eval\<^sub>c\<^sub>s F G Cs
[PROOF STEP]
from deriv
[PROOF STATE]
proof (chain)
picking this:
resolution_deriv Cs Cs' \<and> {} \<in> Cs'
[PROOF STEP]
have "eval\<^sub>c\<^sub>s F G Cs \<longrightarrow> eval\<^sub>c\<^sub>s F G Cs'"
[PROOF STATE]
proof (prove)
using this:
resolution_deriv Cs Cs' \<and> {} \<in> Cs'

goal (1 subgoal):
 1. eval\<^sub>c\<^sub>s F G Cs \<longrightarrow> eval\<^sub>c\<^sub>s F G Cs'
[PROOF STEP]
using derivation_sound
[PROOF STATE]
proof (prove)
using this:
resolution_deriv Cs Cs' \<and> {} \<in> Cs'
\<lbrakk>resolution_deriv ?Cs ?Cs'; eval\<^sub>c\<^sub>s ?F ?G ?Cs\<rbrakk> \<Longrightarrow> eval\<^sub>c\<^sub>s ?F ?G ?Cs'

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

goal (1 subgoal):
 1. \<not> eval\<^sub>c\<^sub>s F G Cs
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
eval\<^sub>c\<^sub>s F G Cs \<longrightarrow> eval\<^sub>c\<^sub>s F G Cs'

goal (1 subgoal):
 1. \<not> eval\<^sub>c\<^sub>s F G Cs
[PROOF STEP]
from deriv
[PROOF STATE]
proof (chain)
picking this:
resolution_deriv Cs Cs' \<and> {} \<in> Cs'
[PROOF STEP]
have "eval\<^sub>c\<^sub>s F G Cs' \<longrightarrow> eval\<^sub>c F G {}"
[PROOF STATE]
proof (prove)
using this:
resolution_deriv Cs Cs' \<and> {} \<in> Cs'

goal (1 subgoal):
 1. eval\<^sub>c\<^sub>s F G Cs' \<longrightarrow> eval\<^sub>c F G {}
[PROOF STEP]
unfolding eval\<^sub>c\<^sub>s_def
[PROOF STATE]
proof (prove)
using this:
resolution_deriv Cs Cs' \<and> {} \<in> Cs'

goal (1 subgoal):
 1. Ball Cs' (eval\<^sub>c F G) \<longrightarrow> eval\<^sub>c F G {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
eval\<^sub>c\<^sub>s F G Cs' \<longrightarrow> eval\<^sub>c F G {}

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

goal (1 subgoal):
 1. \<not> eval\<^sub>c\<^sub>s F G Cs
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
eval\<^sub>c\<^sub>s F G Cs' \<longrightarrow> eval\<^sub>c F G {}
[PROOF STEP]
have "eval\<^sub>c F G {} \<longrightarrow> False"
[PROOF STATE]
proof (prove)
using this:
eval\<^sub>c\<^sub>s F G Cs' \<longrightarrow> eval\<^sub>c F G {}

goal (1 subgoal):
 1. eval\<^sub>c F G {} \<longrightarrow> False
[PROOF STEP]
unfolding eval\<^sub>c_def
[PROOF STATE]
proof (prove)
using this:
eval\<^sub>c\<^sub>s F G Cs' \<longrightarrow> (\<forall>E. Bex {} (eval\<^sub>l E F G))

goal (1 subgoal):
 1. (\<forall>E. Bex {} (eval\<^sub>l E F G)) \<longrightarrow> False
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
eval\<^sub>c F G {} \<longrightarrow> False

goal (1 subgoal):
 1. \<not> eval\<^sub>c\<^sub>s F G Cs
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
eval\<^sub>c\<^sub>s F G Cs \<longrightarrow> eval\<^sub>c\<^sub>s F G Cs'
eval\<^sub>c\<^sub>s F G Cs' \<longrightarrow> eval\<^sub>c F G {}
eval\<^sub>c F G {} \<longrightarrow> False
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
eval\<^sub>c\<^sub>s F G Cs \<longrightarrow> eval\<^sub>c\<^sub>s F G Cs'
eval\<^sub>c\<^sub>s F G Cs' \<longrightarrow> eval\<^sub>c F G {}
eval\<^sub>c F G {} \<longrightarrow> False

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma eval_ground\<^sub>t:
  assumes "ground\<^sub>t t"
  shows "(eval\<^sub>t E HFun t) = hterm_of_fterm t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval\<^sub>t E HFun t = hterm_of_fterm t
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
ground\<^sub>t t

goal (1 subgoal):
 1. eval\<^sub>t E HFun t = hterm_of_fterm t
[PROOF STEP]
by (induction t) auto


[STATEMENT]
lemma eval_ground\<^sub>t\<^sub>s:
  assumes "ground\<^sub>t\<^sub>s ts"
  shows "(eval\<^sub>t\<^sub>s E HFun ts) = hterms_of_fterms ts"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval\<^sub>t\<^sub>s E HFun ts = hterms_of_fterms ts
[PROOF STEP]
unfolding hterms_of_fterms_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval\<^sub>t\<^sub>s E HFun ts = map hterm_of_fterm ts
[PROOF STEP]
using assms eval_ground\<^sub>t
[PROOF STATE]
proof (prove)
using this:
ground\<^sub>t\<^sub>s ts
ground\<^sub>t ?t \<Longrightarrow> eval\<^sub>t ?E HFun ?t = hterm_of_fterm ?t

goal (1 subgoal):
 1. eval\<^sub>t\<^sub>s E HFun ts = map hterm_of_fterm ts
[PROOF STEP]
by (induction ts) auto


[STATEMENT]
lemma eval\<^sub>l_ground\<^sub>t\<^sub>s:
  assumes asm: "ground\<^sub>t\<^sub>s ts"
  shows "eval\<^sub>l E HFun G (Pos P ts) \<longleftrightarrow> G P (hterms_of_fterms ts)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval\<^sub>l E HFun G (Pos P ts) = G P (hterms_of_fterms ts)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. eval\<^sub>l E HFun G (Pos P ts) = G P (hterms_of_fterms ts)
[PROOF STEP]
have "eval\<^sub>l E HFun G (Pos P ts) = G P (eval\<^sub>t\<^sub>s E HFun ts)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval\<^sub>l E HFun G (Pos P ts) = G P (eval\<^sub>t\<^sub>s E HFun ts)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
eval\<^sub>l E HFun G (Pos P ts) = G P (eval\<^sub>t\<^sub>s E HFun ts)

goal (1 subgoal):
 1. eval\<^sub>l E HFun G (Pos P ts) = G P (hterms_of_fterms ts)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
eval\<^sub>l E HFun G (Pos P ts) = G P (eval\<^sub>t\<^sub>s E HFun ts)

goal (1 subgoal):
 1. eval\<^sub>l E HFun G (Pos P ts) = G P (hterms_of_fterms ts)
[PROOF STEP]
have "... = G P (hterms_of_fterms ts)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. G P (eval\<^sub>t\<^sub>s E HFun ts) = G P (hterms_of_fterms ts)
[PROOF STEP]
using asm eval_ground\<^sub>t\<^sub>s
[PROOF STATE]
proof (prove)
using this:
ground\<^sub>t\<^sub>s ts
ground\<^sub>t\<^sub>s ?ts \<Longrightarrow> eval\<^sub>t\<^sub>s ?E HFun ?ts = hterms_of_fterms ?ts

goal (1 subgoal):
 1. G P (eval\<^sub>t\<^sub>s E HFun ts) = G P (hterms_of_fterms ts)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
G P (eval\<^sub>t\<^sub>s E HFun ts) = G P (hterms_of_fterms ts)

goal (1 subgoal):
 1. eval\<^sub>l E HFun G (Pos P ts) = G P (hterms_of_fterms ts)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
eval\<^sub>l E HFun G (Pos P ts) = G P (hterms_of_fterms ts)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
eval\<^sub>l E HFun G (Pos P ts) = G P (hterms_of_fterms ts)

goal (1 subgoal):
 1. eval\<^sub>l E HFun G (Pos P ts) = G P (hterms_of_fterms ts)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
eval\<^sub>l E HFun G (Pos P ts) = G P (hterms_of_fterms ts)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ground_sub_of_denott: "ground\<^sub>t (t \<cdot>\<^sub>t (sub_of_denot E))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ground\<^sub>t (t \<cdot>\<^sub>t sub_of_denot E)
[PROOF STEP]
by (induction t) (auto simp add: ground_fterm_of_hterm)


[STATEMENT]
lemma ground_sub_of_denotts: "ground\<^sub>t\<^sub>s (ts \<cdot>\<^sub>t\<^sub>s sub_of_denot E)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ground\<^sub>t\<^sub>s (ts \<cdot>\<^sub>t\<^sub>s sub_of_denot E)
[PROOF STEP]
using ground_sub_of_denott
[PROOF STATE]
proof (prove)
using this:
ground\<^sub>t (?t \<cdot>\<^sub>t sub_of_denot ?E)

goal (1 subgoal):
 1. ground\<^sub>t\<^sub>s (ts \<cdot>\<^sub>t\<^sub>s sub_of_denot E)
[PROOF STEP]
by simp


[STATEMENT]
lemma ground_sub_of_denotl: "ground\<^sub>l (l \<cdot>\<^sub>l sub_of_denot E)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ground\<^sub>l (l \<cdot>\<^sub>l sub_of_denot E)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ground\<^sub>l (l \<cdot>\<^sub>l sub_of_denot E)
[PROOF STEP]
have "ground\<^sub>t\<^sub>s (subs (get_terms l) (sub_of_denot E))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ground\<^sub>t\<^sub>s (get_terms l \<cdot>\<^sub>t\<^sub>s sub_of_denot E)
[PROOF STEP]
using ground_sub_of_denotts
[PROOF STATE]
proof (prove)
using this:
ground\<^sub>t\<^sub>s (?ts \<cdot>\<^sub>t\<^sub>s sub_of_denot ?E)

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

goal (1 subgoal):
 1. ground\<^sub>l (l \<cdot>\<^sub>l sub_of_denot E)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ground\<^sub>t\<^sub>s (get_terms l \<cdot>\<^sub>t\<^sub>s sub_of_denot E)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
ground\<^sub>t\<^sub>s (get_terms l \<cdot>\<^sub>t\<^sub>s sub_of_denot E)

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sub_of_denot_equivx: "eval\<^sub>t E HFun (sub_of_denot E x) = E x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval\<^sub>t E HFun (sub_of_denot E x) = E x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. eval\<^sub>t E HFun (sub_of_denot E x) = E x
[PROOF STEP]
have "ground\<^sub>t (sub_of_denot E x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ground\<^sub>t (sub_of_denot E x)
[PROOF STEP]
using ground_fterm_of_hterm
[PROOF STATE]
proof (prove)
using this:
ground\<^sub>t (fterm_of_hterm ?t)

goal (1 subgoal):
 1. ground\<^sub>t (sub_of_denot E x)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
ground\<^sub>t (sub_of_denot E x)

goal (1 subgoal):
 1. eval\<^sub>t E HFun (sub_of_denot E x) = E x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ground\<^sub>t (sub_of_denot E x)
[PROOF STEP]
have "eval\<^sub>t E HFun (sub_of_denot E x) = hterm_of_fterm (sub_of_denot E x)"
[PROOF STATE]
proof (prove)
using this:
ground\<^sub>t (sub_of_denot E x)

goal (1 subgoal):
 1. eval\<^sub>t E HFun (sub_of_denot E x) = hterm_of_fterm (sub_of_denot E x)
[PROOF STEP]
using eval_ground\<^sub>t(1)
[PROOF STATE]
proof (prove)
using this:
ground\<^sub>t (sub_of_denot E x)
ground\<^sub>t ?t \<Longrightarrow> eval\<^sub>t ?E HFun ?t = hterm_of_fterm ?t

goal (1 subgoal):
 1. eval\<^sub>t E HFun (sub_of_denot E x) = hterm_of_fterm (sub_of_denot E x)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
eval\<^sub>t E HFun (sub_of_denot E x) = hterm_of_fterm (sub_of_denot E x)

goal (1 subgoal):
 1. eval\<^sub>t E HFun (sub_of_denot E x) = E x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
eval\<^sub>t E HFun (sub_of_denot E x) = hterm_of_fterm (sub_of_denot E x)

goal (1 subgoal):
 1. eval\<^sub>t E HFun (sub_of_denot E x) = E x
[PROOF STEP]
have "... = hterm_of_fterm (fterm_of_hterm (E x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hterm_of_fterm (sub_of_denot E x) = hterm_of_fterm (fterm_of_hterm (E x))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
hterm_of_fterm (sub_of_denot E x) = hterm_of_fterm (fterm_of_hterm (E x))

goal (1 subgoal):
 1. eval\<^sub>t E HFun (sub_of_denot E x) = E x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
hterm_of_fterm (sub_of_denot E x) = hterm_of_fterm (fterm_of_hterm (E x))

goal (1 subgoal):
 1. eval\<^sub>t E HFun (sub_of_denot E x) = E x
[PROOF STEP]
have "... = E x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hterm_of_fterm (fterm_of_hterm (E x)) = E x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
hterm_of_fterm (fterm_of_hterm (E x)) = E x

goal (1 subgoal):
 1. eval\<^sub>t E HFun (sub_of_denot E x) = E x
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
eval\<^sub>t E HFun (sub_of_denot E x) = E x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
eval\<^sub>t E HFun (sub_of_denot E x) = E x

goal (1 subgoal):
 1. eval\<^sub>t E HFun (sub_of_denot E x) = E x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
eval\<^sub>t E HFun (sub_of_denot E x) = E x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sub_of_denot_equivt:
    "eval\<^sub>t E HFun (t \<cdot>\<^sub>t (sub_of_denot E)) = eval\<^sub>t E HFun t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval\<^sub>t E HFun (t \<cdot>\<^sub>t sub_of_denot E) = eval\<^sub>t E HFun t
[PROOF STEP]
using sub_of_denot_equivx
[PROOF STATE]
proof (prove)
using this:
eval\<^sub>t ?E HFun (sub_of_denot ?E ?x) = ?E ?x

goal (1 subgoal):
 1. eval\<^sub>t E HFun (t \<cdot>\<^sub>t sub_of_denot E) = eval\<^sub>t E HFun t
[PROOF STEP]
by (induction t) auto


[STATEMENT]
lemma sub_of_denot_equivts: "eval\<^sub>t\<^sub>s E HFun (ts \<cdot>\<^sub>t\<^sub>s (sub_of_denot E)) = eval\<^sub>t\<^sub>s E HFun ts"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval\<^sub>t\<^sub>s E HFun (ts \<cdot>\<^sub>t\<^sub>s sub_of_denot E) = eval\<^sub>t\<^sub>s E HFun ts
[PROOF STEP]
using sub_of_denot_equivt
[PROOF STATE]
proof (prove)
using this:
eval\<^sub>t ?E HFun (?t \<cdot>\<^sub>t sub_of_denot ?E) = eval\<^sub>t ?E HFun ?t

goal (1 subgoal):
 1. eval\<^sub>t\<^sub>s E HFun (ts \<cdot>\<^sub>t\<^sub>s sub_of_denot E) = eval\<^sub>t\<^sub>s E HFun ts
[PROOF STEP]
by simp


[STATEMENT]
lemma sub_of_denot_equivl: "eval\<^sub>l E HFun G (l \<cdot>\<^sub>l sub_of_denot E) \<longleftrightarrow> eval\<^sub>l E HFun G l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval\<^sub>l E HFun G (l \<cdot>\<^sub>l sub_of_denot E) = eval\<^sub>l E HFun G l
[PROOF STEP]
proof (induction l)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x1 x2. eval\<^sub>l E HFun G (Pos x1 x2 \<cdot>\<^sub>l sub_of_denot E) = eval\<^sub>l E HFun G (Pos x1 x2)
 2. \<And>x1 x2. eval\<^sub>l E HFun G (Neg x1 x2 \<cdot>\<^sub>l sub_of_denot E) = eval\<^sub>l E HFun G (Neg x1 x2)
[PROOF STEP]
case (Pos p ts)
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. \<And>x1 x2. eval\<^sub>l E HFun G (Pos x1 x2 \<cdot>\<^sub>l sub_of_denot E) = eval\<^sub>l E HFun G (Pos x1 x2)
 2. \<And>x1 x2. eval\<^sub>l E HFun G (Neg x1 x2 \<cdot>\<^sub>l sub_of_denot E) = eval\<^sub>l E HFun G (Neg x1 x2)
[PROOF STEP]
have "eval\<^sub>l E HFun G ((Pos p ts) \<cdot>\<^sub>l sub_of_denot E) \<longleftrightarrow> G p (eval\<^sub>t\<^sub>s E HFun (ts \<cdot>\<^sub>t\<^sub>s (sub_of_denot E)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval\<^sub>l E HFun G (Pos p ts \<cdot>\<^sub>l sub_of_denot E) = G p (eval\<^sub>t\<^sub>s E HFun (ts \<cdot>\<^sub>t\<^sub>s sub_of_denot E))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
eval\<^sub>l E HFun G (Pos p ts \<cdot>\<^sub>l sub_of_denot E) = G p (eval\<^sub>t\<^sub>s E HFun (ts \<cdot>\<^sub>t\<^sub>s sub_of_denot E))

goal (2 subgoals):
 1. \<And>x1 x2. eval\<^sub>l E HFun G (Pos x1 x2 \<cdot>\<^sub>l sub_of_denot E) = eval\<^sub>l E HFun G (Pos x1 x2)
 2. \<And>x1 x2. eval\<^sub>l E HFun G (Neg x1 x2 \<cdot>\<^sub>l sub_of_denot E) = eval\<^sub>l E HFun G (Neg x1 x2)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
eval\<^sub>l E HFun G (Pos p ts \<cdot>\<^sub>l sub_of_denot E) = G p (eval\<^sub>t\<^sub>s E HFun (ts \<cdot>\<^sub>t\<^sub>s sub_of_denot E))

goal (2 subgoals):
 1. \<And>x1 x2. eval\<^sub>l E HFun G (Pos x1 x2 \<cdot>\<^sub>l sub_of_denot E) = eval\<^sub>l E HFun G (Pos x1 x2)
 2. \<And>x1 x2. eval\<^sub>l E HFun G (Neg x1 x2 \<cdot>\<^sub>l sub_of_denot E) = eval\<^sub>l E HFun G (Neg x1 x2)
[PROOF STEP]
have " ... \<longleftrightarrow> G p (eval\<^sub>t\<^sub>s E HFun ts)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. G p (eval\<^sub>t\<^sub>s E HFun (ts \<cdot>\<^sub>t\<^sub>s sub_of_denot E)) = G p (eval\<^sub>t\<^sub>s E HFun ts)
[PROOF STEP]
using sub_of_denot_equivts[of E ts]
[PROOF STATE]
proof (prove)
using this:
eval\<^sub>t\<^sub>s E HFun (ts \<cdot>\<^sub>t\<^sub>s sub_of_denot E) = eval\<^sub>t\<^sub>s E HFun ts

goal (1 subgoal):
 1. G p (eval\<^sub>t\<^sub>s E HFun (ts \<cdot>\<^sub>t\<^sub>s sub_of_denot E)) = G p (eval\<^sub>t\<^sub>s E HFun ts)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
G p (eval\<^sub>t\<^sub>s E HFun (ts \<cdot>\<^sub>t\<^sub>s sub_of_denot E)) = G p (eval\<^sub>t\<^sub>s E HFun ts)

goal (2 subgoals):
 1. \<And>x1 x2. eval\<^sub>l E HFun G (Pos x1 x2 \<cdot>\<^sub>l sub_of_denot E) = eval\<^sub>l E HFun G (Pos x1 x2)
 2. \<And>x1 x2. eval\<^sub>l E HFun G (Neg x1 x2 \<cdot>\<^sub>l sub_of_denot E) = eval\<^sub>l E HFun G (Neg x1 x2)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
G p (eval\<^sub>t\<^sub>s E HFun (ts \<cdot>\<^sub>t\<^sub>s sub_of_denot E)) = G p (eval\<^sub>t\<^sub>s E HFun ts)

goal (2 subgoals):
 1. \<And>x1 x2. eval\<^sub>l E HFun G (Pos x1 x2 \<cdot>\<^sub>l sub_of_denot E) = eval\<^sub>l E HFun G (Pos x1 x2)
 2. \<And>x1 x2. eval\<^sub>l E HFun G (Neg x1 x2 \<cdot>\<^sub>l sub_of_denot E) = eval\<^sub>l E HFun G (Neg x1 x2)
[PROOF STEP]
have " ... \<longleftrightarrow> eval\<^sub>l E HFun G (Pos p ts)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. G p (eval\<^sub>t\<^sub>s E HFun ts) = eval\<^sub>l E HFun G (Pos p ts)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
G p (eval\<^sub>t\<^sub>s E HFun ts) = eval\<^sub>l E HFun G (Pos p ts)

goal (2 subgoals):
 1. \<And>x1 x2. eval\<^sub>l E HFun G (Pos x1 x2 \<cdot>\<^sub>l sub_of_denot E) = eval\<^sub>l E HFun G (Pos x1 x2)
 2. \<And>x1 x2. eval\<^sub>l E HFun G (Neg x1 x2 \<cdot>\<^sub>l sub_of_denot E) = eval\<^sub>l E HFun G (Neg x1 x2)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
eval\<^sub>l E HFun G (Pos p ts \<cdot>\<^sub>l sub_of_denot E) = eval\<^sub>l E HFun G (Pos p ts)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
eval\<^sub>l E HFun G (Pos p ts \<cdot>\<^sub>l sub_of_denot E) = eval\<^sub>l E HFun G (Pos p ts)

goal (1 subgoal):
 1. eval\<^sub>l E HFun G (Pos p ts \<cdot>\<^sub>l sub_of_denot E) = eval\<^sub>l E HFun G (Pos p ts)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
eval\<^sub>l E HFun G (Pos p ts \<cdot>\<^sub>l sub_of_denot E) = eval\<^sub>l E HFun G (Pos p ts)

goal (1 subgoal):
 1. \<And>x1 x2. eval\<^sub>l E HFun G (Neg x1 x2 \<cdot>\<^sub>l sub_of_denot E) = eval\<^sub>l E HFun G (Neg x1 x2)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x1 x2. eval\<^sub>l E HFun G (Neg x1 x2 \<cdot>\<^sub>l sub_of_denot E) = eval\<^sub>l E HFun G (Neg x1 x2)
[PROOF STEP]
case (Neg p ts)
[PROOF STATE]
proof (state)
this:

goal (1 subgoal):
 1. \<And>x1 x2. eval\<^sub>l E HFun G (Neg x1 x2 \<cdot>\<^sub>l sub_of_denot E) = eval\<^sub>l E HFun G (Neg x1 x2)
[PROOF STEP]
have "eval\<^sub>l E HFun G ((Neg p ts) \<cdot>\<^sub>l sub_of_denot E) \<longleftrightarrow> \<not>G p (eval\<^sub>t\<^sub>s E HFun (ts \<cdot>\<^sub>t\<^sub>s (sub_of_denot E)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval\<^sub>l E HFun G (Neg p ts \<cdot>\<^sub>l sub_of_denot E) = (\<not> G p (eval\<^sub>t\<^sub>s E HFun (ts \<cdot>\<^sub>t\<^sub>s sub_of_denot E)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
eval\<^sub>l E HFun G (Neg p ts \<cdot>\<^sub>l sub_of_denot E) = (\<not> G p (eval\<^sub>t\<^sub>s E HFun (ts \<cdot>\<^sub>t\<^sub>s sub_of_denot E)))

goal (1 subgoal):
 1. \<And>x1 x2. eval\<^sub>l E HFun G (Neg x1 x2 \<cdot>\<^sub>l sub_of_denot E) = eval\<^sub>l E HFun G (Neg x1 x2)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
eval\<^sub>l E HFun G (Neg p ts \<cdot>\<^sub>l sub_of_denot E) = (\<not> G p (eval\<^sub>t\<^sub>s E HFun (ts \<cdot>\<^sub>t\<^sub>s sub_of_denot E)))

goal (1 subgoal):
 1. \<And>x1 x2. eval\<^sub>l E HFun G (Neg x1 x2 \<cdot>\<^sub>l sub_of_denot E) = eval\<^sub>l E HFun G (Neg x1 x2)
[PROOF STEP]
have " ... \<longleftrightarrow> \<not>G p (eval\<^sub>t\<^sub>s E HFun ts)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<not> G p (eval\<^sub>t\<^sub>s E HFun (ts \<cdot>\<^sub>t\<^sub>s sub_of_denot E))) = (\<not> G p (eval\<^sub>t\<^sub>s E HFun ts))
[PROOF STEP]
using sub_of_denot_equivts[of E ts]
[PROOF STATE]
proof (prove)
using this:
eval\<^sub>t\<^sub>s E HFun (ts \<cdot>\<^sub>t\<^sub>s sub_of_denot E) = eval\<^sub>t\<^sub>s E HFun ts

goal (1 subgoal):
 1. (\<not> G p (eval\<^sub>t\<^sub>s E HFun (ts \<cdot>\<^sub>t\<^sub>s sub_of_denot E))) = (\<not> G p (eval\<^sub>t\<^sub>s E HFun ts))
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
(\<not> G p (eval\<^sub>t\<^sub>s E HFun (ts \<cdot>\<^sub>t\<^sub>s sub_of_denot E))) = (\<not> G p (eval\<^sub>t\<^sub>s E HFun ts))

goal (1 subgoal):
 1. \<And>x1 x2. eval\<^sub>l E HFun G (Neg x1 x2 \<cdot>\<^sub>l sub_of_denot E) = eval\<^sub>l E HFun G (Neg x1 x2)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<not> G p (eval\<^sub>t\<^sub>s E HFun (ts \<cdot>\<^sub>t\<^sub>s sub_of_denot E))) = (\<not> G p (eval\<^sub>t\<^sub>s E HFun ts))

goal (1 subgoal):
 1. \<And>x1 x2. eval\<^sub>l E HFun G (Neg x1 x2 \<cdot>\<^sub>l sub_of_denot E) = eval\<^sub>l E HFun G (Neg x1 x2)
[PROOF STEP]
have " ... = eval\<^sub>l E HFun G (Neg p ts)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<not> G p (eval\<^sub>t\<^sub>s E HFun ts)) = eval\<^sub>l E HFun G (Neg p ts)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<not> G p (eval\<^sub>t\<^sub>s E HFun ts)) = eval\<^sub>l E HFun G (Neg p ts)

goal (1 subgoal):
 1. \<And>x1 x2. eval\<^sub>l E HFun G (Neg x1 x2 \<cdot>\<^sub>l sub_of_denot E) = eval\<^sub>l E HFun G (Neg x1 x2)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
eval\<^sub>l E HFun G (Neg p ts \<cdot>\<^sub>l sub_of_denot E) = eval\<^sub>l E HFun G (Neg p ts)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
eval\<^sub>l E HFun G (Neg p ts \<cdot>\<^sub>l sub_of_denot E) = eval\<^sub>l E HFun G (Neg p ts)

goal (1 subgoal):
 1. eval\<^sub>l E HFun G (Neg p ts \<cdot>\<^sub>l sub_of_denot E) = eval\<^sub>l E HFun G (Neg p ts)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
eval\<^sub>l E HFun G (Neg p ts \<cdot>\<^sub>l sub_of_denot E) = eval\<^sub>l E HFun G (Neg p ts)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sub_of_denot_equiv_ground':
  "eval\<^sub>l E HFun G l = eval\<^sub>l E HFun G (l \<cdot>\<^sub>l sub_of_denot E) \<and> ground\<^sub>l (l \<cdot>\<^sub>l sub_of_denot E)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval\<^sub>l E HFun G l = eval\<^sub>l E HFun G (l \<cdot>\<^sub>l sub_of_denot E) \<and> ground\<^sub>l (l \<cdot>\<^sub>l sub_of_denot E)
[PROOF STEP]
using sub_of_denot_equivl ground_sub_of_denotl
[PROOF STATE]
proof (prove)
using this:
eval\<^sub>l ?E HFun ?G (?l \<cdot>\<^sub>l sub_of_denot ?E) = eval\<^sub>l ?E HFun ?G ?l
ground\<^sub>l (?l \<cdot>\<^sub>l sub_of_denot ?E)

goal (1 subgoal):
 1. eval\<^sub>l E HFun G l = eval\<^sub>l E HFun G (l \<cdot>\<^sub>l sub_of_denot E) \<and> ground\<^sub>l (l \<cdot>\<^sub>l sub_of_denot E)
[PROOF STEP]
by auto


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

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

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

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

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

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

goal (1 subgoal):
 1. instance_of\<^sub>l\<^sub>s C' C
[PROOF STEP]
using C'_p instance_of\<^sub>l\<^sub>s_trans
[PROOF STATE]
proof (prove)
using this:
instance_of\<^sub>l\<^sub>s (C \<cdot>\<^sub>l\<^sub>s \<tau>) C
instance_of\<^sub>l\<^sub>s C' (C \<cdot>\<^sub>l\<^sub>s \<tau>) \<and> falsifies\<^sub>g G C'
\<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 C' C
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
instance_of\<^sub>l\<^sub>s C' C

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

goal (1 subgoal):
 1. falsifies\<^sub>c G C
[PROOF STEP]
using C'_p
[PROOF STATE]
proof (prove)
using this:
instance_of\<^sub>l\<^sub>s C' C
instance_of\<^sub>l\<^sub>s C' (C \<cdot>\<^sub>l\<^sub>s \<tau>) \<and> falsifies\<^sub>g G C'

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sub_of_denot_equiv_ground:
  "((\<exists>l \<in> C. eval\<^sub>l E HFun G l) \<longleftrightarrow> (\<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)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<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)
[PROOF STEP]
using sub_of_denot_equiv_ground'
[PROOF STATE]
proof (prove)
using this:
eval\<^sub>l ?E HFun ?G ?l = eval\<^sub>l ?E HFun ?G (?l \<cdot>\<^sub>l sub_of_denot ?E) \<and> ground\<^sub>l (?l \<cdot>\<^sub>l sub_of_denot ?E)

goal (1 subgoal):
 1. (\<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)
[PROOF STEP]
by auto