[STATEMENT]
lemma finiteUniqAndConsistentTrailsWithGivenVariableSuperset:
  fixes V :: "Variable set"
  assumes "finite V"
  shows "finite {(M::LiteralTrail). vars (elements M) \<subseteq> V \<and> uniq (elements M) \<and> consistent (elements M)}" (is "finite (?trails V)")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {M. vars (elements M) \<subseteq> V \<and> uniq (elements M) \<and> consistent (elements M)}
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. finite {M. vars (elements M) \<subseteq> V \<and> uniq (elements M) \<and> consistent (elements M)}
[PROOF STEP]
have "{M. vars (elements M) \<subseteq> V \<and> uniq (elements M) \<and> consistent (elements M)} =
    (\<Union> v \<in> Pow V.{M. vars (elements M) = v \<and> uniq (elements M) \<and> consistent (elements M)})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {M. vars (elements M) \<subseteq> V \<and> uniq (elements M) \<and> consistent (elements M)} = (\<Union>v\<in>Pow V. {M. vars (elements M) = v \<and> uniq (elements M) \<and> consistent (elements M)})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{M. vars (elements M) \<subseteq> V \<and> uniq (elements M) \<and> consistent (elements M)} = (\<Union>v\<in>Pow V. {M. vars (elements M) = v \<and> uniq (elements M) \<and> consistent (elements M)})

goal (1 subgoal):
 1. finite {M. vars (elements M) \<subseteq> V \<and> uniq (elements M) \<and> consistent (elements M)}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
{M. vars (elements M) \<subseteq> V \<and> uniq (elements M) \<and> consistent (elements M)} = (\<Union>v\<in>Pow V. {M. vars (elements M) = v \<and> uniq (elements M) \<and> consistent (elements M)})

goal (1 subgoal):
 1. finite {M. vars (elements M) \<subseteq> V \<and> uniq (elements M) \<and> consistent (elements M)}
[PROOF STEP]
have "finite (\<Union> v \<in> Pow V.{M. vars (elements M) = v \<and> uniq (elements M) \<and> consistent (elements M)})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (\<Union>v\<in>Pow V. {M. vars (elements M) = v \<and> uniq (elements M) \<and> consistent (elements M)})
[PROOF STEP]
proof (rule finite_UN_I)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. finite (Pow V)
 2. \<And>v. v \<in> Pow V \<Longrightarrow> finite {M. vars (elements M) = v \<and> uniq (elements M) \<and> consistent (elements M)}
[PROOF STEP]
from \<open>finite V\<close>
[PROOF STATE]
proof (chain)
picking this:
finite V
[PROOF STEP]
show "finite (Pow V)"
[PROOF STATE]
proof (prove)
using this:
finite V

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

goal (1 subgoal):
 1. \<And>v. v \<in> Pow V \<Longrightarrow> finite {M. vars (elements M) = v \<and> uniq (elements M) \<and> consistent (elements M)}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>v. v \<in> Pow V \<Longrightarrow> finite {M. vars (elements M) = v \<and> uniq (elements M) \<and> consistent (elements M)}
[PROOF STEP]
fix v
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>v. v \<in> Pow V \<Longrightarrow> finite {M. vars (elements M) = v \<and> uniq (elements M) \<and> consistent (elements M)}
[PROOF STEP]
assume "v \<in> Pow V"
[PROOF STATE]
proof (state)
this:
v \<in> Pow V

goal (1 subgoal):
 1. \<And>v. v \<in> Pow V \<Longrightarrow> finite {M. vars (elements M) = v \<and> uniq (elements M) \<and> consistent (elements M)}
[PROOF STEP]
with \<open>finite V\<close>
[PROOF STATE]
proof (chain)
picking this:
finite V
v \<in> Pow V
[PROOF STEP]
have "finite v"
[PROOF STATE]
proof (prove)
using this:
finite V
v \<in> Pow V

goal (1 subgoal):
 1. finite v
[PROOF STEP]
by (auto simp add: finite_subset)
[PROOF STATE]
proof (state)
this:
finite v

goal (1 subgoal):
 1. \<And>v. v \<in> Pow V \<Longrightarrow> finite {M. vars (elements M) = v \<and> uniq (elements M) \<and> consistent (elements M)}
[PROOF STEP]
thus "finite {M. vars (elements M) = v \<and> uniq (elements M) \<and> consistent (elements M)}"
[PROOF STATE]
proof (prove)
using this:
finite v

goal (1 subgoal):
 1. finite {M. vars (elements M) = v \<and> uniq (elements M) \<and> consistent (elements M)}
[PROOF STEP]
using finiteUniqAndConsistentTrailsWithGivenVariableSet[of "v"]
[PROOF STATE]
proof (prove)
using this:
finite v
finite v \<Longrightarrow> finite {M. vars (elements M) = v \<and> uniq (elements M) \<and> consistent (elements M)}

goal (1 subgoal):
 1. finite {M. vars (elements M) = v \<and> uniq (elements M) \<and> consistent (elements M)}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
finite {M. vars (elements M) = v \<and> uniq (elements M) \<and> consistent (elements M)}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
finite (\<Union>v\<in>Pow V. {M. vars (elements M) = v \<and> uniq (elements M) \<and> consistent (elements M)})

goal (1 subgoal):
 1. finite {M. vars (elements M) \<subseteq> V \<and> uniq (elements M) \<and> consistent (elements M)}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
{M. vars (elements M) \<subseteq> V \<and> uniq (elements M) \<and> consistent (elements M)} = (\<Union>v\<in>Pow V. {M. vars (elements M) = v \<and> uniq (elements M) \<and> consistent (elements M)})
finite (\<Union>v\<in>Pow V. {M. vars (elements M) = v \<and> uniq (elements M) \<and> consistent (elements M)})
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
{M. vars (elements M) \<subseteq> V \<and> uniq (elements M) \<and> consistent (elements M)} = (\<Union>v\<in>Pow V. {M. vars (elements M) = v \<and> uniq (elements M) \<and> consistent (elements M)})
finite (\<Union>v\<in>Pow V. {M. vars (elements M) = v \<and> uniq (elements M) \<and> consistent (elements M)})

goal (1 subgoal):
 1. finite {M. vars (elements M) \<subseteq> V \<and> uniq (elements M) \<and> consistent (elements M)}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
finite {M. vars (elements M) \<subseteq> V \<and> uniq (elements M) \<and> consistent (elements M)}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma wfLexLessRestricted:
  assumes "finite Vbl"
  shows "wf (lexLessRestricted Vbl)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf (lexLessRestricted Vbl)
[PROOF STEP]
proof (rule finite_acyclic_wf)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. finite (lexLessRestricted Vbl)
 2. acyclic (lexLessRestricted Vbl)
[PROOF STEP]
show "finite (lexLessRestricted Vbl)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (lexLessRestricted Vbl)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. finite (lexLessRestricted Vbl)
[PROOF STEP]
let ?X = "{(M1, M2).
      consistent (elements M1) \<and> uniq (elements M1) \<and> vars (elements M1) \<subseteq> Vbl \<and>
      consistent (elements M2) \<and> uniq (elements M2) \<and> vars (elements M2) \<subseteq> Vbl}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. finite (lexLessRestricted Vbl)
[PROOF STEP]
let ?Y = "{M. vars (elements M) \<subseteq> Vbl \<and> uniq (elements M) \<and> consistent (elements M)}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. finite (lexLessRestricted Vbl)
[PROOF STEP]
have "?X = ?Y \<times> ?Y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {(M1, M2). consistent (elements M1) \<and> uniq (elements M1) \<and> vars (elements M1) \<subseteq> Vbl \<and> consistent (elements M2) \<and> uniq (elements M2) \<and> vars (elements M2) \<subseteq> Vbl} = {M. vars (elements M) \<subseteq> Vbl \<and> uniq (elements M) \<and> consistent (elements M)} \<times> {M. vars (elements M) \<subseteq> Vbl \<and> uniq (elements M) \<and> consistent (elements M)}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{(M1, M2). consistent (elements M1) \<and> uniq (elements M1) \<and> vars (elements M1) \<subseteq> Vbl \<and> consistent (elements M2) \<and> uniq (elements M2) \<and> vars (elements M2) \<subseteq> Vbl} = {M. vars (elements M) \<subseteq> Vbl \<and> uniq (elements M) \<and> consistent (elements M)} \<times> {M. vars (elements M) \<subseteq> Vbl \<and> uniq (elements M) \<and> consistent (elements M)}

goal (1 subgoal):
 1. finite (lexLessRestricted Vbl)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
{(M1, M2). consistent (elements M1) \<and> uniq (elements M1) \<and> vars (elements M1) \<subseteq> Vbl \<and> consistent (elements M2) \<and> uniq (elements M2) \<and> vars (elements M2) \<subseteq> Vbl} = {M. vars (elements M) \<subseteq> Vbl \<and> uniq (elements M) \<and> consistent (elements M)} \<times> {M. vars (elements M) \<subseteq> Vbl \<and> uniq (elements M) \<and> consistent (elements M)}

goal (1 subgoal):
 1. finite (lexLessRestricted Vbl)
[PROOF STEP]
have "finite ?Y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {M. vars (elements M) \<subseteq> Vbl \<and> uniq (elements M) \<and> consistent (elements M)}
[PROOF STEP]
using finiteUniqAndConsistentTrailsWithGivenVariableSuperset[of "Vbl"]
        \<open>finite Vbl\<close>
[PROOF STATE]
proof (prove)
using this:
finite Vbl \<Longrightarrow> finite {M. vars (elements M) \<subseteq> Vbl \<and> uniq (elements M) \<and> consistent (elements M)}
finite Vbl

goal (1 subgoal):
 1. finite {M. vars (elements M) \<subseteq> Vbl \<and> uniq (elements M) \<and> consistent (elements M)}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite {M. vars (elements M) \<subseteq> Vbl \<and> uniq (elements M) \<and> consistent (elements M)}

goal (1 subgoal):
 1. finite (lexLessRestricted Vbl)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
{(M1, M2). consistent (elements M1) \<and> uniq (elements M1) \<and> vars (elements M1) \<subseteq> Vbl \<and> consistent (elements M2) \<and> uniq (elements M2) \<and> vars (elements M2) \<subseteq> Vbl} = {M. vars (elements M) \<subseteq> Vbl \<and> uniq (elements M) \<and> consistent (elements M)} \<times> {M. vars (elements M) \<subseteq> Vbl \<and> uniq (elements M) \<and> consistent (elements M)}
finite {M. vars (elements M) \<subseteq> Vbl \<and> uniq (elements M) \<and> consistent (elements M)}
[PROOF STEP]
have "finite ?X"
[PROOF STATE]
proof (prove)
using this:
{(M1, M2). consistent (elements M1) \<and> uniq (elements M1) \<and> vars (elements M1) \<subseteq> Vbl \<and> consistent (elements M2) \<and> uniq (elements M2) \<and> vars (elements M2) \<subseteq> Vbl} = {M. vars (elements M) \<subseteq> Vbl \<and> uniq (elements M) \<and> consistent (elements M)} \<times> {M. vars (elements M) \<subseteq> Vbl \<and> uniq (elements M) \<and> consistent (elements M)}
finite {M. vars (elements M) \<subseteq> Vbl \<and> uniq (elements M) \<and> consistent (elements M)}

goal (1 subgoal):
 1. finite {(M1, M2). consistent (elements M1) \<and> uniq (elements M1) \<and> vars (elements M1) \<subseteq> Vbl \<and> consistent (elements M2) \<and> uniq (elements M2) \<and> vars (elements M2) \<subseteq> Vbl}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
finite {(M1, M2). consistent (elements M1) \<and> uniq (elements M1) \<and> vars (elements M1) \<subseteq> Vbl \<and> consistent (elements M2) \<and> uniq (elements M2) \<and> vars (elements M2) \<subseteq> Vbl}

goal (1 subgoal):
 1. finite (lexLessRestricted Vbl)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
finite {(M1, M2). consistent (elements M1) \<and> uniq (elements M1) \<and> vars (elements M1) \<subseteq> Vbl \<and> consistent (elements M2) \<and> uniq (elements M2) \<and> vars (elements M2) \<subseteq> Vbl}

goal (1 subgoal):
 1. finite (lexLessRestricted Vbl)
