[STATEMENT]
lemma wfLearnLess:
  fixes C::Clause
  shows "wf (learnLess C)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf (learnLess C)
[PROOF STEP]
unfolding wf_eq_minimal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>Q x. x \<in> Q \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. (y, z) \<in> learnLess C \<longrightarrow> y \<notin> Q)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>Q x. x \<in> Q \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. (y, z) \<in> learnLess C \<longrightarrow> y \<notin> Q)
[PROOF STEP]
show "\<forall>Q F. F \<in> Q \<longrightarrow> (\<exists>Fmin\<in>Q. \<forall>F'. (F', Fmin) \<in> learnLess C \<longrightarrow> F' \<notin> Q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>Q F. F \<in> Q \<longrightarrow> (\<exists>Fmin\<in>Q. \<forall>F'. (F', Fmin) \<in> learnLess C \<longrightarrow> F' \<notin> Q)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>Q F. F \<in> Q \<longrightarrow> (\<exists>Fmin\<in>Q. \<forall>F'. (F', Fmin) \<in> learnLess C \<longrightarrow> F' \<notin> Q)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>Q F. F \<in> Q \<longrightarrow> (\<exists>Fmin\<in>Q. \<forall>F'. (F', Fmin) \<in> learnLess C \<longrightarrow> F' \<notin> Q)
[PROOF STEP]
fix F::Formula and Q::"Formula set"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>Q F. F \<in> Q \<longrightarrow> (\<exists>Fmin\<in>Q. \<forall>F'. (F', Fmin) \<in> learnLess C \<longrightarrow> F' \<notin> Q)
[PROOF STEP]
assume "F \<in> Q"
[PROOF STATE]
proof (state)
this:
F \<in> Q

goal (1 subgoal):
 1. \<forall>Q F. F \<in> Q \<longrightarrow> (\<exists>Fmin\<in>Q. \<forall>F'. (F', Fmin) \<in> learnLess C \<longrightarrow> F' \<notin> Q)
[PROOF STEP]
have "\<exists>Fmin\<in>Q. \<forall>F'. (F', Fmin) \<in> learnLess C \<longrightarrow> F' \<notin> Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>Fmin\<in>Q. \<forall>F'. (F', Fmin) \<in> learnLess C \<longrightarrow> F' \<notin> Q
[PROOF STEP]
proof (cases "\<exists> Fc \<in> Q. C el Fc")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<exists>Fc\<in>Q. C el Fc \<Longrightarrow> \<exists>Fmin\<in>Q. \<forall>F'. (F', Fmin) \<in> learnLess C \<longrightarrow> F' \<notin> Q
 2. \<not> (\<exists>Fc\<in>Q. C el Fc) \<Longrightarrow> \<exists>Fmin\<in>Q. \<forall>F'. (F', Fmin) \<in> learnLess C \<longrightarrow> F' \<notin> Q
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
\<exists>Fc\<in>Q. C el Fc

goal (2 subgoals):
 1. \<exists>Fc\<in>Q. C el Fc \<Longrightarrow> \<exists>Fmin\<in>Q. \<forall>F'. (F', Fmin) \<in> learnLess C \<longrightarrow> F' \<notin> Q
 2. \<not> (\<exists>Fc\<in>Q. C el Fc) \<Longrightarrow> \<exists>Fmin\<in>Q. \<forall>F'. (F', Fmin) \<in> learnLess C \<longrightarrow> F' \<notin> Q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>Fc\<in>Q. C el Fc
[PROOF STEP]
obtain Fc where "Fc \<in> Q" "C el Fc"
[PROOF STATE]
proof (prove)
using this:
\<exists>Fc\<in>Q. C el Fc

goal (1 subgoal):
 1. (\<And>Fc. \<lbrakk>Fc \<in> Q; C el Fc\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Fc \<in> Q
C el Fc

goal (2 subgoals):
 1. \<exists>Fc\<in>Q. C el Fc \<Longrightarrow> \<exists>Fmin\<in>Q. \<forall>F'. (F', Fmin) \<in> learnLess C \<longrightarrow> F' \<notin> Q
 2. \<not> (\<exists>Fc\<in>Q. C el Fc) \<Longrightarrow> \<exists>Fmin\<in>Q. \<forall>F'. (F', Fmin) \<in> learnLess C \<longrightarrow> F' \<notin> Q
