[STATEMENT]
lemma max_pos_lit_dominates_cl:
  assumes "maximal_literal (subst_lit L \<sigma>) (subst_cl C \<sigma>)"
  assumes "orient_lit_inst L t s pos \<sigma>"
  assumes "L' \<in> C - { L }"
  assumes "\<not>equivalent_eq_exists t s C I \<sigma> L"
  assumes "vars_of_lit (subst_lit L \<sigma>) = {}"
  assumes "vars_of_lit (subst_lit L' \<sigma>) = {}"
  assumes "fo_interpretation I"
  shows "((subst_lit L' \<sigma>),(subst_lit L \<sigma>)) \<in> lit_ord"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (subst_lit L' \<sigma>, subst_lit L \<sigma>) \<in> lit_ord
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (subst_lit L' \<sigma>, subst_lit L \<sigma>) \<in> lit_ord
[PROOF STEP]
let ?L' = "(subst_lit L' \<sigma>)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (subst_lit L' \<sigma>, subst_lit L \<sigma>) \<in> lit_ord
[PROOF STEP]
let ?L = "(subst_lit L \<sigma>)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (subst_lit L' \<sigma>, subst_lit L \<sigma>) \<in> lit_ord
[PROOF STEP]
let ?t = "(subst t \<sigma>)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (subst_lit L' \<sigma>, subst_lit L \<sigma>) \<in> lit_ord
[PROOF STEP]
let ?s = "(subst s \<sigma>)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (subst_lit L' \<sigma>, subst_lit L \<sigma>) \<in> lit_ord
[PROOF STEP]
from assms(2)
[PROOF STATE]
proof (chain)
picking this:
orient_lit_inst L t s pos \<sigma>
[PROOF STEP]
have "(?t,?s) \<notin> trm_ord"
[PROOF STATE]
proof (prove)
using this:
orient_lit_inst L t s pos \<sigma>

goal (1 subgoal):
 1. (t \<lhd> \<sigma>, s \<lhd> \<sigma>) \<notin> trm_ord
[PROOF STEP]
unfolding orient_lit_inst_def
[PROOF STATE]
proof (prove)
using this:
(L = Pos (Eq t s) \<or> L = Pos (Eq s t)) \<and> (t \<lhd> \<sigma>, s \<lhd> \<sigma>) \<notin> trm_ord \<and> pos = pos \<or> (L = Neg (Eq t s) \<or> L = Neg (Eq s t)) \<and> (t \<lhd> \<sigma>, s \<lhd> \<sigma>) \<notin> trm_ord \<and> pos = neg

goal (1 subgoal):
 1. (t \<lhd> \<sigma>, s \<lhd> \<sigma>) \<notin> trm_ord
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(t \<lhd> \<sigma>, s \<lhd> \<sigma>) \<notin> trm_ord

goal (1 subgoal):
 1. (subst_lit L' \<sigma>, subst_lit L \<sigma>) \<in> lit_ord
[PROOF STEP]
obtain u' v' where "L' = (Pos (Eq u' v')) \<or> L' = (Neg  (Eq u' v'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>u' v'. L' = Pos (Eq u' v') \<or> L' = Neg (Eq u' v') \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using literal.exhaust equation.exhaust
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>x1. ?y = Pos x1 \<Longrightarrow> ?P; \<And>x2. ?y = Neg x2 \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
(\<And>x1 x2. ?y = Eq x1 x2 \<Longrightarrow> ?P) \<Longrightarrow> ?P

goal (1 subgoal):
 1. (\<And>u' v'. L' = Pos (Eq u' v') \<or> L' = Neg (Eq u' v') \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
L' = Pos (Eq u' v') \<or> L' = Neg (Eq u' v')

goal (1 subgoal):
 1. (subst_lit L' \<sigma>, subst_lit L \<sigma>) \<in> lit_ord
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
L' = Pos (Eq u' v') \<or> L' = Neg (Eq u' v')
[PROOF STEP]
obtain polarity u v where "orient_lit_inst L' u v polarity \<sigma>"
    and "((subst u \<sigma>),(subst v \<sigma>)) \<notin>  trm_ord"
[PROOF STATE]
proof (prove)
using this:
L' = Pos (Eq u' v') \<or> L' = Neg (Eq u' v')

goal (1 subgoal):
 1. (\<And>u v polarity. \<lbrakk>orient_lit_inst L' u v polarity \<sigma>; (u \<lhd> \<sigma>, v \<lhd> \<sigma>) \<notin> trm_ord\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using
    trm_ord_trans trm_ord_irrefl
[PROOF STATE]
proof (prove)
using this:
L' = Pos (Eq u' v') \<or> L' = Neg (Eq u' v')
trans trm_ord
irrefl trm_ord

goal (1 subgoal):
 1. (\<And>u v polarity. \<lbrakk>orient_lit_inst L' u v polarity \<sigma>; (u \<lhd> \<sigma>, v \<lhd> \<sigma>) \<notin> trm_ord\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding trans_def irrefl_def orient_lit_inst_def
[PROOF STATE]
proof (prove)
using this:
L' = Pos (Eq u' v') \<or> L' = Neg (Eq u' v')
\<forall>x y z. (x, y) \<in> trm_ord \<longrightarrow> (y, z) \<in> trm_ord \<longrightarrow> (x, z) \<in> trm_ord
\<forall>a. (a, a) \<notin> trm_ord

goal (1 subgoal):
 1. (\<And>u v polarity. \<lbrakk>(L' = Pos (Eq u v) \<or> L' = Pos (Eq v u)) \<and> (u \<lhd> \<sigma>, v \<lhd> \<sigma>) \<notin> trm_ord \<and> polarity = pos \<or> (L' = Neg (Eq u v) \<or> L' = Neg (Eq v u)) \<and> (u \<lhd> \<sigma>, v \<lhd> \<sigma>) \<notin> trm_ord \<and> polarity = neg; (u \<lhd> \<sigma>, v \<lhd> \<sigma>) \<notin> trm_ord\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
orient_lit_inst L' u v polarity \<sigma>
(u \<lhd> \<sigma>, v \<lhd> \<sigma>) \<notin> trm_ord

goal (1 subgoal):
 1. (subst_lit L' \<sigma>, subst_lit L \<sigma>) \<in> lit_ord
[PROOF STEP]
let ?u = "(subst u \<sigma>)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (subst_lit L' \<sigma>, subst_lit L \<sigma>) \<in> lit_ord
[PROOF STEP]
let ?v = "(subst v \<sigma>)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (subst_lit L' \<sigma>, subst_lit L \<sigma>) \<in> lit_ord
[PROOF STEP]
from \<open>orient_lit_inst L' u v polarity \<sigma>\<close>
[PROOF STATE]
proof (chain)
picking this:
orient_lit_inst L' u v polarity \<sigma>
[PROOF STEP]
have "orient_lit ?L' ?u ?v polarity"
[PROOF STATE]
proof (prove)
using this:
orient_lit_inst L' u v polarity \<sigma>

goal (1 subgoal):
 1. orient_lit (subst_lit L' \<sigma>) (u \<lhd> \<sigma>) (v \<lhd> \<sigma>) polarity
[PROOF STEP]
using lift_orient_lit
[PROOF STATE]
proof (prove)
using this:
orient_lit_inst L' u v polarity \<sigma>
orient_lit_inst ?L ?t ?s ?p ?\<sigma> \<Longrightarrow> orient_lit (subst_lit ?L ?\<sigma>) (?t \<lhd> ?\<sigma>) (?s \<lhd> ?\<sigma>) ?p

goal (1 subgoal):
 1. orient_lit (subst_lit L' \<sigma>) (u \<lhd> \<sigma>) (v \<lhd> \<sigma>) polarity
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
orient_lit (subst_lit L' \<sigma>) (u \<lhd> \<sigma>) (v \<lhd> \<sigma>) polarity

goal (1 subgoal):
 1. (subst_lit L' \<sigma>, subst_lit L \<sigma>) \<in> lit_ord
[PROOF STEP]
from \<open>orient_lit_inst L t s pos \<sigma>\<close>
[PROOF STATE]
proof (chain)
picking this:
orient_lit_inst L t s pos \<sigma>
[PROOF STEP]
have "orient_lit ?L ?t ?s pos"
[PROOF STATE]
proof (prove)
using this:
orient_lit_inst L t s pos \<sigma>

goal (1 subgoal):
 1. orient_lit (subst_lit L \<sigma>) (t \<lhd> \<sigma>) (s \<lhd> \<sigma>) pos
[PROOF STEP]
using lift_orient_lit
[PROOF STATE]
proof (prove)
using this:
orient_lit_inst L t s pos \<sigma>
orient_lit_inst ?L ?t ?s ?p ?\<sigma> \<Longrightarrow> orient_lit (subst_lit ?L ?\<sigma>) (?t \<lhd> ?\<sigma>) (?s \<lhd> ?\<sigma>) ?p

goal (1 subgoal):
 1. orient_lit (subst_lit L \<sigma>) (t \<lhd> \<sigma>) (s \<lhd> \<sigma>) pos
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
orient_lit (subst_lit L \<sigma>) (t \<lhd> \<sigma>) (s \<lhd> \<sigma>) pos

goal (1 subgoal):
 1. (subst_lit L' \<sigma>, subst_lit L \<sigma>) \<in> lit_ord
[PROOF STEP]
from assms(6) and \<open>orient_lit ?L' ?u ?v polarity\<close>
[PROOF STATE]
proof (chain)
picking this:
vars_of_lit (subst_lit L' \<sigma>) = {}
orient_lit (subst_lit L' \<sigma>) (u \<lhd> \<sigma>) (v \<lhd> \<sigma>) polarity
[PROOF STEP]
have "vars_of ?u \<subseteq> {}"
[PROOF STATE]
proof (prove)
using this:
vars_of_lit (subst_lit L' \<sigma>) = {}
orient_lit (subst_lit L' \<sigma>) (u \<lhd> \<sigma>) (v \<lhd> \<sigma>) polarity

goal (1 subgoal):
 1. vars_of (u \<lhd> \<sigma>) \<subseteq> {}
[PROOF STEP]
using orient_lit_vars
[PROOF STATE]
proof (prove)
using this:
vars_of_lit (subst_lit L' \<sigma>) = {}
orient_lit (subst_lit L' \<sigma>) (u \<lhd> \<sigma>) (v \<lhd> \<sigma>) polarity
orient_lit ?L ?t ?s ?p \<Longrightarrow> vars_of ?t \<subseteq> vars_of_lit ?L \<and> vars_of ?s \<subseteq> vars_of_lit ?L

goal (1 subgoal):
 1. vars_of (u \<lhd> \<sigma>) \<subseteq> {}
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
vars_of (u \<lhd> \<sigma>) \<subseteq> {}

goal (1 subgoal):
 1. (subst_lit L' \<sigma>, subst_lit L \<sigma>) \<in> lit_ord
[PROOF STEP]
from assms(6) and \<open>orient_lit ?L' ?u ?v polarity\<close>
[PROOF STATE]
proof (chain)
picking this:
vars_of_lit (subst_lit L' \<sigma>) = {}
orient_lit (subst_lit L' \<sigma>) (u \<lhd> \<sigma>) (v \<lhd> \<sigma>) polarity
[PROOF STEP]
have "vars_of ?v \<subseteq> {}"
[PROOF STATE]
proof (prove)
using this:
vars_of_lit (subst_lit L' \<sigma>) = {}
orient_lit (subst_lit L' \<sigma>) (u \<lhd> \<sigma>) (v \<lhd> \<sigma>) polarity

goal (1 subgoal):
 1. vars_of (v \<lhd> \<sigma>) \<subseteq> {}
[PROOF STEP]
using orient_lit_vars
[PROOF STATE]
proof (prove)
using this:
vars_of_lit (subst_lit L' \<sigma>) = {}
orient_lit (subst_lit L' \<sigma>) (u \<lhd> \<sigma>) (v \<lhd> \<sigma>) polarity
orient_lit ?L ?t ?s ?p \<Longrightarrow> vars_of ?t \<subseteq> vars_of_lit ?L \<and> vars_of ?s \<subseteq> vars_of_lit ?L

goal (1 subgoal):
 1. vars_of (v \<lhd> \<sigma>) \<subseteq> {}
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
vars_of (v \<lhd> \<sigma>) \<subseteq> {}

goal (1 subgoal):
 1. (subst_lit L' \<sigma>, subst_lit L \<sigma>) \<in> lit_ord
[PROOF STEP]
from assms(5) and \<open>orient_lit ?L ?t ?s pos\<close>
[PROOF STATE]
proof (chain)
picking this:
vars_of_lit (subst_lit L \<sigma>) = {}
orient_lit (subst_lit L \<sigma>) (t \<lhd> \<sigma>) (s \<lhd> \<sigma>) pos
[PROOF STEP]
have "vars_of ?t \<subseteq> {}"
[PROOF STATE]
proof (prove)
using this:
vars_of_lit (subst_lit L \<sigma>) = {}
orient_lit (subst_lit L \<sigma>) (t \<lhd> \<sigma>) (s \<lhd> \<sigma>) pos

goal (1 subgoal):
 1. vars_of (t \<lhd> \<sigma>) \<subseteq> {}
[PROOF STEP]
using orient_lit_vars
[PROOF STATE]
proof (prove)
using this:
vars_of_lit (subst_lit L \<sigma>) = {}
orient_lit (subst_lit L \<sigma>) (t \<lhd> \<sigma>) (s \<lhd> \<sigma>) pos
orient_lit ?L ?t ?s ?p \<Longrightarrow> vars_of ?t \<subseteq> vars_of_lit ?L \<and> vars_of ?s \<subseteq> vars_of_lit ?L

goal (1 subgoal):
 1. vars_of (t \<lhd> \<sigma>) \<subseteq> {}
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
vars_of (t \<lhd> \<sigma>) \<subseteq> {}

goal (1 subgoal):
 1. (subst_lit L' \<sigma>, subst_lit L \<sigma>) \<in> lit_ord
[PROOF STEP]
from assms(5) and \<open>orient_lit ?L ?t ?s pos\<close>
[PROOF STATE]
proof (chain)
picking this:
vars_of_lit (subst_lit L \<sigma>) = {}
orient_lit (subst_lit L \<sigma>) (t \<lhd> \<sigma>) (s \<lhd> \<sigma>) pos
[PROOF STEP]
have "vars_of ?s \<subseteq> {}"
[PROOF STATE]
proof (prove)
using this:
vars_of_lit (subst_lit L \<sigma>) = {}
orient_lit (subst_lit L \<sigma>) (t \<lhd> \<sigma>) (s \<lhd> \<sigma>) pos

goal (1 subgoal):
 1. vars_of (s \<lhd> \<sigma>) \<subseteq> {}
[PROOF STEP]
using orient_lit_vars
[PROOF STATE]
proof (prove)
using this:
vars_of_lit (subst_lit L \<sigma>) = {}
orient_lit (subst_lit L \<sigma>) (t \<lhd> \<sigma>) (s \<lhd> \<sigma>) pos
orient_lit ?L ?t ?s ?p \<Longrightarrow> vars_of ?t \<subseteq> vars_of_lit ?L \<and> vars_of ?s \<subseteq> vars_of_lit ?L

goal (1 subgoal):
 1. vars_of (s \<lhd> \<sigma>) \<subseteq> {}
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
vars_of (s \<lhd> \<sigma>) \<subseteq> {}

goal (1 subgoal):
 1. (subst_lit L' \<sigma>, subst_lit L \<sigma>) \<in> lit_ord
[PROOF STEP]
from assms(1) and \<open>L' \<in> C - { L }\<close>
[PROOF STATE]
proof (chain)
picking this:
maximal_literal (subst_lit L \<sigma>) (subst_cl C \<sigma>)
L' \<in> C - {L}
[PROOF STEP]
have "(?L,?L') \<notin> lit_ord"
[PROOF STATE]
proof (prove)
using this:
maximal_literal (subst_lit L \<sigma>) (subst_cl C \<sigma>)
L' \<in> C - {L}

goal (1 subgoal):
 1. (subst_lit L \<sigma>, subst_lit L' \<sigma>) \<notin> lit_ord
[PROOF STEP]
unfolding maximal_literal_def
[PROOF STATE]
proof (prove)
using this:
\<forall>x. x \<in> subst_cl C \<sigma> \<longrightarrow> (subst_lit L \<sigma>, x) \<notin> lit_ord
L' \<in> C - {L}

goal (1 subgoal):
 1. (subst_lit L \<sigma>, subst_lit L' \<sigma>) \<notin> lit_ord
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(subst_lit L \<sigma>, subst_lit L' \<sigma>) \<notin> lit_ord

goal (1 subgoal):
 1. (subst_lit L' \<sigma>, subst_lit L \<sigma>) \<in> lit_ord
[PROOF STEP]
from this and \<open>orient_lit ?L ?t ?s pos\<close> \<open>orient_lit ?L' ?u ?v polarity\<close> and assms(5) assms(6)
[PROOF STATE]
proof (chain)
picking this:
(subst_lit L \<sigma>, subst_lit L' \<sigma>) \<notin> lit_ord
orient_lit (subst_lit L \<sigma>) (t \<lhd> \<sigma>) (s \<lhd> \<sigma>) pos
orient_lit (subst_lit L' \<sigma>) (u \<lhd> \<sigma>) (v \<lhd> \<sigma>) polarity
vars_of_lit (subst_lit L \<sigma>) = {}
vars_of_lit (subst_lit L' \<sigma>) = {}
[PROOF STEP]
have "(?t,?u) \<notin> trm_ord"
[PROOF STATE]
proof (prove)
using this:
(subst_lit L \<sigma>, subst_lit L' \<sigma>) \<notin> lit_ord
orient_lit (subst_lit L \<sigma>) (t \<lhd> \<sigma>) (s \<lhd> \<sigma>) pos
orient_lit (subst_lit L' \<sigma>) (u \<lhd> \<sigma>) (v \<lhd> \<sigma>) polarity
vars_of_lit (subst_lit L \<sigma>) = {}
vars_of_lit (subst_lit L' \<sigma>) = {}

goal (1 subgoal):
 1. (t \<lhd> \<sigma>, u \<lhd> \<sigma>) \<notin> trm_ord
[PROOF STEP]
using lit_ord_dominating_term
[PROOF STATE]
proof (prove)
using this:
(subst_lit L \<sigma>, subst_lit L' \<sigma>) \<notin> lit_ord
orient_lit (subst_lit L \<sigma>) (t \<lhd> \<sigma>) (s \<lhd> \<sigma>) pos
orient_lit (subst_lit L' \<sigma>) (u \<lhd> \<sigma>) (v \<lhd> \<sigma>) polarity
vars_of_lit (subst_lit L \<sigma>) = {}
vars_of_lit (subst_lit L' \<sigma>) = {}
\<lbrakk>(?s1.0, ?s2.0) \<in> trm_ord \<or> (?s1.0, ?t2.0) \<in> trm_ord; orient_lit ?x1.0 ?s1.0 ?t1.0 ?p1.0; orient_lit ?x2.0 ?s2.0 ?t2.0 ?p2.0; vars_of_lit ?x1.0 = {}; vars_of_lit ?x2.0 = {}\<rbrakk> \<Longrightarrow> (?x1.0, ?x2.0) \<in> lit_ord

goal (1 subgoal):
 1. (t \<lhd> \<sigma>, u \<lhd> \<sigma>) \<notin> trm_ord
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
(t \<lhd> \<sigma>, u \<lhd> \<sigma>) \<notin> trm_ord

goal (1 subgoal):
 1. (subst_lit L' \<sigma>, subst_lit L \<sigma>) \<in> lit_ord
[PROOF STEP]
from this and \<open>vars_of ?t \<subseteq> {}\<close> \<open>vars_of ?u \<subseteq> {}\<close>
[PROOF STATE]
proof (chain)
picking this:
(t \<lhd> \<sigma>, u \<lhd> \<sigma>) \<notin> trm_ord
vars_of (t \<lhd> \<sigma>) \<subseteq> {}
vars_of (u \<lhd> \<sigma>) \<subseteq> {}
[PROOF STEP]
have "?u = ?t \<or> (?u,?t) \<in> trm_ord"
[PROOF STATE]
proof (prove)
using this:
(t \<lhd> \<sigma>, u \<lhd> \<sigma>) \<notin> trm_ord
vars_of (t \<lhd> \<sigma>) \<subseteq> {}
vars_of (u \<lhd> \<sigma>) \<subseteq> {}

goal (1 subgoal):
 1. u \<lhd> \<sigma> = t \<lhd> \<sigma> \<or> (u \<lhd> \<sigma>, t \<lhd> \<sigma>) \<in> trm_ord
[PROOF STEP]
using trm_ord_ground_total
[PROOF STATE]
proof (prove)
using this:
(t \<lhd> \<sigma>, u \<lhd> \<sigma>) \<notin> trm_ord
vars_of (t \<lhd> \<sigma>) \<subseteq> {}
vars_of (u \<lhd> \<sigma>) \<subseteq> {}
\<forall>x y. ground_term x \<longrightarrow> ground_term y \<longrightarrow> x \<noteq> y \<longrightarrow> (x, y) \<in> trm_ord \<or> (y, x) \<in> trm_ord

goal (1 subgoal):
 1. u \<lhd> \<sigma> = t \<lhd> \<sigma> \<or> (u \<lhd> \<sigma>, t \<lhd> \<sigma>) \<in> trm_ord
[PROOF STEP]
unfolding ground_term_def
[PROOF STATE]
proof (prove)
using this:
(t \<lhd> \<sigma>, u \<lhd> \<sigma>) \<notin> trm_ord
vars_of (t \<lhd> \<sigma>) \<subseteq> {}
vars_of (u \<lhd> \<sigma>) \<subseteq> {}
\<forall>x y. vars_of x = {} \<longrightarrow> vars_of y = {} \<longrightarrow> x \<noteq> y \<longrightarrow> (x, y) \<in> trm_ord \<or> (y, x) \<in> trm_ord

goal (1 subgoal):
 1. u \<lhd> \<sigma> = t \<lhd> \<sigma> \<or> (u \<lhd> \<sigma>, t \<lhd> \<sigma>) \<in> trm_ord
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
u \<lhd> \<sigma> = t \<lhd> \<sigma> \<or> (u \<lhd> \<sigma>, t \<lhd> \<sigma>) \<in> trm_ord

goal (1 subgoal):
 1. (subst_lit L' \<sigma>, subst_lit L \<sigma>) \<in> lit_ord
[PROOF STEP]
from \<open>(?u,?v) \<notin> trm_ord\<close> and \<open>vars_of ?u \<subseteq> {}\<close> \<open>vars_of ?v \<subseteq> {}\<close>
[PROOF STATE]
proof (chain)
picking this:
(u \<lhd> \<sigma>, v \<lhd> \<sigma>) \<notin> trm_ord
vars_of (u \<lhd> \<sigma>) \<subseteq> {}
vars_of (v \<lhd> \<sigma>) \<subseteq> {}
[PROOF STEP]
have "?u = ?v \<or> (?v,?u) \<in> trm_ord"
[PROOF STATE]
proof (prove)
using this:
(u \<lhd> \<sigma>, v \<lhd> \<sigma>) \<notin> trm_ord
vars_of (u \<lhd> \<sigma>) \<subseteq> {}
vars_of (v \<lhd> \<sigma>) \<subseteq> {}

goal (1 subgoal):
 1. u \<lhd> \<sigma> = v \<lhd> \<sigma> \<or> (v \<lhd> \<sigma>, u \<lhd> \<sigma>) \<in> trm_ord
[PROOF STEP]
using trm_ord_ground_total
[PROOF STATE]
proof (prove)
using this:
(u \<lhd> \<sigma>, v \<lhd> \<sigma>) \<notin> trm_ord
vars_of (u \<lhd> \<sigma>) \<subseteq> {}
vars_of (v \<lhd> \<sigma>) \<subseteq> {}
\<forall>x y. ground_term x \<longrightarrow> ground_term y \<longrightarrow> x \<noteq> y \<longrightarrow> (x, y) \<in> trm_ord \<or> (y, x) \<in> trm_ord

goal (1 subgoal):
 1. u \<lhd> \<sigma> = v \<lhd> \<sigma> \<or> (v \<lhd> \<sigma>, u \<lhd> \<sigma>) \<in> trm_ord
[PROOF STEP]
unfolding ground_term_def
[PROOF STATE]
proof (prove)
using this:
(u \<lhd> \<sigma>, v \<lhd> \<sigma>) \<notin> trm_ord
vars_of (u \<lhd> \<sigma>) \<subseteq> {}
vars_of (v \<lhd> \<sigma>) \<subseteq> {}
\<forall>x y. vars_of x = {} \<longrightarrow> vars_of y = {} \<longrightarrow> x \<noteq> y \<longrightarrow> (x, y) \<in> trm_ord \<or> (y, x) \<in> trm_ord

goal (1 subgoal):
 1. u \<lhd> \<sigma> = v \<lhd> \<sigma> \<or> (v \<lhd> \<sigma>, u \<lhd> \<sigma>) \<in> trm_ord
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
u \<lhd> \<sigma> = v \<lhd> \<sigma> \<or> (v \<lhd> \<sigma>, u \<lhd> \<sigma>) \<in> trm_ord

goal (1 subgoal):
 1. (subst_lit L' \<sigma>, subst_lit L \<sigma>) \<in> lit_ord
[PROOF STEP]
from \<open>(?t,?s) \<notin> trm_ord\<close> and \<open>vars_of ?t \<subseteq> {}\<close> \<open>vars_of ?s \<subseteq> {}\<close>
[PROOF STATE]
proof (chain)
picking this:
(t \<lhd> \<sigma>, s \<lhd> \<sigma>) \<notin> trm_ord
vars_of (t \<lhd> \<sigma>) \<subseteq> {}
vars_of (s \<lhd> \<sigma>) \<subseteq> {}
[PROOF STEP]
have "?t = ?s \<or> (?s,?t) \<in> trm_ord"
[PROOF STATE]
proof (prove)
using this:
(t \<lhd> \<sigma>, s \<lhd> \<sigma>) \<notin> trm_ord
vars_of (t \<lhd> \<sigma>) \<subseteq> {}
vars_of (s \<lhd> \<sigma>) \<subseteq> {}

goal (1 subgoal):
 1. t \<lhd> \<sigma> = s \<lhd> \<sigma> \<or> (s \<lhd> \<sigma>, t \<lhd> \<sigma>) \<in> trm_ord
[PROOF STEP]
using trm_ord_ground_total
[PROOF STATE]
proof (prove)
using this:
(t \<lhd> \<sigma>, s \<lhd> \<sigma>) \<notin> trm_ord
vars_of (t \<lhd> \<sigma>) \<subseteq> {}
vars_of (s \<lhd> \<sigma>) \<subseteq> {}
\<forall>x y. ground_term x \<longrightarrow> ground_term y \<longrightarrow> x \<noteq> y \<longrightarrow> (x, y) \<in> trm_ord \<or> (y, x) \<in> trm_ord

goal (1 subgoal):
 1. t \<lhd> \<sigma> = s \<lhd> \<sigma> \<or> (s \<lhd> \<sigma>, t \<lhd> \<sigma>) \<in> trm_ord
[PROOF STEP]
unfolding ground_term_def
[PROOF STATE]
proof (prove)
using this:
(t \<lhd> \<sigma>, s \<lhd> \<sigma>) \<notin> trm_ord
vars_of (t \<lhd> \<sigma>) \<subseteq> {}
vars_of (s \<lhd> \<sigma>) \<subseteq> {}
\<forall>x y. vars_of x = {} \<longrightarrow> vars_of y = {} \<longrightarrow> x \<noteq> y \<longrightarrow> (x, y) \<in> trm_ord \<or> (y, x) \<in> trm_ord

goal (1 subgoal):
 1. t \<lhd> \<sigma> = s \<lhd> \<sigma> \<or> (s \<lhd> \<sigma>, t \<lhd> \<sigma>) \<in> trm_ord
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
t \<lhd> \<sigma> = s \<lhd> \<sigma> \<or> (s \<lhd> \<sigma>, t \<lhd> \<sigma>) \<in> trm_ord

goal (1 subgoal):
 1. (subst_lit L' \<sigma>, subst_lit L \<sigma>) \<in> lit_ord
[PROOF STEP]
from \<open>vars_of ?v \<subseteq> {}\<close> \<open>vars_of ?s \<subseteq> {}\<close>
[PROOF STATE]
proof (chain)
picking this:
vars_of (v \<lhd> \<sigma>) \<subseteq> {}
vars_of (s \<lhd> \<sigma>) \<subseteq> {}
[PROOF STEP]
have "?v = ?s \<or> (?v,?s) \<in> trm_ord \<or> (?s,?v) \<in> trm_ord"
[PROOF STATE]
proof (prove)
using this:
vars_of (v \<lhd> \<sigma>) \<subseteq> {}
vars_of (s \<lhd> \<sigma>) \<subseteq> {}

goal (1 subgoal):
 1. v \<lhd> \<sigma> = s \<lhd> \<sigma> \<or> (v \<lhd> \<sigma>, s \<lhd> \<sigma>) \<in> trm_ord \<or> (s \<lhd> \<sigma>, v \<lhd> \<sigma>) \<in> trm_ord
[PROOF STEP]
using trm_ord_ground_total
[PROOF STATE]
proof (prove)
using this:
vars_of (v \<lhd> \<sigma>) \<subseteq> {}
vars_of (s \<lhd> \<sigma>) \<subseteq> {}
\<forall>x y. ground_term x \<longrightarrow> ground_term y \<longrightarrow> x \<noteq> y \<longrightarrow> (x, y) \<in> trm_ord \<or> (y, x) \<in> trm_ord

goal (1 subgoal):
 1. v \<lhd> \<sigma> = s \<lhd> \<sigma> \<or> (v \<lhd> \<sigma>, s \<lhd> \<sigma>) \<in> trm_ord \<or> (s \<lhd> \<sigma>, v \<lhd> \<sigma>) \<in> trm_ord
[PROOF STEP]
unfolding ground_term_def
[PROOF STATE]
proof (prove)
using this:
vars_of (v \<lhd> \<sigma>) \<subseteq> {}
vars_of (s \<lhd> \<sigma>) \<subseteq> {}
\<forall>x y. vars_of x = {} \<longrightarrow> vars_of y = {} \<longrightarrow> x \<noteq> y \<longrightarrow> (x, y) \<in> trm_ord \<or> (y, x) \<in> trm_ord

goal (1 subgoal):
 1. v \<lhd> \<sigma> = s \<lhd> \<sigma> \<or> (v \<lhd> \<sigma>, s \<lhd> \<sigma>) \<in> trm_ord \<or> (s \<lhd> \<sigma>, v \<lhd> \<sigma>) \<in> trm_ord
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
v \<lhd> \<sigma> = s \<lhd> \<sigma> \<or> (v \<lhd> \<sigma>, s \<lhd> \<sigma>) \<in> trm_ord \<or> (s \<lhd> \<sigma>, v \<lhd> \<sigma>) \<in> trm_ord

goal (1 subgoal):
 1. (subst_lit L' \<sigma>, subst_lit L \<sigma>) \<in> lit_ord
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (subst_lit L' \<sigma>, subst_lit L \<sigma>) \<in> lit_ord
[PROOF STEP]
proof (cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> (subst_lit L' \<sigma>, subst_lit L \<sigma>) \<in> lit_ord
 2. \<not> ?P \<Longrightarrow> (subst_lit L' \<sigma>, subst_lit L \<sigma>) \<in> lit_ord
[PROOF STEP]
assume "(?u,?t) \<in> trm_ord"
[PROOF STATE]
proof (state)
this:
(u \<lhd> \<sigma>, t \<lhd> \<sigma>) \<in> trm_ord

goal (2 subgoals):
 1. ?P \<Longrightarrow> (subst_lit L' \<sigma>, subst_lit L \<sigma>) \<in> lit_ord
 2. \<not> ?P \<Longrightarrow> (subst_lit L' \<sigma>, subst_lit L \<sigma>) \<in> lit_ord
[PROOF STEP]
from this and \<open>?u = ?v \<or> (?v,?u) \<in> trm_ord\<close>
[PROOF STATE]
proof (chain)
picking this:
(u \<lhd> \<sigma>, t \<lhd> \<sigma>) \<in> trm_ord
u \<lhd> \<sigma> = v \<lhd> \<sigma> \<or> (v \<lhd> \<sigma>, u \<lhd> \<sigma>) \<in> trm_ord
[PROOF STEP]
have "(?v,?t) \<in> trm_ord"
[PROOF STATE]
proof (prove)
using this:
(u \<lhd> \<sigma>, t \<lhd> \<sigma>) \<in> trm_ord
u \<lhd> \<sigma> = v \<lhd> \<sigma> \<or> (v \<lhd> \<sigma>, u \<lhd> \<sigma>) \<in> trm_ord

goal (1 subgoal):
 1. (v \<lhd> \<sigma>, t \<lhd> \<sigma>) \<in> trm_ord
[PROOF STEP]
using trm_ord_trans
[PROOF STATE]
proof (prove)
using this:
(u \<lhd> \<sigma>, t \<lhd> \<sigma>) \<in> trm_ord
u \<lhd> \<sigma> = v \<lhd> \<sigma> \<or> (v \<lhd> \<sigma>, u \<lhd> \<sigma>) \<in> trm_ord
trans trm_ord

goal (1 subgoal):
 1. (v \<lhd> \<sigma>, t \<lhd> \<sigma>) \<in> trm_ord
[PROOF STEP]
unfolding trans_def
[PROOF STATE]
proof (prove)
using this:
(u \<lhd> \<sigma>, t \<lhd> \<sigma>) \<in> trm_ord
u \<lhd> \<sigma> = v \<lhd> \<sigma> \<or> (v \<lhd> \<sigma>, u \<lhd> \<sigma>) \<in> trm_ord
\<forall>x y z. (x, y) \<in> trm_ord \<longrightarrow> (y, z) \<in> trm_ord \<longrightarrow> (x, z) \<in> trm_ord

goal (1 subgoal):
 1. (v \<lhd> \<sigma>, t \<lhd> \<sigma>) \<in> trm_ord
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(v \<lhd> \<sigma>, t \<lhd> \<sigma>) \<in> trm_ord

goal (2 subgoals):
 1. ?P \<Longrightarrow> (subst_lit L' \<sigma>, subst_lit L \<sigma>) \<in> lit_ord
 2. \<not> ?P \<Longrightarrow> (subst_lit L' \<sigma>, subst_lit L \<sigma>) \<in> lit_ord
[PROOF STEP]
from this and \<open>(?u,?t) \<in> trm_ord\<close> and \<open>orient_lit ?L ?t ?s pos\<close> \<open>orient_lit ?L' ?u ?v polarity\<close>
      assms(5) assms(6)
[PROOF STATE]
proof (chain)
picking this:
(v \<lhd> \<sigma>, t \<lhd> \<sigma>) \<in> trm_ord
(u \<lhd> \<sigma>, t \<lhd> \<sigma>) \<in> trm_ord
orient_lit (subst_lit L \<sigma>) (t \<lhd> \<sigma>) (s \<lhd> \<sigma>) pos
orient_lit (subst_lit L' \<sigma>) (u \<lhd> \<sigma>) (v \<lhd> \<sigma>) polarity
vars_of_lit (subst_lit L \<sigma>) = {}
vars_of_lit (subst_lit L' \<sigma>) = {}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(v \<lhd> \<sigma>, t \<lhd> \<sigma>) \<in> trm_ord
(u \<lhd> \<sigma>, t \<lhd> \<sigma>) \<in> trm_ord
orient_lit (subst_lit L \<sigma>) (t \<lhd> \<sigma>) (s \<lhd> \<sigma>) pos
orient_lit (subst_lit L' \<sigma>) (u \<lhd> \<sigma>) (v \<lhd> \<sigma>) polarity
vars_of_lit (subst_lit L \<sigma>) = {}
vars_of_lit (subst_lit L' \<sigma>) = {}

goal (1 subgoal):
 1. (subst_lit L' \<sigma>, subst_lit L \<sigma>) \<in> lit_ord
[PROOF STEP]
using  lit_ord_dominating_term
[PROOF STATE]
proof (prove)
using this:
(v \<lhd> \<sigma>, t \<lhd> \<sigma>) \<in> trm_ord
(u \<lhd> \<sigma>, t \<lhd> \<sigma>) \<in> trm_ord
orient_lit (subst_lit L \<sigma>) (t \<lhd> \<sigma>) (s \<lhd> \<sigma>) pos
orient_lit (subst_lit L' \<sigma>) (u \<lhd> \<sigma>) (v \<lhd> \<sigma>) polarity
vars_of_lit (subst_lit L \<sigma>) = {}
vars_of_lit (subst_lit L' \<sigma>) = {}
\<lbrakk>(?s1.0, ?s2.0) \<in> trm_ord \<or> (?s1.0, ?t2.0) \<in> trm_ord; orient_lit ?x1.0 ?s1.0 ?t1.0 ?p1.0; orient_lit ?x2.0 ?s2.0 ?t2.0 ?p2.0; vars_of_lit ?x1.0 = {}; vars_of_lit ?x2.0 = {}\<rbrakk> \<Longrightarrow> (?x1.0, ?x2.0) \<in> lit_ord

goal (1 subgoal):
 1. (subst_lit L' \<sigma>, subst_lit L \<sigma>) \<in> lit_ord
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
(subst_lit L' \<sigma>, subst_lit L \<sigma>) \<in> lit_ord

goal (1 subgoal):
 1. (u \<lhd> \<sigma>, t \<lhd> \<sigma>) \<notin> trm_ord \<Longrightarrow> (subst_lit L' \<sigma>, subst_lit L \<sigma>) \<in> lit_ord
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (u \<lhd> \<sigma>, t \<lhd> \<sigma>) \<notin> trm_ord \<Longrightarrow> (subst_lit L' \<sigma>, subst_lit L \<sigma>) \<in> lit_ord
[PROOF STEP]
assume "(?u,?t) \<notin> trm_ord"
[PROOF STATE]
proof (state)
this:
(u \<lhd> \<sigma>, t \<lhd> \<sigma>) \<notin> trm_ord

goal (1 subgoal):
 1. (u \<lhd> \<sigma>, t \<lhd> \<sigma>) \<notin> trm_ord \<Longrightarrow> (subst_lit L' \<sigma>, subst_lit L \<sigma>) \<in> lit_ord
[PROOF STEP]
from this and \<open>?u = ?t \<or> (?u,?t) \<in> trm_ord\<close>
[PROOF STATE]
proof (chain)
picking this:
(u \<lhd> \<sigma>, t \<lhd> \<sigma>) \<notin> trm_ord
u \<lhd> \<sigma> = t \<lhd> \<sigma> \<or> (u \<lhd> \<sigma>, t \<lhd> \<sigma>) \<in> trm_ord
[PROOF STEP]
have "?u = ?t"
[PROOF STATE]
proof (prove)
using this:
(u \<lhd> \<sigma>, t \<lhd> \<sigma>) \<notin> trm_ord
u \<lhd> \<sigma> = t \<lhd> \<sigma> \<or> (u \<lhd> \<sigma>, t \<lhd> \<sigma>) \<in> trm_ord

goal (1 subgoal):
 1. u \<lhd> \<sigma> = t \<lhd> \<sigma>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
u \<lhd> \<sigma> = t \<lhd> \<sigma>

goal (1 subgoal):
 1. (u \<lhd> \<sigma>, t \<lhd> \<sigma>) \<notin> trm_ord \<Longrightarrow> (subst_lit L' \<sigma>, subst_lit L \<sigma>) \<in> lit_ord
[PROOF STEP]
have "polarity = pos"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. polarity = pos
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. polarity \<noteq> pos \<Longrightarrow> False
[PROOF STEP]
assume "polarity \<noteq> pos"
[PROOF STATE]
proof (state)
this:
polarity \<noteq> pos

goal (1 subgoal):
 1. polarity \<noteq> pos \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
polarity \<noteq> pos
[PROOF STEP]
have "polarity = neg"
[PROOF STATE]
proof (prove)
using this:
polarity \<noteq> pos

goal (1 subgoal):
 1. polarity = neg
[PROOF STEP]
using sign.exhaust
[PROOF STATE]
proof (prove)
using this:
polarity \<noteq> pos
\<lbrakk>?y = pos \<Longrightarrow> ?P; ?y = neg \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

goal (1 subgoal):
 1. polarity = neg
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
polarity = neg

goal (1 subgoal):
 1. polarity \<noteq> pos \<Longrightarrow> False
[PROOF STEP]
from this and \<open>?u = ?t\<close> and  \<open>orient_lit ?L ?t ?s pos\<close>
        \<open>orient_lit ?L' ?u ?v polarity\<close> assms(5) assms(6)
[PROOF STATE]
proof (chain)
picking this:
polarity = neg
u \<lhd> \<sigma> = t \<lhd> \<sigma>
orient_lit (subst_lit L \<sigma>) (t \<lhd> \<sigma>) (s \<lhd> \<sigma>) pos
orient_lit (subst_lit L' \<sigma>) (u \<lhd> \<sigma>) (v \<lhd> \<sigma>) polarity
vars_of_lit (subst_lit L \<sigma>) = {}
vars_of_lit (subst_lit L' \<sigma>) = {}
[PROOF STEP]
have "(?L,?L') \<in> lit_ord"
[PROOF STATE]
proof (prove)
using this:
polarity = neg
u \<lhd> \<sigma> = t \<lhd> \<sigma>
orient_lit (subst_lit L \<sigma>) (t \<lhd> \<sigma>) (s \<lhd> \<sigma>) pos
orient_lit (subst_lit L' \<sigma>) (u \<lhd> \<sigma>) (v \<lhd> \<sigma>) polarity
vars_of_lit (subst_lit L \<sigma>) = {}
vars_of_lit (subst_lit L' \<sigma>) = {}

goal (1 subgoal):
 1. (subst_lit L \<sigma>, subst_lit L' \<sigma>) \<in> lit_ord
[PROOF STEP]
using lit_ord_neg_lit_lhs
[PROOF STATE]
proof (prove)
using this:
polarity = neg
u \<lhd> \<sigma> = t \<lhd> \<sigma>
orient_lit (subst_lit L \<sigma>) (t \<lhd> \<sigma>) (s \<lhd> \<sigma>) pos
orient_lit (subst_lit L' \<sigma>) (u \<lhd> \<sigma>) (v \<lhd> \<sigma>) polarity
vars_of_lit (subst_lit L \<sigma>) = {}
vars_of_lit (subst_lit L' \<sigma>) = {}
\<lbrakk>orient_lit ?x1.0 ?s ?t1.0 pos; orient_lit ?x2.0 ?s ?t2.0 neg; vars_of_lit ?x1.0 = {}; vars_of_lit ?x2.0 = {}\<rbrakk> \<Longrightarrow> (?x1.0, ?x2.0) \<in> lit_ord

goal (1 subgoal):
 1. (subst_lit L \<sigma>, subst_lit L' \<sigma>) \<in> lit_ord
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(subst_lit L \<sigma>, subst_lit L' \<sigma>) \<in> lit_ord

goal (1 subgoal):
 1. polarity \<noteq> pos \<Longrightarrow> False
[PROOF STEP]
from this and \<open>(?L,?L') \<notin> lit_ord\<close>
[PROOF STATE]
proof (chain)
picking this:
(subst_lit L \<sigma>, subst_lit L' \<sigma>) \<in> lit_ord
(subst_lit L \<sigma>, subst_lit L' \<sigma>) \<notin> lit_ord
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
(subst_lit L \<sigma>, subst_lit L' \<sigma>) \<in> lit_ord
(subst_lit L \<sigma>, subst_lit L' \<sigma>) \<notin> lit_ord

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
polarity = pos

goal (1 subgoal):
 1. (u \<lhd> \<sigma>, t \<lhd> \<sigma>) \<notin> trm_ord \<Longrightarrow> (subst_lit L' \<sigma>, subst_lit L \<sigma>) \<in> lit_ord
[PROOF STEP]
have "?v \<noteq> ?s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v \<lhd> \<sigma> \<noteq> s \<lhd> \<sigma>
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. v \<lhd> \<sigma> = s \<lhd> \<sigma> \<Longrightarrow> False
[PROOF STEP]
assume "?v = ?s"
[PROOF STATE]
proof (state)
this:
v \<lhd> \<sigma> = s \<lhd> \<sigma>

goal (1 subgoal):
 1. v \<lhd> \<sigma> = s \<lhd> \<sigma> \<Longrightarrow> False
[PROOF STEP]
from this assms(7)
[PROOF STATE]
proof (chain)
picking this:
v \<lhd> \<sigma> = s \<lhd> \<sigma>
fo_interpretation I
[PROOF STEP]
have "I ?s ?v"
[PROOF STATE]
proof (prove)
using this:
v \<lhd> \<sigma> = s \<lhd> \<sigma>
fo_interpretation I

goal (1 subgoal):
 1. I (s \<lhd> \<sigma>) (v \<lhd> \<sigma>)
[PROOF STEP]
unfolding fo_interpretation_def congruence_def
        equivalence_relation_def reflexive_def
[PROOF STATE]
proof (prove)
using this:
v \<lhd> \<sigma> = s \<lhd> \<sigma>
((\<forall>y. I y y) \<and> symmetric I \<and> transitive I) \<and> compatible_with_structure I

goal (1 subgoal):
 1. I (s \<lhd> \<sigma>) (v \<lhd> \<sigma>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
I (s \<lhd> \<sigma>) (v \<lhd> \<sigma>)

goal (1 subgoal):
 1. v \<lhd> \<sigma> = s \<lhd> \<sigma> \<Longrightarrow> False
[PROOF STEP]
from this and \<open>orient_lit_inst L' u v polarity \<sigma>\<close> \<open>polarity = pos\<close> \<open>?u = ?t\<close>
        and assms(3)
[PROOF STATE]
proof (chain)
picking this:
I (s \<lhd> \<sigma>) (v \<lhd> \<sigma>)
orient_lit_inst L' u v polarity \<sigma>
polarity = pos
u \<lhd> \<sigma> = t \<lhd> \<sigma>
L' \<in> C - {L}
[PROOF STEP]
have "equivalent_eq_exists t s C I \<sigma> L"
[PROOF STATE]
proof (prove)
using this:
I (s \<lhd> \<sigma>) (v \<lhd> \<sigma>)
orient_lit_inst L' u v polarity \<sigma>
polarity = pos
u \<lhd> \<sigma> = t \<lhd> \<sigma>
L' \<in> C - {L}

goal (1 subgoal):
 1. equivalent_eq_exists t s C I \<sigma> L
[PROOF STEP]
unfolding equivalent_eq_exists_def
[PROOF STATE]
proof (prove)
using this:
I (s \<lhd> \<sigma>) (v \<lhd> \<sigma>)
orient_lit_inst L' u v polarity \<sigma>
polarity = pos
u \<lhd> \<sigma> = t \<lhd> \<sigma>
L' \<in> C - {L}

goal (1 subgoal):
 1. \<exists>L\<in>C - {L}. \<exists>u v. orient_lit_inst L u v pos \<sigma> \<and> t \<lhd> \<sigma> = u \<lhd> \<sigma> \<and> I (s \<lhd> \<sigma>) (v \<lhd> \<sigma>)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
equivalent_eq_exists t s C I \<sigma> L

goal (1 subgoal):
 1. v \<lhd> \<sigma> = s \<lhd> \<sigma> \<Longrightarrow> False
[PROOF STEP]
from this and assms(4)
[PROOF STATE]
proof (chain)
picking this:
equivalent_eq_exists t s C I \<sigma> L
\<not> equivalent_eq_exists t s C I \<sigma> L
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
equivalent_eq_exists t s C I \<sigma> L
\<not> equivalent_eq_exists t s C I \<sigma> L

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
v \<lhd> \<sigma> \<noteq> s \<lhd> \<sigma>

goal (1 subgoal):
 1. (u \<lhd> \<sigma>, t \<lhd> \<sigma>) \<notin> trm_ord \<Longrightarrow> (subst_lit L' \<sigma>, subst_lit L \<sigma>) \<in> lit_ord
[PROOF STEP]
have "(?s,?v) \<notin> trm_ord"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (s \<lhd> \<sigma>, v \<lhd> \<sigma>) \<notin> trm_ord
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (s \<lhd> \<sigma>, v \<lhd> \<sigma>) \<in> trm_ord \<Longrightarrow> False
[PROOF STEP]
assume "(?s,?v) \<in> trm_ord"
[PROOF STATE]
proof (state)
this:
(s \<lhd> \<sigma>, v \<lhd> \<sigma>) \<in> trm_ord

goal (1 subgoal):
 1. (s \<lhd> \<sigma>, v \<lhd> \<sigma>) \<in> trm_ord \<Longrightarrow> False
[PROOF STEP]
from this and \<open>?u = ?t\<close> and  \<open>orient_lit ?L ?t ?s pos\<close> \<open>orient_lit ?L' ?u ?v polarity\<close>
        and \<open>polarity=pos\<close> assms(5) assms(6)
[PROOF STATE]
proof (chain)
picking this:
(s \<lhd> \<sigma>, v \<lhd> \<sigma>) \<in> trm_ord
u \<lhd> \<sigma> = t \<lhd> \<sigma>
orient_lit (subst_lit L \<sigma>) (t \<lhd> \<sigma>) (s \<lhd> \<sigma>) pos
orient_lit (subst_lit L' \<sigma>) (u \<lhd> \<sigma>) (v \<lhd> \<sigma>) polarity
polarity = pos
vars_of_lit (subst_lit L \<sigma>) = {}
vars_of_lit (subst_lit L' \<sigma>) = {}
[PROOF STEP]
have "(?L,?L') \<in> lit_ord"
[PROOF STATE]
proof (prove)
using this:
(s \<lhd> \<sigma>, v \<lhd> \<sigma>) \<in> trm_ord
u \<lhd> \<sigma> = t \<lhd> \<sigma>
orient_lit (subst_lit L \<sigma>) (t \<lhd> \<sigma>) (s \<lhd> \<sigma>) pos
orient_lit (subst_lit L' \<sigma>) (u \<lhd> \<sigma>) (v \<lhd> \<sigma>) polarity
polarity = pos
vars_of_lit (subst_lit L \<sigma>) = {}
vars_of_lit (subst_lit L' \<sigma>) = {}

goal (1 subgoal):
 1. (subst_lit L \<sigma>, subst_lit L' \<sigma>) \<in> lit_ord
[PROOF STEP]
using lit_ord_rhs
[PROOF STATE]
proof (prove)
using this:
(s \<lhd> \<sigma>, v \<lhd> \<sigma>) \<in> trm_ord
u \<lhd> \<sigma> = t \<lhd> \<sigma>
orient_lit (subst_lit L \<sigma>) (t \<lhd> \<sigma>) (s \<lhd> \<sigma>) pos
orient_lit (subst_lit L' \<sigma>) (u \<lhd> \<sigma>) (v \<lhd> \<sigma>) polarity
polarity = pos
vars_of_lit (subst_lit L \<sigma>) = {}
vars_of_lit (subst_lit L' \<sigma>) = {}
\<lbrakk>(?t1.0, ?t2.0) \<in> trm_ord; orient_lit ?x1.0 ?s ?t1.0 ?p; orient_lit ?x2.0 ?s ?t2.0 ?p; vars_of_lit ?x1.0 = {}; vars_of_lit ?x2.0 = {}\<rbrakk> \<Longrightarrow> (?x1.0, ?x2.0) \<in> lit_ord

goal (1 subgoal):
 1. (subst_lit L \<sigma>, subst_lit L' \<sigma>) \<in> lit_ord
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(subst_lit L \<sigma>, subst_lit L' \<sigma>) \<in> lit_ord

goal (1 subgoal):
 1. (s \<lhd> \<sigma>, v \<lhd> \<sigma>) \<in> trm_ord \<Longrightarrow> False
[PROOF STEP]
from this and \<open>(?L,?L') \<notin> lit_ord\<close>
[PROOF STATE]
proof (chain)
picking this:
(subst_lit L \<sigma>, subst_lit L' \<sigma>) \<in> lit_ord
(subst_lit L \<sigma>, subst_lit L' \<sigma>) \<notin> lit_ord
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
(subst_lit L \<sigma>, subst_lit L' \<sigma>) \<in> lit_ord
(subst_lit L \<sigma>, subst_lit L' \<sigma>) \<notin> lit_ord

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(s \<lhd> \<sigma>, v \<lhd> \<sigma>) \<notin> trm_ord

goal (1 subgoal):
 1. (u \<lhd> \<sigma>, t \<lhd> \<sigma>) \<notin> trm_ord \<Longrightarrow> (subst_lit L' \<sigma>, subst_lit L \<sigma>) \<in> lit_ord
[PROOF STEP]
from this and \<open>?v \<noteq> ?s\<close> and \<open>?v = ?s \<or> (?v,?s) \<in> trm_ord \<or> (?s,?v) \<in> trm_ord\<close>
[PROOF STATE]
proof (chain)
picking this:
(s \<lhd> \<sigma>, v \<lhd> \<sigma>) \<notin> trm_ord
v \<lhd> \<sigma> \<noteq> s \<lhd> \<sigma>
v \<lhd> \<sigma> = s \<lhd> \<sigma> \<or> (v \<lhd> \<sigma>, s \<lhd> \<sigma>) \<in> trm_ord \<or> (s \<lhd> \<sigma>, v \<lhd> \<sigma>) \<in> trm_ord
[PROOF STEP]
have "(?v,?s) \<in> trm_ord"
[PROOF STATE]
proof (prove)
using this:
(s \<lhd> \<sigma>, v \<lhd> \<sigma>) \<notin> trm_ord
v \<lhd> \<sigma> \<noteq> s \<lhd> \<sigma>
v \<lhd> \<sigma> = s \<lhd> \<sigma> \<or> (v \<lhd> \<sigma>, s \<lhd> \<sigma>) \<in> trm_ord \<or> (s \<lhd> \<sigma>, v \<lhd> \<sigma>) \<in> trm_ord

goal (1 subgoal):
 1. (v \<lhd> \<sigma>, s \<lhd> \<sigma>) \<in> trm_ord
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
(v \<lhd> \<sigma>, s \<lhd> \<sigma>) \<in> trm_ord

goal (1 subgoal):
 1. (u \<lhd> \<sigma>, t \<lhd> \<sigma>) \<notin> trm_ord \<Longrightarrow> (subst_lit L' \<sigma>, subst_lit L \<sigma>) \<in> lit_ord
[PROOF STEP]
from this and \<open>?u = ?t\<close> and  \<open>orient_lit ?L ?t ?s pos\<close> \<open>orient_lit ?L' ?u ?v polarity\<close>
        and \<open>polarity=pos\<close> assms(5) assms(6)
[PROOF STATE]
proof (chain)
picking this:
(v \<lhd> \<sigma>, s \<lhd> \<sigma>) \<in> trm_ord
u \<lhd> \<sigma> = t \<lhd> \<sigma>
orient_lit (subst_lit L \<sigma>) (t \<lhd> \<sigma>) (s \<lhd> \<sigma>) pos
orient_lit (subst_lit L' \<sigma>) (u \<lhd> \<sigma>) (v \<lhd> \<sigma>) polarity
polarity = pos
vars_of_lit (subst_lit L \<sigma>) = {}
vars_of_lit (subst_lit L' \<sigma>) = {}
[PROOF STEP]
show "(?L',?L) \<in> lit_ord"
[PROOF STATE]
proof (prove)
using this:
(v \<lhd> \<sigma>, s \<lhd> \<sigma>) \<in> trm_ord
u \<lhd> \<sigma> = t \<lhd> \<sigma>
orient_lit (subst_lit L \<sigma>) (t \<lhd> \<sigma>) (s \<lhd> \<sigma>) pos
orient_lit (subst_lit L' \<sigma>) (u \<lhd> \<sigma>) (v \<lhd> \<sigma>) polarity
polarity = pos
vars_of_lit (subst_lit L \<sigma>) = {}
vars_of_lit (subst_lit L' \<sigma>) = {}

goal (1 subgoal):
 1. (subst_lit L' \<sigma>, subst_lit L \<sigma>) \<in> lit_ord
[PROOF STEP]
using lit_ord_rhs
[PROOF STATE]
proof (prove)
using this:
(v \<lhd> \<sigma>, s \<lhd> \<sigma>) \<in> trm_ord
u \<lhd> \<sigma> = t \<lhd> \<sigma>
orient_lit (subst_lit L \<sigma>) (t \<lhd> \<sigma>) (s \<lhd> \<sigma>) pos
orient_lit (subst_lit L' \<sigma>) (u \<lhd> \<sigma>) (v \<lhd> \<sigma>) polarity
polarity = pos
vars_of_lit (subst_lit L \<sigma>) = {}
vars_of_lit (subst_lit L' \<sigma>) = {}
\<lbrakk>(?t1.0, ?t2.0) \<in> trm_ord; orient_lit ?x1.0 ?s ?t1.0 ?p; orient_lit ?x2.0 ?s ?t2.0 ?p; vars_of_lit ?x1.0 = {}; vars_of_lit ?x2.0 = {}\<rbrakk> \<Longrightarrow> (?x1.0, ?x2.0) \<in> lit_ord

goal (1 subgoal):
 1. (subst_lit L' \<sigma>, subst_lit L \<sigma>) \<in> lit_ord
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(subst_lit L' \<sigma>, subst_lit L \<sigma>) \<in> lit_ord

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(subst_lit L' \<sigma>, subst_lit L \<sigma>) \<in> lit_ord

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma if_all_smaller_are_false_then_cl_not_valid:
  assumes "(smaller_lits_are_false (subst t \<sigma>) (subst_cl C \<sigma>) S)"
  assumes "(fo_interpretation (same_values (\<lambda>t. (trm_rep t S))))"
  assumes "orient_lit_inst L1 t s pos \<sigma>"
  assumes "maximal_literal (subst_lit L1 \<sigma>) (subst_cl C \<sigma>)"
  assumes "ground_clause (subst_cl C \<sigma>)"
  assumes "(subst_lit L1 \<sigma>) \<in> (subst_cl C \<sigma>)"
  assumes "\<not>equivalent_eq_exists t s C (same_values (\<lambda>t. (trm_rep t S))) \<sigma> L1"
  assumes "trm_rep (subst t \<sigma>) S = trm_rep (subst s \<sigma>) S"
  shows "(\<not> validate_ground_clause (same_values (\<lambda>t. (trm_rep t S))) (subst_cl ( C - { L1 } ) \<sigma>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> validate_ground_clause (same_values (\<lambda>t. trm_rep t S)) (subst_cl (C - {L1}) \<sigma>)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. validate_ground_clause (same_values (\<lambda>t. trm_rep t S)) (subst_cl (C - {L1}) \<sigma>) \<Longrightarrow> False
[PROOF STEP]
let ?I = "(same_values (\<lambda>t. (trm_rep t S)))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. validate_ground_clause (same_values (\<lambda>t. trm_rep t S)) (subst_cl (C - {L1}) \<sigma>) \<Longrightarrow> False
[PROOF STEP]
assume "validate_ground_clause ?I (subst_cl ( C - { L1 } ) \<sigma>)"
[PROOF STATE]
proof (state)
this:
validate_ground_clause (same_values (\<lambda>t. trm_rep t S)) (subst_cl (C - {L1}) \<sigma>)

goal (1 subgoal):
 1. validate_ground_clause (same_values (\<lambda>t. trm_rep t S)) (subst_cl (C - {L1}) \<sigma>) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
validate_ground_clause (same_values (\<lambda>t. trm_rep t S)) (subst_cl (C - {L1}) \<sigma>)
[PROOF STEP]
obtain L where "L \<in> (subst_cl ( C - { L1 } ) \<sigma>)" and "validate_ground_lit ?I L"
[PROOF STATE]
proof (prove)
using this:
validate_ground_clause (same_values (\<lambda>t. trm_rep t S)) (subst_cl (C - {L1}) \<sigma>)

goal (1 subgoal):
 1. (\<And>L. \<lbrakk>L \<in> subst_cl (C - {L1}) \<sigma>; validate_ground_lit (same_values (\<lambda>t. trm_rep t S)) L\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using validate_ground_clause.simps [of ?I "(subst_cl ( C - { L1 } ) \<sigma>)"]
[PROOF STATE]
proof (prove)
using this:
validate_ground_clause (same_values (\<lambda>t. trm_rep t S)) (subst_cl (C - {L1}) \<sigma>)
validate_ground_clause (same_values (\<lambda>t. trm_rep t S)) (subst_cl (C - {L1}) \<sigma>) = (\<exists>L. L \<in> subst_cl (C - {L1}) \<sigma> \<and> validate_ground_lit (same_values (\<lambda>t. trm_rep t S)) L)

goal (1 subgoal):
 1. (\<And>L. \<lbrakk>L \<in> subst_cl (C - {L1}) \<sigma>; validate_ground_lit (same_values (\<lambda>t. trm_rep t S)) L\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
L \<in> subst_cl (C - {L1}) \<sigma>
validate_ground_lit (same_values (\<lambda>t. trm_rep t S)) L

goal (1 subgoal):
 1. validate_ground_clause (same_values (\<lambda>t. trm_rep t S)) (subst_cl (C - {L1}) \<sigma>) \<Longrightarrow> False
[PROOF STEP]
from \<open>L \<in> (subst_cl ( C - { L1 } ) \<sigma>)\<close>
[PROOF STATE]
proof (chain)
picking this:
L \<in> subst_cl (C - {L1}) \<sigma>
[PROOF STEP]
obtain L' where "L' \<in> C - { L1 }" and
    "L = (subst_lit L' \<sigma>)"
[PROOF STATE]
proof (prove)
using this:
L \<in> subst_cl (C - {L1}) \<sigma>

goal (1 subgoal):
 1. (\<And>L'. \<lbrakk>L' \<in> C - {L1}; L = subst_lit L' \<sigma>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
L' \<in> C - {L1}
L = subst_lit L' \<sigma>

goal (1 subgoal):
 1. validate_ground_clause (same_values (\<lambda>t. trm_rep t S)) (subst_cl (C - {L1}) \<sigma>) \<Longrightarrow> False
[PROOF STEP]
from \<open>L' \<in> C - { L1 }\<close>  and \<open>L = (subst_lit L' \<sigma>)\<close>
[PROOF STATE]
proof (chain)
picking this:
L' \<in> C - {L1}
L = subst_lit L' \<sigma>
[PROOF STEP]
have "L \<in>(subst_cl C \<sigma>)"
[PROOF STATE]
proof (prove)
using this:
L' \<in> C - {L1}
L = subst_lit L' \<sigma>

goal (1 subgoal):
 1. L \<in> subst_cl C \<sigma>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
L \<in> subst_cl C \<sigma>

goal (1 subgoal):
 1. validate_ground_clause (same_values (\<lambda>t. trm_rep t S)) (subst_cl (C - {L1}) \<sigma>) \<Longrightarrow> False
[PROOF STEP]
from \<open>L \<in>(subst_cl C \<sigma>)\<close> and assms(5)
[PROOF STATE]
proof (chain)
picking this:
L \<in> subst_cl C \<sigma>
ground_clause (subst_cl C \<sigma>)
[PROOF STEP]
have "vars_of_lit L = {}"
[PROOF STATE]
proof (prove)
using this:
L \<in> subst_cl C \<sigma>
ground_clause (subst_cl C \<sigma>)

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

goal (1 subgoal):
 1. validate_ground_clause (same_values (\<lambda>t. trm_rep t S)) (subst_cl (C - {L1}) \<sigma>) \<Longrightarrow> False
[PROOF STEP]
from assms(6) and assms(5)
[PROOF STATE]
proof (chain)
picking this:
subst_lit L1 \<sigma> \<in> subst_cl C \<sigma>
ground_clause (subst_cl C \<sigma>)
[PROOF STEP]
have "vars_of_lit (subst_lit L1 \<sigma>) = {}"
[PROOF STATE]
proof (prove)
using this:
subst_lit L1 \<sigma> \<in> subst_cl C \<sigma>
ground_clause (subst_cl C \<sigma>)

goal (1 subgoal):
 1. vars_of_lit (subst_lit L1 \<sigma>) = {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vars_of_lit (subst_lit L1 \<sigma>) = {}

goal (1 subgoal):
 1. validate_ground_clause (same_values (\<lambda>t. trm_rep t S)) (subst_cl (C - {L1}) \<sigma>) \<Longrightarrow> False
[PROOF STEP]
obtain u v polarity where o: "orient_lit_inst L' u v polarity \<sigma>"
  and "((subst u \<sigma>), (subst v \<sigma>)) \<notin> trm_ord"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>u v polarity. \<lbrakk>orient_lit_inst L' u v polarity \<sigma>; (u \<lhd> \<sigma>, v \<lhd> \<sigma>) \<notin> trm_ord\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding orient_lit_inst_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>u v polarity. \<lbrakk>(L' = Pos (Eq u v) \<or> L' = Pos (Eq v u)) \<and> (u \<lhd> \<sigma>, v \<lhd> \<sigma>) \<notin> trm_ord \<and> polarity = pos \<or> (L' = Neg (Eq u v) \<or> L' = Neg (Eq v u)) \<and> (u \<lhd> \<sigma>, v \<lhd> \<sigma>) \<notin> trm_ord \<and> polarity = neg; (u \<lhd> \<sigma>, v \<lhd> \<sigma>) \<notin> trm_ord\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using literal.exhaust equation.exhaust
      trm_ord_trans trm_ord_irrefl
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>x1. ?y = Pos x1 \<Longrightarrow> ?P; \<And>x2. ?y = Neg x2 \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
(\<And>x1 x2. ?y = Eq x1 x2 \<Longrightarrow> ?P) \<Longrightarrow> ?P
trans trm_ord
irrefl trm_ord

goal (1 subgoal):
 1. (\<And>u v polarity. \<lbrakk>(L' = Pos (Eq u v) \<or> L' = Pos (Eq v u)) \<and> (u \<lhd> \<sigma>, v \<lhd> \<sigma>) \<notin> trm_ord \<and> polarity = pos \<or> (L' = Neg (Eq u v) \<or> L' = Neg (Eq v u)) \<and> (u \<lhd> \<sigma>, v \<lhd> \<sigma>) \<notin> trm_ord \<and> polarity = neg; (u \<lhd> \<sigma>, v \<lhd> \<sigma>) \<notin> trm_ord\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding trans_def irrefl_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>x1. ?y = Pos x1 \<Longrightarrow> ?P; \<And>x2. ?y = Neg x2 \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
(\<And>x1 x2. ?y = Eq x1 x2 \<Longrightarrow> ?P) \<Longrightarrow> ?P
\<forall>x y z. (x, y) \<in> trm_ord \<longrightarrow> (y, z) \<in> trm_ord \<longrightarrow> (x, z) \<in> trm_ord
\<forall>a. (a, a) \<notin> trm_ord

goal (1 subgoal):
 1. (\<And>u v polarity. \<lbrakk>(L' = Pos (Eq u v) \<or> L' = Pos (Eq v u)) \<and> (u \<lhd> \<sigma>, v \<lhd> \<sigma>) \<notin> trm_ord \<and> polarity = pos \<or> (L' = Neg (Eq u v) \<or> L' = Neg (Eq v u)) \<and> (u \<lhd> \<sigma>, v \<lhd> \<sigma>) \<notin> trm_ord \<and> polarity = neg; (u \<lhd> \<sigma>, v \<lhd> \<sigma>) \<notin> trm_ord\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
orient_lit_inst L' u v polarity \<sigma>
(u \<lhd> \<sigma>, v \<lhd> \<sigma>) \<notin> trm_ord

goal (1 subgoal):
 1. validate_ground_clause (same_values (\<lambda>t. trm_rep t S)) (subst_cl (C - {L1}) \<sigma>) \<Longrightarrow> False
[PROOF STEP]
from o and \<open>L = (subst_lit L' \<sigma>)\<close>
[PROOF STATE]
proof (chain)
picking this:
orient_lit_inst L' u v polarity \<sigma>
L = subst_lit L' \<sigma>
[PROOF STEP]
have o' : "orient_lit L (subst u \<sigma>)  (subst v \<sigma>) polarity"
[PROOF STATE]
proof (prove)
using this:
orient_lit_inst L' u v polarity \<sigma>
L = subst_lit L' \<sigma>

goal (1 subgoal):
 1. orient_lit L (u \<lhd> \<sigma>) (v \<lhd> \<sigma>) polarity
[PROOF STEP]
using lift_orient_lit
[PROOF STATE]
proof (prove)
using this:
orient_lit_inst L' u v polarity \<sigma>
L = subst_lit L' \<sigma>
orient_lit_inst ?L ?t ?s ?p ?\<sigma> \<Longrightarrow> orient_lit (subst_lit ?L ?\<sigma>) (?t \<lhd> ?\<sigma>) (?s \<lhd> ?\<sigma>) ?p

goal (1 subgoal):
 1. orient_lit L (u \<lhd> \<sigma>) (v \<lhd> \<sigma>) polarity
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
orient_lit L (u \<lhd> \<sigma>) (v \<lhd> \<sigma>) polarity

goal (1 subgoal):
 1. validate_ground_clause (same_values (\<lambda>t. trm_rep t S)) (subst_cl (C - {L1}) \<sigma>) \<Longrightarrow> False
[PROOF STEP]
from o' and \<open>vars_of_lit L = {}\<close>
[PROOF STATE]
proof (chain)
picking this:
orient_lit L (u \<lhd> \<sigma>) (v \<lhd> \<sigma>) polarity
vars_of_lit L = {}
[PROOF STEP]
have "vars_of (subst u \<sigma>) = {}"
[PROOF STATE]
proof (prove)
using this:
orient_lit L (u \<lhd> \<sigma>) (v \<lhd> \<sigma>) polarity
vars_of_lit L = {}

goal (1 subgoal):
 1. vars_of (u \<lhd> \<sigma>) = {}
[PROOF STEP]
using orient_lit_vars
[PROOF STATE]
proof (prove)
using this:
orient_lit L (u \<lhd> \<sigma>) (v \<lhd> \<sigma>) polarity
vars_of_lit L = {}
orient_lit ?L ?t ?s ?p \<Longrightarrow> vars_of ?t \<subseteq> vars_of_lit ?L \<and> vars_of ?s \<subseteq> vars_of_lit ?L

goal (1 subgoal):
 1. vars_of (u \<lhd> \<sigma>) = {}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
vars_of (u \<lhd> \<sigma>) = {}

goal (1 subgoal):
 1. validate_ground_clause (same_values (\<lambda>t. trm_rep t S)) (subst_cl (C - {L1}) \<sigma>) \<Longrightarrow> False
[PROOF STEP]
from o' and \<open>vars_of_lit L = {}\<close>
[PROOF STATE]
proof (chain)
picking this:
orient_lit L (u \<lhd> \<sigma>) (v \<lhd> \<sigma>) polarity
vars_of_lit L = {}
[PROOF STEP]
have "vars_of (subst v \<sigma>) = {}"
[PROOF STATE]
proof (prove)
using this:
orient_lit L (u \<lhd> \<sigma>) (v \<lhd> \<sigma>) polarity
vars_of_lit L = {}

goal (1 subgoal):
 1. vars_of (v \<lhd> \<sigma>) = {}
[PROOF STEP]
using orient_lit_vars
[PROOF STATE]
proof (prove)
using this:
orient_lit L (u \<lhd> \<sigma>) (v \<lhd> \<sigma>) polarity
vars_of_lit L = {}
orient_lit ?L ?t ?s ?p \<Longrightarrow> vars_of ?t \<subseteq> vars_of_lit ?L \<and> vars_of ?s \<subseteq> vars_of_lit ?L

goal (1 subgoal):
 1. vars_of (v \<lhd> \<sigma>) = {}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
vars_of (v \<lhd> \<sigma>) = {}

goal (1 subgoal):
 1. validate_ground_clause (same_values (\<lambda>t. trm_rep t S)) (subst_cl (C - {L1}) \<sigma>) \<Longrightarrow> False
[PROOF STEP]
from assms(3)
[PROOF STATE]
proof (chain)
picking this:
orient_lit_inst L1 t s pos \<sigma>
[PROOF STEP]
have o1 : "orient_lit (subst_lit L1 \<sigma>) (subst t \<sigma>) (subst s \<sigma>) pos"
[PROOF STATE]
proof (prove)
using this:
orient_lit_inst L1 t s pos \<sigma>

goal (1 subgoal):
 1. orient_lit (subst_lit L1 \<sigma>) (t \<lhd> \<sigma>) (s \<lhd> \<sigma>) pos
[PROOF STEP]
using lift_orient_lit [of L1 t s pos \<sigma>]
[PROOF STATE]
proof (prove)
using this:
orient_lit_inst L1 t s pos \<sigma>
orient_lit_inst L1 t s pos \<sigma> \<Longrightarrow> orient_lit (subst_lit L1 \<sigma>) (t \<lhd> \<sigma>) (s \<lhd> \<sigma>) pos

goal (1 subgoal):
 1. orient_lit (subst_lit L1 \<sigma>) (t \<lhd> \<sigma>) (s \<lhd> \<sigma>) pos
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
orient_lit (subst_lit L1 \<sigma>) (t \<lhd> \<sigma>) (s \<lhd> \<sigma>) pos

goal (1 subgoal):
 1. validate_ground_clause (same_values (\<lambda>t. trm_rep t S)) (subst_cl (C - {L1}) \<sigma>) \<Longrightarrow> False
[PROOF STEP]
from o1 and \<open>vars_of_lit (subst_lit L1 \<sigma>) = {}\<close>
[PROOF STATE]
proof (chain)
picking this:
orient_lit (subst_lit L1 \<sigma>) (t \<lhd> \<sigma>) (s \<lhd> \<sigma>) pos
vars_of_lit (subst_lit L1 \<sigma>) = {}
[PROOF STEP]
have "vars_of (subst t \<sigma>) = {}"
[PROOF STATE]
proof (prove)
using this:
orient_lit (subst_lit L1 \<sigma>) (t \<lhd> \<sigma>) (s \<lhd> \<sigma>) pos
vars_of_lit (subst_lit L1 \<sigma>) = {}

goal (1 subgoal):
 1. vars_of (t \<lhd> \<sigma>) = {}
[PROOF STEP]
using orient_lit_vars
[PROOF STATE]
proof (prove)
using this:
orient_lit (subst_lit L1 \<sigma>) (t \<lhd> \<sigma>) (s \<lhd> \<sigma>) pos
vars_of_lit (subst_lit L1 \<sigma>) = {}
orient_lit ?L ?t ?s ?p \<Longrightarrow> vars_of ?t \<subseteq> vars_of_lit ?L \<and> vars_of ?s \<subseteq> vars_of_lit ?L

goal (1 subgoal):
 1. vars_of (t \<lhd> \<sigma>) = {}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
vars_of (t \<lhd> \<sigma>) = {}

goal (1 subgoal):
 1. validate_ground_clause (same_values (\<lambda>t. trm_rep t S)) (subst_cl (C - {L1}) \<sigma>) \<Longrightarrow> False
[PROOF STEP]
have "polarity = pos \<or> polarity = neg"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. polarity = pos \<or> polarity = neg
[PROOF STEP]
using sign.exhaust
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?y = pos \<Longrightarrow> ?P; ?y = neg \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

goal (1 subgoal):
 1. polarity = pos \<or> polarity = neg
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
polarity = pos \<or> polarity = neg

goal (1 subgoal):
 1. validate_ground_clause (same_values (\<lambda>t. trm_rep t S)) (subst_cl (C - {L1}) \<sigma>) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
polarity = pos \<or> polarity = neg
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
polarity = pos \<or> polarity = neg

goal (1 subgoal):
 1. False
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. polarity = pos \<Longrightarrow> False
 2. polarity = neg \<Longrightarrow> False
[PROOF STEP]
assume "polarity = pos"
[PROOF STATE]
proof (state)
this:
polarity = pos

goal (2 subgoals):
 1. polarity = pos \<Longrightarrow> False
 2. polarity = neg \<Longrightarrow> False
[PROOF STEP]
from this and o and assms(2) and \<open>validate_ground_lit ?I L\<close> and \<open>L = (subst_lit L' \<sigma>)\<close>
[PROOF STATE]
proof (chain)
picking this:
polarity = pos
orient_lit_inst L' u v polarity \<sigma>
fo_interpretation (same_values (\<lambda>t. trm_rep t S))
validate_ground_lit (same_values (\<lambda>t. trm_rep t S)) L
L = subst_lit L' \<sigma>
[PROOF STEP]
have "(trm_rep (subst u \<sigma>) S) = (trm_rep (subst v \<sigma>) S)"
[PROOF STATE]
proof (prove)
using this:
polarity = pos
orient_lit_inst L' u v polarity \<sigma>
fo_interpretation (same_values (\<lambda>t. trm_rep t S))
validate_ground_lit (same_values (\<lambda>t. trm_rep t S)) L
L = subst_lit L' \<sigma>

goal (1 subgoal):
 1. trm_rep (u \<lhd> \<sigma>) S = trm_rep (v \<lhd> \<sigma>) S
[PROOF STEP]
using orient_lit_semantics_pos [of ?I ]
[PROOF STATE]
proof (prove)
using this:
polarity = pos
orient_lit_inst L' u v polarity \<sigma>
fo_interpretation (same_values (\<lambda>t. trm_rep t S))
validate_ground_lit (same_values (\<lambda>t. trm_rep t S)) L
L = subst_lit L' \<sigma>
\<lbrakk>fo_interpretation (same_values (\<lambda>t. trm_rep t S)); orient_lit_inst ?l ?u ?v pos ?\<eta>; validate_ground_lit (same_values (\<lambda>t. trm_rep t S)) (subst_lit ?l ?\<sigma>)\<rbrakk> \<Longrightarrow> same_values (\<lambda>t. trm_rep t S) (?u \<lhd> ?\<sigma>) (?v \<lhd> ?\<sigma>)

goal (1 subgoal):
 1. trm_rep (u \<lhd> \<sigma>) S = trm_rep (v \<lhd> \<sigma>) S
[PROOF STEP]
unfolding same_values_def
[PROOF STATE]
proof (prove)
using this:
polarity = pos
orient_lit_inst L' u v polarity \<sigma>
fo_interpretation (\<lambda>x y. trm_rep x S = trm_rep y S)
validate_ground_lit (\<lambda>x y. trm_rep x S = trm_rep y S) L
L = subst_lit L' \<sigma>
\<lbrakk>fo_interpretation (\<lambda>x y. trm_rep x S = trm_rep y S); orient_lit_inst ?l ?u ?v pos ?\<eta>; validate_ground_lit (\<lambda>x y. trm_rep x S = trm_rep y S) (subst_lit ?l ?\<sigma>)\<rbrakk> \<Longrightarrow> trm_rep (?u \<lhd> ?\<sigma>) S = trm_rep (?v \<lhd> ?\<sigma>) S

goal (1 subgoal):
 1. trm_rep (u \<lhd> \<sigma>) S = trm_rep (v \<lhd> \<sigma>) S
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
trm_rep (u \<lhd> \<sigma>) S = trm_rep (v \<lhd> \<sigma>) S

goal (2 subgoals):
 1. polarity = pos \<Longrightarrow> False
 2. polarity = neg \<Longrightarrow> False
[PROOF STEP]
from assms(4) and \<open>L \<in>(subst_cl C \<sigma>)\<close>
[PROOF STATE]
proof (chain)
picking this:
maximal_literal (subst_lit L1 \<sigma>) (subst_cl C \<sigma>)
L \<in> subst_cl C \<sigma>
[PROOF STEP]
have "((subst_lit L1 \<sigma>),L) \<notin> lit_ord"
[PROOF STATE]
proof (prove)
using this:
maximal_literal (subst_lit L1 \<sigma>) (subst_cl C \<sigma>)
L \<in> subst_cl C \<sigma>

goal (1 subgoal):
 1. (subst_lit L1 \<sigma>, L) \<notin> lit_ord
[PROOF STEP]
unfolding maximal_literal_def
[PROOF STATE]
proof (prove)
using this:
\<forall>x. x \<in> subst_cl C \<sigma> \<longrightarrow> (subst_lit L1 \<sigma>, x) \<notin> lit_ord
L \<in> subst_cl C \<sigma>

goal (1 subgoal):
 1. (subst_lit L1 \<sigma>, L) \<notin> lit_ord
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(subst_lit L1 \<sigma>, L) \<notin> lit_ord

goal (2 subgoals):
 1. polarity = pos \<Longrightarrow> False
 2. polarity = neg \<Longrightarrow> False
[PROOF STEP]
from this and o' and o1 and \<open>polarity=pos\<close> and \<open>vars_of_lit L = {}\<close> and \<open>L = (subst_lit L' \<sigma>)\<close>
      and \<open>vars_of_lit (subst_lit L1 \<sigma>) = {}\<close>
[PROOF STATE]
proof (chain)
picking this:
(subst_lit L1 \<sigma>, L) \<notin> lit_ord
orient_lit L (u \<lhd> \<sigma>) (v \<lhd> \<sigma>) polarity
orient_lit (subst_lit L1 \<sigma>) (t \<lhd> \<sigma>) (s \<lhd> \<sigma>) pos
polarity = pos
vars_of_lit L = {}
L = subst_lit L' \<sigma>
vars_of_lit (subst_lit L1 \<sigma>) = {}
[PROOF STEP]
have "(subst t \<sigma>, subst u \<sigma>) \<notin> trm_ord"
      and "(subst t \<sigma>, subst v \<sigma>) \<notin> trm_ord"
[PROOF STATE]
proof (prove)
using this:
(subst_lit L1 \<sigma>, L) \<notin> lit_ord
orient_lit L (u \<lhd> \<sigma>) (v \<lhd> \<sigma>) polarity
orient_lit (subst_lit L1 \<sigma>) (t \<lhd> \<sigma>) (s \<lhd> \<sigma>) pos
polarity = pos
vars_of_lit L = {}
L = subst_lit L' \<sigma>
vars_of_lit (subst_lit L1 \<sigma>) = {}

goal (1 subgoal):
 1. (t \<lhd> \<sigma>, u \<lhd> \<sigma>) \<notin> trm_ord &&& (t \<lhd> \<sigma>, v \<lhd> \<sigma>) \<notin> trm_ord
[PROOF STEP]
using lit_ord_dominating_term [of "subst t \<sigma>" "subst u \<sigma>"
          "subst v \<sigma>" "subst_lit L1 \<sigma>" "subst s \<sigma>" pos]
[PROOF STATE]
proof (prove)
using this:
(subst_lit L1 \<sigma>, L) \<notin> lit_ord
orient_lit L (u \<lhd> \<sigma>) (v \<lhd> \<sigma>) polarity
orient_lit (subst_lit L1 \<sigma>) (t \<lhd> \<sigma>) (s \<lhd> \<sigma>) pos
polarity = pos
vars_of_lit L = {}
L = subst_lit L' \<sigma>
vars_of_lit (subst_lit L1 \<sigma>) = {}
\<lbrakk>(t \<lhd> \<sigma>, u \<lhd> \<sigma>) \<in> trm_ord \<or> (t \<lhd> \<sigma>, v \<lhd> \<sigma>) \<in> trm_ord; orient_lit (subst_lit L1 \<sigma>) (t \<lhd> \<sigma>) (s \<lhd> \<sigma>) pos; orient_lit ?x2.0 (u \<lhd> \<sigma>) (v \<lhd> \<sigma>) ?p2.0; vars_of_lit (subst_lit L1 \<sigma>) = {}; vars_of_lit ?x2.0 = {}\<rbrakk> \<Longrightarrow> (subst_lit L1 \<sigma>, ?x2.0) \<in> lit_ord

goal (1 subgoal):
 1. (t \<lhd> \<sigma>, u \<lhd> \<sigma>) \<notin> trm_ord &&& (t \<lhd> \<sigma>, v \<lhd> \<sigma>) \<notin> trm_ord
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(t \<lhd> \<sigma>, u \<lhd> \<sigma>) \<notin> trm_ord
(t \<lhd> \<sigma>, v \<lhd> \<sigma>) \<notin> trm_ord

goal (2 subgoals):
 1. polarity = pos \<Longrightarrow> False
 2. polarity = neg \<Longrightarrow> False
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. False
[PROOF STEP]
proof (cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> False
 2. \<not> ?P \<Longrightarrow> False
[PROOF STEP]
assume "(subst t \<sigma>) = (subst u \<sigma>)"
[PROOF STATE]
proof (state)
this:
t \<lhd> \<sigma> = u \<lhd> \<sigma>

goal (2 subgoals):
 1. ?P \<Longrightarrow> False
 2. \<not> ?P \<Longrightarrow> False
[PROOF STEP]
from this and assms(8) and \<open>(trm_rep (subst u \<sigma>) S) = (trm_rep (subst v \<sigma>) S)\<close>
[PROOF STATE]
proof (chain)
picking this:
t \<lhd> \<sigma> = u \<lhd> \<sigma>
trm_rep (t \<lhd> \<sigma>) S = trm_rep (s \<lhd> \<sigma>) S
trm_rep (u \<lhd> \<sigma>) S = trm_rep (v \<lhd> \<sigma>) S
[PROOF STEP]
have "(trm_rep (subst s \<sigma>) S) = (trm_rep (subst v \<sigma>) S)"
[PROOF STATE]
proof (prove)
using this:
t \<lhd> \<sigma> = u \<lhd> \<sigma>
trm_rep (t \<lhd> \<sigma>) S = trm_rep (s \<lhd> \<sigma>) S
trm_rep (u \<lhd> \<sigma>) S = trm_rep (v \<lhd> \<sigma>) S

goal (1 subgoal):
 1. trm_rep (s \<lhd> \<sigma>) S = trm_rep (v \<lhd> \<sigma>) S
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
trm_rep (s \<lhd> \<sigma>) S = trm_rep (v \<lhd> \<sigma>) S

goal (2 subgoals):
 1. ?P \<Longrightarrow> False
 2. \<not> ?P \<Longrightarrow> False
[PROOF STEP]
from this o and \<open>L' \<in> C - { L1 }\<close> \<open>polarity = pos\<close> \<open>(subst t \<sigma>) = (subst u \<sigma>)\<close> assms(7)
[PROOF STATE]
proof (chain)
picking this:
trm_rep (s \<lhd> \<sigma>) S = trm_rep (v \<lhd> \<sigma>) S
orient_lit_inst L' u v polarity \<sigma>
L' \<in> C - {L1}
polarity = pos
t \<lhd> \<sigma> = u \<lhd> \<sigma>
\<not> equivalent_eq_exists t s C (same_values (\<lambda>t. trm_rep t S)) \<sigma> L1
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
trm_rep (s \<lhd> \<sigma>) S = trm_rep (v \<lhd> \<sigma>) S
orient_lit_inst L' u v polarity \<sigma>
L' \<in> C - {L1}
polarity = pos
t \<lhd> \<sigma> = u \<lhd> \<sigma>
\<not> equivalent_eq_exists t s C (same_values (\<lambda>t. trm_rep t S)) \<sigma> L1

goal (1 subgoal):
 1. False
[PROOF STEP]
unfolding equivalent_eq_exists_def same_values_def
[PROOF STATE]
proof (prove)
using this:
trm_rep (s \<lhd> \<sigma>) S = trm_rep (v \<lhd> \<sigma>) S
orient_lit_inst L' u v polarity \<sigma>
L' \<in> C - {L1}
polarity = pos
t \<lhd> \<sigma> = u \<lhd> \<sigma>
\<not> (\<exists>L\<in>C - {L1}. \<exists>u v. orient_lit_inst L u v pos \<sigma> \<and> t \<lhd> \<sigma> = u \<lhd> \<sigma> \<and> trm_rep (s \<lhd> \<sigma>) S = trm_rep (v \<lhd> \<sigma>) S)

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

goal (1 subgoal):
 1. t \<lhd> \<sigma> \<noteq> u \<lhd> \<sigma> \<Longrightarrow> False
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. t \<lhd> \<sigma> \<noteq> u \<lhd> \<sigma> \<Longrightarrow> False
[PROOF STEP]
assume "(subst t \<sigma>) \<noteq> (subst u \<sigma>)"
[PROOF STATE]
proof (state)
this:
t \<lhd> \<sigma> \<noteq> u \<lhd> \<sigma>

goal (1 subgoal):
 1. t \<lhd> \<sigma> \<noteq> u \<lhd> \<sigma> \<Longrightarrow> False
[PROOF STEP]
from this and \<open>(subst t \<sigma>, subst u \<sigma>)  \<notin> trm_ord\<close>
        and \<open>vars_of (subst t \<sigma>) = {}\<close> and \<open>vars_of (subst u \<sigma>) = {}\<close>
[PROOF STATE]
proof (chain)
picking this:
t \<lhd> \<sigma> \<noteq> u \<lhd> \<sigma>
(t \<lhd> \<sigma>, u \<lhd> \<sigma>) \<notin> trm_ord
vars_of (t \<lhd> \<sigma>) = {}
vars_of (u \<lhd> \<sigma>) = {}
[PROOF STEP]
have "(subst u \<sigma>, subst t \<sigma>) \<in> trm_ord"
[PROOF STATE]
proof (prove)
using this:
t \<lhd> \<sigma> \<noteq> u \<lhd> \<sigma>
(t \<lhd> \<sigma>, u \<lhd> \<sigma>) \<notin> trm_ord
vars_of (t \<lhd> \<sigma>) = {}
vars_of (u \<lhd> \<sigma>) = {}

goal (1 subgoal):
 1. (u \<lhd> \<sigma>, t \<lhd> \<sigma>) \<in> trm_ord
[PROOF STEP]
using trm_ord_ground_total
[PROOF STATE]
proof (prove)
using this:
t \<lhd> \<sigma> \<noteq> u \<lhd> \<sigma>
(t \<lhd> \<sigma>, u \<lhd> \<sigma>) \<notin> trm_ord
vars_of (t \<lhd> \<sigma>) = {}
vars_of (u \<lhd> \<sigma>) = {}
\<forall>x y. ground_term x \<longrightarrow> ground_term y \<longrightarrow> x \<noteq> y \<longrightarrow> (x, y) \<in> trm_ord \<or> (y, x) \<in> trm_ord

goal (1 subgoal):
 1. (u \<lhd> \<sigma>, t \<lhd> \<sigma>) \<in> trm_ord
[PROOF STEP]
unfolding ground_term_def
[PROOF STATE]
proof (prove)
using this:
t \<lhd> \<sigma> \<noteq> u \<lhd> \<sigma>
(t \<lhd> \<sigma>, u \<lhd> \<sigma>) \<notin> trm_ord
vars_of (t \<lhd> \<sigma>) = {}
vars_of (u \<lhd> \<sigma>) = {}
\<forall>x y. vars_of x = {} \<longrightarrow> vars_of y = {} \<longrightarrow> x \<noteq> y \<longrightarrow> (x, y) \<in> trm_ord \<or> (y, x) \<in> trm_ord

goal (1 subgoal):
 1. (u \<lhd> \<sigma>, t \<lhd> \<sigma>) \<in> trm_ord
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(u \<lhd> \<sigma>, t \<lhd> \<sigma>) \<in> trm_ord

goal (1 subgoal):
 1. t \<lhd> \<sigma> \<noteq> u \<lhd> \<sigma> \<Longrightarrow> False
[PROOF STEP]
from this and \<open>(subst u \<sigma>, subst v \<sigma>)  \<notin> trm_ord\<close>
        and \<open>vars_of (subst v \<sigma>) = {}\<close> and \<open>vars_of (subst t \<sigma>) = {}\<close>
[PROOF STATE]
proof (chain)
picking this:
(u \<lhd> \<sigma>, t \<lhd> \<sigma>) \<in> trm_ord
(u \<lhd> \<sigma>, v \<lhd> \<sigma>) \<notin> trm_ord
vars_of (v \<lhd> \<sigma>) = {}
vars_of (t \<lhd> \<sigma>) = {}
[PROOF STEP]
have "(subst v \<sigma>, subst t \<sigma>) \<in> trm_ord"
[PROOF STATE]
proof (prove)
using this:
(u \<lhd> \<sigma>, t \<lhd> \<sigma>) \<in> trm_ord
(u \<lhd> \<sigma>, v \<lhd> \<sigma>) \<notin> trm_ord
vars_of (v \<lhd> \<sigma>) = {}
vars_of (t \<lhd> \<sigma>) = {}

goal (1 subgoal):
 1. (v \<lhd> \<sigma>, t \<lhd> \<sigma>) \<in> trm_ord
[PROOF STEP]
using trm_ord_ground_total trm_ord_trans
[PROOF STATE]
proof (prove)
using this:
(u \<lhd> \<sigma>, t \<lhd> \<sigma>) \<in> trm_ord
(u \<lhd> \<sigma>, v \<lhd> \<sigma>) \<notin> trm_ord
vars_of (v \<lhd> \<sigma>) = {}
vars_of (t \<lhd> \<sigma>) = {}
\<forall>x y. ground_term x \<longrightarrow> ground_term y \<longrightarrow> x \<noteq> y \<longrightarrow> (x, y) \<in> trm_ord \<or> (y, x) \<in> trm_ord
trans trm_ord

goal (1 subgoal):
 1. (v \<lhd> \<sigma>, t \<lhd> \<sigma>) \<in> trm_ord
[PROOF STEP]
unfolding ground_term_def trans_def
[PROOF STATE]
proof (prove)
using this:
(u \<lhd> \<sigma>, t \<lhd> \<sigma>) \<in> trm_ord
(u \<lhd> \<sigma>, v \<lhd> \<sigma>) \<notin> trm_ord
vars_of (v \<lhd> \<sigma>) = {}
vars_of (t \<lhd> \<sigma>) = {}
\<forall>x y. vars_of x = {} \<longrightarrow> vars_of y = {} \<longrightarrow> x \<noteq> y \<longrightarrow> (x, y) \<in> trm_ord \<or> (y, x) \<in> trm_ord
\<forall>x y z. (x, y) \<in> trm_ord \<longrightarrow> (y, z) \<in> trm_ord \<longrightarrow> (x, z) \<in> trm_ord

goal (1 subgoal):
 1. (v \<lhd> \<sigma>, t \<lhd> \<sigma>) \<in> trm_ord
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
(v \<lhd> \<sigma>, t \<lhd> \<sigma>) \<in> trm_ord

goal (1 subgoal):
 1. t \<lhd> \<sigma> \<noteq> u \<lhd> \<sigma> \<Longrightarrow> False
[PROOF STEP]
from \<open>polarity = pos\<close> and o' and assms(1) and \<open>L \<in>(subst_cl C \<sigma>)\<close> and \<open>L = (subst_lit L' \<sigma>)\<close>
          and \<open>((subst u \<sigma>), subst t \<sigma>) \<in> trm_ord\<close>
          and \<open>((subst v \<sigma>), subst t \<sigma>) \<in> trm_ord\<close>
[PROOF STATE]
proof (chain)
picking this:
polarity = pos
orient_lit L (u \<lhd> \<sigma>) (v \<lhd> \<sigma>) polarity
smaller_lits_are_false (t \<lhd> \<sigma>) (subst_cl C \<sigma>) S
L \<in> subst_cl C \<sigma>
L = subst_lit L' \<sigma>
(u \<lhd> \<sigma>, t \<lhd> \<sigma>) \<in> trm_ord
(v \<lhd> \<sigma>, t \<lhd> \<sigma>) \<in> trm_ord
[PROOF STEP]
have "trm_rep (subst u \<sigma>) S \<noteq> trm_rep (subst v \<sigma>) S"
[PROOF STATE]
proof (prove)
using this:
polarity = pos
orient_lit L (u \<lhd> \<sigma>) (v \<lhd> \<sigma>) polarity
smaller_lits_are_false (t \<lhd> \<sigma>) (subst_cl C \<sigma>) S
L \<in> subst_cl C \<sigma>
L = subst_lit L' \<sigma>
(u \<lhd> \<sigma>, t \<lhd> \<sigma>) \<in> trm_ord
(v \<lhd> \<sigma>, t \<lhd> \<sigma>) \<in> trm_ord

goal (1 subgoal):
 1. trm_rep (u \<lhd> \<sigma>) S \<noteq> trm_rep (v \<lhd> \<sigma>) S
[PROOF STEP]
unfolding smaller_lits_are_false_def
[PROOF STATE]
proof (prove)
using this:
polarity = pos
orient_lit L (u \<lhd> \<sigma>) (v \<lhd> \<sigma>) polarity
\<forall>L u v. (L \<in> subst_cl C \<sigma> \<longrightarrow> orient_lit L u v pos \<longrightarrow> (u, t \<lhd> \<sigma>) \<in> trm_ord \<longrightarrow> (v, t \<lhd> \<sigma>) \<in> trm_ord \<longrightarrow> trm_rep u S \<noteq> trm_rep v S) \<and> (L \<in> subst_cl C \<sigma> \<longrightarrow> orient_lit L u v neg \<longrightarrow> (u, t \<lhd> \<sigma>) \<in> trm_ord \<longrightarrow> (v, t \<lhd> \<sigma>) \<in> trm_ord \<longrightarrow> trm_rep u S = trm_rep v S)
L \<in> subst_cl C \<sigma>
L = subst_lit L' \<sigma>
(u \<lhd> \<sigma>, t \<lhd> \<sigma>) \<in> trm_ord
(v \<lhd> \<sigma>, t \<lhd> \<sigma>) \<in> trm_ord

goal (1 subgoal):
 1. trm_rep (u \<lhd> \<sigma>) S \<noteq> trm_rep (v \<lhd> \<sigma>) S
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
trm_rep (u \<lhd> \<sigma>) S \<noteq> trm_rep (v \<lhd> \<sigma>) S

goal (1 subgoal):
 1. t \<lhd> \<sigma> \<noteq> u \<lhd> \<sigma> \<Longrightarrow> False
[PROOF STEP]
from this and \<open>trm_rep (subst u \<sigma>) S = trm_rep (subst v \<sigma>) S\<close>
[PROOF STATE]
proof (chain)
picking this:
trm_rep (u \<lhd> \<sigma>) S \<noteq> trm_rep (v \<lhd> \<sigma>) S
trm_rep (u \<lhd> \<sigma>) S = trm_rep (v \<lhd> \<sigma>) S
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
trm_rep (u \<lhd> \<sigma>) S \<noteq> trm_rep (v \<lhd> \<sigma>) S
trm_rep (u \<lhd> \<sigma>) S = trm_rep (v \<lhd> \<sigma>) S

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

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

goal (1 subgoal):
 1. polarity = neg \<Longrightarrow> False
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. polarity = neg \<Longrightarrow> False
[PROOF STEP]
assume "polarity = neg"
[PROOF STATE]
proof (state)
this:
polarity = neg

goal (1 subgoal):
 1. polarity = neg \<Longrightarrow> False
[PROOF STEP]
from this and o and assms(2) and \<open>validate_ground_lit ?I L\<close> and \<open>L = (subst_lit L' \<sigma>)\<close>
[PROOF STATE]
proof (chain)
picking this:
polarity = neg
orient_lit_inst L' u v polarity \<sigma>
fo_interpretation (same_values (\<lambda>t. trm_rep t S))
validate_ground_lit (same_values (\<lambda>t. trm_rep t S)) L
L = subst_lit L' \<sigma>
[PROOF STEP]
have "(trm_rep (subst u \<sigma>) S) \<noteq> (trm_rep (subst v \<sigma>) S)"
[PROOF STATE]
proof (prove)
using this:
polarity = neg
orient_lit_inst L' u v polarity \<sigma>
fo_interpretation (same_values (\<lambda>t. trm_rep t S))
validate_ground_lit (same_values (\<lambda>t. trm_rep t S)) L
L = subst_lit L' \<sigma>

goal (1 subgoal):
 1. trm_rep (u \<lhd> \<sigma>) S \<noteq> trm_rep (v \<lhd> \<sigma>) S
[PROOF STEP]
using orient_lit_semantics_neg [of ?I ]
[PROOF STATE]
proof (prove)
using this:
polarity = neg
orient_lit_inst L' u v polarity \<sigma>
fo_interpretation (same_values (\<lambda>t. trm_rep t S))
validate_ground_lit (same_values (\<lambda>t. trm_rep t S)) L
L = subst_lit L' \<sigma>
\<lbrakk>fo_interpretation (same_values (\<lambda>t. trm_rep t S)); orient_lit_inst ?l ?u ?v neg ?\<theta>; validate_ground_lit (same_values (\<lambda>t. trm_rep t S)) (subst_lit ?l ?\<sigma>)\<rbrakk> \<Longrightarrow> \<not> same_values (\<lambda>t. trm_rep t S) (?u \<lhd> ?\<sigma>) (?v \<lhd> ?\<sigma>)

goal (1 subgoal):
 1. trm_rep (u \<lhd> \<sigma>) S \<noteq> trm_rep (v \<lhd> \<sigma>) S
[PROOF STEP]
unfolding same_values_def
[PROOF STATE]
proof (prove)
using this:
polarity = neg
orient_lit_inst L' u v polarity \<sigma>
fo_interpretation (\<lambda>x y. trm_rep x S = trm_rep y S)
validate_ground_lit (\<lambda>x y. trm_rep x S = trm_rep y S) L
L = subst_lit L' \<sigma>
\<lbrakk>fo_interpretation (\<lambda>x y. trm_rep x S = trm_rep y S); orient_lit_inst ?l ?u ?v neg ?\<theta>; validate_ground_lit (\<lambda>x y. trm_rep x S = trm_rep y S) (subst_lit ?l ?\<sigma>)\<rbrakk> \<Longrightarrow> trm_rep (?u \<lhd> ?\<sigma>) S \<noteq> trm_rep (?v \<lhd> ?\<sigma>) S

goal (1 subgoal):
 1. trm_rep (u \<lhd> \<sigma>) S \<noteq> trm_rep (v \<lhd> \<sigma>) S
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
trm_rep (u \<lhd> \<sigma>) S \<noteq> trm_rep (v \<lhd> \<sigma>) S

goal (1 subgoal):
 1. polarity = neg \<Longrightarrow> False
[PROOF STEP]
from assms(4) and \<open>L \<in>(subst_cl C \<sigma>)\<close>
[PROOF STATE]
proof (chain)
picking this:
maximal_literal (subst_lit L1 \<sigma>) (subst_cl C \<sigma>)
L \<in> subst_cl C \<sigma>
[PROOF STEP]
have "((subst_lit L1 \<sigma>),L) \<notin> lit_ord"
[PROOF STATE]
proof (prove)
using this:
maximal_literal (subst_lit L1 \<sigma>) (subst_cl C \<sigma>)
L \<in> subst_cl C \<sigma>

goal (1 subgoal):
 1. (subst_lit L1 \<sigma>, L) \<notin> lit_ord
[PROOF STEP]
unfolding maximal_literal_def
[PROOF STATE]
proof (prove)
using this:
\<forall>x. x \<in> subst_cl C \<sigma> \<longrightarrow> (subst_lit L1 \<sigma>, x) \<notin> lit_ord
L \<in> subst_cl C \<sigma>

goal (1 subgoal):
 1. (subst_lit L1 \<sigma>, L) \<notin> lit_ord
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(subst_lit L1 \<sigma>, L) \<notin> lit_ord

goal (1 subgoal):
 1. polarity = neg \<Longrightarrow> False
[PROOF STEP]
from this and o' and o1 and \<open>vars_of_lit L = {}\<close> and \<open>L = (subst_lit L' \<sigma>)\<close>
      and \<open>vars_of_lit (subst_lit L1 \<sigma>) = {}\<close>
[PROOF STATE]
proof (chain)
picking this:
(subst_lit L1 \<sigma>, L) \<notin> lit_ord
orient_lit L (u \<lhd> \<sigma>) (v \<lhd> \<sigma>) polarity
orient_lit (subst_lit L1 \<sigma>) (t \<lhd> \<sigma>) (s \<lhd> \<sigma>) pos
vars_of_lit L = {}
L = subst_lit L' \<sigma>
vars_of_lit (subst_lit L1 \<sigma>) = {}
[PROOF STEP]
have "(subst t \<sigma>, subst u \<sigma>) \<notin> trm_ord"
      and "(subst t \<sigma>, subst v \<sigma>) \<notin> trm_ord"
[PROOF STATE]
proof (prove)
using this:
(subst_lit L1 \<sigma>, L) \<notin> lit_ord
orient_lit L (u \<lhd> \<sigma>) (v \<lhd> \<sigma>) polarity
orient_lit (subst_lit L1 \<sigma>) (t \<lhd> \<sigma>) (s \<lhd> \<sigma>) pos
vars_of_lit L = {}
L = subst_lit L' \<sigma>
vars_of_lit (subst_lit L1 \<sigma>) = {}

goal (1 subgoal):
 1. (t \<lhd> \<sigma>, u \<lhd> \<sigma>) \<notin> trm_ord &&& (t \<lhd> \<sigma>, v \<lhd> \<sigma>) \<notin> trm_ord
[PROOF STEP]
using lit_ord_dominating_term [of "subst t \<sigma>" "subst u \<sigma>"
            "subst v \<sigma>" "subst_lit L1 \<sigma>" "subst s \<sigma>" pos]
[PROOF STATE]
proof (prove)
using this:
(subst_lit L1 \<sigma>, L) \<notin> lit_ord
orient_lit L (u \<lhd> \<sigma>) (v \<lhd> \<sigma>) polarity
orient_lit (subst_lit L1 \<sigma>) (t \<lhd> \<sigma>) (s \<lhd> \<sigma>) pos
vars_of_lit L = {}
L = subst_lit L' \<sigma>
vars_of_lit (subst_lit L1 \<sigma>) = {}
\<lbrakk>(t \<lhd> \<sigma>, u \<lhd> \<sigma>) \<in> trm_ord \<or> (t \<lhd> \<sigma>, v \<lhd> \<sigma>) \<in> trm_ord; orient_lit (subst_lit L1 \<sigma>) (t \<lhd> \<sigma>) (s \<lhd> \<sigma>) pos; orient_lit ?x2.0 (u \<lhd> \<sigma>) (v \<lhd> \<sigma>) ?p2.0; vars_of_lit (subst_lit L1 \<sigma>) = {}; vars_of_lit ?x2.0 = {}\<rbrakk> \<Longrightarrow> (subst_lit L1 \<sigma>, ?x2.0) \<in> lit_ord

goal (1 subgoal):
 1. (t \<lhd> \<sigma>, u \<lhd> \<sigma>) \<notin> trm_ord &&& (t \<lhd> \<sigma>, v \<lhd> \<sigma>) \<notin> trm_ord
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(t \<lhd> \<sigma>, u \<lhd> \<sigma>) \<notin> trm_ord
(t \<lhd> \<sigma>, v \<lhd> \<sigma>) \<notin> trm_ord

goal (1 subgoal):
 1. polarity = neg \<Longrightarrow> False
[PROOF STEP]
from \<open>((subst_lit L1 \<sigma>),L) \<notin> lit_ord\<close> and o' and o1 and \<open>polarity=neg\<close> and \<open>vars_of_lit L = {}\<close>
      and \<open>L = (subst_lit L' \<sigma>)\<close> and \<open>vars_of_lit (subst_lit L1 \<sigma>) = {}\<close>
[PROOF STATE]
proof (chain)
picking this:
(subst_lit L1 \<sigma>, L) \<notin> lit_ord
orient_lit L (u \<lhd> \<sigma>) (v \<lhd> \<sigma>) polarity
orient_lit (subst_lit L1 \<sigma>) (t \<lhd> \<sigma>) (s \<lhd> \<sigma>) pos
polarity = neg
vars_of_lit L = {}
L = subst_lit L' \<sigma>
vars_of_lit (subst_lit L1 \<sigma>) = {}
[PROOF STEP]
have "subst t \<sigma> \<noteq> subst u \<sigma>"
[PROOF STATE]
proof (prove)
using this:
(subst_lit L1 \<sigma>, L) \<notin> lit_ord
orient_lit L (u \<lhd> \<sigma>) (v \<lhd> \<sigma>) polarity
orient_lit (subst_lit L1 \<sigma>) (t \<lhd> \<sigma>) (s \<lhd> \<sigma>) pos
polarity = neg
vars_of_lit L = {}
L = subst_lit L' \<sigma>
vars_of_lit (subst_lit L1 \<sigma>) = {}

goal (1 subgoal):
 1. t \<lhd> \<sigma> \<noteq> u \<lhd> \<sigma>
[PROOF STEP]
using lit_ord_neg_lit_lhs
[PROOF STATE]
proof (prove)
using this:
(subst_lit L1 \<sigma>, L) \<notin> lit_ord
orient_lit L (u \<lhd> \<sigma>) (v \<lhd> \<sigma>) polarity
orient_lit (subst_lit L1 \<sigma>) (t \<lhd> \<sigma>) (s \<lhd> \<sigma>) pos
polarity = neg
vars_of_lit L = {}
L = subst_lit L' \<sigma>
vars_of_lit (subst_lit L1 \<sigma>) = {}
\<lbrakk>orient_lit ?x1.0 ?s ?t1.0 pos; orient_lit ?x2.0 ?s ?t2.0 neg; vars_of_lit ?x1.0 = {}; vars_of_lit ?x2.0 = {}\<rbrakk> \<Longrightarrow> (?x1.0, ?x2.0) \<in> lit_ord

goal (1 subgoal):
 1. t \<lhd> \<sigma> \<noteq> u \<lhd> \<sigma>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
t \<lhd> \<sigma> \<noteq> u \<lhd> \<sigma>

goal (1 subgoal):
 1. polarity = neg \<Longrightarrow> False
[PROOF STEP]
from this and \<open>(subst t \<sigma>, subst u \<sigma>)  \<notin> trm_ord\<close> and \<open>vars_of (subst t \<sigma>) = {}\<close>
        and \<open>vars_of (subst u \<sigma>) = {}\<close>
[PROOF STATE]
proof (chain)
picking this:
t \<lhd> \<sigma> \<noteq> u \<lhd> \<sigma>
(t \<lhd> \<sigma>, u \<lhd> \<sigma>) \<notin> trm_ord
vars_of (t \<lhd> \<sigma>) = {}
vars_of (u \<lhd> \<sigma>) = {}
[PROOF STEP]
have "(subst u \<sigma>, subst t \<sigma>) \<in> trm_ord"
[PROOF STATE]
proof (prove)
using this:
t \<lhd> \<sigma> \<noteq> u \<lhd> \<sigma>
(t \<lhd> \<sigma>, u \<lhd> \<sigma>) \<notin> trm_ord
vars_of (t \<lhd> \<sigma>) = {}
vars_of (u \<lhd> \<sigma>) = {}

goal (1 subgoal):
 1. (u \<lhd> \<sigma>, t \<lhd> \<sigma>) \<in> trm_ord
[PROOF STEP]
using trm_ord_ground_total
[PROOF STATE]
proof (prove)
using this:
t \<lhd> \<sigma> \<noteq> u \<lhd> \<sigma>
(t \<lhd> \<sigma>, u \<lhd> \<sigma>) \<notin> trm_ord
vars_of (t \<lhd> \<sigma>) = {}
vars_of (u \<lhd> \<sigma>) = {}
\<forall>x y. ground_term x \<longrightarrow> ground_term y \<longrightarrow> x \<noteq> y \<longrightarrow> (x, y) \<in> trm_ord \<or> (y, x) \<in> trm_ord

goal (1 subgoal):
 1. (u \<lhd> \<sigma>, t \<lhd> \<sigma>) \<in> trm_ord
[PROOF STEP]
unfolding ground_term_def
[PROOF STATE]
proof (prove)
using this:
t \<lhd> \<sigma> \<noteq> u \<lhd> \<sigma>
(t \<lhd> \<sigma>, u \<lhd> \<sigma>) \<notin> trm_ord
vars_of (t \<lhd> \<sigma>) = {}
vars_of (u \<lhd> \<sigma>) = {}
\<forall>x y. vars_of x = {} \<longrightarrow> vars_of y = {} \<longrightarrow> x \<noteq> y \<longrightarrow> (x, y) \<in> trm_ord \<or> (y, x) \<in> trm_ord

goal (1 subgoal):
 1. (u \<lhd> \<sigma>, t \<lhd> \<sigma>) \<in> trm_ord
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(u \<lhd> \<sigma>, t \<lhd> \<sigma>) \<in> trm_ord

goal (1 subgoal):
 1. polarity = neg \<Longrightarrow> False
[PROOF STEP]
from this and \<open>(subst u \<sigma>, subst v \<sigma>)  \<notin> trm_ord\<close> and \<open>vars_of (subst v \<sigma>) = {}\<close>
        and \<open>vars_of (subst t \<sigma>) = {}\<close>
[PROOF STATE]
proof (chain)
picking this:
(u \<lhd> \<sigma>, t \<lhd> \<sigma>) \<in> trm_ord
(u \<lhd> \<sigma>, v \<lhd> \<sigma>) \<notin> trm_ord
vars_of (v \<lhd> \<sigma>) = {}
vars_of (t \<lhd> \<sigma>) = {}
[PROOF STEP]
have "(subst v \<sigma>, subst t \<sigma>) \<in> trm_ord"
[PROOF STATE]
proof (prove)
using this:
(u \<lhd> \<sigma>, t \<lhd> \<sigma>) \<in> trm_ord
(u \<lhd> \<sigma>, v \<lhd> \<sigma>) \<notin> trm_ord
vars_of (v \<lhd> \<sigma>) = {}
vars_of (t \<lhd> \<sigma>) = {}

goal (1 subgoal):
 1. (v \<lhd> \<sigma>, t \<lhd> \<sigma>) \<in> trm_ord
[PROOF STEP]
using trm_ord_ground_total trm_ord_trans
[PROOF STATE]
proof (prove)
using this:
(u \<lhd> \<sigma>, t \<lhd> \<sigma>) \<in> trm_ord
(u \<lhd> \<sigma>, v \<lhd> \<sigma>) \<notin> trm_ord
vars_of (v \<lhd> \<sigma>) = {}
vars_of (t \<lhd> \<sigma>) = {}
\<forall>x y. ground_term x \<longrightarrow> ground_term y \<longrightarrow> x \<noteq> y \<longrightarrow> (x, y) \<in> trm_ord \<or> (y, x) \<in> trm_ord
trans trm_ord

goal (1 subgoal):
 1. (v \<lhd> \<sigma>, t \<lhd> \<sigma>) \<in> trm_ord
[PROOF STEP]
unfolding ground_term_def trans_def
[PROOF STATE]
proof (prove)
using this:
(u \<lhd> \<sigma>, t \<lhd> \<sigma>) \<in> trm_ord
(u \<lhd> \<sigma>, v \<lhd> \<sigma>) \<notin> trm_ord
vars_of (v \<lhd> \<sigma>) = {}
vars_of (t \<lhd> \<sigma>) = {}
\<forall>x y. vars_of x = {} \<longrightarrow> vars_of y = {} \<longrightarrow> x \<noteq> y \<longrightarrow> (x, y) \<in> trm_ord \<or> (y, x) \<in> trm_ord
\<forall>x y z. (x, y) \<in> trm_ord \<longrightarrow> (y, z) \<in> trm_ord \<longrightarrow> (x, z) \<in> trm_ord

goal (1 subgoal):
 1. (v \<lhd> \<sigma>, t \<lhd> \<sigma>) \<in> trm_ord
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
(v \<lhd> \<sigma>, t \<lhd> \<sigma>) \<in> trm_ord

goal (1 subgoal):
 1. polarity = neg \<Longrightarrow> False
[PROOF STEP]
from \<open>polarity = neg\<close> and o' and assms(1) and \<open>L \<in>(subst_cl C \<sigma>)\<close> and \<open>L = (subst_lit L' \<sigma>)\<close>
          and \<open>((subst u \<sigma>), subst t \<sigma>) \<in> trm_ord\<close> and \<open>((subst v \<sigma>), subst t \<sigma>) \<in> trm_ord\<close>
[PROOF STATE]
proof (chain)
picking this:
polarity = neg
orient_lit L (u \<lhd> \<sigma>) (v \<lhd> \<sigma>) polarity
smaller_lits_are_false (t \<lhd> \<sigma>) (subst_cl C \<sigma>) S
L \<in> subst_cl C \<sigma>
L = subst_lit L' \<sigma>
(u \<lhd> \<sigma>, t \<lhd> \<sigma>) \<in> trm_ord
(v \<lhd> \<sigma>, t \<lhd> \<sigma>) \<in> trm_ord
[PROOF STEP]
have "trm_rep (subst u \<sigma>) S = trm_rep (subst v \<sigma>) S"
[PROOF STATE]
proof (prove)
using this:
polarity = neg
orient_lit L (u \<lhd> \<sigma>) (v \<lhd> \<sigma>) polarity
smaller_lits_are_false (t \<lhd> \<sigma>) (subst_cl C \<sigma>) S
L \<in> subst_cl C \<sigma>
L = subst_lit L' \<sigma>
(u \<lhd> \<sigma>, t \<lhd> \<sigma>) \<in> trm_ord
(v \<lhd> \<sigma>, t \<lhd> \<sigma>) \<in> trm_ord

goal (1 subgoal):
 1. trm_rep (u \<lhd> \<sigma>) S = trm_rep (v \<lhd> \<sigma>) S
[PROOF STEP]
unfolding smaller_lits_are_false_def
[PROOF STATE]
proof (prove)
using this:
polarity = neg
orient_lit L (u \<lhd> \<sigma>) (v \<lhd> \<sigma>) polarity
\<forall>L u v. (L \<in> subst_cl C \<sigma> \<longrightarrow> orient_lit L u v pos \<longrightarrow> (u, t \<lhd> \<sigma>) \<in> trm_ord \<longrightarrow> (v, t \<lhd> \<sigma>) \<in> trm_ord \<longrightarrow> trm_rep u S \<noteq> trm_rep v S) \<and> (L \<in> subst_cl C \<sigma> \<longrightarrow> orient_lit L u v neg \<longrightarrow> (u, t \<lhd> \<sigma>) \<in> trm_ord \<longrightarrow> (v, t \<lhd> \<sigma>) \<in> trm_ord \<longrightarrow> trm_rep u S = trm_rep v S)
L \<in> subst_cl C \<sigma>
L = subst_lit L' \<sigma>
(u \<lhd> \<sigma>, t \<lhd> \<sigma>) \<in> trm_ord
(v \<lhd> \<sigma>, t \<lhd> \<sigma>) \<in> trm_ord

goal (1 subgoal):
 1. trm_rep (u \<lhd> \<sigma>) S = trm_rep (v \<lhd> \<sigma>) S
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
trm_rep (u \<lhd> \<sigma>) S = trm_rep (v \<lhd> \<sigma>) S

goal (1 subgoal):
 1. polarity = neg \<Longrightarrow> False
[PROOF STEP]
from this and \<open>trm_rep (subst u \<sigma>) S \<noteq> trm_rep (subst v \<sigma>) S\<close>
[PROOF STATE]
proof (chain)
picking this:
trm_rep (u \<lhd> \<sigma>) S = trm_rep (v \<lhd> \<sigma>) S
trm_rep (u \<lhd> \<sigma>) S \<noteq> trm_rep (v \<lhd> \<sigma>) S
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
trm_rep (u \<lhd> \<sigma>) S = trm_rep (v \<lhd> \<sigma>) S
trm_rep (u \<lhd> \<sigma>) S \<noteq> trm_rep (v \<lhd> \<sigma>) S

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

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

goal:
No subgoals!
[PROOF STEP]
qed