[PROOF STEP]
have "lexLessRestricted Vbl \<subseteq> ?X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lexLessRestricted Vbl \<subseteq> {(M1, M2). consistent (elements M1) \<and> uniq (elements M1) \<and> vars (elements M1) \<subseteq> Vbl \<and> consistent (elements M2) \<and> uniq (elements M2) \<and> vars (elements M2) \<subseteq> Vbl}
[PROOF STEP]
unfolding lexLessRestricted_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {(M1, M2). vars (elements M1) \<subseteq> Vbl \<and> consistent (elements M1) \<and> uniq (elements M1) \<and> vars (elements M2) \<subseteq> Vbl \<and> consistent (elements M2) \<and> uniq (elements M2) \<and> (M1, M2) \<in> lexLess} \<subseteq> {(M1, M2). consistent (elements M1) \<and> uniq (elements M1) \<and> vars (elements M1) \<subseteq> Vbl \<and> consistent (elements M2) \<and> uniq (elements M2) \<and> vars (elements M2) \<subseteq> Vbl}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
lexLessRestricted Vbl \<subseteq> {(M1, M2). consistent (elements M1) \<and> uniq (elements M1) \<and> vars (elements M1) \<subseteq> Vbl \<and> consistent (elements M2) \<and> uniq (elements M2) \<and> vars (elements M2) \<subseteq> Vbl}

goal (1 subgoal):
 1. finite (lexLessRestricted Vbl)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
finite {(M1, M2). consistent (elements M1) \<and> uniq (elements M1) \<and> vars (elements M1) \<subseteq> Vbl \<and> consistent (elements M2) \<and> uniq (elements M2) \<and> vars (elements M2) \<subseteq> Vbl}
lexLessRestricted Vbl \<subseteq> {(M1, M2). consistent (elements M1) \<and> uniq (elements M1) \<and> vars (elements M1) \<subseteq> Vbl \<and> consistent (elements M2) \<and> uniq (elements M2) \<and> vars (elements M2) \<subseteq> Vbl}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
finite {(M1, M2). consistent (elements M1) \<and> uniq (elements M1) \<and> vars (elements M1) \<subseteq> Vbl \<and> consistent (elements M2) \<and> uniq (elements M2) \<and> vars (elements M2) \<subseteq> Vbl}
lexLessRestricted Vbl \<subseteq> {(M1, M2). consistent (elements M1) \<and> uniq (elements M1) \<and> vars (elements M1) \<subseteq> Vbl \<and> consistent (elements M2) \<and> uniq (elements M2) \<and> vars (elements M2) \<subseteq> Vbl}

goal (1 subgoal):
 1. finite (lexLessRestricted Vbl)
[PROOF STEP]
by (simp add: finite_subset)
[PROOF STATE]
proof (state)
this:
finite (lexLessRestricted Vbl)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
finite (lexLessRestricted Vbl)

goal (1 subgoal):
 1. acyclic (lexLessRestricted Vbl)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. acyclic (lexLessRestricted Vbl)
[PROOF STEP]
show "acyclic (lexLessRestricted Vbl)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. acyclic (lexLessRestricted Vbl)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. acyclic (lexLessRestricted Vbl)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. acyclic (lexLessRestricted Vbl)
[PROOF STEP]
assume "\<not> ?thesis"
[PROOF STATE]
proof (state)
this:
\<not> acyclic (lexLessRestricted Vbl)

goal (1 subgoal):
 1. acyclic (lexLessRestricted Vbl)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> acyclic (lexLessRestricted Vbl)
[PROOF STEP]
obtain x where "(x, x) \<in> (lexLessRestricted Vbl)^+"
[PROOF STATE]
proof (prove)
using this:
\<not> acyclic (lexLessRestricted Vbl)