[PROOF STEP]
have "\<forall>F'. (F', Fc) \<in> learnLess C \<longrightarrow> F' \<notin> Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>F'. (F', Fc) \<in> learnLess C \<longrightarrow> F' \<notin> Q
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>F'. (F', Fc) \<in> learnLess C \<longrightarrow> F' \<notin> Q
[PROOF STEP]
fix F'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>F'. (F', Fc) \<in> learnLess C \<longrightarrow> F' \<notin> Q
[PROOF STEP]
show "(F', Fc) \<in> learnLess C \<longrightarrow> F' \<notin> Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (F', Fc) \<in> learnLess C \<longrightarrow> F' \<notin> Q
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (F', Fc) \<in> learnLess C \<Longrightarrow> F' \<notin> Q
[PROOF STEP]
assume "(F', Fc) \<in> learnLess C"
[PROOF STATE]
proof (state)
this:
(F', Fc) \<in> learnLess C

goal (1 subgoal):
 1. (F', Fc) \<in> learnLess C \<Longrightarrow> F' \<notin> Q
[PROOF STEP]
hence "\<not> C el Fc"
[PROOF STATE]
proof (prove)
using this:
(F', Fc) \<in> learnLess C

goal (1 subgoal):
 1. \<not> C el Fc
[PROOF STEP]
unfolding learnLess_def
[PROOF STATE]
proof (prove)
using this:
(F', Fc) \<in> {(F1, F2). C el F1 \<and> \<not> C el F2}

goal (1 subgoal):
 1. \<not> C el Fc
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<not> C el Fc

goal (1 subgoal):
 1. (F', Fc) \<in> learnLess C \<Longrightarrow> F' \<notin> Q
[PROOF STEP]
with \<open>C el Fc\<close>
[PROOF STATE]
proof (chain)
picking this:
C el Fc
\<not> C el Fc
[PROOF STEP]
have False
[PROOF STATE]
proof (prove)
using this:
C el Fc
\<not> C el Fc

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

goal (1 subgoal):
 1. (F', Fc) \<in> learnLess C \<Longrightarrow> F' \<notin> Q
[PROOF STEP]
thus "F' \<notin> Q"
[PROOF STATE]
proof (prove)
using this:
False

goal (1 subgoal):
 1. F' \<notin> Q
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
F' \<notin> Q

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(F', Fc) \<in> learnLess C \<longrightarrow> F' \<notin> Q

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>F'. (F', Fc) \<in> learnLess C \<longrightarrow> F' \<notin> Q

goal (2 subgoals):
 1. \<exists>Fc\<in>Q. C el Fc \<Longrightarrow> \<exists>Fmin\<in>Q. \<forall>F'. (F', Fmin) \<in> learnLess C \<longrightarrow> F' \<notin> Q
 2. \<not> (\<exists>Fc\<in>Q. C el Fc) \<Longrightarrow> \<exists>Fmin\<in>Q. \<forall>F'. (F', Fmin) \<in> learnLess C \<longrightarrow> F' \<notin> Q
[PROOF STEP]
with \<open>Fc \<in> Q\<close>
[PROOF STATE]
proof (chain)
picking this:
Fc \<in> Q
\<forall>F'. (F', Fc) \<in> learnLess C \<longrightarrow> F' \<notin> Q
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
Fc \<in> Q
\<forall>F'. (F', Fc) \<in> learnLess C \<longrightarrow> F' \<notin> Q

goal (1 subgoal):
 1. \<exists>Fmin\<in>Q. \<forall>F'. (F', Fmin) \<in> learnLess C \<longrightarrow> F' \<notin> Q
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>Fmin\<in>Q. \<forall>F'. (F', Fmin) \<in> learnLess C \<longrightarrow> F' \<notin> Q

goal (1 subgoal):
 1. \<not> (\<exists>Fc\<in>Q. C el Fc) \<Longrightarrow> \<exists>Fmin\<in>Q. \<forall>F'. (F', Fmin) \<in> learnLess C \<longrightarrow> F' \<notin> Q
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (\<exists>Fc\<in>Q. C el Fc) \<Longrightarrow> \<exists>Fmin\<in>Q. \<forall>F'. (F', Fmin) \<in> learnLess C \<longrightarrow> F' \<notin> Q
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> (\<exists>Fc\<in>Q. C el Fc)

goal (1 subgoal):
 1. \<not> (\<exists>Fc\<in>Q. C el Fc) \<Longrightarrow> \<exists>Fmin\<in>Q. \<forall>F'. (F', Fmin) \<in> learnLess C \<longrightarrow> F' \<notin> Q
