[STATEMENT]
lemma dvd_repr:
  fixes a b :: nat
  shows "a dvd b \<longleftrightarrow> (\<exists>x. x * a = b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a dvd b) = (\<exists>x. x * a = b)
[PROOF STEP]
using dvd_class.dvd_def
[PROOF STATE]
proof (prove)
using this:
(?b dvd ?a) = (\<exists>k. ?a = ?b * k)

goal (1 subgoal):
 1. (a dvd b) = (\<exists>x. x * a = b)
[PROOF STEP]
by auto


[STATEMENT]
lemma dvd_dioph[dioph]: "is_dioph_rel (DVD Q R)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_dioph_rel DVD Q R
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. is_dioph_rel DVD Q R
[PROOF STEP]
define Q' R' where pushed_defs: "Q' \<equiv> push_param Q 1" "R' \<equiv> push_param R 1"
[PROOF STATE]
proof (state)
this:
Q' \<equiv> push_param Q 1
R' \<equiv> push_param R 1

goal (1 subgoal):
 1. is_dioph_rel DVD Q R
[PROOF STEP]
define D where "D \<equiv> [\<exists>] (Param 0 [*] Q' [=] R')"
[PROOF STATE]
proof (state)
this:
D \<equiv> [\<exists>] polynomial.Param 0 [*] Q' [=] R'

goal (1 subgoal):
 1. is_dioph_rel DVD Q R
[PROOF STEP]
have "eval (DVD Q R) a = eval D a" for a
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval DVD Q R a = eval D a
[PROOF STEP]
unfolding D_def pushed_defs defs
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval DVD Q R a = (\<exists>k. eval (NARY (\<lambda>l. l ! 0 = l ! 1) [polynomial.Param 0 [*] push_param Q 1, push_param R 1]) (push a k))
[PROOF STEP]
using push_push1
[PROOF STATE]
proof (prove)
using this:
peval (push_param ?P 1) (push ?a ?k) = peval ?P ?a

goal (1 subgoal):
 1. eval DVD Q R a = (\<exists>k. eval (NARY (\<lambda>l. l ! 0 = l ! 1) [polynomial.Param 0 [*] push_param Q 1, push_param R 1]) (push a k))
[PROOF STEP]
apply (auto simp: push0)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<And>P a k. peval (push_param P (Suc 0)) (push a k) = peval P a; eval DVD Q R a\<rbrakk> \<Longrightarrow> \<exists>k. k * peval Q a = peval R a
 2. \<And>k. \<lbrakk>\<And>P a k. peval (push_param P (Suc 0)) (push a k) = peval P a; k * peval Q a = peval R a\<rbrakk> \<Longrightarrow> eval DVD Q R a
[PROOF STEP]
unfolding dvd_def
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<And>P a k. peval (push_param P (Suc 0)) (push a k) = peval P a; eval (BINARY (dvd) Q R) a\<rbrakk> \<Longrightarrow> \<exists>k. k * peval Q a = peval R a
 2. \<And>k. \<lbrakk>\<And>P a k. peval (push_param P (Suc 0)) (push a k) = peval P a; k * peval Q a = peval R a\<rbrakk> \<Longrightarrow> eval (BINARY (dvd) Q R) a
[PROOF STEP]
by (auto simp: dvd_repr binary_eval)
[PROOF STATE]
proof (state)
this:
eval DVD Q R ?a = eval D ?a

goal (1 subgoal):
 1. is_dioph_rel DVD Q R
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
eval DVD Q R ?a = eval D ?a

goal (1 subgoal):
 1. is_dioph_rel DVD Q R
[PROOF STEP]
have "is_dioph_rel D"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_dioph_rel D
[PROOF STEP]
unfolding D_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_dioph_rel ([\<exists>] polynomial.Param 0 [*] Q' [=] R')
[PROOF STEP]
by (auto simp: dioph)
[PROOF STATE]
proof (state)
this:
is_dioph_rel D

goal (1 subgoal):
 1. is_dioph_rel DVD Q R
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
eval DVD Q R ?a = eval D ?a
is_dioph_rel D
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
eval DVD Q R ?a = eval D ?a
is_dioph_rel D

goal (1 subgoal):
 1. is_dioph_rel DVD Q R
[PROOF STEP]
by (auto simp: is_dioph_rel_def)
[PROOF STATE]
proof (state)
this:
is_dioph_rel DVD Q R

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mod_repr:
  fixes a b c :: nat
  shows "a mod b = c mod b \<longleftrightarrow> (\<exists>x y. c + x*b = a + y*b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a mod b = c mod b) = (\<exists>x y. c + x * b = a + y * b)
[PROOF STEP]
by (metis mult.commute nat_mod_eq_iff)


[STATEMENT]
lemma mod_dioph[dioph]:
  fixes A B C
  defines "D \<equiv> (MOD A B C)"
  shows "is_dioph_rel D"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_dioph_rel D
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. is_dioph_rel D
[PROOF STEP]
define A' B' C' where pushed_defs: "A' \<equiv> push_param A 2" "B' \<equiv> push_param B 2" "C' \<equiv> push_param C 2"
[PROOF STATE]
proof (state)
this:
A' \<equiv> push_param A 2
B' \<equiv> push_param B 2
C' \<equiv> push_param C 2

goal (1 subgoal):
 1. is_dioph_rel D
[PROOF STEP]
define DS where "DS \<equiv> [\<exists>2] (Param 0 [*] B' [+] C' [=] Param 1 [*] B' [+] A')"
[PROOF STATE]
proof (state)
this:
DS \<equiv> [\<exists>2] polynomial.Param 0 [*] B' [+] C' [=] polynomial.Param 1 [*] B' [+] A'

goal (1 subgoal):
 1. is_dioph_rel D
[PROOF STEP]
have "eval DS a = eval D a" for a
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval DS a = eval D a
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. eval DS a \<Longrightarrow> eval D a
 2. eval D a \<Longrightarrow> eval DS a
[PROOF STEP]
show "eval DS a \<Longrightarrow> eval D a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval DS a \<Longrightarrow> eval D a
[PROOF STEP]
unfolding DS_def defs D_def mod_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval ([\<exists>2] NARY (\<lambda>l. l ! 0 = l ! 1) [polynomial.Param 0 [*] B' [+] C', polynomial.Param 1 [*] B' [+] A']) a \<Longrightarrow> eval (NARY (\<lambda>l. l ! 0 mod l ! 1 = l ! 2 mod l ! 1) [A, B, C]) a
[PROOF STEP]
by auto (metis mod_mult_self3 push_push_simp pushed_defs(1) pushed_defs(2) pushed_defs(3))
[PROOF STATE]
proof (state)
this:
eval DS a \<Longrightarrow> eval D a

goal (1 subgoal):
 1. eval D a \<Longrightarrow> eval DS a