goal (1 subgoal):
 1. (\<And>x. (x, x) \<in> (lexLessRestricted Vbl)\<^sup>+ \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding acyclic_def
[PROOF STATE]
proof (prove)
using this:
\<not> (\<forall>x. (x, x) \<notin> (lexLessRestricted Vbl)\<^sup>+)

goal (1 subgoal):
 1. (\<And>x. (x, x) \<in> (lexLessRestricted Vbl)\<^sup>+ \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(x, x) \<in> (lexLessRestricted Vbl)\<^sup>+

goal (1 subgoal):
 1. acyclic (lexLessRestricted Vbl)
[PROOF STEP]
have "lexLessRestricted Vbl \<subseteq> lexLess"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lexLessRestricted Vbl \<subseteq> lexLess
[PROOF STEP]
unfolding lexLessRestricted_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {(M1, M2). vars (elements M1) \<subseteq> Vbl \<and> consistent (elements M1) \<and> uniq (elements M1) \<and> vars (elements M2) \<subseteq> Vbl \<and> consistent (elements M2) \<and> uniq (elements M2) \<and> (M1, M2) \<in> lexLess} \<subseteq> lexLess
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
lexLessRestricted Vbl \<subseteq> lexLess

goal (1 subgoal):
 1. acyclic (lexLessRestricted Vbl)
[PROOF STEP]
have "(lexLessRestricted Vbl)^+ \<subseteq> lexLess^+"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (lexLessRestricted Vbl)\<^sup>+ \<subseteq> lexLess\<^sup>+
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> (lexLessRestricted Vbl)\<^sup>+ \<Longrightarrow> x \<in> lexLess\<^sup>+
[PROOF STEP]
fix a
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> (lexLessRestricted Vbl)\<^sup>+ \<Longrightarrow> x \<in> lexLess\<^sup>+
[PROOF STEP]
assume "a \<in> (lexLessRestricted Vbl)^+"
[PROOF STATE]
proof (state)
this:
a \<in> (lexLessRestricted Vbl)\<^sup>+

goal (1 subgoal):
 1. \<And>x. x \<in> (lexLessRestricted Vbl)\<^sup>+ \<Longrightarrow> x \<in> lexLess\<^sup>+
[PROOF STEP]
with \<open>lexLessRestricted Vbl \<subseteq> lexLess\<close>
[PROOF STATE]
proof (chain)
picking this:
lexLessRestricted Vbl \<subseteq> lexLess
a \<in> (lexLessRestricted Vbl)\<^sup>+
[PROOF STEP]
show "a \<in> lexLess^+"
[PROOF STATE]
proof (prove)
using this:
lexLessRestricted Vbl \<subseteq> lexLess
a \<in> (lexLessRestricted Vbl)\<^sup>+

goal (1 subgoal):
 1. a \<in> lexLess\<^sup>+
[PROOF STEP]
using trancl_mono[of "a" "lexLessRestricted Vbl" "lexLess"]
[PROOF STATE]
proof (prove)
using this:
lexLessRestricted Vbl \<subseteq> lexLess
a \<in> (lexLessRestricted Vbl)\<^sup>+
\<lbrakk>a \<in> (lexLessRestricted Vbl)\<^sup>+; lexLessRestricted Vbl \<subseteq> lexLess\<rbrakk> \<Longrightarrow> a \<in> lexLess\<^sup>+

goal (1 subgoal):
 1. a \<in> lexLess\<^sup>+
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
a \<in> lexLess\<^sup>+

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(lexLessRestricted Vbl)\<^sup>+ \<subseteq> lexLess\<^sup>+

goal (1 subgoal):
 1. acyclic (lexLessRestricted Vbl)
[PROOF STEP]
with \<open>(x, x) \<in> (lexLessRestricted Vbl)^+\<close>
[PROOF STATE]
proof (chain)
picking this:
(x, x) \<in> (lexLessRestricted Vbl)\<^sup>+
(lexLessRestricted Vbl)\<^sup>+ \<subseteq> lexLess\<^sup>+
[PROOF STEP]
have "(x, x) \<in> lexLess^+"
[PROOF STATE]
proof (prove)
using this:
(x, x) \<in> (lexLessRestricted Vbl)\<^sup>+
(lexLessRestricted Vbl)\<^sup>+ \<subseteq> lexLess\<^sup>+

goal (1 subgoal):
 1. (x, x) \<in> lexLess\<^sup>+
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(x, x) \<in> lexLess\<^sup>+

goal (1 subgoal):
 1. acyclic (lexLessRestricted Vbl)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(x, x) \<in> lexLess\<^sup>+

goal (1 subgoal):
 1. acyclic (lexLessRestricted Vbl)
[PROOF STEP]
have "trans lexLess"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trans lexLess
[PROOF STEP]
using translexLess
[PROOF STATE]
proof (prove)
using this:
trans lexLess

goal (1 subgoal):
 1. trans lexLess
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
trans lexLess

goal (1 subgoal):
 1. acyclic (lexLessRestricted Vbl)
[PROOF STEP]
hence "lexLess^+ = lexLess"
[PROOF STATE]
proof (prove)
using this:
trans lexLess

goal (1 subgoal):
 1. lexLess\<^sup>+ = lexLess
[PROOF STEP]
by (rule trancl_id)
[PROOF STATE]
proof (state)
this:
lexLess\<^sup>+ = lexLess

goal (1 subgoal):
 1. acyclic (lexLessRestricted Vbl)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(x, x) \<in> lexLess\<^sup>+
lexLess\<^sup>+ = lexLess
[PROOF STEP]
have "(x, x) \<in> lexLess"
[PROOF STATE]
proof (prove)
using this:
(x, x) \<in> lexLess\<^sup>+
lexLess\<^sup>+ = lexLess

goal (1 subgoal):
 1. (x, x) \<in> lexLess
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(x, x) \<in> lexLess

goal (1 subgoal):
 1. acyclic (lexLessRestricted Vbl)
[PROOF STEP]
with irreflexiveLexLess[of "x"]
[PROOF STATE]
proof (chain)
picking this:
(x, x) \<notin> lexLess
(x, x) \<in> lexLess
[PROOF STEP]
have False
[PROOF STATE]
proof (prove)
using this:
(x, x) \<notin> lexLess
(x, x) \<in> lexLess

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

goal (1 subgoal):
 1. acyclic (lexLessRestricted Vbl)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<not> acyclic (lexLessRestricted Vbl) \<Longrightarrow> False

goal (1 subgoal):
 1. acyclic (lexLessRestricted Vbl)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> acyclic (lexLessRestricted Vbl) \<Longrightarrow> False

goal (1 subgoal):
 1. acyclic (lexLessRestricted Vbl)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
acyclic (lexLessRestricted Vbl)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
acyclic (lexLessRestricted Vbl)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma transLexLessRestricted:
  shows "trans (lexLessRestricted Vbl)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trans (lexLessRestricted Vbl)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. trans (lexLessRestricted Vbl)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. trans (lexLessRestricted Vbl)
[PROOF STEP]
fix x::LiteralTrail and y::LiteralTrail and z::LiteralTrail
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. trans (lexLessRestricted Vbl)
[PROOF STEP]
assume "(x, y) \<in> lexLessRestricted Vbl" "(y, z) \<in> lexLessRestricted Vbl"
[PROOF STATE]
proof (state)
this:
(x, y) \<in> lexLessRestricted Vbl
(y, z) \<in> lexLessRestricted Vbl

goal (1 subgoal):
 1. trans (lexLessRestricted Vbl)
[PROOF STEP]
hence "(x, z) \<in> lexLessRestricted Vbl"
[PROOF STATE]
proof (prove)
using this:
(x, y) \<in> lexLessRestricted Vbl
(y, z) \<in> lexLessRestricted Vbl

goal (1 subgoal):
 1. (x, z) \<in> lexLessRestricted Vbl
[PROOF STEP]
unfolding lexLessRestricted_def
[PROOF STATE]
proof (prove)
using this:
(x, y) \<in> {(M1, M2). vars (elements M1) \<subseteq> Vbl \<and> consistent (elements M1) \<and> uniq (elements M1) \<and> vars (elements M2) \<subseteq> Vbl \<and> consistent (elements M2) \<and> uniq (elements M2) \<and> (M1, M2) \<in> lexLess}
(y, z) \<in> {(M1, M2). vars (elements M1) \<subseteq> Vbl \<and> consistent (elements M1) \<and> uniq (elements M1) \<and> vars (elements M2) \<subseteq> Vbl \<and> consistent (elements M2) \<and> uniq (elements M2) \<and> (M1, M2) \<in> lexLess}

goal (1 subgoal):
 1. (x, z) \<in> {(M1, M2). vars (elements M1) \<subseteq> Vbl \<and> consistent (elements M1) \<and> uniq (elements M1) \<and> vars (elements M2) \<subseteq> Vbl \<and> consistent (elements M2) \<and> uniq (elements M2) \<and> (M1, M2) \<in> lexLess}
[PROOF STEP]
using translexLess
[PROOF STATE]
proof (prove)
using this:
(x, y) \<in> {(M1, M2). vars (elements M1) \<subseteq> Vbl \<and> consistent (elements M1) \<and> uniq (elements M1) \<and> vars (elements M2) \<subseteq> Vbl \<and> consistent (elements M2) \<and> uniq (elements M2) \<and> (M1, M2) \<in> lexLess}
(y, z) \<in> {(M1, M2). vars (elements M1) \<subseteq> Vbl \<and> consistent (elements M1) \<and> uniq (elements M1) \<and> vars (elements M2) \<subseteq> Vbl \<and> consistent (elements M2) \<and> uniq (elements M2) \<and> (M1, M2) \<in> lexLess}
trans lexLess

goal (1 subgoal):
 1. (x, z) \<in> {(M1, M2). vars (elements M1) \<subseteq> Vbl \<and> consistent (elements M1) \<and> uniq (elements M1) \<and> vars (elements M2) \<subseteq> Vbl \<and> consistent (elements M2) \<and> uniq (elements M2) \<and> (M1, M2) \<in> lexLess}
[PROOF STEP]
unfolding trans_def
[PROOF STATE]
proof (prove)
using this:
(x, y) \<in> {(M1, M2). vars (elements M1) \<subseteq> Vbl \<and> consistent (elements M1) \<and> uniq (elements M1) \<and> vars (elements M2) \<subseteq> Vbl \<and> consistent (elements M2) \<and> uniq (elements M2) \<and> (M1, M2) \<in> lexLess}
(y, z) \<in> {(M1, M2). vars (elements M1) \<subseteq> Vbl \<and> consistent (elements M1) \<and> uniq (elements M1) \<and> vars (elements M2) \<subseteq> Vbl \<and> consistent (elements M2) \<and> uniq (elements M2) \<and> (M1, M2) \<in> lexLess}
\<forall>x y z. (x, y) \<in> lexLess \<longrightarrow> (y, z) \<in> lexLess \<longrightarrow> (x, z) \<in> lexLess

goal (1 subgoal):
 1. (x, z) \<in> {(M1, M2). vars (elements M1) \<subseteq> Vbl \<and> consistent (elements M1) \<and> uniq (elements M1) \<and> vars (elements M2) \<subseteq> Vbl \<and> consistent (elements M2) \<and> uniq (elements M2) \<and> (M1, M2) \<in> lexLess}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(x, z) \<in> lexLessRestricted Vbl

goal (1 subgoal):
 1. trans (lexLessRestricted Vbl)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>(?x2, ?y2) \<in> lexLessRestricted Vbl; (?y2, ?z2) \<in> lexLessRestricted Vbl\<rbrakk> \<Longrightarrow> (?x2, ?z2) \<in> lexLessRestricted Vbl

goal (1 subgoal):
 1. trans (lexLessRestricted Vbl)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(?x2, ?y2) \<in> lexLessRestricted Vbl; (?y2, ?z2) \<in> lexLessRestricted Vbl\<rbrakk> \<Longrightarrow> (?x2, ?z2) \<in> lexLessRestricted Vbl

goal (1 subgoal):
 1. trans (lexLessRestricted Vbl)
[PROOF STEP]
unfolding trans_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(?x2, ?y2) \<in> lexLessRestricted Vbl; (?y2, ?z2) \<in> lexLessRestricted Vbl\<rbrakk> \<Longrightarrow> (?x2, ?z2) \<in> lexLessRestricted Vbl

goal (1 subgoal):
 1. \<forall>x y z. (x, y) \<in> lexLessRestricted Vbl \<longrightarrow> (y, z) \<in> lexLessRestricted Vbl \<longrightarrow> (x, z) \<in> lexLessRestricted Vbl
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
trans (lexLessRestricted Vbl)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma multLessResolve:
  assumes
  "opposite l el C" and
  "isReason reason l (elements M)"
  shows
  "(resolve C reason (opposite l), C) \<in> multLess  M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (resolve C reason (opposite l), C) \<in> multLess M
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (resolve C reason (opposite l), C) \<in> multLess M
[PROOF STEP]
let ?X = "mset (remdups (oppositeLiteralList C))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (resolve C reason (opposite l), C) \<in> multLess M
[PROOF STEP]
let ?Y = "mset (remdups (oppositeLiteralList (resolve C reason (opposite l))))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (resolve C reason (opposite l), C) \<in> multLess M
[PROOF STEP]
let ?ord = "precedesOrder (elements M)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (resolve C reason (opposite l), C) \<in> multLess M
[PROOF STEP]
have "(?Y, ?X) \<in> (mult1 ?ord)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (mset (remdups (oppositeLiteralList (resolve C reason (opposite l)))), mset (remdups (oppositeLiteralList C))) \<in> mult1 (precedesOrder (elements M))
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (mset (remdups (oppositeLiteralList (resolve C reason (opposite l)))), mset (remdups (oppositeLiteralList C))) \<in> mult1 (precedesOrder (elements M))
[PROOF STEP]
let ?Z = "mset (remdups (oppositeLiteralList (removeAll (opposite l) C)))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (mset (remdups (oppositeLiteralList (resolve C reason (opposite l)))), mset (remdups (oppositeLiteralList C))) \<in> mult1 (precedesOrder (elements M))
[PROOF STEP]
let ?W = "mset (remdups (oppositeLiteralList (removeAll l (list_diff reason C))))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (mset (remdups (oppositeLiteralList (resolve C reason (opposite l)))), mset (remdups (oppositeLiteralList C))) \<in> mult1 (precedesOrder (elements M))
[PROOF STEP]
let ?a = "l"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (mset (remdups (oppositeLiteralList (resolve C reason (opposite l)))), mset (remdups (oppositeLiteralList C))) \<in> mult1 (precedesOrder (elements M))
[PROOF STEP]
from \<open>(opposite l) el C\<close>
[PROOF STATE]
proof (chain)
picking this:
opposite l el C
[PROOF STEP]
have "?X = ?Z + {#?a#}"
[PROOF STATE]
proof (prove)
using this:
opposite l el C

goal (1 subgoal):
 1. mset (remdups (oppositeLiteralList C)) = mset (remdups (oppositeLiteralList (removeAll (opposite l) C))) + {#l#}
[PROOF STEP]
using removeAll_multiset[of "remdups (oppositeLiteralList C)" "l"]
[PROOF STATE]
proof (prove)
using this:
opposite l el C
\<lbrakk>distinct (remdups (oppositeLiteralList C)); l \<in> set (remdups (oppositeLiteralList C))\<rbrakk> \<Longrightarrow> mset (remdups (oppositeLiteralList C)) = {#l#} + mset (removeAll l (remdups (oppositeLiteralList C)))

goal (1 subgoal):
 1. mset (remdups (oppositeLiteralList C)) = mset (remdups (oppositeLiteralList (removeAll (opposite l) C))) + {#l#}
[PROOF STEP]
using oppositeLiteralListRemove[of "opposite l" "C"]
[PROOF STATE]
proof (prove)
using this:
opposite l el C
\<lbrakk>distinct (remdups (oppositeLiteralList C)); l \<in> set (remdups (oppositeLiteralList C))\<rbrakk> \<Longrightarrow> mset (remdups (oppositeLiteralList C)) = {#l#} + mset (removeAll l (remdups (oppositeLiteralList C)))
oppositeLiteralList (removeAll (opposite l) C) = removeAll (opposite (opposite l)) (oppositeLiteralList C)

goal (1 subgoal):
 1. mset (remdups (oppositeLiteralList C)) = mset (remdups (oppositeLiteralList (removeAll (opposite l) C))) + {#l#}
[PROOF STEP]
using literalElListIffOppositeLiteralElOppositeLiteralList[of "l" "oppositeLiteralList C"]
[PROOF STATE]
proof (prove)
using this:
opposite l el C
\<lbrakk>distinct (remdups (oppositeLiteralList C)); l \<in> set (remdups (oppositeLiteralList C))\<rbrakk> \<Longrightarrow> mset (remdups (oppositeLiteralList C)) = {#l#} + mset (removeAll l (remdups (oppositeLiteralList C)))
oppositeLiteralList (removeAll (opposite l) C) = removeAll (opposite (opposite l)) (oppositeLiteralList C)
l el oppositeLiteralList C = opposite l el oppositeLiteralList (oppositeLiteralList C)

goal (1 subgoal):
 1. mset (remdups (oppositeLiteralList C)) = mset (remdups (oppositeLiteralList (removeAll (opposite l) C))) + {#l#}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
mset (remdups (oppositeLiteralList C)) = mset (remdups (oppositeLiteralList (removeAll (opposite l) C))) + {#l#}

goal (1 subgoal):
 1. (mset (remdups (oppositeLiteralList (resolve C reason (opposite l)))), mset (remdups (oppositeLiteralList C))) \<in> mult1 (precedesOrder (elements M))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
mset (remdups (oppositeLiteralList C)) = mset (remdups (oppositeLiteralList (removeAll (opposite l) C))) + {#l#}

goal (1 subgoal):
 1. (mset (remdups (oppositeLiteralList (resolve C reason (opposite l)))), mset (remdups (oppositeLiteralList C))) \<in> mult1 (precedesOrder (elements M))
[PROOF STEP]
have "?Y = ?Z + ?W"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mset (remdups (oppositeLiteralList (resolve C reason (opposite l)))) = mset (remdups (oppositeLiteralList (removeAll (opposite l) C))) + mset (remdups (oppositeLiteralList (removeAll l (list_diff reason C))))
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mset (remdups (oppositeLiteralList (resolve C reason (opposite l)))) = mset (remdups (oppositeLiteralList (removeAll (opposite l) C))) + mset (remdups (oppositeLiteralList (removeAll l (list_diff reason C))))
[PROOF STEP]
have "list_diff (oppositeLiteralList (removeAll l reason)) (oppositeLiteralList (removeAll (opposite l) C)) =
        oppositeLiteralList (removeAll l (list_diff reason C))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list_diff (oppositeLiteralList (removeAll l reason)) (oppositeLiteralList (removeAll (opposite l) C)) = oppositeLiteralList (removeAll l (list_diff reason C))
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. list_diff (oppositeLiteralList (removeAll l reason)) (oppositeLiteralList (removeAll (opposite l) C)) = oppositeLiteralList (removeAll l (list_diff reason C))
[PROOF STEP]
from \<open>isReason reason l (elements M)\<close>
[PROOF STATE]
proof (chain)
picking this:
isReason reason l (elements M)
[PROOF STEP]
have "opposite l \<notin> set (removeAll l reason)"
[PROOF STATE]
proof (prove)
using this:
isReason reason l (elements M)

goal (1 subgoal):
 1. opposite l \<notin> set (removeAll l reason)
[PROOF STEP]
unfolding isReason_def
[PROOF STATE]
proof (prove)
using this:
l el reason \<and> clauseFalse (removeAll l reason) (elements M) \<and> (\<forall>literal'. literal' el removeAll l reason \<longrightarrow> precedes (opposite literal') l (elements M) \<and> opposite literal' \<noteq> l)

goal (1 subgoal):
 1. opposite l \<notin> set (removeAll l reason)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
opposite l \<notin> set (removeAll l reason)

goal (1 subgoal):
 1. list_diff (oppositeLiteralList (removeAll l reason)) (oppositeLiteralList (removeAll (opposite l) C)) = oppositeLiteralList (removeAll l (list_diff reason C))
[PROOF STEP]
hence "list_diff (removeAll l reason) (removeAll (opposite l) C) = list_diff (removeAll l reason) C"
[PROOF STATE]
proof (prove)
using this:
opposite l \<notin> set (removeAll l reason)

goal (1 subgoal):
 1. list_diff (removeAll l reason) (removeAll (opposite l) C) = list_diff (removeAll l reason) C
[PROOF STEP]
using listDiffRemoveAllNonMember[of "opposite l" "removeAll l reason" "C"]
[PROOF STATE]
proof (prove)
using this:
opposite l \<notin> set (removeAll l reason)
opposite l \<notin> set (removeAll l reason) \<Longrightarrow> list_diff (removeAll l reason) C = list_diff (removeAll l reason) (removeAll (opposite l) C)

goal (1 subgoal):
 1. list_diff (removeAll l reason) (removeAll (opposite l) C) = list_diff (removeAll l reason) C
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
list_diff (removeAll l reason) (removeAll (opposite l) C) = list_diff (removeAll l reason) C

goal (1 subgoal):
 1. list_diff (oppositeLiteralList (removeAll l reason)) (oppositeLiteralList (removeAll (opposite l) C)) = oppositeLiteralList (removeAll l (list_diff reason C))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
list_diff (removeAll l reason) (removeAll (opposite l) C) = list_diff (removeAll l reason) C

goal (1 subgoal):
 1. list_diff (oppositeLiteralList (removeAll l reason)) (oppositeLiteralList (removeAll (opposite l) C)) = oppositeLiteralList (removeAll l (list_diff reason C))
[PROOF STEP]
unfolding oppositeLiteralList_def
[PROOF STATE]
proof (prove)
using this:
list_diff (removeAll l reason) (removeAll (opposite l) C) = list_diff (removeAll l reason) C

goal (1 subgoal):
 1. list_diff (map opposite (removeAll l reason)) (map opposite (removeAll (opposite l) C)) = map opposite (removeAll l (list_diff reason C))
[PROOF STEP]
using listDiffMap[of "opposite" "removeAll l reason" "removeAll (opposite l) C"]
[PROOF STATE]
proof (prove)
using this:
list_diff (removeAll l reason) (removeAll (opposite l) C) = list_diff (removeAll l reason) C
\<forall>x y. x \<noteq> y \<longrightarrow> opposite x \<noteq> opposite y \<Longrightarrow> map opposite (list_diff (removeAll l reason) (removeAll (opposite l) C)) = list_diff (map opposite (removeAll l reason)) (map opposite (removeAll (opposite l) C))

goal (1 subgoal):
 1. list_diff (map opposite (removeAll l reason)) (map opposite (removeAll (opposite l) C)) = map opposite (removeAll l (list_diff reason C))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
list_diff (oppositeLiteralList (removeAll l reason)) (oppositeLiteralList (removeAll (opposite l) C)) = oppositeLiteralList (removeAll l (list_diff reason C))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
list_diff (oppositeLiteralList (removeAll l reason)) (oppositeLiteralList (removeAll (opposite l) C)) = oppositeLiteralList (removeAll l (list_diff reason C))

goal (1 subgoal):
 1. mset (remdups (oppositeLiteralList (resolve C reason (opposite l)))) = mset (remdups (oppositeLiteralList (removeAll (opposite l) C))) + mset (remdups (oppositeLiteralList (removeAll l (list_diff reason C))))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
list_diff (oppositeLiteralList (removeAll l reason)) (oppositeLiteralList (removeAll (opposite l) C)) = oppositeLiteralList (removeAll l (list_diff reason C))

goal (1 subgoal):
 1. mset (remdups (oppositeLiteralList (resolve C reason (opposite l)))) = mset (remdups (oppositeLiteralList (removeAll (opposite l) C))) + mset (remdups (oppositeLiteralList (removeAll l (list_diff reason C))))
[PROOF STEP]
unfolding resolve_def
[PROOF STATE]
proof (prove)
using this:
list_diff (oppositeLiteralList (removeAll l reason)) (oppositeLiteralList (removeAll (opposite l) C)) = oppositeLiteralList (removeAll l (list_diff reason C))

goal (1 subgoal):
 1. mset (remdups (oppositeLiteralList (removeAll (opposite l) C @ removeAll (opposite (opposite l)) reason))) = mset (remdups (oppositeLiteralList (removeAll (opposite l) C))) + mset (remdups (oppositeLiteralList (removeAll l (list_diff reason C))))
[PROOF STEP]
using remdupsAppendMultiSet[of "oppositeLiteralList (removeAll (opposite l) C)" "oppositeLiteralList (removeAll l reason)"]
[PROOF STATE]
proof (prove)
using this:
list_diff (oppositeLiteralList (removeAll l reason)) (oppositeLiteralList (removeAll (opposite l) C)) = oppositeLiteralList (removeAll l (list_diff reason C))
mset (remdups (oppositeLiteralList (removeAll (opposite l) C) @ oppositeLiteralList (removeAll l reason))) = mset (remdups (oppositeLiteralList (removeAll (opposite l) C)) @ remdups (list_diff (oppositeLiteralList (removeAll l reason)) (oppositeLiteralList (removeAll (opposite l) C))))

goal (1 subgoal):
 1. mset (remdups (oppositeLiteralList (removeAll (opposite l) C @ removeAll (opposite (opposite l)) reason))) = mset (remdups (oppositeLiteralList (removeAll (opposite l) C))) + mset (remdups (oppositeLiteralList (removeAll l (list_diff reason C))))
[PROOF STEP]
unfolding oppositeLiteralList_def
[PROOF STATE]
proof (prove)
using this:
list_diff (map opposite (removeAll l reason)) (map opposite (removeAll (opposite l) C)) = map opposite (removeAll l (list_diff reason C))
mset (remdups (map opposite (removeAll (opposite l) C) @ map opposite (removeAll l reason))) = mset (remdups (map opposite (removeAll (opposite l) C)) @ remdups (list_diff (map opposite (removeAll l reason)) (map opposite (removeAll (opposite l) C))))

goal (1 subgoal):
 1. mset (remdups (map opposite (removeAll (opposite l) C @ removeAll (opposite (opposite l)) reason))) = mset (remdups (map opposite (removeAll (opposite l) C))) + mset (remdups (map opposite (removeAll l (list_diff reason C))))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
mset (remdups (oppositeLiteralList (resolve C reason (opposite l)))) = mset (remdups (oppositeLiteralList (removeAll (opposite l) C))) + mset (remdups (oppositeLiteralList (removeAll l (list_diff reason C))))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
mset (remdups (oppositeLiteralList (resolve C reason (opposite l)))) = mset (remdups (oppositeLiteralList (removeAll (opposite l) C))) + mset (remdups (oppositeLiteralList (removeAll l (list_diff reason C))))

goal (1 subgoal):
 1. (mset (remdups (oppositeLiteralList (resolve C reason (opposite l)))), mset (remdups (oppositeLiteralList C))) \<in> mult1 (precedesOrder (elements M))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
mset (remdups (oppositeLiteralList (resolve C reason (opposite l)))) = mset (remdups (oppositeLiteralList (removeAll (opposite l) C))) + mset (remdups (oppositeLiteralList (removeAll l (list_diff reason C))))

goal (1 subgoal):
 1. (mset (remdups (oppositeLiteralList (resolve C reason (opposite l)))), mset (remdups (oppositeLiteralList C))) \<in> mult1 (precedesOrder (elements M))
[PROOF STEP]
have "\<forall> b. b \<in># ?W \<longrightarrow> (b, ?a) \<in> ?ord"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>b. b \<in># mset (remdups (oppositeLiteralList (removeAll l (list_diff reason C)))) \<longrightarrow> (b, l) \<in> precedesOrder (elements M)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>b. b \<in># mset (remdups (oppositeLiteralList (removeAll l (list_diff reason C)))) \<longrightarrow> (b, l) \<in> precedesOrder (elements M)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>b. b \<in># mset (remdups (oppositeLiteralList (removeAll l (list_diff reason C)))) \<longrightarrow> (b, l) \<in> precedesOrder (elements M)
[PROOF STEP]
fix b
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>b. b \<in># mset (remdups (oppositeLiteralList (removeAll l (list_diff reason C)))) \<longrightarrow> (b, l) \<in> precedesOrder (elements M)
[PROOF STEP]
assume "b \<in># ?W"
[PROOF STATE]
proof (state)
this:
b \<in># mset (remdups (oppositeLiteralList (removeAll l (list_diff reason C))))

goal (1 subgoal):
 1. \<forall>b. b \<in># mset (remdups (oppositeLiteralList (removeAll l (list_diff reason C)))) \<longrightarrow> (b, l) \<in> precedesOrder (elements M)
[PROOF STEP]
hence "opposite b \<in> set (removeAll l reason)"
[PROOF STATE]
proof (prove)
using this:
b \<in># mset (remdups (oppositeLiteralList (removeAll l (list_diff reason C))))

goal (1 subgoal):
 1. opposite b \<in> set (removeAll l reason)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. b \<in># mset (remdups (oppositeLiteralList (removeAll l (list_diff reason C)))) \<Longrightarrow> opposite b \<in> set (removeAll l reason)
[PROOF STEP]
from \<open>b \<in># ?W\<close>
[PROOF STATE]
proof (chain)
picking this:
b \<in># mset (remdups (oppositeLiteralList (removeAll l (list_diff reason C))))
[PROOF STEP]
have "b el remdups (oppositeLiteralList (removeAll l (list_diff reason C)))"
[PROOF STATE]
proof (prove)
using this:
b \<in># mset (remdups (oppositeLiteralList (removeAll l (list_diff reason C))))

goal (1 subgoal):
 1. b el remdups (oppositeLiteralList (removeAll l (list_diff reason C)))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
b el remdups (oppositeLiteralList (removeAll l (list_diff reason C)))

goal (1 subgoal):
 1. b \<in># mset (remdups (oppositeLiteralList (removeAll l (list_diff reason C)))) \<Longrightarrow> opposite b \<in> set (removeAll l reason)
[PROOF STEP]
hence "opposite b el removeAll l (list_diff reason C)"
[PROOF STATE]
proof (prove)
using this:
b el remdups (oppositeLiteralList (removeAll l (list_diff reason C)))

goal (1 subgoal):
 1. opposite b el removeAll l (list_diff reason C)
[PROOF STEP]
using literalElListIffOppositeLiteralElOppositeLiteralList[of "opposite b" "removeAll l (list_diff reason C)"]
[PROOF STATE]
proof (prove)
using this:
b el remdups (oppositeLiteralList (removeAll l (list_diff reason C)))
opposite b el removeAll l (list_diff reason C) = opposite (opposite b) el oppositeLiteralList (removeAll l (list_diff reason C))

goal (1 subgoal):
 1. opposite b el removeAll l (list_diff reason C)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
opposite b el removeAll l (list_diff reason C)

goal (1 subgoal):
 1. b \<in># mset (remdups (oppositeLiteralList (removeAll l (list_diff reason C)))) \<Longrightarrow> opposite b \<in> set (removeAll l reason)
[PROOF STEP]
hence "opposite b el list_diff (removeAll l reason) C"
[PROOF STATE]
proof (prove)
using this:
opposite b el removeAll l (list_diff reason C)

goal (1 subgoal):
 1. opposite b el list_diff (removeAll l reason) C
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
opposite b el list_diff (removeAll l reason) C

goal (1 subgoal):
 1. b \<in># mset (remdups (oppositeLiteralList (removeAll l (list_diff reason C)))) \<Longrightarrow> opposite b \<in> set (removeAll l reason)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
opposite b el list_diff (removeAll l reason) C

goal (1 subgoal):
 1. opposite b \<in> set (removeAll l reason)
[PROOF STEP]
using listDiffIff[of "opposite b" "removeAll l reason" "C"]
[PROOF STATE]
proof (prove)
using this:
opposite b el list_diff (removeAll l reason) C
(opposite b \<in> set (removeAll l reason) \<and> opposite b \<notin> set C) = (opposite b \<in> set (list_diff (removeAll l reason) C))

goal (1 subgoal):
 1. opposite b \<in> set (removeAll l reason)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
opposite b \<in> set (removeAll l reason)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
opposite b \<in> set (removeAll l reason)

goal (1 subgoal):
 1. \<forall>b. b \<in># mset (remdups (oppositeLiteralList (removeAll l (list_diff reason C)))) \<longrightarrow> (b, l) \<in> precedesOrder (elements M)
[PROOF STEP]
with \<open>isReason reason l (elements M)\<close>
[PROOF STATE]
proof (chain)
picking this:
isReason reason l (elements M)
opposite b \<in> set (removeAll l reason)
[PROOF STEP]
have "precedes b l (elements M)" "b \<noteq> l"
[PROOF STATE]
proof (prove)
using this:
isReason reason l (elements M)
opposite b \<in> set (removeAll l reason)

goal (1 subgoal):
 1. precedes b l (elements M) &&& b \<noteq> l
[PROOF STEP]
unfolding isReason_def
[PROOF STATE]
proof (prove)
using this:
l el reason \<and> clauseFalse (removeAll l reason) (elements M) \<and> (\<forall>literal'. literal' el removeAll l reason \<longrightarrow> precedes (opposite literal') l (elements M) \<and> opposite literal' \<noteq> l)
opposite b \<in> set (removeAll l reason)

goal (1 subgoal):
 1. precedes b l (elements M) &&& b \<noteq> l
[PROOF STEP]
unfolding precedes_def
[PROOF STATE]
proof (prove)
using this:
l el reason \<and> clauseFalse (removeAll l reason) (elements M) \<and> (\<forall>literal'. literal' el removeAll l reason \<longrightarrow> (opposite literal' \<in> set (elements M) \<and> l \<in> set (elements M) \<and> firstPos (opposite literal') (elements M) \<le> firstPos l (elements M)) \<and> opposite literal' \<noteq> l)
opposite b \<in> set (removeAll l reason)

goal (1 subgoal):
 1. b \<in> set (elements M) \<and> l \<in> set (elements M) \<and> firstPos b (elements M) \<le> firstPos l (elements M) &&& b \<noteq> l
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
precedes b l (elements M)
b \<noteq> l

goal (1 subgoal):
 1. \<forall>b. b \<in># mset (remdups (oppositeLiteralList (removeAll l (list_diff reason C)))) \<longrightarrow> (b, l) \<in> precedesOrder (elements M)
[PROOF STEP]
hence "(b, ?a) \<in> ?ord"
[PROOF STATE]
proof (prove)
using this:
precedes b l (elements M)
b \<noteq> l

goal (1 subgoal):
 1. (b, l) \<in> precedesOrder (elements M)
[PROOF STEP]
unfolding precedesOrder_def
[PROOF STATE]
proof (prove)
using this:
precedes b l (elements M)
b \<noteq> l

goal (1 subgoal):
 1. (b, l) \<in> {(a, b). precedes a b (elements M) \<and> a \<noteq> b}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(b, l) \<in> precedesOrder (elements M)

goal (1 subgoal):
 1. \<forall>b. b \<in># mset (remdups (oppositeLiteralList (removeAll l (list_diff reason C)))) \<longrightarrow> (b, l) \<in> precedesOrder (elements M)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?b2 \<in># mset (remdups (oppositeLiteralList (removeAll l (list_diff reason C)))) \<Longrightarrow> (?b2, l) \<in> precedesOrder (elements M)

goal (1 subgoal):
 1. \<forall>b. b \<in># mset (remdups (oppositeLiteralList (removeAll l (list_diff reason C)))) \<longrightarrow> (b, l) \<in> precedesOrder (elements M)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
?b2 \<in># mset (remdups (oppositeLiteralList (removeAll l (list_diff reason C)))) \<Longrightarrow> (?b2, l) \<in> precedesOrder (elements M)

goal (1 subgoal):
 1. \<forall>b. b \<in># mset (remdups (oppositeLiteralList (removeAll l (list_diff reason C)))) \<longrightarrow> (b, l) \<in> precedesOrder (elements M)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>b. b \<in># mset (remdups (oppositeLiteralList (removeAll l (list_diff reason C)))) \<longrightarrow> (b, l) \<in> precedesOrder (elements M)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>b. b \<in># mset (remdups (oppositeLiteralList (removeAll l (list_diff reason C)))) \<longrightarrow> (b, l) \<in> precedesOrder (elements M)

goal (1 subgoal):
 1. (mset (remdups (oppositeLiteralList (resolve C reason (opposite l)))), mset (remdups (oppositeLiteralList C))) \<in> mult1 (precedesOrder (elements M))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
mset (remdups (oppositeLiteralList C)) = mset (remdups (oppositeLiteralList (removeAll (opposite l) C))) + {#l#}
mset (remdups (oppositeLiteralList (resolve C reason (opposite l)))) = mset (remdups (oppositeLiteralList (removeAll (opposite l) C))) + mset (remdups (oppositeLiteralList (removeAll l (list_diff reason C))))
\<forall>b. b \<in># mset (remdups (oppositeLiteralList (removeAll l (list_diff reason C)))) \<longrightarrow> (b, l) \<in> precedesOrder (elements M)
[PROOF STEP]
have "\<exists> a M0 K. ?X = M0 + {#a#} \<and> ?Y = M0 + K \<and> (\<forall>b. b \<in># K \<longrightarrow> (b, a) \<in> ?ord)"
[PROOF STATE]
proof (prove)
using this:
mset (remdups (oppositeLiteralList C)) = mset (remdups (oppositeLiteralList (removeAll (opposite l) C))) + {#l#}
mset (remdups (oppositeLiteralList (resolve C reason (opposite l)))) = mset (remdups (oppositeLiteralList (removeAll (opposite l) C))) + mset (remdups (oppositeLiteralList (removeAll l (list_diff reason C))))
\<forall>b. b \<in># mset (remdups (oppositeLiteralList (removeAll l (list_diff reason C)))) \<longrightarrow> (b, l) \<in> precedesOrder (elements M)

goal (1 subgoal):
 1. \<exists>a M0 K. mset (remdups (oppositeLiteralList C)) = M0 + {#a#} \<and> mset (remdups (oppositeLiteralList (resolve C reason (opposite l)))) = M0 + K \<and> (\<forall>b. b \<in># K \<longrightarrow> (b, a) \<in> precedesOrder (elements M))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>a M0 K. mset (remdups (oppositeLiteralList C)) = M0 + {#a#} \<and> mset (remdups (oppositeLiteralList (resolve C reason (opposite l)))) = M0 + K \<and> (\<forall>b. b \<in># K \<longrightarrow> (b, a) \<in> precedesOrder (elements M))

goal (1 subgoal):
 1. (mset (remdups (oppositeLiteralList (resolve C reason (opposite l)))), mset (remdups (oppositeLiteralList C))) \<in> mult1 (precedesOrder (elements M))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<exists>a M0 K. mset (remdups (oppositeLiteralList C)) = M0 + {#a#} \<and> mset (remdups (oppositeLiteralList (resolve C reason (opposite l)))) = M0 + K \<and> (\<forall>b. b \<in># K \<longrightarrow> (b, a) \<in> precedesOrder (elements M))

goal (1 subgoal):
 1. (mset (remdups (oppositeLiteralList (resolve C reason (opposite l)))), mset (remdups (oppositeLiteralList C))) \<in> mult1 (precedesOrder (elements M))
[PROOF STEP]
unfolding mult1_def
[PROOF STATE]
proof (prove)
using this:
\<exists>a M0 K. mset (remdups (oppositeLiteralList C)) = M0 + {#a#} \<and> mset (remdups (oppositeLiteralList (resolve C reason (opposite l)))) = M0 + K \<and> (\<forall>b. b \<in># K \<longrightarrow> (b, a) \<in> precedesOrder (elements M))

goal (1 subgoal):
 1. (mset (remdups (oppositeLiteralList (resolve C reason (opposite l)))), mset (remdups (oppositeLiteralList C))) \<in> {(N, Ma). \<exists>a M0 K. Ma = add_mset a M0 \<and> N = M0 + K \<and> (\<forall>b. b \<in># K \<longrightarrow> (b, a) \<in> precedesOrder (elements M))}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(mset (remdups (oppositeLiteralList (resolve C reason (opposite l)))), mset (remdups (oppositeLiteralList C))) \<in> mult1 (precedesOrder (elements M))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(mset (remdups (oppositeLiteralList (resolve C reason (opposite l)))), mset (remdups (oppositeLiteralList C))) \<in> mult1 (precedesOrder (elements M))

goal (1 subgoal):
 1. (resolve C reason (opposite l), C) \<in> multLess M
[PROOF STEP]
hence "(?Y, ?X) \<in> (mult1 ?ord)\<^sup>+"
[PROOF STATE]
proof (prove)
using this:
(mset (remdups (oppositeLiteralList (resolve C reason (opposite l)))), mset (remdups (oppositeLiteralList C))) \<in> mult1 (precedesOrder (elements M))

goal (1 subgoal):
 1. (mset (remdups (oppositeLiteralList (resolve C reason (opposite l)))), mset (remdups (oppositeLiteralList C))) \<in> (mult1 (precedesOrder (elements M)))\<^sup>+
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(mset (remdups (oppositeLiteralList (resolve C reason (opposite l)))), mset (remdups (oppositeLiteralList C))) \<in> (mult1 (precedesOrder (elements M)))\<^sup>+

goal (1 subgoal):
 1. (resolve C reason (opposite l), C) \<in> multLess M
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(mset (remdups (oppositeLiteralList (resolve C reason (opposite l)))), mset (remdups (oppositeLiteralList C))) \<in> (mult1 (precedesOrder (elements M)))\<^sup>+

goal (1 subgoal):
 1. (resolve C reason (opposite l), C) \<in> multLess M
[PROOF STEP]
unfolding multLess_def
[PROOF STATE]
proof (prove)
using this:
(mset (remdups (oppositeLiteralList (resolve C reason (opposite l)))), mset (remdups (oppositeLiteralList C))) \<in> (mult1 (precedesOrder (elements M)))\<^sup>+

goal (1 subgoal):
 1. (resolve C reason (opposite l), C) \<in> inv_image (mult (precedesOrder (elements M))) (\<lambda>x. mset (remdups (oppositeLiteralList x)))
[PROOF STEP]
unfolding mult_def
[PROOF STATE]
proof (prove)
using this:
(mset (remdups (oppositeLiteralList (resolve C reason (opposite l)))), mset (remdups (oppositeLiteralList C))) \<in> (mult1 (precedesOrder (elements M)))\<^sup>+

goal (1 subgoal):
 1. (resolve C reason (opposite l), C) \<in> inv_image ((mult1 (precedesOrder (elements M)))\<^sup>+) (\<lambda>x. mset (remdups (oppositeLiteralList x)))
[PROOF STEP]
unfolding inv_image_def
[PROOF STATE]
proof (prove)
using this:
(mset (remdups (oppositeLiteralList (resolve C reason (opposite l)))), mset (remdups (oppositeLiteralList C))) \<in> (mult1 (precedesOrder (elements M)))\<^sup>+

goal (1 subgoal):
 1. (resolve C reason (opposite l), C) \<in> {(x, y). (mset (remdups (oppositeLiteralList x)), mset (remdups (oppositeLiteralList y))) \<in> (mult1 (precedesOrder (elements M)))\<^sup>+}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(resolve C reason (opposite l), C) \<in> multLess M

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma multLessListDiff:
assumes
  "(a, b) \<in> multLess M"
shows
  "(list_diff a x, b) \<in> multLess M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (list_diff a x, b) \<in> multLess M
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (list_diff a x, b) \<in> multLess M
[PROOF STEP]
let ?pOrd = "precedesOrder (elements M)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (list_diff a x, b) \<in> multLess M
[PROOF STEP]
let ?f = "\<lambda> l. remdups (map opposite l)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (list_diff a x, b) \<in> multLess M
[PROOF STEP]
have "trans ?pOrd"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trans (precedesOrder (elements M))
[PROOF STEP]
using transPrecedesOrder[of "elements M"]
[PROOF STATE]
proof (prove)
using this:
trans (precedesOrder (elements M))

goal (1 subgoal):
 1. trans (precedesOrder (elements M))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
trans (precedesOrder (elements M))

goal (1 subgoal):
 1. (list_diff a x, b) \<in> multLess M
[PROOF STEP]
have  "(mset (?f a), mset (?f b)) \<in> mult ?pOrd"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (mset (remdups (map opposite a)), mset (remdups (map opposite b))) \<in> mult (precedesOrder (elements M))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(a, b) \<in> multLess M

goal (1 subgoal):
 1. (mset (remdups (map opposite a)), mset (remdups (map opposite b))) \<in> mult (precedesOrder (elements M))
[PROOF STEP]
unfolding multLess_def
[PROOF STATE]
proof (prove)
using this:
(a, b) \<in> inv_image (mult (precedesOrder (elements M))) (\<lambda>x. mset (remdups (oppositeLiteralList x)))

goal (1 subgoal):
 1. (mset (remdups (map opposite a)), mset (remdups (map opposite b))) \<in> mult (precedesOrder (elements M))
[PROOF STEP]
unfolding oppositeLiteralList_def
[PROOF STATE]
proof (prove)
using this:
(a, b) \<in> inv_image (mult (precedesOrder (elements M))) (\<lambda>x. mset (remdups (map opposite x)))

goal (1 subgoal):
 1. (mset (remdups (map opposite a)), mset (remdups (map opposite b))) \<in> mult (precedesOrder (elements M))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(mset (remdups (map opposite a)), mset (remdups (map opposite b))) \<in> mult (precedesOrder (elements M))

goal (1 subgoal):
 1. (list_diff a x, b) \<in> multLess M
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(mset (remdups (map opposite a)), mset (remdups (map opposite b))) \<in> mult (precedesOrder (elements M))

goal (1 subgoal):
 1. (list_diff a x, b) \<in> multLess M
[PROOF STEP]
have "multiset_le (mset (list_diff (?f a) (?f x)))
                    (mset (?f a))
                    ?pOrd"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. multiset_le (mset (list_diff (remdups (map opposite a)) (remdups (map opposite x)))) (mset (remdups (map opposite a))) (precedesOrder (elements M))
[PROOF STEP]
using \<open>trans ?pOrd\<close>
[PROOF STATE]
proof (prove)
using this:
trans (precedesOrder (elements M))

goal (1 subgoal):
 1. multiset_le (mset (list_diff (remdups (map opposite a)) (remdups (map opposite x)))) (mset (remdups (map opposite a))) (precedesOrder (elements M))
[PROOF STEP]
using multisetLeListDiff[of "?pOrd" "?f a" "?f x"]
[PROOF STATE]
proof (prove)
using this:
trans (precedesOrder (elements M))
trans (precedesOrder (elements M)) \<Longrightarrow> multiset_le (mset (list_diff (remdups (map opposite a)) (remdups (map opposite x)))) (mset (remdups (map opposite a))) (precedesOrder (elements M))

goal (1 subgoal):
 1. multiset_le (mset (list_diff (remdups (map opposite a)) (remdups (map opposite x)))) (mset (remdups (map opposite a))) (precedesOrder (elements M))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
multiset_le (mset (list_diff (remdups (map opposite a)) (remdups (map opposite x)))) (mset (remdups (map opposite a))) (precedesOrder (elements M))

goal (1 subgoal):
 1. (list_diff a x, b) \<in> multLess M
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(mset (remdups (map opposite a)), mset (remdups (map opposite b))) \<in> mult (precedesOrder (elements M))
multiset_le (mset (list_diff (remdups (map opposite a)) (remdups (map opposite x)))) (mset (remdups (map opposite a))) (precedesOrder (elements M))
[PROOF STEP]
have "(mset (list_diff (?f a) (?f x)), mset (?f b)) \<in> mult ?pOrd"
[PROOF STATE]
proof (prove)
using this:
(mset (remdups (map opposite a)), mset (remdups (map opposite b))) \<in> mult (precedesOrder (elements M))
multiset_le (mset (list_diff (remdups (map opposite a)) (remdups (map opposite x)))) (mset (remdups (map opposite a))) (precedesOrder (elements M))

goal (1 subgoal):
 1. (mset (list_diff (remdups (map opposite a)) (remdups (map opposite x))), mset (remdups (map opposite b))) \<in> mult (precedesOrder (elements M))
[PROOF STEP]
unfolding multiset_le_def
[PROOF STATE]
proof (prove)
using this:
(mset (remdups (map opposite a)), mset (remdups (map opposite b))) \<in> mult (precedesOrder (elements M))
mset (list_diff (remdups (map opposite a)) (remdups (map opposite x))) = mset (remdups (map opposite a)) \<or> (mset (list_diff (remdups (map opposite a)) (remdups (map opposite x))), mset (remdups (map opposite a))) \<in> mult (precedesOrder (elements M))

goal (1 subgoal):
 1. (mset (list_diff (remdups (map opposite a)) (remdups (map opposite x))), mset (remdups (map opposite b))) \<in> mult (precedesOrder (elements M))
[PROOF STEP]
unfolding mult_def
[PROOF STATE]
proof (prove)
using this:
(mset (remdups (map opposite a)), mset (remdups (map opposite b))) \<in> (mult1 (precedesOrder (elements M)))\<^sup>+
mset (list_diff (remdups (map opposite a)) (remdups (map opposite x))) = mset (remdups (map opposite a)) \<or> (mset (list_diff (remdups (map opposite a)) (remdups (map opposite x))), mset (remdups (map opposite a))) \<in> (mult1 (precedesOrder (elements M)))\<^sup>+

goal (1 subgoal):
 1. (mset (list_diff (remdups (map opposite a)) (remdups (map opposite x))), mset (remdups (map opposite b))) \<in> (mult1 (precedesOrder (elements M)))\<^sup>+
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(mset (list_diff (remdups (map opposite a)) (remdups (map opposite x))), mset (remdups (map opposite b))) \<in> mult (precedesOrder (elements M))

goal (1 subgoal):
 1. (list_diff a x, b) \<in> multLess M
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(mset (list_diff (remdups (map opposite a)) (remdups (map opposite x))), mset (remdups (map opposite b))) \<in> mult (precedesOrder (elements M))

goal (1 subgoal):
 1. (list_diff a x, b) \<in> multLess M
[PROOF STEP]
unfolding multLess_def
[PROOF STATE]
proof (prove)
using this:
(mset (list_diff (remdups (map opposite a)) (remdups (map opposite x))), mset (remdups (map opposite b))) \<in> mult (precedesOrder (elements M))

goal (1 subgoal):
 1. (list_diff a x, b) \<in> inv_image (mult (precedesOrder (elements M))) (\<lambda>x. mset (remdups (oppositeLiteralList x)))
[PROOF STEP]
unfolding oppositeLiteralList_def
[PROOF STATE]
proof (prove)
using this:
(mset (list_diff (remdups (map opposite a)) (remdups (map opposite x))), mset (remdups (map opposite b))) \<in> mult (precedesOrder (elements M))

goal (1 subgoal):
 1. (list_diff a x, b) \<in> inv_image (mult (precedesOrder (elements M))) (\<lambda>x. mset (remdups (map opposite x)))
[PROOF STEP]
by (simp add: listDiffMap remdupsListDiff)
[PROOF STATE]
proof (state)
this:
(list_diff a x, b) \<in> multLess M

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma multLessRemdups:
assumes
  "(a, b) \<in> multLess M"
shows
  "(remdups a, remdups b) \<in> multLess M \<and>
   (remdups a, b) \<in> multLess M \<and>
   (a, remdups b) \<in> multLess M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (remdups a, remdups b) \<in> multLess M \<and> (remdups a, b) \<in> multLess M \<and> (a, remdups b) \<in> multLess M
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (remdups a, remdups b) \<in> multLess M \<and> (remdups a, b) \<in> multLess M \<and> (a, remdups b) \<in> multLess M
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (remdups a, remdups b) \<in> multLess M \<and> (remdups a, b) \<in> multLess M \<and> (a, remdups b) \<in> multLess M
[PROOF STEP]
fix l
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (remdups a, remdups b) \<in> multLess M \<and> (remdups a, b) \<in> multLess M \<and> (a, remdups b) \<in> multLess M
[PROOF STEP]
have "remdups (map opposite l) = remdups (map opposite (remdups l))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. remdups (map opposite l) = remdups (map opposite (remdups l))
[PROOF STEP]
by (induct l) auto
[PROOF STATE]
proof (state)
this:
remdups (map opposite l) = remdups (map opposite (remdups l))

goal (1 subgoal):
 1. (remdups a, remdups b) \<in> multLess M \<and> (remdups a, b) \<in> multLess M \<and> (a, remdups b) \<in> multLess M
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
remdups (map opposite ?l2) = remdups (map opposite (remdups ?l2))

goal (1 subgoal):
 1. (remdups a, remdups b) \<in> multLess M \<and> (remdups a, b) \<in> multLess M \<and> (a, remdups b) \<in> multLess M
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
remdups (map opposite ?l2) = remdups (map opposite (remdups ?l2))

goal (1 subgoal):
 1. (remdups a, remdups b) \<in> multLess M \<and> (remdups a, b) \<in> multLess M \<and> (a, remdups b) \<in> multLess M
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
remdups (map opposite ?l2) = remdups (map opposite (remdups ?l2))
(a, b) \<in> multLess M

goal (1 subgoal):
 1. (remdups a, remdups b) \<in> multLess M \<and> (remdups a, b) \<in> multLess M \<and> (a, remdups b) \<in> multLess M
[PROOF STEP]
unfolding multLess_def
[PROOF STATE]
proof (prove)
using this:
remdups (map opposite ?l2) = remdups (map opposite (remdups ?l2))
(a, b) \<in> inv_image (mult (precedesOrder (elements M))) (\<lambda>x. mset (remdups (oppositeLiteralList x)))

goal (1 subgoal):
 1. (remdups a, remdups b) \<in> inv_image (mult (precedesOrder (elements M))) (\<lambda>x. mset (remdups (oppositeLiteralList x))) \<and> (remdups a, b) \<in> inv_image (mult (precedesOrder (elements M))) (\<lambda>x. mset (remdups (oppositeLiteralList x))) \<and> (a, remdups b) \<in> inv_image (mult (precedesOrder (elements M))) (\<lambda>x. mset (remdups (oppositeLiteralList x)))
[PROOF STEP]
unfolding oppositeLiteralList_def
[PROOF STATE]
proof (prove)
using this:
remdups (map opposite ?l2) = remdups (map opposite (remdups ?l2))
(a, b) \<in> inv_image (mult (precedesOrder (elements M))) (\<lambda>x. mset (remdups (map opposite x)))

goal (1 subgoal):
 1. (remdups a, remdups b) \<in> inv_image (mult (precedesOrder (elements M))) (\<lambda>x. mset (remdups (map opposite x))) \<and> (remdups a, b) \<in> inv_image (mult (precedesOrder (elements M))) (\<lambda>x. mset (remdups (map opposite x))) \<and> (a, remdups b) \<in> inv_image (mult (precedesOrder (elements M))) (\<lambda>x. mset (remdups (map opposite x)))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(remdups a, remdups b) \<in> multLess M \<and> (remdups a, b) \<in> multLess M \<and> (a, remdups b) \<in> multLess M

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma wfMultLess:
  shows "wf (multLess M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf (multLess M)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. wf (multLess M)
[PROOF STEP]
have "wf (precedesOrder (elements M))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf (precedesOrder (elements M))
[PROOF STEP]
by (simp add: wellFoundedPrecedesOrder)
[PROOF STATE]
proof (state)
this:
wf (precedesOrder (elements M))

goal (1 subgoal):
 1. wf (multLess M)
[PROOF STEP]
hence "wf (mult (precedesOrder (elements M)))"
[PROOF STATE]
proof (prove)
using this:
wf (precedesOrder (elements M))

goal (1 subgoal):
 1. wf (mult (precedesOrder (elements M)))
[PROOF STEP]
by (simp add: wf_mult)
[PROOF STATE]
proof (state)
this:
wf (mult (precedesOrder (elements M)))

goal (1 subgoal):
 1. wf (multLess M)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
wf (mult (precedesOrder (elements M)))

goal (1 subgoal):
 1. wf (multLess M)
[PROOF STEP]
unfolding multLess_def
[PROOF STATE]
proof (prove)
using this:
wf (mult (precedesOrder (elements M)))

goal (1 subgoal):
 1. wf (inv_image (mult (precedesOrder (elements M))) (\<lambda>x. mset (remdups (oppositeLiteralList x))))
[PROOF STEP]
using wf_inv_image[of "(mult (precedesOrder (elements M)))"]
[PROOF STATE]
proof (prove)
using this:
wf (mult (precedesOrder (elements M)))
wf (mult (precedesOrder (elements M))) \<Longrightarrow> wf (inv_image (mult (precedesOrder (elements M))) ?f)

goal (1 subgoal):
 1. wf (inv_image (mult (precedesOrder (elements M))) (\<lambda>x. mset (remdups (oppositeLiteralList x))))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
wf (multLess M)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma transBoolLess:
  shows "trans boolLess"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trans boolLess
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. trans boolLess
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. trans boolLess
[PROOF STEP]
fix x::bool and y::bool and z::bool
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. trans boolLess
[PROOF STEP]
assume "(x, y) \<in> boolLess"
[PROOF STATE]
proof (state)
this:
(x, y) \<in> boolLess

goal (1 subgoal):
 1. trans boolLess
[PROOF STEP]
hence "x = True" "y = False"
[PROOF STATE]
proof (prove)
using this:
(x, y) \<in> boolLess

goal (1 subgoal):
 1. x = True &&& y = False
[PROOF STEP]
unfolding boolLess_def
[PROOF STATE]
proof (prove)
using this:
(x, y) \<in> {(True, False)}

goal (1 subgoal):
 1. x = True &&& y = False
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x = True
y = False

goal (1 subgoal):
 1. trans boolLess
[PROOF STEP]
assume "(y, z) \<in> boolLess"
[PROOF STATE]
proof (state)
this:
(y, z) \<in> boolLess

goal (1 subgoal):
 1. trans boolLess
[PROOF STEP]
hence "y = True" "z = False"
[PROOF STATE]
proof (prove)
using this:
(y, z) \<in> boolLess

goal (1 subgoal):
 1. y = True &&& z = False
[PROOF STEP]
unfolding boolLess_def
[PROOF STATE]
proof (prove)
using this:
(y, z) \<in> {(True, False)}

goal (1 subgoal):
 1. y = True &&& z = False
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
y = True
z = False

goal (1 subgoal):
 1. trans boolLess
[PROOF STEP]
from \<open>y = False\<close> \<open>y = True\<close>
[PROOF STATE]
proof (chain)
picking this:
y = False
y = True
[PROOF STEP]
have False
[PROOF STATE]
proof (prove)
using this:
y = False
y = True

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

goal (1 subgoal):
 1. trans boolLess
[PROOF STEP]
hence "(x, z) \<in> boolLess"
[PROOF STATE]
proof (prove)
using this:
False

goal (1 subgoal):
 1. (x, z) \<in> boolLess
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(x, z) \<in> boolLess

goal (1 subgoal):
 1. trans boolLess
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>(?x2, ?y2) \<in> boolLess; (?y2, ?z2) \<in> boolLess\<rbrakk> \<Longrightarrow> (?x2, ?z2) \<in> boolLess

goal (1 subgoal):
 1. trans boolLess
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(?x2, ?y2) \<in> boolLess; (?y2, ?z2) \<in> boolLess\<rbrakk> \<Longrightarrow> (?x2, ?z2) \<in> boolLess

goal (1 subgoal):
 1. trans boolLess
[PROOF STEP]
unfolding trans_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(?x2, ?y2) \<in> boolLess; (?y2, ?z2) \<in> boolLess\<rbrakk> \<Longrightarrow> (?x2, ?z2) \<in> boolLess

goal (1 subgoal):
 1. \<forall>x y z. (x, y) \<in> boolLess \<longrightarrow> (y, z) \<in> boolLess \<longrightarrow> (x, z) \<in> boolLess
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
trans boolLess

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma wfBoolLess:
  shows "wf boolLess"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf boolLess
[PROOF STEP]
proof (rule finite_acyclic_wf)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. finite boolLess
 2. acyclic boolLess
[PROOF STEP]
show "finite boolLess"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite boolLess
[PROOF STEP]
unfolding boolLess_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {(True, False)}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
finite boolLess

goal (1 subgoal):
 1. acyclic boolLess
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. acyclic boolLess
[PROOF STEP]
have "boolLess^+ = boolLess"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. boolLess\<^sup>+ = boolLess
[PROOF STEP]
using transBoolLess
[PROOF STATE]
proof (prove)
using this:
trans boolLess

goal (1 subgoal):
 1. boolLess\<^sup>+ = boolLess
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
boolLess\<^sup>+ = boolLess

goal (1 subgoal):
 1. acyclic boolLess
[PROOF STEP]
thus "acyclic boolLess"
[PROOF STATE]
proof (prove)
using this:
boolLess\<^sup>+ = boolLess

goal (1 subgoal):
 1. acyclic boolLess
[PROOF STEP]
unfolding boolLess_def
[PROOF STATE]
proof (prove)
using this:
{(True, False)}\<^sup>+ = {(True, False)}

goal (1 subgoal):
 1. acyclic {(True, False)}
[PROOF STEP]
unfolding acyclic_def
[PROOF STATE]
proof (prove)
using this:
{(True, False)}\<^sup>+ = {(True, False)}

goal (1 subgoal):
 1. \<forall>x. (x, x) \<notin> {(True, False)}\<^sup>+
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
acyclic boolLess

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma wellFoundedEmbed:
  fixes rel :: "('a \<times> 'a) set" and rel' :: "('a \<times> 'a) set"
  assumes "\<forall> x y. (x, y) \<in> rel \<longrightarrow> (x, y) \<in> rel'" and "wf rel'"
  shows "wf rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf rel
[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> rel \<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> rel \<longrightarrow> y \<notin> Q)
[PROOF STEP]
show "\<forall>Q x. x \<in> Q \<longrightarrow> (\<exists>zmin\<in>Q. \<forall>z. (z, zmin) \<in> rel \<longrightarrow> z \<notin> Q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>Q x. x \<in> Q \<longrightarrow> (\<exists>zmin\<in>Q. \<forall>z. (z, zmin) \<in> rel \<longrightarrow> z \<notin> Q)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>Q x. x \<in> Q \<longrightarrow> (\<exists>zmin\<in>Q. \<forall>z. (z, zmin) \<in> rel \<longrightarrow> z \<notin> Q)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>Q x. x \<in> Q \<longrightarrow> (\<exists>zmin\<in>Q. \<forall>z. (z, zmin) \<in> rel \<longrightarrow> z \<notin> Q)
[PROOF STEP]
fix x::"'a" and Q::"'a set"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>Q x. x \<in> Q \<longrightarrow> (\<exists>zmin\<in>Q. \<forall>z. (z, zmin) \<in> rel \<longrightarrow> z \<notin> Q)
[PROOF STEP]
assume "x \<in> Q"
[PROOF STATE]
proof (state)
this:
x \<in> Q

goal (1 subgoal):
 1. \<forall>Q x. x \<in> Q \<longrightarrow> (\<exists>zmin\<in>Q. \<forall>z. (z, zmin) \<in> rel \<longrightarrow> z \<notin> Q)
[PROOF STEP]
have "\<exists>zmin\<in>Q. \<forall>z. (z, zmin) \<in> rel \<longrightarrow> z \<notin> Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>zmin\<in>Q. \<forall>z. (z, zmin) \<in> rel \<longrightarrow> z \<notin> Q
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>zmin\<in>Q. \<forall>z. (z, zmin) \<in> rel \<longrightarrow> z \<notin> Q
[PROOF STEP]
from \<open>wf rel'\<close> \<open>x \<in> Q\<close>
[PROOF STATE]
proof (chain)
picking this:
wf rel'
x \<in> Q
[PROOF STEP]
obtain zmin::"'a"
          where "zmin \<in> Q" and "\<forall>z. (z, zmin) \<in> rel' \<longrightarrow> z \<notin> Q"
[PROOF STATE]
proof (prove)
using this:
wf rel'
x \<in> Q

goal (1 subgoal):
 1. (\<And>zmin. \<lbrakk>zmin \<in> Q; \<forall>z. (z, zmin) \<in> rel' \<longrightarrow> z \<notin> Q\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding wf_eq_minimal
[PROOF STATE]
proof (prove)
using this:
\<forall>Q x. x \<in> Q \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. (y, z) \<in> rel' \<longrightarrow> y \<notin> Q)
x \<in> Q

goal (1 subgoal):
 1. (\<And>zmin. \<lbrakk>zmin \<in> Q; \<forall>z. (z, zmin) \<in> rel' \<longrightarrow> z \<notin> Q\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
zmin \<in> Q
\<forall>z. (z, zmin) \<in> rel' \<longrightarrow> z \<notin> Q

goal (1 subgoal):
 1. \<exists>zmin\<in>Q. \<forall>z. (z, zmin) \<in> rel \<longrightarrow> z \<notin> Q
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
zmin \<in> Q
\<forall>z. (z, zmin) \<in> rel' \<longrightarrow> z \<notin> Q

goal (1 subgoal):
 1. \<exists>zmin\<in>Q. \<forall>z. (z, zmin) \<in> rel \<longrightarrow> z \<notin> Q
[PROOF STEP]
fix z::"'a"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>zmin\<in>Q. \<forall>z. (z, zmin) \<in> rel \<longrightarrow> z \<notin> Q
[PROOF STEP]
assume "(z, zmin) \<in> rel"
[PROOF STATE]
proof (state)
this:
(z, zmin) \<in> rel

goal (1 subgoal):
 1. \<exists>zmin\<in>Q. \<forall>z. (z, zmin) \<in> rel \<longrightarrow> z \<notin> Q
[PROOF STEP]
have "z \<notin> Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. z \<notin> Q
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. z \<notin> Q
[PROOF STEP]
from \<open>\<forall> x y. (x, y) \<in> rel \<longrightarrow> (x, y) \<in> rel'\<close> \<open>(z, zmin) \<in> rel\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>x y. (x, y) \<in> rel \<longrightarrow> (x, y) \<in> rel'
(z, zmin) \<in> rel
[PROOF STEP]
have "(z, zmin) \<in> rel'"
[PROOF STATE]
proof (prove)
using this:
\<forall>x y. (x, y) \<in> rel \<longrightarrow> (x, y) \<in> rel'
(z, zmin) \<in> rel

goal (1 subgoal):
 1. (z, zmin) \<in> rel'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(z, zmin) \<in> rel'

goal (1 subgoal):
 1. z \<notin> Q
[PROOF STEP]
with \<open>\<forall>z. (z, zmin) \<in> rel' \<longrightarrow> z \<notin> Q\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>z. (z, zmin) \<in> rel' \<longrightarrow> z \<notin> Q
(z, zmin) \<in> rel'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>z. (z, zmin) \<in> rel' \<longrightarrow> z \<notin> Q
(z, zmin) \<in> rel'

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
z \<notin> Q

goal (1 subgoal):
 1. \<exists>zmin\<in>Q. \<forall>z. (z, zmin) \<in> rel \<longrightarrow> z \<notin> Q
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
(?z2, zmin) \<in> rel \<Longrightarrow> ?z2 \<notin> Q

goal (1 subgoal):
 1. \<exists>zmin\<in>Q. \<forall>z. (z, zmin) \<in> rel \<longrightarrow> z \<notin> Q
[PROOF STEP]
with \<open>zmin \<in> Q\<close>
[PROOF STATE]
proof (chain)
picking this:
zmin \<in> Q
(?z2, zmin) \<in> rel \<Longrightarrow> ?z2 \<notin> Q
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
zmin \<in> Q
(?z2, zmin) \<in> rel \<Longrightarrow> ?z2 \<notin> Q

goal (1 subgoal):
 1. \<exists>zmin\<in>Q. \<forall>z. (z, zmin) \<in> rel \<longrightarrow> z \<notin> Q
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>zmin\<in>Q. \<forall>z. (z, zmin) \<in> rel \<longrightarrow> z \<notin> Q

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>zmin\<in>Q. \<forall>z. (z, zmin) \<in> rel \<longrightarrow> z \<notin> Q

goal (1 subgoal):
 1. \<forall>Q x. x \<in> Q \<longrightarrow> (\<exists>zmin\<in>Q. \<forall>z. (z, zmin) \<in> rel \<longrightarrow> z \<notin> Q)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?x2 \<in> ?Q2 \<Longrightarrow> \<exists>zmin\<in>?Q2. \<forall>z. (z, zmin) \<in> rel \<longrightarrow> z \<notin> ?Q2

goal (1 subgoal):
 1. \<forall>Q x. x \<in> Q \<longrightarrow> (\<exists>zmin\<in>Q. \<forall>z. (z, zmin) \<in> rel \<longrightarrow> z \<notin> Q)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
?x2 \<in> ?Q2 \<Longrightarrow> \<exists>zmin\<in>?Q2. \<forall>z. (z, zmin) \<in> rel \<longrightarrow> z \<notin> ?Q2

goal (1 subgoal):
 1. \<forall>Q x. x \<in> Q \<longrightarrow> (\<exists>zmin\<in>Q. \<forall>z. (z, zmin) \<in> rel \<longrightarrow> z \<notin> Q)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>Q x. x \<in> Q \<longrightarrow> (\<exists>zmin\<in>Q. \<forall>z. (z, zmin) \<in> rel \<longrightarrow> z \<notin> Q)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>Q x. x \<in> Q \<longrightarrow> (\<exists>zmin\<in>Q. \<forall>z. (z, zmin) \<in> rel \<longrightarrow> z \<notin> Q)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma field_differentiable_on_subset:
  assumes "f field_differentiable_on S"
      and "T \<subseteq> S"
    shows "f field_differentiable_on T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f field_differentiable_on T
[PROOF STEP]
by (meson assms field_differentiable_on_def field_differentiable_within_subset in_mono)


[STATEMENT]
lemma once_field_differentiable_at:
  "f twice_field_differentiable_at x \<Longrightarrow> f field_differentiable (at x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f twice_field_differentiable_at x \<Longrightarrow> f field_differentiable at x
[PROOF STEP]
by (metis at_within_interior field_differentiable_on_def interior_subset subsetD twice_field_differentiable_at_def)


[STATEMENT]
lemma deriv_field_differentiable_at:
  "f twice_field_differentiable_at x \<Longrightarrow> deriv f field_differentiable (at x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f twice_field_differentiable_at x \<Longrightarrow> deriv f field_differentiable at x
[PROOF STEP]
using twice_field_differentiable_at_def
[PROOF STATE]
proof (prove)
using this:
?f twice_field_differentiable_at ?x \<equiv> \<exists>S. ?f field_differentiable_on S \<and> ?x \<in> interior S \<and> deriv ?f field_differentiable at ?x

goal (1 subgoal):
 1. f twice_field_differentiable_at x \<Longrightarrow> deriv f field_differentiable at x
[PROOF STEP]
by blast


[STATEMENT]
lemma eventually_deriv_compose:
  assumes "\<exists>S. f field_differentiable_on S \<and> x \<in> interior S"
      and "g twice_field_differentiable_at (f x)"
    shows "\<forall>\<^sub>F x in nhds x. deriv (\<lambda>x. g (f x)) x = deriv g (f x) * deriv f x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<^sub>F x in nhds x. deriv (\<lambda>x. g (f x)) x = deriv g (f x) * deriv f x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>\<^sub>F x in nhds x. deriv (\<lambda>x. g (f x)) x = deriv g (f x) * deriv f x
[PROOF STEP]
obtain S S'
   where Df_on_S:  "f field_differentiable_on S" and x_int_S: "x \<in> interior S"
     and Dg_on_S': "g field_differentiable_on S'" and fx_int_S': "f x \<in> interior S'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>S S'. \<lbrakk>f field_differentiable_on S; x \<in> interior S; g field_differentiable_on S'; f x \<in> interior S'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms twice_field_differentiable_at_def
[PROOF STATE]
proof (prove)
using this:
\<exists>S. f field_differentiable_on S \<and> x \<in> interior S
g twice_field_differentiable_at f x
?f twice_field_differentiable_at ?x \<equiv> \<exists>S. ?f field_differentiable_on S \<and> ?x \<in> interior S \<and> deriv ?f field_differentiable at ?x

goal (1 subgoal):
 1. (\<And>S S'. \<lbrakk>f field_differentiable_on S; x \<in> interior S; g field_differentiable_on S'; f x \<in> interior S'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
f field_differentiable_on S
x \<in> interior S
g field_differentiable_on S'
f x \<in> interior S'

goal (1 subgoal):
 1. \<forall>\<^sub>F x in nhds x. deriv (\<lambda>x. g (f x)) x = deriv g (f x) * deriv f x
[PROOF STEP]
let ?T = "{x \<in> interior S. f x \<in> interior S'}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>\<^sub>F x in nhds x. deriv (\<lambda>x. g (f x)) x = deriv g (f x) * deriv f x
[PROOF STEP]
have "continuous_on (interior S) f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. continuous_on (interior S) f
[PROOF STEP]
by (meson Df_on_S continuous_on_eq_continuous_within continuous_on_subset field_differentiable_imp_continuous_at
         field_differentiable_on_def interior_subset)
[PROOF STATE]
proof (state)
this:
continuous_on (interior S) f

goal (1 subgoal):
 1. \<forall>\<^sub>F x in nhds x. deriv (\<lambda>x. g (f x)) x = deriv g (f x) * deriv f x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
continuous_on (interior S) f
[PROOF STEP]
have "open (interior S \<inter> {x. f x \<in> interior S'})"
[PROOF STATE]
proof (prove)
using this:
continuous_on (interior S) f

goal (1 subgoal):
 1. open (interior S \<inter> {x. f x \<in> interior S'})
[PROOF STEP]
by (metis continuous_open_preimage open_interior vimage_def)
[PROOF STATE]
proof (state)
this:
open (interior S \<inter> {x. f x \<in> interior S'})

goal (1 subgoal):
 1. \<forall>\<^sub>F x in nhds x. deriv (\<lambda>x. g (f x)) x = deriv g (f x) * deriv f x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
open (interior S \<inter> {x. f x \<in> interior S'})
[PROOF STEP]
have x_int_T: "x \<in> interior ?T"
[PROOF STATE]
proof (prove)
using this:
open (interior S \<inter> {x. f x \<in> interior S'})

goal (1 subgoal):
 1. x \<in> interior {x \<in> interior S. f x \<in> interior S'}
[PROOF STEP]
by (metis (no_types) Collect_conj_eq Collect_mem_eq Int_Collect fx_int_S' interior_eq x_int_S)
[PROOF STATE]
proof (state)
this:
x \<in> interior {x \<in> interior S. f x \<in> interior S'}

goal (1 subgoal):
 1. \<forall>\<^sub>F x in nhds x. deriv (\<lambda>x. g (f x)) x = deriv g (f x) * deriv f x
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
x \<in> interior {x \<in> interior S. f x \<in> interior S'}

goal (1 subgoal):
 1. \<forall>\<^sub>F x in nhds x. deriv (\<lambda>x. g (f x)) x = deriv g (f x) * deriv f x
[PROOF STEP]
have  Dg_on_fT: "g field_differentiable_on f`?T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g field_differentiable_on f ` {x \<in> interior S. f x \<in> interior S'}
[PROOF STEP]
by (metis (no_types, lifting) Dg_on_S' field_differentiable_on_subset image_Collect_subsetI interior_subset)
[PROOF STATE]
proof (state)
this:
g field_differentiable_on f ` {x \<in> interior S. f x \<in> interior S'}

goal (1 subgoal):
 1. \<forall>\<^sub>F x in nhds x. deriv (\<lambda>x. g (f x)) x = deriv g (f x) * deriv f x
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
g field_differentiable_on f ` {x \<in> interior S. f x \<in> interior S'}

goal (1 subgoal):
 1. \<forall>\<^sub>F x in nhds x. deriv (\<lambda>x. g (f x)) x = deriv g (f x) * deriv f x
[PROOF STEP]
have Df_on_T: "f field_differentiable_on ?T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f field_differentiable_on {x \<in> interior S. f x \<in> interior S'}
[PROOF STEP]
using  field_differentiable_on_subset Df_on_S
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?f field_differentiable_on ?S; ?T \<subseteq> ?S\<rbrakk> \<Longrightarrow> ?f field_differentiable_on ?T
f field_differentiable_on S

goal (1 subgoal):
 1. f field_differentiable_on {x \<in> interior S. f x \<in> interior S'}
[PROOF STEP]
by (metis Collect_subset interior_subset)
[PROOF STATE]
proof (state)
this:
f field_differentiable_on {x \<in> interior S. f x \<in> interior S'}

goal (1 subgoal):
 1. \<forall>\<^sub>F x in nhds x. deriv (\<lambda>x. g (f x)) x = deriv g (f x) * deriv f x
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
f field_differentiable_on {x \<in> interior S. f x \<in> interior S'}

goal (1 subgoal):
 1. \<forall>\<^sub>F x in nhds x. deriv (\<lambda>x. g (f x)) x = deriv g (f x) * deriv f x
[PROOF STEP]
have "\<forall>x \<in> interior ?T. deriv (\<lambda>x. g (f x)) x = deriv g (f x) * deriv f x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>interior {x \<in> interior S. f x \<in> interior S'}. deriv (\<lambda>x. g (f x)) x = deriv g (f x) * deriv f x
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> interior {x \<in> interior S. f x \<in> interior S'} \<Longrightarrow> deriv (\<lambda>x. g (f x)) x = deriv g (f x) * deriv f x
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> interior {x \<in> interior S. f x \<in> interior S'} \<Longrightarrow> deriv (\<lambda>x. g (f x)) x = deriv g (f x) * deriv f x
[PROOF STEP]
assume x_int_T: "x \<in> interior ?T"
[PROOF STATE]
proof (state)
this:
x \<in> interior {x \<in> interior S. f x \<in> interior S'}

goal (1 subgoal):
 1. \<And>x. x \<in> interior {x \<in> interior S. f x \<in> interior S'} \<Longrightarrow> deriv (\<lambda>x. g (f x)) x = deriv g (f x) * deriv f x
[PROOF STEP]
have "f field_differentiable at x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f field_differentiable at x
[PROOF STEP]
by (metis (no_types, lifting) Df_on_T at_within_interior field_differentiable_on_def
          interior_subset subsetD x_int_T)
[PROOF STATE]
proof (state)
this:
f field_differentiable at x

goal (1 subgoal):
 1. \<And>x. x \<in> interior {x \<in> interior S. f x \<in> interior S'} \<Longrightarrow> deriv (\<lambda>x. g (f x)) x = deriv g (f x) * deriv f x
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
f field_differentiable at x

goal (1 subgoal):
 1. \<And>x. x \<in> interior {x \<in> interior S. f x \<in> interior S'} \<Longrightarrow> deriv (\<lambda>x. g (f x)) x = deriv g (f x) * deriv f x
[PROOF STEP]
have "g field_differentiable at (f x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g field_differentiable at (f x)
[PROOF STEP]
by (metis (no_types, lifting) Dg_on_S' at_within_interior field_differentiable_on_def
          interior_subset mem_Collect_eq subsetD x_int_T)
[PROOF STATE]
proof (state)
this:
g field_differentiable at (f x)

goal (1 subgoal):
 1. \<And>x. x \<in> interior {x \<in> interior S. f x \<in> interior S'} \<Longrightarrow> deriv (\<lambda>x. g (f x)) x = deriv g (f x) * deriv f x
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
f field_differentiable at x
g field_differentiable at (f x)
[PROOF STEP]
have "deriv (g \<circ> f) x = deriv g (f x) * deriv f x"
[PROOF STATE]
proof (prove)
using this:
f field_differentiable at x
g field_differentiable at (f x)

goal (1 subgoal):
 1. deriv (g \<circ> f) x = deriv g (f x) * deriv f x
[PROOF STEP]
using deriv_chain[of f x g]
[PROOF STATE]
proof (prove)
using this:
f field_differentiable at x
g field_differentiable at (f x)
\<lbrakk>f field_differentiable at x; g field_differentiable at (f x)\<rbrakk> \<Longrightarrow> deriv (g \<circ> f) x = deriv g (f x) * deriv f x

goal (1 subgoal):
 1. deriv (g \<circ> f) x = deriv g (f x) * deriv f x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
deriv (g \<circ> f) x = deriv g (f x) * deriv f x

goal (1 subgoal):
 1. \<And>x. x \<in> interior {x \<in> interior S. f x \<in> interior S'} \<Longrightarrow> deriv (\<lambda>x. g (f x)) x = deriv g (f x) * deriv f x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
deriv (g \<circ> f) x = deriv g (f x) * deriv f x
[PROOF STEP]
show "deriv (\<lambda>x. g (f x)) x = deriv g (f x) * deriv f x"
[PROOF STATE]
proof (prove)
using this:
deriv (g \<circ> f) x = deriv g (f x) * deriv f x

goal (1 subgoal):
 1. deriv (\<lambda>x. g (f x)) x = deriv g (f x) * deriv f x
[PROOF STEP]
by (simp add: comp_def)
[PROOF STATE]
proof (state)
this:
deriv (\<lambda>x. g (f x)) x = deriv g (f x) * deriv f x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>interior {x \<in> interior S. f x \<in> interior S'}. deriv (\<lambda>x. g (f x)) x = deriv g (f x) * deriv f x

goal (1 subgoal):
 1. \<forall>\<^sub>F x in nhds x. deriv (\<lambda>x. g (f x)) x = deriv g (f x) * deriv f x
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
x \<in> interior {x \<in> interior S. f x \<in> interior S'}
g field_differentiable_on f ` {x \<in> interior S. f x \<in> interior S'}
f field_differentiable_on {x \<in> interior S. f x \<in> interior S'}
\<forall>x\<in>interior {x \<in> interior S. f x \<in> interior S'}. deriv (\<lambda>x. g (f x)) x = deriv g (f x) * deriv f x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x \<in> interior {x \<in> interior S. f x \<in> interior S'}
g field_differentiable_on f ` {x \<in> interior S. f x \<in> interior S'}
f field_differentiable_on {x \<in> interior S. f x \<in> interior S'}
\<forall>x\<in>interior {x \<in> interior S. f x \<in> interior S'}. deriv (\<lambda>x. g (f x)) x = deriv g (f x) * deriv f x

goal (1 subgoal):
 1. \<forall>\<^sub>F x in nhds x. deriv (\<lambda>x. g (f x)) x = deriv g (f x) * deriv f x
[PROOF STEP]
using eventually_nhds
[PROOF STATE]
proof (prove)
using this:
x \<in> interior {x \<in> interior S. f x \<in> interior S'}
g field_differentiable_on f ` {x \<in> interior S. f x \<in> interior S'}
f field_differentiable_on {x \<in> interior S. f x \<in> interior S'}
\<forall>x\<in>interior {x \<in> interior S. f x \<in> interior S'}. deriv (\<lambda>x. g (f x)) x = deriv g (f x) * deriv f x
eventually ?P (nhds ?a) = (\<exists>S. open S \<and> ?a \<in> S \<and> (\<forall>x\<in>S. ?P x))

goal (1 subgoal):
 1. \<forall>\<^sub>F x in nhds x. deriv (\<lambda>x. g (f x)) x = deriv g (f x) * deriv f x
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F x in nhds x. deriv (\<lambda>x. g (f x)) x = deriv g (f x) * deriv f x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma eventually_deriv_compose':
  assumes "f twice_field_differentiable_at x"
      and "g twice_field_differentiable_at (f x)"
    shows "\<forall>\<^sub>F x in nhds x. deriv (\<lambda>x. g (f x)) x = deriv g (f x) * deriv f x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<^sub>F x in nhds x. deriv (\<lambda>x. g (f x)) x = deriv g (f x) * deriv f x
[PROOF STEP]
using assms eventually_deriv_compose twice_field_differentiable_at_def
[PROOF STATE]
proof (prove)
using this:
f twice_field_differentiable_at x
g twice_field_differentiable_at f x
\<lbrakk>\<exists>S. ?f field_differentiable_on S \<and> ?x \<in> interior S; ?g twice_field_differentiable_at ?f ?x\<rbrakk> \<Longrightarrow> \<forall>\<^sub>F x in nhds ?x. deriv (\<lambda>x. ?g (?f x)) x = deriv ?g (?f x) * deriv ?f x
?f twice_field_differentiable_at ?x \<equiv> \<exists>S. ?f field_differentiable_on S \<and> ?x \<in> interior S \<and> deriv ?f field_differentiable at ?x

goal (1 subgoal):
 1. \<forall>\<^sub>F x in nhds x. deriv (\<lambda>x. g (f x)) x = deriv g (f x) * deriv f x
[PROOF STEP]
by blast