[PROOF STEP]
have "\<forall>F'. (F', F) \<in> learnLess C \<longrightarrow> F' \<notin> Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>F'. (F', F) \<in> learnLess C \<longrightarrow> F' \<notin> Q
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>F'. (F', F) \<in> learnLess C \<longrightarrow> F' \<notin> Q
[PROOF STEP]
fix F'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>F'. (F', F) \<in> learnLess C \<longrightarrow> F' \<notin> Q
[PROOF STEP]
show "(F', F) \<in> learnLess C \<longrightarrow> F' \<notin> Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (F', F) \<in> learnLess C \<longrightarrow> F' \<notin> Q
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (F', F) \<in> learnLess C \<Longrightarrow> F' \<notin> Q
[PROOF STEP]
assume "(F', F) \<in> learnLess C"
[PROOF STATE]
proof (state)
this:
(F', F) \<in> learnLess C

goal (1 subgoal):
 1. (F', F) \<in> learnLess C \<Longrightarrow> F' \<notin> Q
[PROOF STEP]
hence "C el F'"
[PROOF STATE]
proof (prove)
using this:
(F', F) \<in> learnLess C

goal (1 subgoal):
 1. C el F'
[PROOF STEP]
unfolding learnLess_def
[PROOF STATE]
proof (prove)
using this:
(F', F) \<in> {(F1, F2). C el F1 \<and> \<not> C el F2}

goal (1 subgoal):
 1. C el F'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
C el F'

goal (1 subgoal):
 1. (F', F) \<in> learnLess C \<Longrightarrow> F' \<notin> Q
[PROOF STEP]
with False
[PROOF STATE]
proof (chain)
picking this:
\<not> (\<exists>Fc\<in>Q. C el Fc)
C el F'
[PROOF STEP]
show "F' \<notin> Q"
[PROOF STATE]
proof (prove)
using this:
\<not> (\<exists>Fc\<in>Q. C el Fc)
C el F'

goal (1 subgoal):
 1. F' \<notin> Q
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
F' \<notin> Q

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(F', F) \<in> learnLess C \<longrightarrow> F' \<notin> Q

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>F'. (F', F) \<in> learnLess C \<longrightarrow> F' \<notin> Q

goal (1 subgoal):
 1. \<not> (\<exists>Fc\<in>Q. C el Fc) \<Longrightarrow> \<exists>Fmin\<in>Q. \<forall>F'. (F', Fmin) \<in> learnLess C \<longrightarrow> F' \<notin> Q
[PROOF STEP]
with \<open>F \<in> Q\<close>
[PROOF STATE]
proof (chain)
picking this:
F \<in> Q
\<forall>F'. (F', F) \<in> learnLess C \<longrightarrow> F' \<notin> Q
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
F \<in> Q
\<forall>F'. (F', F) \<in> learnLess C \<longrightarrow> F' \<notin> Q

goal (1 subgoal):
 1. \<exists>Fmin\<in>Q. \<forall>F'. (F', Fmin) \<in> learnLess C \<longrightarrow> F' \<notin> Q
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>Fmin\<in>Q. \<forall>F'. (F', Fmin) \<in> learnLess C \<longrightarrow> F' \<notin> Q

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>Fmin\<in>Q. \<forall>F'. (F', Fmin) \<in> learnLess C \<longrightarrow> F' \<notin> Q

goal (1 subgoal):
 1. \<forall>Q F. F \<in> Q \<longrightarrow> (\<exists>Fmin\<in>Q. \<forall>F'. (F', Fmin) \<in> learnLess C \<longrightarrow> F' \<notin> Q)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?F2 \<in> ?Q2 \<Longrightarrow> \<exists>Fmin\<in>?Q2. \<forall>F'. (F', Fmin) \<in> learnLess C \<longrightarrow> F' \<notin> ?Q2

goal (1 subgoal):
 1. \<forall>Q F. F \<in> Q \<longrightarrow> (\<exists>Fmin\<in>Q. \<forall>F'. (F', Fmin) \<in> learnLess C \<longrightarrow> F' \<notin> Q)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
?F2 \<in> ?Q2 \<Longrightarrow> \<exists>Fmin\<in>?Q2. \<forall>F'. (F', Fmin) \<in> learnLess C \<longrightarrow> F' \<notin> ?Q2

goal (1 subgoal):
 1. \<forall>Q F. F \<in> Q \<longrightarrow> (\<exists>Fmin\<in>Q. \<forall>F'. (F', Fmin) \<in> learnLess C \<longrightarrow> F' \<notin> Q)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>Q F. F \<in> Q \<longrightarrow> (\<exists>Fmin\<in>Q. \<forall>F'. (F', Fmin) \<in> learnLess C \<longrightarrow> F' \<notin> Q)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>Q F. F \<in> Q \<longrightarrow> (\<exists>Fmin\<in>Q. \<forall>F'. (F', Fmin) \<in> learnLess C \<longrightarrow> F' \<notin> Q)

goal:
No subgoals!
[PROOF STEP]
qed