[PROOF STEP]
show "eval D a \<Longrightarrow> eval DS a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval D a \<Longrightarrow> eval DS a
[PROOF STEP]
unfolding DS_def defs D_def mod_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval (NARY (\<lambda>l. l ! 0 mod l ! 1 = l ! 2 mod l ! 1) [A, B, C]) a \<Longrightarrow> eval ([\<exists>2] NARY (\<lambda>l. l ! 0 = l ! 1) [polynomial.Param 0 [*] B' [+] C', polynomial.Param 1 [*] B' [+] A']) a
[PROOF STEP]
apply (auto simp add: mod_repr)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. peval C a + x * peval B a = peval A a + y * peval B a \<Longrightarrow> \<exists>ks. length ks = 2 \<and> push_list a ks 0 * peval B' (push_list a ks) + peval C' (push_list a ks) = push_list a ks (Suc 0) * peval B' (push_list a ks) + peval A' (push_list a ks)
[PROOF STEP]
subgoal for x y
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. peval C a + x * peval B a = peval A a + y * peval B a \<Longrightarrow> \<exists>ks. length ks = 2 \<and> push_list a ks 0 * peval B' (push_list a ks) + peval C' (push_list a ks) = push_list a ks (Suc 0) * peval B' (push_list a ks) + peval A' (push_list a ks)
[PROOF STEP]
apply (rule exI[of _ "[x, y]"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. peval C a + x * peval B a = peval A a + y * peval B a \<Longrightarrow> length [x, y] = 2 \<and> push_list a [x, y] 0 * peval B' (push_list a [x, y]) + peval C' (push_list a [x, y]) = push_list a [x, y] (Suc 0) * peval B' (push_list a [x, y]) + peval A' (push_list a [x, y])
[PROOF STEP]
unfolding pushed_defs
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. peval C a + x * peval B a = peval A a + y * peval B a \<Longrightarrow> length [x, y] = 2 \<and> push_list a [x, y] 0 * peval (push_param B 2) (push_list a [x, y]) + peval (push_param C 2) (push_list a [x, y]) = push_list a [x, y] (Suc 0) * peval (push_param B 2) (push_list a [x, y]) + peval (push_param A 2) (push_list a [x, y])
[PROOF STEP]
by (simp add: push_push[where ?n = 2] push_list_eval)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
eval D a \<Longrightarrow> eval DS a

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
eval DS ?a = eval D ?a

goal (1 subgoal):
 1. is_dioph_rel D
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
eval DS ?a = eval D ?a

goal (1 subgoal):
 1. is_dioph_rel D
[PROOF STEP]
have "is_dioph_rel DS"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_dioph_rel DS
[PROOF STEP]
unfolding DS_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_dioph_rel ([\<exists>2] polynomial.Param 0 [*] B' [+] C' [=] polynomial.Param 1 [*] B' [+] A')
[PROOF STEP]
by (simp add: dioph)
[PROOF STATE]
proof (state)
this:
is_dioph_rel DS

goal (1 subgoal):
 1. is_dioph_rel D
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
eval DS ?a = eval D ?a
is_dioph_rel DS
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
eval DS ?a = eval D ?a
is_dioph_rel DS

goal (1 subgoal):
 1. is_dioph_rel D
[PROOF STEP]
by (auto simp: is_dioph_rel_def)
[PROOF STATE]
proof (state)
this:
is_dioph_rel D

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma lift_orient_lit:
  assumes "orient_lit_inst L t s p \<sigma>"
  shows "orient_lit (subst_lit L \<sigma>) (subst t \<sigma>)  (subst s \<sigma>) p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. orient_lit (subst_lit L \<sigma>) (t \<lhd> \<sigma>) (s \<lhd> \<sigma>) p
[PROOF STEP]
unfolding orient_lit_inst_def orient_lit_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (subst_lit L \<sigma> = Pos (Eq (t \<lhd> \<sigma>) (s \<lhd> \<sigma>)) \<or> subst_lit L \<sigma> = Pos (Eq (s \<lhd> \<sigma>) (t \<lhd> \<sigma>))) \<and> (t \<lhd> \<sigma>, s \<lhd> \<sigma>) \<notin> trm_ord \<and> p = pos \<or> (subst_lit L \<sigma> = Neg (Eq (t \<lhd> \<sigma>) (s \<lhd> \<sigma>)) \<or> subst_lit L \<sigma> = Neg (Eq (s \<lhd> \<sigma>) (t \<lhd> \<sigma>))) \<and> (t \<lhd> \<sigma>, s \<lhd> \<sigma>) \<notin> trm_ord \<and> p = neg
[PROOF STEP]
using assms orient_lit_inst_def
[PROOF STATE]
proof (prove)
using this:
orient_lit_inst L t s p \<sigma>
orient_lit_inst ?L ?u ?v ?s ?\<sigma> = ((?L = Pos (Eq ?u ?v) \<or> ?L = Pos (Eq ?v ?u)) \<and> (?u \<lhd> ?\<sigma>, ?v \<lhd> ?\<sigma>) \<notin> trm_ord \<and> ?s = pos \<or> (?L = Neg (Eq ?u ?v) \<or> ?L = Neg (Eq ?v ?u)) \<and> (?u \<lhd> ?\<sigma>, ?v \<lhd> ?\<sigma>) \<notin> trm_ord \<and> ?s = neg)

goal (1 subgoal):
 1. (subst_lit L \<sigma> = Pos (Eq (t \<lhd> \<sigma>) (s \<lhd> \<sigma>)) \<or> subst_lit L \<sigma> = Pos (Eq (s \<lhd> \<sigma>) (t \<lhd> \<sigma>))) \<and> (t \<lhd> \<sigma>, s \<lhd> \<sigma>) \<notin> trm_ord \<and> p = pos \<or> (subst_lit L \<sigma> = Neg (Eq (t \<lhd> \<sigma>) (s \<lhd> \<sigma>)) \<or> subst_lit L \<sigma> = Neg (Eq (s \<lhd> \<sigma>) (t \<lhd> \<sigma>))) \<and> (t \<lhd> \<sigma>, s \<lhd> \<sigma>) \<notin> trm_ord \<and> p = neg
[PROOF STEP]
by auto


[STATEMENT]
lemma orient_lit_vars:
  assumes "orient_lit L t s p"
  shows "vars_of t \<subseteq> vars_of_lit L \<and> vars_of s \<subseteq> vars_of_lit L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vars_of t \<subseteq> vars_of_lit L \<and> vars_of s \<subseteq> vars_of_lit L
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. vars_of t \<subseteq> vars_of_lit L \<and> vars_of s \<subseteq> vars_of_lit L
[PROOF STEP]
have "p = neg \<or> p = pos"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p = neg \<or> p = pos
[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. p = neg \<or> p = pos
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p = neg \<or> p = pos

goal (1 subgoal):
 1. vars_of t \<subseteq> vars_of_lit L \<and> vars_of s \<subseteq> vars_of_lit L
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p = neg \<or> p = pos
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
p = neg \<or> p = pos

goal (1 subgoal):
 1. vars_of t \<subseteq> vars_of_lit L \<and> vars_of s \<subseteq> vars_of_lit L
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. p = neg \<Longrightarrow> vars_of t \<subseteq> vars_of_lit L \<and> vars_of s \<subseteq> vars_of_lit L
 2. p = pos \<Longrightarrow> vars_of t \<subseteq> vars_of_lit L \<and> vars_of s \<subseteq> vars_of_lit L
[PROOF STEP]
assume "p = neg"
[PROOF STATE]
proof (state)
this:
p = neg

goal (2 subgoals):
 1. p = neg \<Longrightarrow> vars_of t \<subseteq> vars_of_lit L \<and> vars_of s \<subseteq> vars_of_lit L
 2. p = pos \<Longrightarrow> vars_of t \<subseteq> vars_of_lit L \<and> vars_of s \<subseteq> vars_of_lit L
[PROOF STEP]
from this and assms(1)
[PROOF STATE]
proof (chain)
picking this:
p = neg
orient_lit L t s p
[PROOF STEP]
have "(L = Neg (Eq t s)) \<or> (L = (Neg (Eq s t)))"
[PROOF STATE]
proof (prove)
using this:
p = neg
orient_lit L t s p

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

goal (1 subgoal):
 1. L = Neg (Eq t s) \<or> L = Neg (Eq s t)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
L = Neg (Eq t s) \<or> L = Neg (Eq s t)

goal (2 subgoals):
 1. p = neg \<Longrightarrow> vars_of t \<subseteq> vars_of_lit L \<and> vars_of s \<subseteq> vars_of_lit L
 2. p = pos \<Longrightarrow> vars_of t \<subseteq> vars_of_lit L \<and> vars_of s \<subseteq> vars_of_lit L
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
L = Neg (Eq t s) \<or> L = Neg (Eq s t)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
L = Neg (Eq t s) \<or> L = Neg (Eq s t)

goal (1 subgoal):
 1. vars_of t \<subseteq> vars_of_lit L \<and> vars_of s \<subseteq> vars_of_lit L
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. L = Neg (Eq t s) \<Longrightarrow> vars_of t \<subseteq> vars_of_lit L \<and> vars_of s \<subseteq> vars_of_lit L
 2. L = Neg (Eq s t) \<Longrightarrow> vars_of t \<subseteq> vars_of_lit L \<and> vars_of s \<subseteq> vars_of_lit L
[PROOF STEP]
assume "L = Neg (Eq t s)"
[PROOF STATE]
proof (state)
this:
L = Neg (Eq t s)

goal (2 subgoals):
 1. L = Neg (Eq t s) \<Longrightarrow> vars_of t \<subseteq> vars_of_lit L \<and> vars_of s \<subseteq> vars_of_lit L
 2. L = Neg (Eq s t) \<Longrightarrow> vars_of t \<subseteq> vars_of_lit L \<and> vars_of s \<subseteq> vars_of_lit L
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
L = Neg (Eq t s)
[PROOF STEP]
have "vars_of_lit L = vars_of t \<union> vars_of s"
[PROOF STATE]
proof (prove)
using this:
L = Neg (Eq t s)

goal (1 subgoal):
 1. vars_of_lit L = vars_of t \<union> vars_of s
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
vars_of_lit L = vars_of t \<union> vars_of s

goal (2 subgoals):
 1. L = Neg (Eq t s) \<Longrightarrow> vars_of t \<subseteq> vars_of_lit L \<and> vars_of s \<subseteq> vars_of_lit L
 2. L = Neg (Eq s t) \<Longrightarrow> vars_of t \<subseteq> vars_of_lit L \<and> vars_of s \<subseteq> vars_of_lit L
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
vars_of_lit L = vars_of t \<union> vars_of s
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
vars_of_lit L = vars_of t \<union> vars_of s

goal (1 subgoal):
 1. vars_of t \<subseteq> vars_of_lit L \<and> vars_of s \<subseteq> vars_of_lit L
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
vars_of t \<subseteq> vars_of_lit L \<and> vars_of s \<subseteq> vars_of_lit L

goal (1 subgoal):
 1. L = Neg (Eq s t) \<Longrightarrow> vars_of t \<subseteq> vars_of_lit L \<and> vars_of s \<subseteq> vars_of_lit L
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. L = Neg (Eq s t) \<Longrightarrow> vars_of t \<subseteq> vars_of_lit L \<and> vars_of s \<subseteq> vars_of_lit L
[PROOF STEP]
assume "L = Neg (Eq s t)"
[PROOF STATE]
proof (state)
this:
L = Neg (Eq s t)

goal (1 subgoal):
 1. L = Neg (Eq s t) \<Longrightarrow> vars_of t \<subseteq> vars_of_lit L \<and> vars_of s \<subseteq> vars_of_lit L
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
L = Neg (Eq s t)
[PROOF STEP]
have "vars_of_lit L = vars_of s \<union> vars_of t"
[PROOF STATE]
proof (prove)
using this:
L = Neg (Eq s t)

goal (1 subgoal):
 1. vars_of_lit L = vars_of s \<union> vars_of t
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
vars_of_lit L = vars_of s \<union> vars_of t

goal (1 subgoal):
 1. L = Neg (Eq s t) \<Longrightarrow> vars_of t \<subseteq> vars_of_lit L \<and> vars_of s \<subseteq> vars_of_lit L
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
vars_of_lit L = vars_of s \<union> vars_of t
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
vars_of_lit L = vars_of s \<union> vars_of t

goal (1 subgoal):
 1. vars_of t \<subseteq> vars_of_lit L \<and> vars_of s \<subseteq> vars_of_lit L
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
vars_of t \<subseteq> vars_of_lit L \<and> vars_of s \<subseteq> vars_of_lit L

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
vars_of t \<subseteq> vars_of_lit L \<and> vars_of s \<subseteq> vars_of_lit L

goal (1 subgoal):
 1. p = pos \<Longrightarrow> vars_of t \<subseteq> vars_of_lit L \<and> vars_of s \<subseteq> vars_of_lit L
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. p = pos \<Longrightarrow> vars_of t \<subseteq> vars_of_lit L \<and> vars_of s \<subseteq> vars_of_lit L
[PROOF STEP]
assume "p = pos"
[PROOF STATE]
proof (state)
this:
p = pos

goal (1 subgoal):
 1. p = pos \<Longrightarrow> vars_of t \<subseteq> vars_of_lit L \<and> vars_of s \<subseteq> vars_of_lit L
[PROOF STEP]
from this and assms(1)
[PROOF STATE]
proof (chain)
picking this:
p = pos
orient_lit L t s p
[PROOF STEP]
have "(L = Pos (Eq t s)) \<or> (L = (Pos (Eq s t)))"
[PROOF STATE]
proof (prove)
using this:
p = pos
orient_lit L t s p

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

goal (1 subgoal):
 1. L = Pos (Eq t s) \<or> L = Pos (Eq s t)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
L = Pos (Eq t s) \<or> L = Pos (Eq s t)

goal (1 subgoal):
 1. p = pos \<Longrightarrow> vars_of t \<subseteq> vars_of_lit L \<and> vars_of s \<subseteq> vars_of_lit L
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
L = Pos (Eq t s) \<or> L = Pos (Eq s t)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
L = Pos (Eq t s) \<or> L = Pos (Eq s t)

goal (1 subgoal):
 1. vars_of t \<subseteq> vars_of_lit L \<and> vars_of s \<subseteq> vars_of_lit L
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. L = Pos (Eq t s) \<Longrightarrow> vars_of t \<subseteq> vars_of_lit L \<and> vars_of s \<subseteq> vars_of_lit L
 2. L = Pos (Eq s t) \<Longrightarrow> vars_of t \<subseteq> vars_of_lit L \<and> vars_of s \<subseteq> vars_of_lit L
[PROOF STEP]
assume "L = Pos (Eq t s)"
[PROOF STATE]
proof (state)
this:
L = Pos (Eq t s)

goal (2 subgoals):
 1. L = Pos (Eq t s) \<Longrightarrow> vars_of t \<subseteq> vars_of_lit L \<and> vars_of s \<subseteq> vars_of_lit L
 2. L = Pos (Eq s t) \<Longrightarrow> vars_of t \<subseteq> vars_of_lit L \<and> vars_of s \<subseteq> vars_of_lit L
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
L = Pos (Eq t s)
[PROOF STEP]
have "vars_of_lit L = vars_of t \<union> vars_of s"
[PROOF STATE]
proof (prove)
using this:
L = Pos (Eq t s)

goal (1 subgoal):
 1. vars_of_lit L = vars_of t \<union> vars_of s
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
vars_of_lit L = vars_of t \<union> vars_of s

goal (2 subgoals):
 1. L = Pos (Eq t s) \<Longrightarrow> vars_of t \<subseteq> vars_of_lit L \<and> vars_of s \<subseteq> vars_of_lit L
 2. L = Pos (Eq s t) \<Longrightarrow> vars_of t \<subseteq> vars_of_lit L \<and> vars_of s \<subseteq> vars_of_lit L
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
vars_of_lit L = vars_of t \<union> vars_of s
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
vars_of_lit L = vars_of t \<union> vars_of s

goal (1 subgoal):
 1. vars_of t \<subseteq> vars_of_lit L \<and> vars_of s \<subseteq> vars_of_lit L
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
vars_of t \<subseteq> vars_of_lit L \<and> vars_of s \<subseteq> vars_of_lit L

goal (1 subgoal):
 1. L = Pos (Eq s t) \<Longrightarrow> vars_of t \<subseteq> vars_of_lit L \<and> vars_of s \<subseteq> vars_of_lit L
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. L = Pos (Eq s t) \<Longrightarrow> vars_of t \<subseteq> vars_of_lit L \<and> vars_of s \<subseteq> vars_of_lit L
[PROOF STEP]
assume "L = Pos (Eq s t)"
[PROOF STATE]
proof (state)
this:
L = Pos (Eq s t)

goal (1 subgoal):
 1. L = Pos (Eq s t) \<Longrightarrow> vars_of t \<subseteq> vars_of_lit L \<and> vars_of s \<subseteq> vars_of_lit L
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
L = Pos (Eq s t)
[PROOF STEP]
have "vars_of_lit L = vars_of s \<union> vars_of t"
[PROOF STATE]
proof (prove)
using this:
L = Pos (Eq s t)

goal (1 subgoal):
 1. vars_of_lit L = vars_of s \<union> vars_of t
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
vars_of_lit L = vars_of s \<union> vars_of t

goal (1 subgoal):
 1. L = Pos (Eq s t) \<Longrightarrow> vars_of t \<subseteq> vars_of_lit L \<and> vars_of s \<subseteq> vars_of_lit L
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
vars_of_lit L = vars_of s \<union> vars_of t
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
vars_of_lit L = vars_of s \<union> vars_of t

goal (1 subgoal):
 1. vars_of t \<subseteq> vars_of_lit L \<and> vars_of s \<subseteq> vars_of_lit L
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
vars_of t \<subseteq> vars_of_lit L \<and> vars_of s \<subseteq> vars_of_lit L

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
vars_of t \<subseteq> vars_of_lit L \<and> vars_of s \<subseteq> vars_of_lit L

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
vars_of t \<subseteq> vars_of_lit L \<and> vars_of s \<subseteq> vars_of_lit L

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma orient_lit_inst_vars:
  assumes "orient_lit_inst L t s p \<sigma>"
  shows "vars_of t \<subseteq> vars_of_lit L \<and> vars_of s \<subseteq> vars_of_lit L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vars_of t \<subseteq> vars_of_lit L \<and> vars_of s \<subseteq> vars_of_lit L
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. vars_of t \<subseteq> vars_of_lit L \<and> vars_of s \<subseteq> vars_of_lit L
[PROOF STEP]
have "p = neg \<or> p = pos"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p = neg \<or> p = pos
[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. p = neg \<or> p = pos
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p = neg \<or> p = pos

goal (1 subgoal):
 1. vars_of t \<subseteq> vars_of_lit L \<and> vars_of s \<subseteq> vars_of_lit L
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p = neg \<or> p = pos
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
p = neg \<or> p = pos

goal (1 subgoal):
 1. vars_of t \<subseteq> vars_of_lit L \<and> vars_of s \<subseteq> vars_of_lit L
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. p = neg \<Longrightarrow> vars_of t \<subseteq> vars_of_lit L \<and> vars_of s \<subseteq> vars_of_lit L
 2. p = pos \<Longrightarrow> vars_of t \<subseteq> vars_of_lit L \<and> vars_of s \<subseteq> vars_of_lit L
[PROOF STEP]
assume "p = neg"
[PROOF STATE]
proof (state)
this:
p = neg

goal (2 subgoals):
 1. p = neg \<Longrightarrow> vars_of t \<subseteq> vars_of_lit L \<and> vars_of s \<subseteq> vars_of_lit L
 2. p = pos \<Longrightarrow> vars_of t \<subseteq> vars_of_lit L \<and> vars_of s \<subseteq> vars_of_lit L
[PROOF STEP]
from this and assms(1)
[PROOF STATE]
proof (chain)
picking this:
p = neg
orient_lit_inst L t s p \<sigma>
[PROOF STEP]
have "(L = Neg (Eq t s)) \<or> (L = (Neg (Eq s t)))"
[PROOF STATE]
proof (prove)
using this:
p = neg
orient_lit_inst L t s p \<sigma>

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

goal (1 subgoal):
 1. L = Neg (Eq t s) \<or> L = Neg (Eq s t)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
L = Neg (Eq t s) \<or> L = Neg (Eq s t)

goal (2 subgoals):
 1. p = neg \<Longrightarrow> vars_of t \<subseteq> vars_of_lit L \<and> vars_of s \<subseteq> vars_of_lit L
 2. p = pos \<Longrightarrow> vars_of t \<subseteq> vars_of_lit L \<and> vars_of s \<subseteq> vars_of_lit L
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
L = Neg (Eq t s) \<or> L = Neg (Eq s t)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
L = Neg (Eq t s) \<or> L = Neg (Eq s t)

goal (1 subgoal):
 1. vars_of t \<subseteq> vars_of_lit L \<and> vars_of s \<subseteq> vars_of_lit L
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. L = Neg (Eq t s) \<Longrightarrow> vars_of t \<subseteq> vars_of_lit L \<and> vars_of s \<subseteq> vars_of_lit L
 2. L = Neg (Eq s t) \<Longrightarrow> vars_of t \<subseteq> vars_of_lit L \<and> vars_of s \<subseteq> vars_of_lit L
[PROOF STEP]
assume "L = Neg (Eq t s)"
[PROOF STATE]
proof (state)
this:
L = Neg (Eq t s)

goal (2 subgoals):
 1. L = Neg (Eq t s) \<Longrightarrow> vars_of t \<subseteq> vars_of_lit L \<and> vars_of s \<subseteq> vars_of_lit L
 2. L = Neg (Eq s t) \<Longrightarrow> vars_of t \<subseteq> vars_of_lit L \<and> vars_of s \<subseteq> vars_of_lit L
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
L = Neg (Eq t s)
[PROOF STEP]
have "vars_of_lit L = vars_of t \<union> vars_of s"
[PROOF STATE]
proof (prove)
using this:
L = Neg (Eq t s)

goal (1 subgoal):
 1. vars_of_lit L = vars_of t \<union> vars_of s
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
vars_of_lit L = vars_of t \<union> vars_of s

goal (2 subgoals):
 1. L = Neg (Eq t s) \<Longrightarrow> vars_of t \<subseteq> vars_of_lit L \<and> vars_of s \<subseteq> vars_of_lit L
 2. L = Neg (Eq s t) \<Longrightarrow> vars_of t \<subseteq> vars_of_lit L \<and> vars_of s \<subseteq> vars_of_lit L
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
vars_of_lit L = vars_of t \<union> vars_of s
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
vars_of_lit L = vars_of t \<union> vars_of s

goal (1 subgoal):
 1. vars_of t \<subseteq> vars_of_lit L \<and> vars_of s \<subseteq> vars_of_lit L
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
vars_of t \<subseteq> vars_of_lit L \<and> vars_of s \<subseteq> vars_of_lit L

goal (1 subgoal):
 1. L = Neg (Eq s t) \<Longrightarrow> vars_of t \<subseteq> vars_of_lit L \<and> vars_of s \<subseteq> vars_of_lit L
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. L = Neg (Eq s t) \<Longrightarrow> vars_of t \<subseteq> vars_of_lit L \<and> vars_of s \<subseteq> vars_of_lit L
[PROOF STEP]
assume "L = Neg (Eq s t)"
[PROOF STATE]
proof (state)
this:
L = Neg (Eq s t)

goal (1 subgoal):
 1. L = Neg (Eq s t) \<Longrightarrow> vars_of t \<subseteq> vars_of_lit L \<and> vars_of s \<subseteq> vars_of_lit L
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
L = Neg (Eq s t)
[PROOF STEP]
have "vars_of_lit L = vars_of s \<union> vars_of t"
[PROOF STATE]
proof (prove)
using this:
L = Neg (Eq s t)

goal (1 subgoal):
 1. vars_of_lit L = vars_of s \<union> vars_of t
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
vars_of_lit L = vars_of s \<union> vars_of t

goal (1 subgoal):
 1. L = Neg (Eq s t) \<Longrightarrow> vars_of t \<subseteq> vars_of_lit L \<and> vars_of s \<subseteq> vars_of_lit L
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
vars_of_lit L = vars_of s \<union> vars_of t
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
vars_of_lit L = vars_of s \<union> vars_of t

goal (1 subgoal):
 1. vars_of t \<subseteq> vars_of_lit L \<and> vars_of s \<subseteq> vars_of_lit L
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
vars_of t \<subseteq> vars_of_lit L \<and> vars_of s \<subseteq> vars_of_lit L

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
vars_of t \<subseteq> vars_of_lit L \<and> vars_of s \<subseteq> vars_of_lit L

goal (1 subgoal):
 1. p = pos \<Longrightarrow> vars_of t \<subseteq> vars_of_lit L \<and> vars_of s \<subseteq> vars_of_lit L
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. p = pos \<Longrightarrow> vars_of t \<subseteq> vars_of_lit L \<and> vars_of s \<subseteq> vars_of_lit L
[PROOF STEP]
assume "p = pos"
[PROOF STATE]
proof (state)
this:
p = pos

goal (1 subgoal):
 1. p = pos \<Longrightarrow> vars_of t \<subseteq> vars_of_lit L \<and> vars_of s \<subseteq> vars_of_lit L
[PROOF STEP]
from this and assms(1)
[PROOF STATE]
proof (chain)
picking this:
p = pos
orient_lit_inst L t s p \<sigma>
[PROOF STEP]
have "(L = Pos (Eq t s)) \<or> (L = (Pos (Eq s t)))"
[PROOF STATE]
proof (prove)
using this:
p = pos
orient_lit_inst L t s p \<sigma>

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

goal (1 subgoal):
 1. L = Pos (Eq t s) \<or> L = Pos (Eq s t)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
L = Pos (Eq t s) \<or> L = Pos (Eq s t)

goal (1 subgoal):
 1. p = pos \<Longrightarrow> vars_of t \<subseteq> vars_of_lit L \<and> vars_of s \<subseteq> vars_of_lit L
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
L = Pos (Eq t s) \<or> L = Pos (Eq s t)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
L = Pos (Eq t s) \<or> L = Pos (Eq s t)

goal (1 subgoal):
 1. vars_of t \<subseteq> vars_of_lit L \<and> vars_of s \<subseteq> vars_of_lit L
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. L = Pos (Eq t s) \<Longrightarrow> vars_of t \<subseteq> vars_of_lit L \<and> vars_of s \<subseteq> vars_of_lit L
 2. L = Pos (Eq s t) \<Longrightarrow> vars_of t \<subseteq> vars_of_lit L \<and> vars_of s \<subseteq> vars_of_lit L
[PROOF STEP]
assume "L = Pos (Eq t s)"
[PROOF STATE]
proof (state)
this:
L = Pos (Eq t s)

goal (2 subgoals):
 1. L = Pos (Eq t s) \<Longrightarrow> vars_of t \<subseteq> vars_of_lit L \<and> vars_of s \<subseteq> vars_of_lit L
 2. L = Pos (Eq s t) \<Longrightarrow> vars_of t \<subseteq> vars_of_lit L \<and> vars_of s \<subseteq> vars_of_lit L
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
L = Pos (Eq t s)
[PROOF STEP]
have "vars_of_lit L = vars_of t \<union> vars_of s"
[PROOF STATE]
proof (prove)
using this:
L = Pos (Eq t s)

goal (1 subgoal):
 1. vars_of_lit L = vars_of t \<union> vars_of s
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
vars_of_lit L = vars_of t \<union> vars_of s

goal (2 subgoals):
 1. L = Pos (Eq t s) \<Longrightarrow> vars_of t \<subseteq> vars_of_lit L \<and> vars_of s \<subseteq> vars_of_lit L
 2. L = Pos (Eq s t) \<Longrightarrow> vars_of t \<subseteq> vars_of_lit L \<and> vars_of s \<subseteq> vars_of_lit L
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
vars_of_lit L = vars_of t \<union> vars_of s
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
vars_of_lit L = vars_of t \<union> vars_of s

goal (1 subgoal):
 1. vars_of t \<subseteq> vars_of_lit L \<and> vars_of s \<subseteq> vars_of_lit L
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
vars_of t \<subseteq> vars_of_lit L \<and> vars_of s \<subseteq> vars_of_lit L

goal (1 subgoal):
 1. L = Pos (Eq s t) \<Longrightarrow> vars_of t \<subseteq> vars_of_lit L \<and> vars_of s \<subseteq> vars_of_lit L
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. L = Pos (Eq s t) \<Longrightarrow> vars_of t \<subseteq> vars_of_lit L \<and> vars_of s \<subseteq> vars_of_lit L
[PROOF STEP]
assume "L = Pos (Eq s t)"
[PROOF STATE]
proof (state)
this:
L = Pos (Eq s t)

goal (1 subgoal):
 1. L = Pos (Eq s t) \<Longrightarrow> vars_of t \<subseteq> vars_of_lit L \<and> vars_of s \<subseteq> vars_of_lit L
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
L = Pos (Eq s t)
[PROOF STEP]
have "vars_of_lit L = vars_of s \<union> vars_of t"
[PROOF STATE]
proof (prove)
using this:
L = Pos (Eq s t)

goal (1 subgoal):
 1. vars_of_lit L = vars_of s \<union> vars_of t
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
vars_of_lit L = vars_of s \<union> vars_of t

goal (1 subgoal):
 1. L = Pos (Eq s t) \<Longrightarrow> vars_of t \<subseteq> vars_of_lit L \<and> vars_of s \<subseteq> vars_of_lit L
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
vars_of_lit L = vars_of s \<union> vars_of t
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
vars_of_lit L = vars_of s \<union> vars_of t

goal (1 subgoal):
 1. vars_of t \<subseteq> vars_of_lit L \<and> vars_of s \<subseteq> vars_of_lit L
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
vars_of t \<subseteq> vars_of_lit L \<and> vars_of s \<subseteq> vars_of_lit L

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
vars_of t \<subseteq> vars_of_lit L \<and> vars_of s \<subseteq> vars_of_lit L

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
vars_of t \<subseteq> vars_of_lit L \<and> vars_of s \<subseteq> vars_of_lit L

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma orient_lit_inst_coincide:
  assumes "orient_lit_inst L1 t s polarity \<sigma>"
  assumes "coincide_on \<sigma> \<eta> (vars_of_lit L1)"
  shows "orient_lit_inst L1 t s polarity \<eta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. orient_lit_inst L1 t s polarity \<eta>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. orient_lit_inst L1 t s polarity \<eta>
[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. orient_lit_inst L1 t s polarity \<eta>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
polarity = pos \<or> polarity = neg
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
polarity = pos \<or> polarity = neg

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

goal (2 subgoals):
 1. polarity = pos \<Longrightarrow> orient_lit_inst L1 t s polarity \<eta>
 2. polarity = neg \<Longrightarrow> orient_lit_inst L1 t s polarity \<eta>
[PROOF STEP]
from this and assms(1)
[PROOF STATE]
proof (chain)
picking this:
polarity = pos
orient_lit_inst L1 t s polarity \<sigma>
[PROOF STEP]
have "L1 = Pos (Eq t s) \<or> L1 = Pos (Eq s t)"
      and "( (subst t \<sigma>),  (subst s \<sigma>)) \<notin> trm_ord"
[PROOF STATE]
proof (prove)
using this:
polarity = pos
orient_lit_inst L1 t s polarity \<sigma>

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

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

goal (2 subgoals):
 1. polarity = pos \<Longrightarrow> orient_lit_inst L1 t s polarity \<eta>
 2. polarity = neg \<Longrightarrow> orient_lit_inst L1 t s polarity \<eta>
[PROOF STEP]
from \<open>L1 = Pos (Eq t s) \<or> L1 = Pos (Eq s t)\<close>
[PROOF STATE]
proof (chain)
picking this:
L1 = Pos (Eq t s) \<or> L1 = Pos (Eq s t)
[PROOF STEP]
have "vars_of t \<subseteq> vars_of_lit L1" and "vars_of s \<subseteq> vars_of_lit L1"
[PROOF STATE]
proof (prove)
using this:
L1 = Pos (Eq t s) \<or> L1 = Pos (Eq s t)

goal (1 subgoal):
 1. vars_of t \<subseteq> vars_of_lit L1 &&& vars_of s \<subseteq> vars_of_lit L1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vars_of t \<subseteq> vars_of_lit L1
vars_of s \<subseteq> vars_of_lit L1

goal (2 subgoals):
 1. polarity = pos \<Longrightarrow> orient_lit_inst L1 t s polarity \<eta>
 2. polarity = neg \<Longrightarrow> orient_lit_inst L1 t s polarity \<eta>
[PROOF STEP]
from \<open>vars_of t \<subseteq> vars_of_lit L1\<close> and assms(2)
[PROOF STATE]
proof (chain)
picking this:
vars_of t \<subseteq> vars_of_lit L1
coincide_on \<sigma> \<eta> (vars_of_lit L1)
[PROOF STEP]
have "coincide_on \<sigma> \<eta> (vars_of t)"
[PROOF STATE]
proof (prove)
using this:
vars_of t \<subseteq> vars_of_lit L1
coincide_on \<sigma> \<eta> (vars_of_lit L1)

goal (1 subgoal):
 1. coincide_on \<sigma> \<eta> (vars_of t)
[PROOF STEP]
unfolding coincide_on_def
[PROOF STATE]
proof (prove)
using this:
vars_of t \<subseteq> vars_of_lit L1
\<forall>x\<in>vars_of_lit L1. Var x \<lhd> \<sigma> = Var x \<lhd> \<eta>

goal (1 subgoal):
 1. \<forall>x\<in>vars_of t. Var x \<lhd> \<sigma> = Var x \<lhd> \<eta>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
coincide_on \<sigma> \<eta> (vars_of t)

goal (2 subgoals):
 1. polarity = pos \<Longrightarrow> orient_lit_inst L1 t s polarity \<eta>
 2. polarity = neg \<Longrightarrow> orient_lit_inst L1 t s polarity \<eta>
[PROOF STEP]
from \<open>vars_of s \<subseteq> vars_of_lit L1\<close> and assms(2)
[PROOF STATE]
proof (chain)
picking this:
vars_of s \<subseteq> vars_of_lit L1
coincide_on \<sigma> \<eta> (vars_of_lit L1)
[PROOF STEP]
have "coincide_on \<sigma> \<eta> (vars_of s)"
[PROOF STATE]
proof (prove)
using this:
vars_of s \<subseteq> vars_of_lit L1
coincide_on \<sigma> \<eta> (vars_of_lit L1)

goal (1 subgoal):
 1. coincide_on \<sigma> \<eta> (vars_of s)
[PROOF STEP]
unfolding coincide_on_def
[PROOF STATE]
proof (prove)
using this:
vars_of s \<subseteq> vars_of_lit L1
\<forall>x\<in>vars_of_lit L1. Var x \<lhd> \<sigma> = Var x \<lhd> \<eta>

goal (1 subgoal):
 1. \<forall>x\<in>vars_of s. Var x \<lhd> \<sigma> = Var x \<lhd> \<eta>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
coincide_on \<sigma> \<eta> (vars_of s)

goal (2 subgoals):
 1. polarity = pos \<Longrightarrow> orient_lit_inst L1 t s polarity \<eta>
 2. polarity = neg \<Longrightarrow> orient_lit_inst L1 t s polarity \<eta>
[PROOF STEP]
from \<open>( (subst t \<sigma>),  (subst s \<sigma>)) \<notin> trm_ord\<close>
      and \<open>coincide_on \<sigma> \<eta> (vars_of t)\<close> and \<open>coincide_on \<sigma> \<eta> (vars_of s)\<close> assms(2)
[PROOF STATE]
proof (chain)
picking this:
(t \<lhd> \<sigma>, s \<lhd> \<sigma>) \<notin> trm_ord
coincide_on \<sigma> \<eta> (vars_of t)
coincide_on \<sigma> \<eta> (vars_of s)
coincide_on \<sigma> \<eta> (vars_of_lit L1)
[PROOF STEP]
have "( (subst t \<eta>),  (subst s \<eta>)) \<notin> trm_ord"
[PROOF STATE]
proof (prove)
using this:
(t \<lhd> \<sigma>, s \<lhd> \<sigma>) \<notin> trm_ord
coincide_on \<sigma> \<eta> (vars_of t)
coincide_on \<sigma> \<eta> (vars_of s)
coincide_on \<sigma> \<eta> (vars_of_lit L1)

goal (1 subgoal):
 1. (t \<lhd> \<eta>, s \<lhd> \<eta>) \<notin> trm_ord
[PROOF STEP]
using coincide_on_term
[PROOF STATE]
proof (prove)
using this:
(t \<lhd> \<sigma>, s \<lhd> \<sigma>) \<notin> trm_ord
coincide_on \<sigma> \<eta> (vars_of t)
coincide_on \<sigma> \<eta> (vars_of s)
coincide_on \<sigma> \<eta> (vars_of_lit L1)
coincide_on ?\<sigma> ?\<eta> (vars_of ?t) \<Longrightarrow> ?t \<lhd> ?\<sigma> = ?t \<lhd> ?\<eta>

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

goal (2 subgoals):
 1. polarity = pos \<Longrightarrow> orient_lit_inst L1 t s polarity \<eta>
 2. polarity = neg \<Longrightarrow> orient_lit_inst L1 t s polarity \<eta>
[PROOF STEP]
from this and \<open>polarity = pos\<close> and \<open>L1 = Pos (Eq t s) \<or> L1 = Pos (Eq s t)\<close>
[PROOF STATE]
proof (chain)
picking this:
(t \<lhd> \<eta>, s \<lhd> \<eta>) \<notin> trm_ord
polarity = pos
L1 = Pos (Eq t s) \<or> L1 = Pos (Eq s t)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(t \<lhd> \<eta>, s \<lhd> \<eta>) \<notin> trm_ord
polarity = pos
L1 = Pos (Eq t s) \<or> L1 = Pos (Eq s t)

goal (1 subgoal):
 1. orient_lit_inst L1 t s polarity \<eta>
[PROOF STEP]
unfolding orient_lit_inst_def
[PROOF STATE]
proof (prove)
using this:
(t \<lhd> \<eta>, s \<lhd> \<eta>) \<notin> trm_ord
polarity = pos
L1 = Pos (Eq t s) \<or> L1 = Pos (Eq s t)

goal (1 subgoal):
 1. (L1 = Pos (Eq t s) \<or> L1 = Pos (Eq s t)) \<and> (t \<lhd> \<eta>, s \<lhd> \<eta>) \<notin> trm_ord \<and> polarity = pos \<or> (L1 = Neg (Eq t s) \<or> L1 = Neg (Eq s t)) \<and> (t \<lhd> \<eta>, s \<lhd> \<eta>) \<notin> trm_ord \<and> polarity = neg
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
orient_lit_inst L1 t s polarity \<eta>

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

goal (1 subgoal):
 1. polarity = neg \<Longrightarrow> orient_lit_inst L1 t s polarity \<eta>
[PROOF STEP]
from this and assms(1)
[PROOF STATE]
proof (chain)
picking this:
polarity = neg
orient_lit_inst L1 t s polarity \<sigma>
[PROOF STEP]
have "L1 = Neg (Eq t s) \<or> L1 = Neg (Eq s t)"
      and "( (subst t \<sigma>),  (subst s \<sigma>)) \<notin> trm_ord"
[PROOF STATE]
proof (prove)
using this:
polarity = neg
orient_lit_inst L1 t s polarity \<sigma>

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

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

goal (1 subgoal):
 1. polarity = neg \<Longrightarrow> orient_lit_inst L1 t s polarity \<eta>
[PROOF STEP]
from \<open>L1 = Neg (Eq t s) \<or> L1 = Neg (Eq s t)\<close>
[PROOF STATE]
proof (chain)
picking this:
L1 = Neg (Eq t s) \<or> L1 = Neg (Eq s t)
[PROOF STEP]
have "vars_of t \<subseteq> vars_of_lit L1" and "vars_of s \<subseteq> vars_of_lit L1"
[PROOF STATE]
proof (prove)
using this:
L1 = Neg (Eq t s) \<or> L1 = Neg (Eq s t)

goal (1 subgoal):
 1. vars_of t \<subseteq> vars_of_lit L1 &&& vars_of s \<subseteq> vars_of_lit L1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vars_of t \<subseteq> vars_of_lit L1
vars_of s \<subseteq> vars_of_lit L1

goal (1 subgoal):
 1. polarity = neg \<Longrightarrow> orient_lit_inst L1 t s polarity \<eta>
[PROOF STEP]
from \<open>vars_of t \<subseteq> vars_of_lit L1\<close> and assms(2)
[PROOF STATE]
proof (chain)
picking this:
vars_of t \<subseteq> vars_of_lit L1
coincide_on \<sigma> \<eta> (vars_of_lit L1)
[PROOF STEP]
have "coincide_on \<sigma> \<eta> (vars_of t)"
[PROOF STATE]
proof (prove)
using this:
vars_of t \<subseteq> vars_of_lit L1
coincide_on \<sigma> \<eta> (vars_of_lit L1)

goal (1 subgoal):
 1. coincide_on \<sigma> \<eta> (vars_of t)
[PROOF STEP]
unfolding coincide_on_def
[PROOF STATE]
proof (prove)
using this:
vars_of t \<subseteq> vars_of_lit L1
\<forall>x\<in>vars_of_lit L1. Var x \<lhd> \<sigma> = Var x \<lhd> \<eta>

goal (1 subgoal):
 1. \<forall>x\<in>vars_of t. Var x \<lhd> \<sigma> = Var x \<lhd> \<eta>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
coincide_on \<sigma> \<eta> (vars_of t)

goal (1 subgoal):
 1. polarity = neg \<Longrightarrow> orient_lit_inst L1 t s polarity \<eta>
[PROOF STEP]
from \<open>vars_of s \<subseteq> vars_of_lit L1\<close> and assms(2)
[PROOF STATE]
proof (chain)
picking this:
vars_of s \<subseteq> vars_of_lit L1
coincide_on \<sigma> \<eta> (vars_of_lit L1)
[PROOF STEP]
have "coincide_on \<sigma> \<eta> (vars_of s)"
[PROOF STATE]
proof (prove)
using this:
vars_of s \<subseteq> vars_of_lit L1
coincide_on \<sigma> \<eta> (vars_of_lit L1)

goal (1 subgoal):
 1. coincide_on \<sigma> \<eta> (vars_of s)
[PROOF STEP]
unfolding coincide_on_def
[PROOF STATE]
proof (prove)
using this:
vars_of s \<subseteq> vars_of_lit L1
\<forall>x\<in>vars_of_lit L1. Var x \<lhd> \<sigma> = Var x \<lhd> \<eta>

goal (1 subgoal):
 1. \<forall>x\<in>vars_of s. Var x \<lhd> \<sigma> = Var x \<lhd> \<eta>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
coincide_on \<sigma> \<eta> (vars_of s)

goal (1 subgoal):
 1. polarity = neg \<Longrightarrow> orient_lit_inst L1 t s polarity \<eta>
[PROOF STEP]
from \<open>( (subst t \<sigma>),  (subst s \<sigma>)) \<notin> trm_ord\<close>
      and \<open>coincide_on \<sigma> \<eta> (vars_of t)\<close> and \<open>coincide_on \<sigma> \<eta> (vars_of s)\<close> assms(2)
[PROOF STATE]
proof (chain)
picking this:
(t \<lhd> \<sigma>, s \<lhd> \<sigma>) \<notin> trm_ord
coincide_on \<sigma> \<eta> (vars_of t)
coincide_on \<sigma> \<eta> (vars_of s)
coincide_on \<sigma> \<eta> (vars_of_lit L1)
[PROOF STEP]
have "( (subst t \<eta>),  (subst s \<eta>)) \<notin> trm_ord"
[PROOF STATE]
proof (prove)
using this:
(t \<lhd> \<sigma>, s \<lhd> \<sigma>) \<notin> trm_ord
coincide_on \<sigma> \<eta> (vars_of t)
coincide_on \<sigma> \<eta> (vars_of s)
coincide_on \<sigma> \<eta> (vars_of_lit L1)

goal (1 subgoal):
 1. (t \<lhd> \<eta>, s \<lhd> \<eta>) \<notin> trm_ord
[PROOF STEP]
using coincide_on_term
[PROOF STATE]
proof (prove)
using this:
(t \<lhd> \<sigma>, s \<lhd> \<sigma>) \<notin> trm_ord
coincide_on \<sigma> \<eta> (vars_of t)
coincide_on \<sigma> \<eta> (vars_of s)
coincide_on \<sigma> \<eta> (vars_of_lit L1)
coincide_on ?\<sigma> ?\<eta> (vars_of ?t) \<Longrightarrow> ?t \<lhd> ?\<sigma> = ?t \<lhd> ?\<eta>

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

goal (1 subgoal):
 1. polarity = neg \<Longrightarrow> orient_lit_inst L1 t s polarity \<eta>
[PROOF STEP]
from this and \<open>polarity = neg\<close> and \<open>L1 = Neg (Eq t s) \<or> L1 = Neg (Eq s t)\<close>
[PROOF STATE]
proof (chain)
picking this:
(t \<lhd> \<eta>, s \<lhd> \<eta>) \<notin> trm_ord
polarity = neg
L1 = Neg (Eq t s) \<or> L1 = Neg (Eq s t)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(t \<lhd> \<eta>, s \<lhd> \<eta>) \<notin> trm_ord
polarity = neg
L1 = Neg (Eq t s) \<or> L1 = Neg (Eq s t)

goal (1 subgoal):
 1. orient_lit_inst L1 t s polarity \<eta>
[PROOF STEP]
unfolding orient_lit_inst_def
[PROOF STATE]
proof (prove)
using this:
(t \<lhd> \<eta>, s \<lhd> \<eta>) \<notin> trm_ord
polarity = neg
L1 = Neg (Eq t s) \<or> L1 = Neg (Eq s t)

goal (1 subgoal):
 1. (L1 = Pos (Eq t s) \<or> L1 = Pos (Eq s t)) \<and> (t \<lhd> \<eta>, s \<lhd> \<eta>) \<notin> trm_ord \<and> polarity = pos \<or> (L1 = Neg (Eq t s) \<or> L1 = Neg (Eq s t)) \<and> (t \<lhd> \<eta>, s \<lhd> \<eta>) \<notin> trm_ord \<and> polarity = neg
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
orient_lit_inst L1 t s polarity \<eta>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
orient_lit_inst L1 t s polarity \<eta>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma orient_lit_inst_subterms:
  assumes "orient_lit_inst L t s polarity \<sigma>"
  assumes "u \<in> subterms_of t"
  shows "u \<in> subterms_of_lit L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u \<in> subterms_of_lit L
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. u \<in> subterms_of_lit L
[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. u \<in> subterms_of_lit L
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
polarity = pos \<or> polarity = neg
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
polarity = pos \<or> polarity = neg

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

goal (2 subgoals):
 1. polarity = pos \<Longrightarrow> u \<in> subterms_of_lit L
 2. polarity = neg \<Longrightarrow> u \<in> subterms_of_lit L
[PROOF STEP]
from this and assms(1)
[PROOF STATE]
proof (chain)
picking this:
polarity = pos
orient_lit_inst L t s polarity \<sigma>
[PROOF STEP]
have "L = (Pos (Eq t s)) \<or> L = (Pos (Eq s t))"
[PROOF STATE]
proof (prove)
using this:
polarity = pos
orient_lit_inst L t s polarity \<sigma>

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

goal (1 subgoal):
 1. L = Pos (Eq t s) \<or> L = Pos (Eq s t)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
L = Pos (Eq t s) \<or> L = Pos (Eq s t)

goal (2 subgoals):
 1. polarity = pos \<Longrightarrow> u \<in> subterms_of_lit L
 2. polarity = neg \<Longrightarrow> u \<in> subterms_of_lit L
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
L = Pos (Eq t s) \<or> L = Pos (Eq s t)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
L = Pos (Eq t s) \<or> L = Pos (Eq s t)

goal (1 subgoal):
 1. u \<in> subterms_of_lit L
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. L = Pos (Eq t s) \<Longrightarrow> u \<in> subterms_of_lit L
 2. L = Pos (Eq s t) \<Longrightarrow> u \<in> subterms_of_lit L
[PROOF STEP]
assume "L = (Pos (Eq t s))"
[PROOF STATE]
proof (state)
this:
L = Pos (Eq t s)

goal (2 subgoals):
 1. L = Pos (Eq t s) \<Longrightarrow> u \<in> subterms_of_lit L
 2. L = Pos (Eq s t) \<Longrightarrow> u \<in> subterms_of_lit L
[PROOF STEP]
from this and assms(2)
[PROOF STATE]
proof (chain)
picking this:
L = Pos (Eq t s)
u \<in> subterms_of t
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
L = Pos (Eq t s)
u \<in> subterms_of t

goal (1 subgoal):
 1. u \<in> subterms_of_lit L
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
u \<in> subterms_of_lit L

goal (1 subgoal):
 1. L = Pos (Eq s t) \<Longrightarrow> u \<in> subterms_of_lit L
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. L = Pos (Eq s t) \<Longrightarrow> u \<in> subterms_of_lit L
[PROOF STEP]
assume "L = (Pos (Eq s t))"
[PROOF STATE]
proof (state)
this:
L = Pos (Eq s t)

goal (1 subgoal):
 1. L = Pos (Eq s t) \<Longrightarrow> u \<in> subterms_of_lit L
[PROOF STEP]
from this and assms(2)
[PROOF STATE]
proof (chain)
picking this:
L = Pos (Eq s t)
u \<in> subterms_of t
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
L = Pos (Eq s t)
u \<in> subterms_of t

goal (1 subgoal):
 1. u \<in> subterms_of_lit L
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
u \<in> subterms_of_lit L

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
u \<in> subterms_of_lit L

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

goal (1 subgoal):
 1. polarity = neg \<Longrightarrow> u \<in> subterms_of_lit L
[PROOF STEP]
from this and assms(1)
[PROOF STATE]
proof (chain)
picking this:
polarity = neg
orient_lit_inst L t s polarity \<sigma>
[PROOF STEP]
have "L = (Neg (Eq t s)) \<or> L = (Neg (Eq s t))"
[PROOF STATE]
proof (prove)
using this:
polarity = neg
orient_lit_inst L t s polarity \<sigma>

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

goal (1 subgoal):
 1. L = Neg (Eq t s) \<or> L = Neg (Eq s t)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
L = Neg (Eq t s) \<or> L = Neg (Eq s t)

goal (1 subgoal):
 1. polarity = neg \<Longrightarrow> u \<in> subterms_of_lit L
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
L = Neg (Eq t s) \<or> L = Neg (Eq s t)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
L = Neg (Eq t s) \<or> L = Neg (Eq s t)

goal (1 subgoal):
 1. u \<in> subterms_of_lit L
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. L = Neg (Eq t s) \<Longrightarrow> u \<in> subterms_of_lit L
 2. L = Neg (Eq s t) \<Longrightarrow> u \<in> subterms_of_lit L
[PROOF STEP]
assume "L = (Neg (Eq t s))"
[PROOF STATE]
proof (state)
this:
L = Neg (Eq t s)

goal (2 subgoals):
 1. L = Neg (Eq t s) \<Longrightarrow> u \<in> subterms_of_lit L
 2. L = Neg (Eq s t) \<Longrightarrow> u \<in> subterms_of_lit L
[PROOF STEP]
from this and assms(2)
[PROOF STATE]
proof (chain)
picking this:
L = Neg (Eq t s)
u \<in> subterms_of t
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
L = Neg (Eq t s)
u \<in> subterms_of t

goal (1 subgoal):
 1. u \<in> subterms_of_lit L
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
u \<in> subterms_of_lit L

goal (1 subgoal):
 1. L = Neg (Eq s t) \<Longrightarrow> u \<in> subterms_of_lit L
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. L = Neg (Eq s t) \<Longrightarrow> u \<in> subterms_of_lit L
[PROOF STEP]
assume "L = (Neg (Eq s t))"
[PROOF STATE]
proof (state)
this:
L = Neg (Eq s t)

goal (1 subgoal):
 1. L = Neg (Eq s t) \<Longrightarrow> u \<in> subterms_of_lit L
[PROOF STEP]
from this and assms(2)
[PROOF STATE]
proof (chain)
picking this:
L = Neg (Eq s t)
u \<in> subterms_of t
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
L = Neg (Eq s t)
u \<in> subterms_of t

goal (1 subgoal):
 1. u \<in> subterms_of_lit L
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
u \<in> subterms_of_lit L

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
u \<in> subterms_of_lit L

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
u \<in> subterms_of_lit L

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mset_ecl_and_mset_lit:
  assumes "L \<in> (cl_ecl C)"
  assumes "finite (cl_ecl C)"
  shows "(mset_lit (subst_lit L \<sigma>)) \<in># (mset_ecl (C,\<sigma>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mset_lit (subst_lit L \<sigma>) \<in># mset_ecl (C, \<sigma>)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mset_lit (subst_lit L \<sigma>) \<in># mset_ecl (C, \<sigma>)
[PROOF STEP]
from assms(1) assms(2)
[PROOF STATE]
proof (chain)
picking this:
L \<in> cl_ecl C
finite (cl_ecl C)
[PROOF STEP]
have "L \<in># (mset_set (cl_ecl C))"
[PROOF STATE]
proof (prove)
using this:
L \<in> cl_ecl C
finite (cl_ecl C)

goal (1 subgoal):
 1. L \<in># mset_set (cl_ecl C)
[PROOF STEP]
by (simp)
[PROOF STATE]
proof (state)
this:
L \<in># mset_set (cl_ecl C)

goal (1 subgoal):
 1. mset_lit (subst_lit L \<sigma>) \<in># mset_ecl (C, \<sigma>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
L \<in># mset_set (cl_ecl C)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
L \<in># mset_set (cl_ecl C)

goal (1 subgoal):
 1. mset_lit (subst_lit L \<sigma>) \<in># mset_ecl (C, \<sigma>)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. L \<in># mset_set (cl_ecl C) \<Longrightarrow> mset_lit (subst_lit L \<sigma>) \<in># mset_ecl (C, \<sigma>)
[PROOF STEP]
have f1: "mset_set (cl_ecl C) - {#L#} + {#L#} = mset_set (cl_ecl C)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mset_set (cl_ecl C) - {#L#} + {#L#} = mset_set (cl_ecl C)
[PROOF STEP]
by (meson \<open>L \<in># mset_set (cl_ecl C)\<close> insert_DiffM2)
[PROOF STATE]
proof (state)
this:
mset_set (cl_ecl C) - {#L#} + {#L#} = mset_set (cl_ecl C)

goal (1 subgoal):
 1. L \<in># mset_set (cl_ecl C) \<Longrightarrow> mset_lit (subst_lit L \<sigma>) \<in># mset_ecl (C, \<sigma>)
[PROOF STEP]
have "count {#mset_lit (subst_lit L \<sigma>)#} (mset_lit (subst_lit L \<sigma>)) = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. count {#mset_lit (subst_lit L \<sigma>)#} (mset_lit (subst_lit L \<sigma>)) = 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
count {#mset_lit (subst_lit L \<sigma>)#} (mset_lit (subst_lit L \<sigma>)) = 1

goal (1 subgoal):
 1. L \<in># mset_set (cl_ecl C) \<Longrightarrow> mset_lit (subst_lit L \<sigma>) \<in># mset_ecl (C, \<sigma>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
count {#mset_lit (subst_lit L \<sigma>)#} (mset_lit (subst_lit L \<sigma>)) = 1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
count {#mset_lit (subst_lit L \<sigma>)#} (mset_lit (subst_lit L \<sigma>)) = 1

goal (1 subgoal):
 1. mset_lit (subst_lit L \<sigma>) \<in># mset_ecl (C, \<sigma>)
[PROOF STEP]
by (metis (no_types, lifting) f1 image_mset_add_mset insert_iff mset_ecl.simps set_mset_add_mset_insert union_mset_add_mset_right)
[PROOF STATE]
proof (state)
this:
mset_lit (subst_lit L \<sigma>) \<in># mset_ecl (C, \<sigma>)

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ecl_ord_coincide:
  assumes "coincide_on \<sigma> \<sigma>' (vars_of_cl (cl_ecl C))"
  shows "mset_ecl (C,\<sigma>) = mset_ecl (C,\<sigma>')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mset_ecl (C, \<sigma>) = mset_ecl (C, \<sigma>')
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mset_ecl (C, \<sigma>) = mset_ecl (C, \<sigma>')
[PROOF STEP]
have "\<forall>x. (x \<in> (cl_ecl C) \<longrightarrow> ((subst_lit x \<sigma>) = (subst_lit x \<sigma>')))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x. x \<in> cl_ecl C \<longrightarrow> subst_lit x \<sigma> = subst_lit x \<sigma>'
[PROOF STEP]
proof ((rule allI),(rule impI))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> cl_ecl C \<Longrightarrow> subst_lit x \<sigma> = subst_lit x \<sigma>'
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> cl_ecl C \<Longrightarrow> subst_lit x \<sigma> = subst_lit x \<sigma>'
[PROOF STEP]
assume "x \<in> (cl_ecl C)"
[PROOF STATE]
proof (state)
this:
x \<in> cl_ecl C

goal (1 subgoal):
 1. \<And>x. x \<in> cl_ecl C \<Longrightarrow> subst_lit x \<sigma> = subst_lit x \<sigma>'
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
x \<in> cl_ecl C
[PROOF STEP]
have "vars_of_lit x \<subseteq> (vars_of_cl (cl_ecl C))"
[PROOF STATE]
proof (prove)
using this:
x \<in> cl_ecl C

goal (1 subgoal):
 1. vars_of_lit x \<subseteq> vars_of_cl (cl_ecl C)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vars_of_lit x \<subseteq> vars_of_cl (cl_ecl C)

goal (1 subgoal):
 1. \<And>x. x \<in> cl_ecl C \<Longrightarrow> subst_lit x \<sigma> = subst_lit x \<sigma>'
[PROOF STEP]
from this and assms(1)
[PROOF STATE]
proof (chain)
picking this:
vars_of_lit x \<subseteq> vars_of_cl (cl_ecl C)
coincide_on \<sigma> \<sigma>' (vars_of_cl (cl_ecl C))
[PROOF STEP]
have "coincide_on \<sigma> \<sigma>' (vars_of_lit x)"
[PROOF STATE]
proof (prove)
using this:
vars_of_lit x \<subseteq> vars_of_cl (cl_ecl C)
coincide_on \<sigma> \<sigma>' (vars_of_cl (cl_ecl C))

goal (1 subgoal):
 1. coincide_on \<sigma> \<sigma>' (vars_of_lit x)
[PROOF STEP]
unfolding coincide_on_def
[PROOF STATE]
proof (prove)
using this:
vars_of_lit x \<subseteq> vars_of_cl (cl_ecl C)
\<forall>x\<in>vars_of_cl (cl_ecl C). Var x \<lhd> \<sigma> = Var x \<lhd> \<sigma>'

goal (1 subgoal):
 1. \<forall>x\<in>vars_of_lit x. Var x \<lhd> \<sigma> = Var x \<lhd> \<sigma>'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
coincide_on \<sigma> \<sigma>' (vars_of_lit x)

goal (1 subgoal):
 1. \<And>x. x \<in> cl_ecl C \<Longrightarrow> subst_lit x \<sigma> = subst_lit x \<sigma>'
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
coincide_on \<sigma> \<sigma>' (vars_of_lit x)
[PROOF STEP]
show "((subst_lit x \<sigma>) = (subst_lit x \<sigma>'))"
[PROOF STATE]
proof (prove)
using this:
coincide_on \<sigma> \<sigma>' (vars_of_lit x)

goal (1 subgoal):
 1. subst_lit x \<sigma> = subst_lit x \<sigma>'
[PROOF STEP]
by (simp add: coincide_on_lit)
[PROOF STATE]
proof (state)
this:
subst_lit x \<sigma> = subst_lit x \<sigma>'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>x. x \<in> cl_ecl C \<longrightarrow> subst_lit x \<sigma> = subst_lit x \<sigma>'

goal (1 subgoal):
 1. mset_ecl (C, \<sigma>) = mset_ecl (C, \<sigma>')
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>x. x \<in> cl_ecl C \<longrightarrow> subst_lit x \<sigma> = subst_lit x \<sigma>'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>x. x \<in> cl_ecl C \<longrightarrow> subst_lit x \<sigma> = subst_lit x \<sigma>'

goal (1 subgoal):
 1. mset_ecl (C, \<sigma>) = mset_ecl (C, \<sigma>')
[PROOF STEP]
using equal_image_mset
  [of  "cl_ecl C" "\<lambda>x. (mset_lit (subst_lit x \<sigma>))"  "\<lambda>x. (mset_lit (subst_lit x \<sigma>'))"]
[PROOF STATE]
proof (prove)
using this:
\<forall>x. x \<in> cl_ecl C \<longrightarrow> subst_lit x \<sigma> = subst_lit x \<sigma>'
\<forall>x\<in>cl_ecl C. mset_lit (subst_lit x \<sigma>) = mset_lit (subst_lit x \<sigma>') \<Longrightarrow> {#mset_lit (subst_lit x \<sigma>). x \<in># mset_set (cl_ecl C)#} = {#mset_lit (subst_lit x \<sigma>'). x \<in># mset_set (cl_ecl C)#}

goal (1 subgoal):
 1. mset_ecl (C, \<sigma>) = mset_ecl (C, \<sigma>')
[PROOF STEP]
by (metis  mset_ecl.simps)
[PROOF STATE]
proof (state)
this:
mset_ecl (C, \<sigma>) = mset_ecl (C, \<sigma>')

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mult_trm_ord_trans:
  shows "trans (mult trm_ord)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trans (mult trm_ord)
[PROOF STEP]
by (metis (no_types, lifting)  mult_def transI transitive_closure_trans(2))


[STATEMENT]
lemma lit_ord_trans:
  shows "trans  lit_ord"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trans lit_ord
[PROOF STEP]
by (metis (no_types, lifting) basic_superposition.lit_ord_def basic_superposition_axioms
    case_prodD case_prodI mem_Collect_eq mult_def transI transitive_closure_trans(2))


[STATEMENT]
lemma lit_ord_wf:
  shows "wf lit_ord"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf lit_ord
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. wf lit_ord
[PROOF STEP]
from trm_ord_wf
[PROOF STATE]
proof (chain)
picking this:
wf trm_ord
[PROOF STEP]
have "wf (mult trm_ord)"
[PROOF STATE]
proof (prove)
using this:
wf trm_ord

goal (1 subgoal):
 1. wf (mult trm_ord)
[PROOF STEP]
using wf_mult
[PROOF STATE]
proof (prove)
using this:
wf trm_ord
wf ?r \<Longrightarrow> wf (mult ?r)

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

goal (1 subgoal):
 1. wf lit_ord
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
wf (mult trm_ord)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
wf (mult trm_ord)

goal (1 subgoal):
 1. wf lit_ord
[PROOF STEP]
using lit_ord_def
        and measure_wf [of "(mult trm_ord)" lit_ord mset_lit]
[PROOF STATE]
proof (prove)
using this:
wf (mult trm_ord)
lit_ord = {(x, y). (mset_lit x, mset_lit y) \<in> mult trm_ord}
\<lbrakk>wf (mult trm_ord); lit_ord = {(x, y). (mset_lit x, mset_lit y) \<in> mult trm_ord}\<rbrakk> \<Longrightarrow> wf lit_ord

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mult_mult_trm_ord_trans:
  shows "trans (mult (mult trm_ord))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trans (mult (mult trm_ord))
[PROOF STEP]
by (metis (no_types, lifting)  mult_def transI transitive_closure_trans(2))


[STATEMENT]
lemma ecl_ord_trans:
  shows "trans  ecl_ord"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trans ecl_ord
[PROOF STEP]
by (metis (no_types, lifting) basic_superposition.ecl_ord_def basic_superposition_axioms case_prodD
    case_prodI mem_Collect_eq mult_def transI transitive_closure_trans(2))


[STATEMENT]
lemma cl_ord_trans:
  shows "trans cl_ord"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trans cl_ord
[PROOF STEP]
by (metis (no_types, lifting) basic_superposition.cl_ord_def basic_superposition_axioms case_prodD
    case_prodI mem_Collect_eq mult_def transI transitive_closure_trans(2))