[STATEMENT]
lemma trm_rep_is_lower:
  shows "(t \<noteq> (trm_rep t S)) \<longrightarrow> (((trm_rep t S),t) \<in> trm_ord)" (is "?P t")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t \<noteq> trm_rep t S \<longrightarrow> (trm_rep t S, t) \<in> trm_ord
[PROOF STEP]
proof ((rule wf_induct [of "trm_ord" "?P" "t"]),(simp add: trm_ord_wf))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<forall>y. (y, x) \<in> trm_ord \<longrightarrow> y \<noteq> trm_rep y S \<longrightarrow> (trm_rep y S, y) \<in> trm_ord \<Longrightarrow> x \<noteq> trm_rep x S \<longrightarrow> (trm_rep x S, x) \<in> trm_ord
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<forall>y. (y, x) \<in> trm_ord \<longrightarrow> y \<noteq> trm_rep y S \<longrightarrow> (trm_rep y S, y) \<in> trm_ord \<Longrightarrow> x \<noteq> trm_rep x S \<longrightarrow> (trm_rep x S, x) \<in> trm_ord
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<forall>y. (y, x) \<in> trm_ord \<longrightarrow> y \<noteq> trm_rep y S \<longrightarrow> (trm_rep y S, y) \<in> trm_ord \<Longrightarrow> x \<noteq> trm_rep x S \<longrightarrow> (trm_rep x S, x) \<in> trm_ord
[PROOF STEP]
assume hyp_ind: "\<forall>y. (y,x) \<in> trm_ord \<longrightarrow> (?P y)"
[PROOF STATE]
proof (state)
this:
\<forall>y. (y, x) \<in> trm_ord \<longrightarrow> y \<noteq> trm_rep y S \<longrightarrow> (trm_rep y S, y) \<in> trm_ord

goal (1 subgoal):
 1. \<And>x. \<forall>y. (y, x) \<in> trm_ord \<longrightarrow> y \<noteq> trm_rep y S \<longrightarrow> (trm_rep y S, y) \<in> trm_ord \<Longrightarrow> x \<noteq> trm_rep x S \<longrightarrow> (trm_rep x S, x) \<in> trm_ord
[PROOF STEP]
let ?v = "(Comb (trm_rep (lhs x) S) (trm_rep (rhs x) S))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<forall>y. (y, x) \<in> trm_ord \<longrightarrow> y \<noteq> trm_rep y S \<longrightarrow> (trm_rep y S, y) \<in> trm_ord \<Longrightarrow> x \<noteq> trm_rep x S \<longrightarrow> (trm_rep x S, x) \<in> trm_ord
[PROOF STEP]
show "(?P x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<noteq> trm_rep x S \<longrightarrow> (trm_rep x S, x) \<in> trm_ord
[PROOF STEP]
proof (rule impI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<noteq> trm_rep x S \<Longrightarrow> (trm_rep x S, x) \<in> trm_ord
[PROOF STEP]
assume "x \<noteq> (trm_rep x S)"
[PROOF STATE]
proof (state)
this:
x \<noteq> trm_rep x S

goal (1 subgoal):
 1. x \<noteq> trm_rep x S \<Longrightarrow> (trm_rep x S, x) \<in> trm_ord
[PROOF STEP]
show "((trm_rep x S),x) \<in> trm_ord"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (trm_rep x S, x) \<in> trm_ord
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> (trm_rep x S, x) \<in> trm_ord
 2. \<not> ?P \<Longrightarrow> (trm_rep x S, x) \<in> trm_ord
[PROOF STEP]
assume c1: "subterm_reduction_applicable S x"
[PROOF STATE]
proof (state)
this:
subterm_reduction_applicable S x

goal (2 subgoals):
 1. ?P \<Longrightarrow> (trm_rep x S, x) \<in> trm_ord
 2. \<not> ?P \<Longrightarrow> (trm_rep x S, x) \<in> trm_ord
[PROOF STEP]
from this and hyp_ind
[PROOF STATE]
proof (chain)
picking this:
subterm_reduction_applicable S x
\<forall>y. (y, x) \<in> trm_ord \<longrightarrow> y \<noteq> trm_rep y S \<longrightarrow> (trm_rep y S, y) \<in> trm_ord
[PROOF STEP]
have "(?v,x) \<in> trm_ord"
[PROOF STATE]
proof (prove)
using this:
subterm_reduction_applicable S x
\<forall>y. (y, x) \<in> trm_ord \<longrightarrow> y \<noteq> trm_rep y S \<longrightarrow> (trm_rep y S, y) \<in> trm_ord

goal (1 subgoal):
 1. (trm_rep (lhs x) S \<cdot> trm_rep (rhs x) S, x) \<in> trm_ord
[PROOF STEP]
using trm_rep_is_lower_aux
[PROOF STATE]
proof (prove)
using this:
subterm_reduction_applicable S x
\<forall>y. (y, x) \<in> trm_ord \<longrightarrow> y \<noteq> trm_rep y S \<longrightarrow> (trm_rep y S, y) \<in> trm_ord
\<lbrakk>\<forall>y. (y, ?t) \<in> trm_ord \<longrightarrow> y \<noteq> trm_rep y ?S \<longrightarrow> (trm_rep y ?S, y) \<in> trm_ord; subterm_reduction_applicable ?S ?t\<rbrakk> \<Longrightarrow> (trm_rep (lhs ?t) ?S \<cdot> trm_rep (rhs ?t) ?S, ?t) \<in> trm_ord

goal (1 subgoal):
 1. (trm_rep (lhs x) S \<cdot> trm_rep (rhs x) S, x) \<in> trm_ord
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
(trm_rep (lhs x) S \<cdot> trm_rep (rhs x) S, x) \<in> trm_ord

goal (2 subgoals):
 1. ?P \<Longrightarrow> (trm_rep x S, x) \<in> trm_ord
 2. \<not> ?P \<Longrightarrow> (trm_rep x S, x) \<in> trm_ord
[PROOF STEP]
from c1 and hyp_ind
[PROOF STATE]
proof (chain)
picking this:
subterm_reduction_applicable S x
\<forall>y. (y, x) \<in> trm_ord \<longrightarrow> y \<noteq> trm_rep y S \<longrightarrow> (trm_rep y S, y) \<in> trm_ord
[PROOF STEP]
have "(trm_rep x S) = (subterm_reduction S x)"
[PROOF STATE]
proof (prove)
using this:
subterm_reduction_applicable S x
\<forall>y. (y, x) \<in> trm_ord \<longrightarrow> y \<noteq> trm_rep y S \<longrightarrow> (trm_rep y S, y) \<in> trm_ord

goal (1 subgoal):
 1. trm_rep x S = subterm_reduction S x
[PROOF STEP]
using trm_rep_aux_def [of x S]
[PROOF STATE]
proof (prove)
using this:
subterm_reduction_applicable S x
\<forall>y. (y, x) \<in> trm_ord \<longrightarrow> y \<noteq> trm_rep y S \<longrightarrow> (trm_rep y S, y) \<in> trm_ord
\<forall>y. (y, x) \<in> trm_ord \<longrightarrow> y \<noteq> trm_rep y S \<longrightarrow> (trm_rep y S, y) \<in> trm_ord \<Longrightarrow> trm_rep x S = (if subterm_reduction_applicable S x then subterm_reduction S x else get_min x (set_of_candidate_values S x))

goal (1 subgoal):
 1. trm_rep x S = subterm_reduction S x
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
trm_rep x S = subterm_reduction S x

goal (2 subgoals):
 1. ?P \<Longrightarrow> (trm_rep x S, x) \<in> trm_ord
 2. \<not> ?P \<Longrightarrow> (trm_rep x S, x) \<in> trm_ord
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
trm_rep x S = subterm_reduction S x
[PROOF STEP]
have "(trm_rep x S) = (trm_rep ?v S)"
[PROOF STATE]
proof (prove)
using this:
trm_rep x S = subterm_reduction S x

goal (1 subgoal):
 1. trm_rep x S = trm_rep (trm_rep (lhs x) S \<cdot> trm_rep (rhs x) S) S
[PROOF STEP]
unfolding subterm_reduction_def
[PROOF STATE]
proof (prove)
using this:
trm_rep x S = trm_rep (trm_rep (lhs x) S \<cdot> trm_rep (rhs x) S) S

goal (1 subgoal):
 1. trm_rep x S = trm_rep (trm_rep (lhs x) S \<cdot> trm_rep (rhs x) S) S
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
trm_rep x S = trm_rep (trm_rep (lhs x) S \<cdot> trm_rep (rhs x) S) S

goal (2 subgoals):
 1. ?P \<Longrightarrow> (trm_rep x S, x) \<in> trm_ord
 2. \<not> ?P \<Longrightarrow> (trm_rep x S, x) \<in> trm_ord
[PROOF STEP]
from \<open>(?v,x) \<in> trm_ord\<close> and hyp_ind
[PROOF STATE]
proof (chain)
picking this:
(trm_rep (lhs x) S \<cdot> trm_rep (rhs x) S, x) \<in> trm_ord
\<forall>y. (y, x) \<in> trm_ord \<longrightarrow> y \<noteq> trm_rep y S \<longrightarrow> (trm_rep y S, y) \<in> trm_ord
[PROOF STEP]
have "?P ?v"
[PROOF STATE]
proof (prove)
using this:
(trm_rep (lhs x) S \<cdot> trm_rep (rhs x) S, x) \<in> trm_ord
\<forall>y. (y, x) \<in> trm_ord \<longrightarrow> y \<noteq> trm_rep y S \<longrightarrow> (trm_rep y S, y) \<in> trm_ord

goal (1 subgoal):
 1. trm_rep (lhs x) S \<cdot> trm_rep (rhs x) S \<noteq> trm_rep (trm_rep (lhs x) S \<cdot> trm_rep (rhs x) S) S \<longrightarrow> (trm_rep (trm_rep (lhs x) S \<cdot> trm_rep (rhs x) S) S, trm_rep (lhs x) S \<cdot> trm_rep (rhs x) S) \<in> trm_ord
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
trm_rep (lhs x) S \<cdot> trm_rep (rhs x) S \<noteq> trm_rep (trm_rep (lhs x) S \<cdot> trm_rep (rhs x) S) S \<longrightarrow> (trm_rep (trm_rep (lhs x) S \<cdot> trm_rep (rhs x) S) S, trm_rep (lhs x) S \<cdot> trm_rep (rhs x) S) \<in> trm_ord

goal (2 subgoals):
 1. ?P \<Longrightarrow> (trm_rep x S, x) \<in> trm_ord
 2. \<not> ?P \<Longrightarrow> (trm_rep x S, x) \<in> trm_ord
[PROOF STEP]
from this and \<open>(trm_rep x S) = (trm_rep ?v S)\<close>
[PROOF STATE]
proof (chain)
picking this:
trm_rep (lhs x) S \<cdot> trm_rep (rhs x) S \<noteq> trm_rep (trm_rep (lhs x) S \<cdot> trm_rep (rhs x) S) S \<longrightarrow> (trm_rep (trm_rep (lhs x) S \<cdot> trm_rep (rhs x) S) S, trm_rep (lhs x) S \<cdot> trm_rep (rhs x) S) \<in> trm_ord
trm_rep x S = trm_rep (trm_rep (lhs x) S \<cdot> trm_rep (rhs x) S) S
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
trm_rep (lhs x) S \<cdot> trm_rep (rhs x) S \<noteq> trm_rep (trm_rep (lhs x) S \<cdot> trm_rep (rhs x) S) S \<longrightarrow> (trm_rep (trm_rep (lhs x) S \<cdot> trm_rep (rhs x) S) S, trm_rep (lhs x) S \<cdot> trm_rep (rhs x) S) \<in> trm_ord
trm_rep x S = trm_rep (trm_rep (lhs x) S \<cdot> trm_rep (rhs x) S) S

goal (1 subgoal):
 1. (trm_rep x S, x) \<in> trm_ord
[PROOF STEP]
by (metis \<open>(trm_rep (lhs x) S \<cdot> trm_rep (rhs x) S, x) \<in> trm_ord\<close> trm_ord_trans transE)
[PROOF STATE]
proof (state)
this:
(trm_rep x S, x) \<in> trm_ord

goal (1 subgoal):
 1. \<not> subterm_reduction_applicable S x \<Longrightarrow> (trm_rep x S, x) \<in> trm_ord
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> subterm_reduction_applicable S x \<Longrightarrow> (trm_rep x S, x) \<in> trm_ord
[PROOF STEP]
assume c2: "\<not>subterm_reduction_applicable S x"
[PROOF STATE]
proof (state)
this:
\<not> subterm_reduction_applicable S x

goal (1 subgoal):
 1. \<not> subterm_reduction_applicable S x \<Longrightarrow> (trm_rep x S, x) \<in> trm_ord
[PROOF STEP]
from c2 and hyp_ind
[PROOF STATE]
proof (chain)
picking this:
\<not> subterm_reduction_applicable S x
\<forall>y. (y, x) \<in> trm_ord \<longrightarrow> y \<noteq> trm_rep y S \<longrightarrow> (trm_rep y S, y) \<in> trm_ord
[PROOF STEP]
have "(trm_rep x S) = (get_min x (set_of_candidate_values S x))"
[PROOF STATE]
proof (prove)
using this:
\<not> subterm_reduction_applicable S x
\<forall>y. (y, x) \<in> trm_ord \<longrightarrow> y \<noteq> trm_rep y S \<longrightarrow> (trm_rep y S, y) \<in> trm_ord

goal (1 subgoal):
 1. trm_rep x S = get_min x (set_of_candidate_values S x)
[PROOF STEP]
using trm_rep_aux_def [of x S]
[PROOF STATE]
proof (prove)
using this:
\<not> subterm_reduction_applicable S x
\<forall>y. (y, x) \<in> trm_ord \<longrightarrow> y \<noteq> trm_rep y S \<longrightarrow> (trm_rep y S, y) \<in> trm_ord
\<forall>y. (y, x) \<in> trm_ord \<longrightarrow> y \<noteq> trm_rep y S \<longrightarrow> (trm_rep y S, y) \<in> trm_ord \<Longrightarrow> trm_rep x S = (if subterm_reduction_applicable S x then subterm_reduction S x else get_min x (set_of_candidate_values S x))

goal (1 subgoal):
 1. trm_rep x S = get_min x (set_of_candidate_values S x)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
trm_rep x S = get_min x (set_of_candidate_values S x)

goal (1 subgoal):
 1. \<not> subterm_reduction_applicable S x \<Longrightarrow> (trm_rep x S, x) \<in> trm_ord
[PROOF STEP]
from this and \<open>x \<noteq> (trm_rep x S)\<close>
[PROOF STATE]
proof (chain)
picking this:
trm_rep x S = get_min x (set_of_candidate_values S x)
x \<noteq> trm_rep x S
[PROOF STEP]
have "(trm_rep x S) \<in> (min_trms (set_of_candidate_values S x))"
[PROOF STATE]
proof (prove)
using this:
trm_rep x S = get_min x (set_of_candidate_values S x)
x \<noteq> trm_rep x S

goal (1 subgoal):
 1. trm_rep x S \<in> min_trms (set_of_candidate_values S x)
[PROOF STEP]
unfolding get_min_def
[PROOF STATE]
proof (prove)
using this:
trm_rep x S = (if min_trms (set_of_candidate_values S x) = {} then x else SOME xa. xa \<in> min_trms (set_of_candidate_values S x))
x \<noteq> trm_rep x S

goal (1 subgoal):
 1. trm_rep x S \<in> min_trms (set_of_candidate_values S x)
[PROOF STEP]
by (metis (full_types) some_in_eq)
[PROOF STATE]
proof (state)
this:
trm_rep x S \<in> min_trms (set_of_candidate_values S x)

goal (1 subgoal):
 1. \<not> subterm_reduction_applicable S x \<Longrightarrow> (trm_rep x S, x) \<in> trm_ord
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
trm_rep x S \<in> min_trms (set_of_candidate_values S x)
[PROOF STEP]
obtain pair where  "pair \<in> (set_of_candidate_values S x)" "(trm_rep x S) = fst pair"
[PROOF STATE]
proof (prove)
using this:
trm_rep x S \<in> min_trms (set_of_candidate_values S x)

goal (1 subgoal):
 1. (\<And>pair. \<lbrakk>pair \<in> set_of_candidate_values S x; trm_rep x S = fst pair\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding min_trms_def
[PROOF STATE]
proof (prove)
using this:
trm_rep x S \<in> {xa. \<exists>pair. (pair \<in> set_of_candidate_values S x \<and> (\<forall>pair'\<in>set_of_candidate_values S x. (snd pair', snd pair) \<notin> trm_ord)) \<and> xa = fst pair}

goal (1 subgoal):
 1. (\<And>pair. \<lbrakk>pair \<in> set_of_candidate_values S x; trm_rep x S = fst pair\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
pair \<in> set_of_candidate_values S x
trm_rep x S = fst pair

goal (1 subgoal):
 1. \<not> subterm_reduction_applicable S x \<Longrightarrow> (trm_rep x S, x) \<in> trm_ord
[PROOF STEP]
from \<open>pair \<in> (set_of_candidate_values S x)\<close>
[PROOF STATE]
proof (chain)
picking this:
pair \<in> set_of_candidate_values S x
[PROOF STEP]
have
          "\<exists> CC C' C  L L' \<sigma> t' s'. candidate_values (fst pair) CC C' C (snd pair) L L' \<sigma> t' s' x S"
[PROOF STATE]
proof (prove)
using this:
pair \<in> set_of_candidate_values S x

goal (1 subgoal):
 1. \<exists>CC C' C L L' \<sigma> t' s'. candidate_values (fst pair) CC C' C (snd pair) L L' \<sigma> t' s' x S
[PROOF STEP]
unfolding set_of_candidate_values_def
[PROOF STATE]
proof (prove)
using this:
pair \<in> {pair. \<exists>z CC C' C s L L' \<sigma> t' s'. pair = (z, s) \<and> candidate_values z CC C' C s L L' \<sigma> t' s' x S}

goal (1 subgoal):
 1. \<exists>CC C' C L L' \<sigma> t' s'. candidate_values (fst pair) CC C' C (snd pair) L L' \<sigma> t' s' x S
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<exists>CC C' C L L' \<sigma> t' s'. candidate_values (fst pair) CC C' C (snd pair) L L' \<sigma> t' s' x S

goal (1 subgoal):
 1. \<not> subterm_reduction_applicable S x \<Longrightarrow> (trm_rep x S, x) \<in> trm_ord
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
\<exists>CC C' C L L' \<sigma> t' s'. candidate_values (fst pair) CC C' C (snd pair) L L' \<sigma> t' s' x S
[PROOF STEP]
have "(snd pair,x) \<in> trm_ord"
[PROOF STATE]
proof (prove)
using this:
\<exists>CC C' C L L' \<sigma> t' s'. candidate_values (fst pair) CC C' C (snd pair) L L' \<sigma> t' s' x S

goal (1 subgoal):
 1. (snd pair, x) \<in> trm_ord
[PROOF STEP]
unfolding candidate_values_def
[PROOF STATE]
proof (prove)
using this:
\<exists>CC C' C L L' \<sigma> t' s'. CC \<in> S \<and> x \<notin> subst_set (trms_ecl CC) \<sigma> \<and> trms_irreducible CC \<sigma> S x \<and> C' = cl_ecl CC \<and> (snd pair, x) \<in> trm_ord \<and> ((snd pair, x) \<in> trm_ord \<longrightarrow> fst pair = trm_rep (snd pair) S) \<and> orient_lit_inst L' t' s' pos \<sigma> \<and> sel C' = {} \<and> L' \<in> C' \<and> maximal_literal L C \<and> L = subst_lit L' \<sigma> \<and> C = subst_cl C' \<sigma> \<and> ground_clause C \<and> x = t' \<lhd> \<sigma> \<and> snd pair = s' \<lhd> \<sigma> \<and> finite C' \<and> smaller_lits_are_false x C S \<and> maximal_literal_is_unique x (snd pair) C' L' S \<sigma>

goal (1 subgoal):
 1. (snd pair, x) \<in> trm_ord
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(snd pair, x) \<in> trm_ord

goal (1 subgoal):
 1. \<not> subterm_reduction_applicable S x \<Longrightarrow> (trm_rep x S, x) \<in> trm_ord
[PROOF STEP]
from
          \<open>\<exists> CC C' C  L L' \<sigma> t' s'. candidate_values (fst pair) CC C' C (snd pair) L L' \<sigma> t' s' x S\<close>
[PROOF STATE]
proof (chain)
picking this:
\<exists>CC C' C L L' \<sigma> t' s'. candidate_values (fst pair) CC C' C (snd pair) L L' \<sigma> t' s' x S
[PROOF STEP]
have "((snd pair, x) \<in> trm_ord \<longrightarrow> fst pair = trm_rep (snd pair) S)"
[PROOF STATE]
proof (prove)
using this:
\<exists>CC C' C L L' \<sigma> t' s'. candidate_values (fst pair) CC C' C (snd pair) L L' \<sigma> t' s' x S

goal (1 subgoal):
 1. (snd pair, x) \<in> trm_ord \<longrightarrow> fst pair = trm_rep (snd pair) S
[PROOF STEP]
unfolding candidate_values_def
[PROOF STATE]
proof (prove)
using this:
\<exists>CC C' C L L' \<sigma> t' s'. CC \<in> S \<and> x \<notin> subst_set (trms_ecl CC) \<sigma> \<and> trms_irreducible CC \<sigma> S x \<and> C' = cl_ecl CC \<and> (snd pair, x) \<in> trm_ord \<and> ((snd pair, x) \<in> trm_ord \<longrightarrow> fst pair = trm_rep (snd pair) S) \<and> orient_lit_inst L' t' s' pos \<sigma> \<and> sel C' = {} \<and> L' \<in> C' \<and> maximal_literal L C \<and> L = subst_lit L' \<sigma> \<and> C = subst_cl C' \<sigma> \<and> ground_clause C \<and> x = t' \<lhd> \<sigma> \<and> snd pair = s' \<lhd> \<sigma> \<and> finite C' \<and> smaller_lits_are_false x C S \<and> maximal_literal_is_unique x (snd pair) C' L' S \<sigma>

goal (1 subgoal):
 1. (snd pair, x) \<in> trm_ord \<longrightarrow> fst pair = trm_rep (snd pair) S
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(snd pair, x) \<in> trm_ord \<longrightarrow> fst pair = trm_rep (snd pair) S

goal (1 subgoal):
 1. \<not> subterm_reduction_applicable S x \<Longrightarrow> (trm_rep x S, x) \<in> trm_ord
[PROOF STEP]
from \<open>(snd pair,x) \<in> trm_ord\<close> \<open>((snd pair, x) \<in> trm_ord \<longrightarrow> fst pair = trm_rep (snd pair) S)\<close>
[PROOF STATE]
proof (chain)
picking this:
(snd pair, x) \<in> trm_ord
(snd pair, x) \<in> trm_ord \<longrightarrow> fst pair = trm_rep (snd pair) S
[PROOF STEP]
have "fst pair = trm_rep (snd pair) S"
[PROOF STATE]
proof (prove)
using this:
(snd pair, x) \<in> trm_ord
(snd pair, x) \<in> trm_ord \<longrightarrow> fst pair = trm_rep (snd pair) S

goal (1 subgoal):
 1. fst pair = trm_rep (snd pair) S
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
fst pair = trm_rep (snd pair) S

goal (1 subgoal):
 1. \<not> subterm_reduction_applicable S x \<Longrightarrow> (trm_rep x S, x) \<in> trm_ord
[PROOF STEP]
from \<open>(snd pair,x) \<in> trm_ord\<close> and hyp_ind
[PROOF STATE]
proof (chain)
picking this:
(snd pair, x) \<in> trm_ord
\<forall>y. (y, x) \<in> trm_ord \<longrightarrow> y \<noteq> trm_rep y S \<longrightarrow> (trm_rep y S, y) \<in> trm_ord
[PROOF STEP]
have "(?P (snd pair))"
[PROOF STATE]
proof (prove)
using this:
(snd pair, x) \<in> trm_ord
\<forall>y. (y, x) \<in> trm_ord \<longrightarrow> y \<noteq> trm_rep y S \<longrightarrow> (trm_rep y S, y) \<in> trm_ord

goal (1 subgoal):
 1. snd pair \<noteq> trm_rep (snd pair) S \<longrightarrow> (trm_rep (snd pair) S, snd pair) \<in> trm_ord
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
snd pair \<noteq> trm_rep (snd pair) S \<longrightarrow> (trm_rep (snd pair) S, snd pair) \<in> trm_ord

goal (1 subgoal):
 1. \<not> subterm_reduction_applicable S x \<Longrightarrow> (trm_rep x S, x) \<in> trm_ord
[PROOF STEP]
from this and \<open>fst pair = (trm_rep (snd pair) S)\<close>
[PROOF STATE]
proof (chain)
picking this:
snd pair \<noteq> trm_rep (snd pair) S \<longrightarrow> (trm_rep (snd pair) S, snd pair) \<in> trm_ord
fst pair = trm_rep (snd pair) S
[PROOF STEP]
have "fst pair = snd pair \<or> (fst pair,snd pair) \<in> trm_ord"
[PROOF STATE]
proof (prove)
using this:
snd pair \<noteq> trm_rep (snd pair) S \<longrightarrow> (trm_rep (snd pair) S, snd pair) \<in> trm_ord
fst pair = trm_rep (snd pair) S

goal (1 subgoal):
 1. fst pair = snd pair \<or> (fst pair, snd pair) \<in> trm_ord
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
fst pair = snd pair \<or> (fst pair, snd pair) \<in> trm_ord

goal (1 subgoal):
 1. \<not> subterm_reduction_applicable S x \<Longrightarrow> (trm_rep x S, x) \<in> trm_ord
[PROOF STEP]
from this and \<open>(trm_rep x S) = fst pair\<close> and \<open>(snd pair,x) \<in> trm_ord\<close> \<open>x \<noteq> (trm_rep x S)\<close>
[PROOF STATE]
proof (chain)
picking this:
fst pair = snd pair \<or> (fst pair, snd pair) \<in> trm_ord
trm_rep x S = fst pair
(snd pair, x) \<in> trm_ord
x \<noteq> trm_rep x S
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
fst pair = snd pair \<or> (fst pair, snd pair) \<in> trm_ord
trm_rep x S = fst pair
(snd pair, x) \<in> trm_ord
x \<noteq> trm_rep x S

goal (1 subgoal):
 1. (trm_rep x S, x) \<in> trm_ord
[PROOF STEP]
by (metis trm_ord_trans transD)
[PROOF STATE]
proof (state)
this:
(trm_rep x S, x) \<in> trm_ord

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(trm_rep x S, x) \<in> trm_ord

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
x \<noteq> trm_rep x S \<longrightarrow> (trm_rep x S, x) \<in> trm_ord

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma trm_rep_is_lower_subt_red:
  assumes "(subterm_reduction_applicable S x)"
  shows "((trm_rep x S),x) \<in> trm_ord"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (trm_rep x S, x) \<in> trm_ord
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (trm_rep x S, x) \<in> trm_ord
[PROOF STEP]
let ?v = "(Comb (trm_rep (lhs x) S) (trm_rep (rhs x) S))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (trm_rep x S, x) \<in> trm_ord
[PROOF STEP]
from assms(1)
[PROOF STATE]
proof (chain)
picking this:
subterm_reduction_applicable S x
[PROOF STEP]
have "(?v,x) \<in> trm_ord"
[PROOF STATE]
proof (prove)
using this:
subterm_reduction_applicable S x

goal (1 subgoal):
 1. (trm_rep (lhs x) S \<cdot> trm_rep (rhs x) S, x) \<in> trm_ord
[PROOF STEP]
using trm_rep_is_lower_aux trm_rep_is_lower
[PROOF STATE]
proof (prove)
using this:
subterm_reduction_applicable S x
\<lbrakk>\<forall>y. (y, ?t) \<in> trm_ord \<longrightarrow> y \<noteq> trm_rep y ?S \<longrightarrow> (trm_rep y ?S, y) \<in> trm_ord; subterm_reduction_applicable ?S ?t\<rbrakk> \<Longrightarrow> (trm_rep (lhs ?t) ?S \<cdot> trm_rep (rhs ?t) ?S, ?t) \<in> trm_ord
?t \<noteq> trm_rep ?t ?S \<longrightarrow> (trm_rep ?t ?S, ?t) \<in> trm_ord

goal (1 subgoal):
 1. (trm_rep (lhs x) S \<cdot> trm_rep (rhs x) S, x) \<in> trm_ord
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
(trm_rep (lhs x) S \<cdot> trm_rep (rhs x) S, x) \<in> trm_ord

goal (1 subgoal):
 1. (trm_rep x S, x) \<in> trm_ord
[PROOF STEP]
from assms(1)
[PROOF STATE]
proof (chain)
picking this:
subterm_reduction_applicable S x
[PROOF STEP]
have "(trm_rep x S) = (subterm_reduction S x)"
[PROOF STATE]
proof (prove)
using this:
subterm_reduction_applicable S x

goal (1 subgoal):
 1. trm_rep x S = subterm_reduction S x
[PROOF STEP]
using trm_rep_aux_def [of x S] trm_rep_is_lower
[PROOF STATE]
proof (prove)
using this:
subterm_reduction_applicable S x
\<forall>y. (y, x) \<in> trm_ord \<longrightarrow> y \<noteq> trm_rep y S \<longrightarrow> (trm_rep y S, y) \<in> trm_ord \<Longrightarrow> trm_rep x S = (if subterm_reduction_applicable S x then subterm_reduction S x else get_min x (set_of_candidate_values S x))
?t \<noteq> trm_rep ?t ?S \<longrightarrow> (trm_rep ?t ?S, ?t) \<in> trm_ord

goal (1 subgoal):
 1. trm_rep x S = subterm_reduction S x
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
trm_rep x S = subterm_reduction S x

goal (1 subgoal):
 1. (trm_rep x S, x) \<in> trm_ord
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
trm_rep x S = subterm_reduction S x
[PROOF STEP]
have "(trm_rep x S) = (trm_rep ?v S)"
[PROOF STATE]
proof (prove)
using this:
trm_rep x S = subterm_reduction S x

goal (1 subgoal):
 1. trm_rep x S = trm_rep (trm_rep (lhs x) S \<cdot> trm_rep (rhs x) S) S
[PROOF STEP]
unfolding subterm_reduction_def
[PROOF STATE]
proof (prove)
using this:
trm_rep x S = trm_rep (trm_rep (lhs x) S \<cdot> trm_rep (rhs x) S) S

goal (1 subgoal):
 1. trm_rep x S = trm_rep (trm_rep (lhs x) S \<cdot> trm_rep (rhs x) S) S
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
trm_rep x S = trm_rep (trm_rep (lhs x) S \<cdot> trm_rep (rhs x) S) S

goal (1 subgoal):
 1. (trm_rep x S, x) \<in> trm_ord
[PROOF STEP]
have "?v = trm_rep ?v S \<or> (trm_rep ?v S,?v) \<in> trm_ord"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trm_rep (lhs x) S \<cdot> trm_rep (rhs x) S = trm_rep (trm_rep (lhs x) S \<cdot> trm_rep (rhs x) S) S \<or> (trm_rep (trm_rep (lhs x) S \<cdot> trm_rep (rhs x) S) S, trm_rep (lhs x) S \<cdot> trm_rep (rhs x) S) \<in> trm_ord
[PROOF STEP]
using trm_rep_is_lower
[PROOF STATE]
proof (prove)
using this:
?t \<noteq> trm_rep ?t ?S \<longrightarrow> (trm_rep ?t ?S, ?t) \<in> trm_ord

goal (1 subgoal):
 1. trm_rep (lhs x) S \<cdot> trm_rep (rhs x) S = trm_rep (trm_rep (lhs x) S \<cdot> trm_rep (rhs x) S) S \<or> (trm_rep (trm_rep (lhs x) S \<cdot> trm_rep (rhs x) S) S, trm_rep (lhs x) S \<cdot> trm_rep (rhs x) S) \<in> trm_ord
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
trm_rep (lhs x) S \<cdot> trm_rep (rhs x) S = trm_rep (trm_rep (lhs x) S \<cdot> trm_rep (rhs x) S) S \<or> (trm_rep (trm_rep (lhs x) S \<cdot> trm_rep (rhs x) S) S, trm_rep (lhs x) S \<cdot> trm_rep (rhs x) S) \<in> trm_ord

goal (1 subgoal):
 1. (trm_rep x S, x) \<in> trm_ord
[PROOF STEP]
from this and \<open>(trm_rep x S) = (trm_rep ?v S)\<close>
[PROOF STATE]
proof (chain)
picking this:
trm_rep (lhs x) S \<cdot> trm_rep (rhs x) S = trm_rep (trm_rep (lhs x) S \<cdot> trm_rep (rhs x) S) S \<or> (trm_rep (trm_rep (lhs x) S \<cdot> trm_rep (rhs x) S) S, trm_rep (lhs x) S \<cdot> trm_rep (rhs x) S) \<in> trm_ord
trm_rep x S = trm_rep (trm_rep (lhs x) S \<cdot> trm_rep (rhs x) S) S
[PROOF STEP]
show "(((trm_rep x S),x) \<in> trm_ord)"
[PROOF STATE]
proof (prove)
using this:
trm_rep (lhs x) S \<cdot> trm_rep (rhs x) S = trm_rep (trm_rep (lhs x) S \<cdot> trm_rep (rhs x) S) S \<or> (trm_rep (trm_rep (lhs x) S \<cdot> trm_rep (rhs x) S) S, trm_rep (lhs x) S \<cdot> trm_rep (rhs x) S) \<in> trm_ord
trm_rep x S = trm_rep (trm_rep (lhs x) S \<cdot> trm_rep (rhs x) S) S

goal (1 subgoal):
 1. (trm_rep x S, x) \<in> trm_ord
[PROOF STEP]
by (metis \<open>(trm_rep (lhs x) S \<cdot> trm_rep (rhs x) S, x) \<in> trm_ord\<close> trm_ord_trans transE)
[PROOF STATE]
proof (state)
this:
(trm_rep x S, x) \<in> trm_ord

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma trm_rep_is_lower_root_red:
  assumes "\<not>(subterm_reduction_applicable S x)"
  assumes "min_trms (set_of_candidate_values S x) \<noteq> {}"
  shows "(((trm_rep x S),x) \<in> trm_ord)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (trm_rep x S, x) \<in> trm_ord
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (trm_rep x S, x) \<in> trm_ord
[PROOF STEP]
from assms(1)
[PROOF STATE]
proof (chain)
picking this:
\<not> subterm_reduction_applicable S x
[PROOF STEP]
have "(trm_rep x S) = (get_min x (set_of_candidate_values S x))"
[PROOF STATE]
proof (prove)
using this:
\<not> subterm_reduction_applicable S x

goal (1 subgoal):
 1. trm_rep x S = get_min x (set_of_candidate_values S x)
[PROOF STEP]
using trm_rep_aux_def [of x S] trm_rep_is_lower
[PROOF STATE]
proof (prove)
using this:
\<not> subterm_reduction_applicable S x
\<forall>y. (y, x) \<in> trm_ord \<longrightarrow> y \<noteq> trm_rep y S \<longrightarrow> (trm_rep y S, y) \<in> trm_ord \<Longrightarrow> trm_rep x S = (if subterm_reduction_applicable S x then subterm_reduction S x else get_min x (set_of_candidate_values S x))
?t \<noteq> trm_rep ?t ?S \<longrightarrow> (trm_rep ?t ?S, ?t) \<in> trm_ord

goal (1 subgoal):
 1. trm_rep x S = get_min x (set_of_candidate_values S x)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
trm_rep x S = get_min x (set_of_candidate_values S x)

goal (1 subgoal):
 1. (trm_rep x S, x) \<in> trm_ord
[PROOF STEP]
from this and assms(2)
[PROOF STATE]
proof (chain)
picking this:
trm_rep x S = get_min x (set_of_candidate_values S x)
min_trms (set_of_candidate_values S x) \<noteq> {}
[PROOF STEP]
have "(trm_rep x S) \<in> (min_trms (set_of_candidate_values S x))"
[PROOF STATE]
proof (prove)
using this:
trm_rep x S = get_min x (set_of_candidate_values S x)
min_trms (set_of_candidate_values S x) \<noteq> {}

goal (1 subgoal):
 1. trm_rep x S \<in> min_trms (set_of_candidate_values S x)
[PROOF STEP]
unfolding get_min_def
[PROOF STATE]
proof (prove)
using this:
trm_rep x S = (if min_trms (set_of_candidate_values S x) = {} then x else SOME xa. xa \<in> min_trms (set_of_candidate_values S x))
min_trms (set_of_candidate_values S x) \<noteq> {}

goal (1 subgoal):
 1. trm_rep x S \<in> min_trms (set_of_candidate_values S x)
[PROOF STEP]
by (metis (full_types) some_in_eq)
[PROOF STATE]
proof (state)
this:
trm_rep x S \<in> min_trms (set_of_candidate_values S x)

goal (1 subgoal):
 1. (trm_rep x S, x) \<in> trm_ord
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
trm_rep x S \<in> min_trms (set_of_candidate_values S x)
[PROOF STEP]
obtain pair where  "pair \<in> (set_of_candidate_values S x)" and "(trm_rep x S) = fst pair"
[PROOF STATE]
proof (prove)
using this:
trm_rep x S \<in> min_trms (set_of_candidate_values S x)

goal (1 subgoal):
 1. (\<And>pair. \<lbrakk>pair \<in> set_of_candidate_values S x; trm_rep x S = fst pair\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding min_trms_def
[PROOF STATE]
proof (prove)
using this:
trm_rep x S \<in> {xa. \<exists>pair. (pair \<in> set_of_candidate_values S x \<and> (\<forall>pair'\<in>set_of_candidate_values S x. (snd pair', snd pair) \<notin> trm_ord)) \<and> xa = fst pair}

goal (1 subgoal):
 1. (\<And>pair. \<lbrakk>pair \<in> set_of_candidate_values S x; trm_rep x S = fst pair\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
pair \<in> set_of_candidate_values S x
trm_rep x S = fst pair

goal (1 subgoal):
 1. (trm_rep x S, x) \<in> trm_ord
[PROOF STEP]
from \<open>pair \<in> (set_of_candidate_values S x)\<close>
[PROOF STATE]
proof (chain)
picking this:
pair \<in> set_of_candidate_values S x
[PROOF STEP]
have "\<exists> CC C' C  L L' \<sigma> t' s'. candidate_values (fst pair) CC C' C (snd pair) L L' \<sigma> t' s' x S"
[PROOF STATE]
proof (prove)
using this:
pair \<in> set_of_candidate_values S x

goal (1 subgoal):
 1. \<exists>CC C' C L L' \<sigma> t' s'. candidate_values (fst pair) CC C' C (snd pair) L L' \<sigma> t' s' x S
[PROOF STEP]
unfolding set_of_candidate_values_def
[PROOF STATE]
proof (prove)
using this:
pair \<in> {pair. \<exists>z CC C' C s L L' \<sigma> t' s'. pair = (z, s) \<and> candidate_values z CC C' C s L L' \<sigma> t' s' x S}

goal (1 subgoal):
 1. \<exists>CC C' C L L' \<sigma> t' s'. candidate_values (fst pair) CC C' C (snd pair) L L' \<sigma> t' s' x S
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<exists>CC C' C L L' \<sigma> t' s'. candidate_values (fst pair) CC C' C (snd pair) L L' \<sigma> t' s' x S

goal (1 subgoal):
 1. (trm_rep x S, x) \<in> trm_ord
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
\<exists>CC C' C L L' \<sigma> t' s'. candidate_values (fst pair) CC C' C (snd pair) L L' \<sigma> t' s' x S
[PROOF STEP]
have "(snd pair,x) \<in> trm_ord"
[PROOF STATE]
proof (prove)
using this:
\<exists>CC C' C L L' \<sigma> t' s'. candidate_values (fst pair) CC C' C (snd pair) L L' \<sigma> t' s' x S

goal (1 subgoal):
 1. (snd pair, x) \<in> trm_ord
[PROOF STEP]
unfolding candidate_values_def
[PROOF STATE]
proof (prove)
using this:
\<exists>CC C' C L L' \<sigma> t' s'. CC \<in> S \<and> x \<notin> subst_set (trms_ecl CC) \<sigma> \<and> trms_irreducible CC \<sigma> S x \<and> C' = cl_ecl CC \<and> (snd pair, x) \<in> trm_ord \<and> ((snd pair, x) \<in> trm_ord \<longrightarrow> fst pair = trm_rep (snd pair) S) \<and> orient_lit_inst L' t' s' pos \<sigma> \<and> sel C' = {} \<and> L' \<in> C' \<and> maximal_literal L C \<and> L = subst_lit L' \<sigma> \<and> C = subst_cl C' \<sigma> \<and> ground_clause C \<and> x = t' \<lhd> \<sigma> \<and> snd pair = s' \<lhd> \<sigma> \<and> finite C' \<and> smaller_lits_are_false x C S \<and> maximal_literal_is_unique x (snd pair) C' L' S \<sigma>

goal (1 subgoal):
 1. (snd pair, x) \<in> trm_ord
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(snd pair, x) \<in> trm_ord

goal (1 subgoal):
 1. (trm_rep x S, x) \<in> trm_ord
[PROOF STEP]
from \<open>\<exists> CC C' C  L L' \<sigma> t' s'. candidate_values (fst pair) CC C' C (snd pair) L L' \<sigma> t' s' x S\<close>
[PROOF STATE]
proof (chain)
picking this:
\<exists>CC C' C L L' \<sigma> t' s'. candidate_values (fst pair) CC C' C (snd pair) L L' \<sigma> t' s' x S
[PROOF STEP]
have "((snd pair, x) \<in> trm_ord \<longrightarrow> fst pair = trm_rep (snd pair) S)"
[PROOF STATE]
proof (prove)
using this:
\<exists>CC C' C L L' \<sigma> t' s'. candidate_values (fst pair) CC C' C (snd pair) L L' \<sigma> t' s' x S

goal (1 subgoal):
 1. (snd pair, x) \<in> trm_ord \<longrightarrow> fst pair = trm_rep (snd pair) S
[PROOF STEP]
unfolding candidate_values_def
[PROOF STATE]
proof (prove)
using this:
\<exists>CC C' C L L' \<sigma> t' s'. CC \<in> S \<and> x \<notin> subst_set (trms_ecl CC) \<sigma> \<and> trms_irreducible CC \<sigma> S x \<and> C' = cl_ecl CC \<and> (snd pair, x) \<in> trm_ord \<and> ((snd pair, x) \<in> trm_ord \<longrightarrow> fst pair = trm_rep (snd pair) S) \<and> orient_lit_inst L' t' s' pos \<sigma> \<and> sel C' = {} \<and> L' \<in> C' \<and> maximal_literal L C \<and> L = subst_lit L' \<sigma> \<and> C = subst_cl C' \<sigma> \<and> ground_clause C \<and> x = t' \<lhd> \<sigma> \<and> snd pair = s' \<lhd> \<sigma> \<and> finite C' \<and> smaller_lits_are_false x C S \<and> maximal_literal_is_unique x (snd pair) C' L' S \<sigma>

goal (1 subgoal):
 1. (snd pair, x) \<in> trm_ord \<longrightarrow> fst pair = trm_rep (snd pair) S
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(snd pair, x) \<in> trm_ord \<longrightarrow> fst pair = trm_rep (snd pair) S

goal (1 subgoal):
 1. (trm_rep x S, x) \<in> trm_ord
[PROOF STEP]
from \<open>(snd pair,x) \<in> trm_ord\<close> and \<open>((snd pair, x) \<in> trm_ord \<longrightarrow> fst pair = trm_rep (snd pair) S)\<close>
[PROOF STATE]
proof (chain)
picking this:
(snd pair, x) \<in> trm_ord
(snd pair, x) \<in> trm_ord \<longrightarrow> fst pair = trm_rep (snd pair) S
[PROOF STEP]
have "fst pair = trm_rep (snd pair) S"
[PROOF STATE]
proof (prove)
using this:
(snd pair, x) \<in> trm_ord
(snd pair, x) \<in> trm_ord \<longrightarrow> fst pair = trm_rep (snd pair) S

goal (1 subgoal):
 1. fst pair = trm_rep (snd pair) S
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
fst pair = trm_rep (snd pair) S

goal (1 subgoal):
 1. (trm_rep x S, x) \<in> trm_ord
[PROOF STEP]
have "snd pair = trm_rep (snd pair) S \<or> (trm_rep (snd pair) S,snd pair) \<in> trm_ord"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd pair = trm_rep (snd pair) S \<or> (trm_rep (snd pair) S, snd pair) \<in> trm_ord
[PROOF STEP]
using trm_rep_is_lower
[PROOF STATE]
proof (prove)
using this:
?t \<noteq> trm_rep ?t ?S \<longrightarrow> (trm_rep ?t ?S, ?t) \<in> trm_ord

goal (1 subgoal):
 1. snd pair = trm_rep (snd pair) S \<or> (trm_rep (snd pair) S, snd pair) \<in> trm_ord
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
snd pair = trm_rep (snd pair) S \<or> (trm_rep (snd pair) S, snd pair) \<in> trm_ord

goal (1 subgoal):
 1. (trm_rep x S, x) \<in> trm_ord
[PROOF STEP]
from this and \<open>(snd pair,x) \<in> trm_ord\<close>
[PROOF STATE]
proof (chain)
picking this:
snd pair = trm_rep (snd pair) S \<or> (trm_rep (snd pair) S, snd pair) \<in> trm_ord
(snd pair, x) \<in> trm_ord
[PROOF STEP]
have "(trm_rep (snd pair) S,x) \<in> trm_ord"
[PROOF STATE]
proof (prove)
using this:
snd pair = trm_rep (snd pair) S \<or> (trm_rep (snd pair) S, snd pair) \<in> trm_ord
(snd pair, x) \<in> trm_ord

goal (1 subgoal):
 1. (trm_rep (snd pair) S, x) \<in> trm_ord
[PROOF STEP]
using trm_ord_trans trans_def
[PROOF STATE]
proof (prove)
using this:
snd pair = trm_rep (snd pair) S \<or> (trm_rep (snd pair) S, snd pair) \<in> trm_ord
(snd pair, x) \<in> trm_ord
trans trm_ord
trans ?r = (\<forall>x y z. (x, y) \<in> ?r \<longrightarrow> (y, z) \<in> ?r \<longrightarrow> (x, z) \<in> ?r)

goal (1 subgoal):
 1. (trm_rep (snd pair) S, x) \<in> trm_ord
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
(trm_rep (snd pair) S, x) \<in> trm_ord

goal (1 subgoal):
 1. (trm_rep x S, x) \<in> trm_ord
[PROOF STEP]
from this and \<open>(trm_rep x S) = fst pair\<close> and \<open>fst pair = trm_rep (snd pair) S\<close>
[PROOF STATE]
proof (chain)
picking this:
(trm_rep (snd pair) S, x) \<in> trm_ord
trm_rep x S = fst pair
fst pair = trm_rep (snd pair) S
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(trm_rep (snd pair) S, x) \<in> trm_ord
trm_rep x S = fst pair
fst pair = trm_rep (snd pair) S

goal (1 subgoal):
 1. (trm_rep x S, x) \<in> trm_ord
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
(trm_rep x S, x) \<in> trm_ord

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma trm_rep_simp_def:
  shows "(trm_rep t S) = (if (subterm_reduction_applicable S t)
                        then (subterm_reduction S t)
                        else (get_min t (set_of_candidate_values S t)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trm_rep t S = (if subterm_reduction_applicable S t then subterm_reduction S t else get_min t (set_of_candidate_values S t))
[PROOF STEP]
using trm_rep_is_lower  trm_rep_aux_def
[PROOF STATE]
proof (prove)
using this:
?t \<noteq> trm_rep ?t ?S \<longrightarrow> (trm_rep ?t ?S, ?t) \<in> trm_ord
\<forall>y. (y, ?t) \<in> trm_ord \<longrightarrow> y \<noteq> trm_rep y ?S \<longrightarrow> (trm_rep y ?S, y) \<in> trm_ord \<Longrightarrow> trm_rep ?t ?S = (if subterm_reduction_applicable ?S ?t then subterm_reduction ?S ?t else get_min ?t (set_of_candidate_values ?S ?t))

goal (1 subgoal):
 1. trm_rep t S = (if subterm_reduction_applicable S t then subterm_reduction S t else get_min t (set_of_candidate_values S t))
[PROOF STEP]
by blast


[STATEMENT]
lemma trm_rep_involutive:
  shows "(trm_rep (trm_rep t S) S) = (trm_rep t S)" (is "?P t")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trm_rep (trm_rep t S) S = trm_rep t S
[PROOF STEP]
proof ((rule wf_induct [of "trm_ord" "?P" "t"]),(simp add: trm_ord_wf))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<forall>y. (y, x) \<in> trm_ord \<longrightarrow> trm_rep (trm_rep y S) S = trm_rep y S \<Longrightarrow> trm_rep (trm_rep x S) S = trm_rep x S
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<forall>y. (y, x) \<in> trm_ord \<longrightarrow> trm_rep (trm_rep y S) S = trm_rep y S \<Longrightarrow> trm_rep (trm_rep x S) S = trm_rep x S
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<forall>y. (y, x) \<in> trm_ord \<longrightarrow> trm_rep (trm_rep y S) S = trm_rep y S \<Longrightarrow> trm_rep (trm_rep x S) S = trm_rep x S
[PROOF STEP]
assume hyp_ind: "\<forall>y. (y,x) \<in> trm_ord \<longrightarrow> (?P y)"
[PROOF STATE]
proof (state)
this:
\<forall>y. (y, x) \<in> trm_ord \<longrightarrow> trm_rep (trm_rep y S) S = trm_rep y S

goal (1 subgoal):
 1. \<And>x. \<forall>y. (y, x) \<in> trm_ord \<longrightarrow> trm_rep (trm_rep y S) S = trm_rep y S \<Longrightarrow> trm_rep (trm_rep x S) S = trm_rep x S
[PROOF STEP]
let ?v = "(Comb (trm_rep (lhs x) S) (trm_rep (rhs x) S))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<forall>y. (y, x) \<in> trm_ord \<longrightarrow> trm_rep (trm_rep y S) S = trm_rep y S \<Longrightarrow> trm_rep (trm_rep x S) S = trm_rep x S
[PROOF STEP]
show "(?P x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trm_rep (trm_rep x S) S = trm_rep x S
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> trm_rep (trm_rep x S) S = trm_rep x S
 2. \<not> ?P \<Longrightarrow> trm_rep (trm_rep x S) S = trm_rep x S
[PROOF STEP]
assume c1: "subterm_reduction_applicable S x"
[PROOF STATE]
proof (state)
this:
subterm_reduction_applicable S x

goal (2 subgoals):
 1. ?P \<Longrightarrow> trm_rep (trm_rep x S) S = trm_rep x S
 2. \<not> ?P \<Longrightarrow> trm_rep (trm_rep x S) S = trm_rep x S
[PROOF STEP]
from this and hyp_ind
[PROOF STATE]
proof (chain)
picking this:
subterm_reduction_applicable S x
\<forall>y. (y, x) \<in> trm_ord \<longrightarrow> trm_rep (trm_rep y S) S = trm_rep y S
[PROOF STEP]
have "(?v,x) \<in> trm_ord"
[PROOF STATE]
proof (prove)
using this:
subterm_reduction_applicable S x
\<forall>y. (y, x) \<in> trm_ord \<longrightarrow> trm_rep (trm_rep y S) S = trm_rep y S

goal (1 subgoal):
 1. (trm_rep (lhs x) S \<cdot> trm_rep (rhs x) S, x) \<in> trm_ord
[PROOF STEP]
using trm_rep_is_lower_aux trm_rep_is_lower
[PROOF STATE]
proof (prove)
using this:
subterm_reduction_applicable S x
\<forall>y. (y, x) \<in> trm_ord \<longrightarrow> trm_rep (trm_rep y S) S = trm_rep y S
\<lbrakk>\<forall>y. (y, ?t) \<in> trm_ord \<longrightarrow> y \<noteq> trm_rep y ?S \<longrightarrow> (trm_rep y ?S, y) \<in> trm_ord; subterm_reduction_applicable ?S ?t\<rbrakk> \<Longrightarrow> (trm_rep (lhs ?t) ?S \<cdot> trm_rep (rhs ?t) ?S, ?t) \<in> trm_ord
?t \<noteq> trm_rep ?t ?S \<longrightarrow> (trm_rep ?t ?S, ?t) \<in> trm_ord

goal (1 subgoal):
 1. (trm_rep (lhs x) S \<cdot> trm_rep (rhs x) S, x) \<in> trm_ord
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
(trm_rep (lhs x) S \<cdot> trm_rep (rhs x) S, x) \<in> trm_ord

goal (2 subgoals):
 1. ?P \<Longrightarrow> trm_rep (trm_rep x S) S = trm_rep x S
 2. \<not> ?P \<Longrightarrow> trm_rep (trm_rep x S) S = trm_rep x S
[PROOF STEP]
from this hyp_ind
[PROOF STATE]
proof (chain)
picking this:
(trm_rep (lhs x) S \<cdot> trm_rep (rhs x) S, x) \<in> trm_ord
\<forall>y. (y, x) \<in> trm_ord \<longrightarrow> trm_rep (trm_rep y S) S = trm_rep y S
[PROOF STEP]
have "(trm_rep (trm_rep ?v S) S) =  (trm_rep ?v S)"
[PROOF STATE]
proof (prove)
using this:
(trm_rep (lhs x) S \<cdot> trm_rep (rhs x) S, x) \<in> trm_ord
\<forall>y. (y, x) \<in> trm_ord \<longrightarrow> trm_rep (trm_rep y S) S = trm_rep y S

goal (1 subgoal):
 1. trm_rep (trm_rep (trm_rep (lhs x) S \<cdot> trm_rep (rhs x) S) S) S = trm_rep (trm_rep (lhs x) S \<cdot> trm_rep (rhs x) S) S
[PROOF STEP]
using trm_rep_aux_def [of x S]
[PROOF STATE]
proof (prove)
using this:
(trm_rep (lhs x) S \<cdot> trm_rep (rhs x) S, x) \<in> trm_ord
\<forall>y. (y, x) \<in> trm_ord \<longrightarrow> trm_rep (trm_rep y S) S = trm_rep y S
\<forall>y. (y, x) \<in> trm_ord \<longrightarrow> y \<noteq> trm_rep y S \<longrightarrow> (trm_rep y S, y) \<in> trm_ord \<Longrightarrow> trm_rep x S = (if subterm_reduction_applicable S x then subterm_reduction S x else get_min x (set_of_candidate_values S x))

goal (1 subgoal):
 1. trm_rep (trm_rep (trm_rep (lhs x) S \<cdot> trm_rep (rhs x) S) S) S = trm_rep (trm_rep (lhs x) S \<cdot> trm_rep (rhs x) S) S
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
trm_rep (trm_rep (trm_rep (lhs x) S \<cdot> trm_rep (rhs x) S) S) S = trm_rep (trm_rep (lhs x) S \<cdot> trm_rep (rhs x) S) S

goal (2 subgoals):
 1. ?P \<Longrightarrow> trm_rep (trm_rep x S) S = trm_rep x S
 2. \<not> ?P \<Longrightarrow> trm_rep (trm_rep x S) S = trm_rep x S
[PROOF STEP]
from c1
[PROOF STATE]
proof (chain)
picking this:
subterm_reduction_applicable S x
[PROOF STEP]
have "trm_rep x S = trm_rep ?v S"
[PROOF STATE]
proof (prove)
using this:
subterm_reduction_applicable S x

goal (1 subgoal):
 1. trm_rep x S = trm_rep (trm_rep (lhs x) S \<cdot> trm_rep (rhs x) S) S
[PROOF STEP]
using trm_rep_simp_def [of x S]
[PROOF STATE]
proof (prove)
using this:
subterm_reduction_applicable S x
trm_rep x S = (if subterm_reduction_applicable S x then subterm_reduction S x else get_min x (set_of_candidate_values S x))

goal (1 subgoal):
 1. trm_rep x S = trm_rep (trm_rep (lhs x) S \<cdot> trm_rep (rhs x) S) S
[PROOF STEP]
unfolding subterm_reduction_def
[PROOF STATE]
proof (prove)
using this:
subterm_reduction_applicable S x
trm_rep x S = (if subterm_reduction_applicable S x then trm_rep (trm_rep (lhs x) S \<cdot> trm_rep (rhs x) S) S else get_min x (set_of_candidate_values S x))

goal (1 subgoal):
 1. trm_rep x S = trm_rep (trm_rep (lhs x) S \<cdot> trm_rep (rhs x) S) S
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
trm_rep x S = trm_rep (trm_rep (lhs x) S \<cdot> trm_rep (rhs x) S) S

goal (2 subgoals):
 1. ?P \<Longrightarrow> trm_rep (trm_rep x S) S = trm_rep x S
 2. \<not> ?P \<Longrightarrow> trm_rep (trm_rep x S) S = trm_rep x S
[PROOF STEP]
from this and \<open>(trm_rep (trm_rep ?v S) S) =  (trm_rep ?v S)\<close> \<open>trm_rep x S = trm_rep ?v S\<close>
[PROOF STATE]
proof (chain)
picking this:
trm_rep x S = trm_rep (trm_rep (lhs x) S \<cdot> trm_rep (rhs x) S) S
trm_rep (trm_rep (trm_rep (lhs x) S \<cdot> trm_rep (rhs x) S) S) S = trm_rep (trm_rep (lhs x) S \<cdot> trm_rep (rhs x) S) S
trm_rep x S = trm_rep (trm_rep (lhs x) S \<cdot> trm_rep (rhs x) S) S
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
trm_rep x S = trm_rep (trm_rep (lhs x) S \<cdot> trm_rep (rhs x) S) S
trm_rep (trm_rep (trm_rep (lhs x) S \<cdot> trm_rep (rhs x) S) S) S = trm_rep (trm_rep (lhs x) S \<cdot> trm_rep (rhs x) S) S
trm_rep x S = trm_rep (trm_rep (lhs x) S \<cdot> trm_rep (rhs x) S) S

goal (1 subgoal):
 1. trm_rep (trm_rep x S) S = trm_rep x S
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
trm_rep (trm_rep x S) S = trm_rep x S

goal (1 subgoal):
 1. \<not> subterm_reduction_applicable S x \<Longrightarrow> trm_rep (trm_rep x S) S = trm_rep x S
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> subterm_reduction_applicable S x \<Longrightarrow> trm_rep (trm_rep x S) S = trm_rep x S
[PROOF STEP]
assume c2: "\<not>subterm_reduction_applicable S x"
[PROOF STATE]
proof (state)
this:
\<not> subterm_reduction_applicable S x

goal (1 subgoal):
 1. \<not> subterm_reduction_applicable S x \<Longrightarrow> trm_rep (trm_rep x S) S = trm_rep x S
[PROOF STEP]
from c2
[PROOF STATE]
proof (chain)
picking this:
\<not> subterm_reduction_applicable S x
[PROOF STEP]
have "(trm_rep x S) = (get_min x (set_of_candidate_values S x))"
[PROOF STATE]
proof (prove)
using this:
\<not> subterm_reduction_applicable S x

goal (1 subgoal):
 1. trm_rep x S = get_min x (set_of_candidate_values S x)
[PROOF STEP]
using trm_rep_simp_def [of x S]
[PROOF STATE]
proof (prove)
using this:
\<not> subterm_reduction_applicable S x
trm_rep x S = (if subterm_reduction_applicable S x then subterm_reduction S x else get_min x (set_of_candidate_values S x))

goal (1 subgoal):
 1. trm_rep x S = get_min x (set_of_candidate_values S x)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
trm_rep x S = get_min x (set_of_candidate_values S x)

goal (1 subgoal):
 1. \<not> subterm_reduction_applicable S x \<Longrightarrow> trm_rep (trm_rep x S) S = trm_rep x S
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trm_rep (trm_rep x S) S = trm_rep x S
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. trm_rep (trm_rep x S) S \<noteq> trm_rep x S \<Longrightarrow> False
[PROOF STEP]
assume "(trm_rep (trm_rep x S) S) \<noteq> (trm_rep x S)"
[PROOF STATE]
proof (state)
this:
trm_rep (trm_rep x S) S \<noteq> trm_rep x S

goal (1 subgoal):
 1. trm_rep (trm_rep x S) S \<noteq> trm_rep x S \<Longrightarrow> False
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
trm_rep (trm_rep x S) S \<noteq> trm_rep x S
[PROOF STEP]
have "x \<noteq> (trm_rep x S)"
[PROOF STATE]
proof (prove)
using this:
trm_rep (trm_rep x S) S \<noteq> trm_rep x S

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

goal (1 subgoal):
 1. trm_rep (trm_rep x S) S \<noteq> trm_rep x S \<Longrightarrow> False
[PROOF STEP]
from c2 and \<open>x \<noteq> (trm_rep x S)\<close>
[PROOF STATE]
proof (chain)
picking this:
\<not> subterm_reduction_applicable S x
x \<noteq> trm_rep x S
[PROOF STEP]
have "(trm_rep x S) \<in> (min_trms (set_of_candidate_values S x))"
[PROOF STATE]
proof (prove)
using this:
\<not> subterm_reduction_applicable S x
x \<noteq> trm_rep x S

goal (1 subgoal):
 1. trm_rep x S \<in> min_trms (set_of_candidate_values S x)
[PROOF STEP]
using trm_rep_simp_def [of x S]
[PROOF STATE]
proof (prove)
using this:
\<not> subterm_reduction_applicable S x
x \<noteq> trm_rep x S
trm_rep x S = (if subterm_reduction_applicable S x then subterm_reduction S x else get_min x (set_of_candidate_values S x))

goal (1 subgoal):
 1. trm_rep x S \<in> min_trms (set_of_candidate_values S x)
[PROOF STEP]
unfolding get_min_def
[PROOF STATE]
proof (prove)
using this:
\<not> subterm_reduction_applicable S x
x \<noteq> trm_rep x S
trm_rep x S = (if subterm_reduction_applicable S x then subterm_reduction S x else if min_trms (set_of_candidate_values S x) = {} then x else SOME xa. xa \<in> min_trms (set_of_candidate_values S x))

goal (1 subgoal):
 1. trm_rep x S \<in> min_trms (set_of_candidate_values S x)
[PROOF STEP]
by (metis (full_types) some_in_eq)
[PROOF STATE]
proof (state)
this:
trm_rep x S \<in> min_trms (set_of_candidate_values S x)

goal (1 subgoal):
 1. trm_rep (trm_rep x S) S \<noteq> trm_rep x S \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
trm_rep x S \<in> min_trms (set_of_candidate_values S x)
[PROOF STEP]
obtain pair where
            "pair \<in> (set_of_candidate_values S x)" and "(trm_rep x S) = fst pair"
[PROOF STATE]
proof (prove)
using this:
trm_rep x S \<in> min_trms (set_of_candidate_values S x)

goal (1 subgoal):
 1. (\<And>pair. \<lbrakk>pair \<in> set_of_candidate_values S x; trm_rep x S = fst pair\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding min_trms_def
[PROOF STATE]
proof (prove)
using this:
trm_rep x S \<in> {xa. \<exists>pair. (pair \<in> set_of_candidate_values S x \<and> (\<forall>pair'\<in>set_of_candidate_values S x. (snd pair', snd pair) \<notin> trm_ord)) \<and> xa = fst pair}

goal (1 subgoal):
 1. (\<And>pair. \<lbrakk>pair \<in> set_of_candidate_values S x; trm_rep x S = fst pair\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
pair \<in> set_of_candidate_values S x
trm_rep x S = fst pair

goal (1 subgoal):
 1. trm_rep (trm_rep x S) S \<noteq> trm_rep x S \<Longrightarrow> False
[PROOF STEP]
from \<open>pair \<in> (set_of_candidate_values S x)\<close>
[PROOF STATE]
proof (chain)
picking this:
pair \<in> set_of_candidate_values S x
[PROOF STEP]
have i: "\<exists> CC C' C  L L' \<sigma> t' s'.
                    candidate_values (fst pair) CC C' C (snd pair) L L' \<sigma> t' s' x S"
[PROOF STATE]
proof (prove)
using this:
pair \<in> set_of_candidate_values S x

goal (1 subgoal):
 1. \<exists>CC C' C L L' \<sigma> t' s'. candidate_values (fst pair) CC C' C (snd pair) L L' \<sigma> t' s' x S
[PROOF STEP]
unfolding set_of_candidate_values_def
[PROOF STATE]
proof (prove)
using this:
pair \<in> {pair. \<exists>z CC C' C s L L' \<sigma> t' s'. pair = (z, s) \<and> candidate_values z CC C' C s L L' \<sigma> t' s' x S}

goal (1 subgoal):
 1. \<exists>CC C' C L L' \<sigma> t' s'. candidate_values (fst pair) CC C' C (snd pair) L L' \<sigma> t' s' x S
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<exists>CC C' C L L' \<sigma> t' s'. candidate_values (fst pair) CC C' C (snd pair) L L' \<sigma> t' s' x S

goal (1 subgoal):
 1. trm_rep (trm_rep x S) S \<noteq> trm_rep x S \<Longrightarrow> False
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
\<exists>CC C' C L L' \<sigma> t' s'. candidate_values (fst pair) CC C' C (snd pair) L L' \<sigma> t' s' x S
[PROOF STEP]
have "(snd pair,x) \<in> trm_ord"
[PROOF STATE]
proof (prove)
using this:
\<exists>CC C' C L L' \<sigma> t' s'. candidate_values (fst pair) CC C' C (snd pair) L L' \<sigma> t' s' x S

goal (1 subgoal):
 1. (snd pair, x) \<in> trm_ord
[PROOF STEP]
unfolding candidate_values_def
[PROOF STATE]
proof (prove)
using this:
\<exists>CC C' C L L' \<sigma> t' s'. CC \<in> S \<and> x \<notin> subst_set (trms_ecl CC) \<sigma> \<and> trms_irreducible CC \<sigma> S x \<and> C' = cl_ecl CC \<and> (snd pair, x) \<in> trm_ord \<and> ((snd pair, x) \<in> trm_ord \<longrightarrow> fst pair = trm_rep (snd pair) S) \<and> orient_lit_inst L' t' s' pos \<sigma> \<and> sel C' = {} \<and> L' \<in> C' \<and> maximal_literal L C \<and> L = subst_lit L' \<sigma> \<and> C = subst_cl C' \<sigma> \<and> ground_clause C \<and> x = t' \<lhd> \<sigma> \<and> snd pair = s' \<lhd> \<sigma> \<and> finite C' \<and> smaller_lits_are_false x C S \<and> maximal_literal_is_unique x (snd pair) C' L' S \<sigma>

goal (1 subgoal):
 1. (snd pair, x) \<in> trm_ord
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(snd pair, x) \<in> trm_ord

goal (1 subgoal):
 1. trm_rep (trm_rep x S) S \<noteq> trm_rep x S \<Longrightarrow> False
[PROOF STEP]
from i
[PROOF STATE]
proof (chain)
picking this:
\<exists>CC C' C L L' \<sigma> t' s'. candidate_values (fst pair) CC C' C (snd pair) L L' \<sigma> t' s' x S
[PROOF STEP]
have "((snd pair, x) \<in> trm_ord \<longrightarrow> fst pair = trm_rep (snd pair) S)"
[PROOF STATE]
proof (prove)
using this:
\<exists>CC C' C L L' \<sigma> t' s'. candidate_values (fst pair) CC C' C (snd pair) L L' \<sigma> t' s' x S

goal (1 subgoal):
 1. (snd pair, x) \<in> trm_ord \<longrightarrow> fst pair = trm_rep (snd pair) S
[PROOF STEP]
unfolding candidate_values_def
[PROOF STATE]
proof (prove)
using this:
\<exists>CC C' C L L' \<sigma> t' s'. CC \<in> S \<and> x \<notin> subst_set (trms_ecl CC) \<sigma> \<and> trms_irreducible CC \<sigma> S x \<and> C' = cl_ecl CC \<and> (snd pair, x) \<in> trm_ord \<and> ((snd pair, x) \<in> trm_ord \<longrightarrow> fst pair = trm_rep (snd pair) S) \<and> orient_lit_inst L' t' s' pos \<sigma> \<and> sel C' = {} \<and> L' \<in> C' \<and> maximal_literal L C \<and> L = subst_lit L' \<sigma> \<and> C = subst_cl C' \<sigma> \<and> ground_clause C \<and> x = t' \<lhd> \<sigma> \<and> snd pair = s' \<lhd> \<sigma> \<and> finite C' \<and> smaller_lits_are_false x C S \<and> maximal_literal_is_unique x (snd pair) C' L' S \<sigma>

goal (1 subgoal):
 1. (snd pair, x) \<in> trm_ord \<longrightarrow> fst pair = trm_rep (snd pair) S
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(snd pair, x) \<in> trm_ord \<longrightarrow> fst pair = trm_rep (snd pair) S

goal (1 subgoal):
 1. trm_rep (trm_rep x S) S \<noteq> trm_rep x S \<Longrightarrow> False
[PROOF STEP]
from \<open>(snd pair,x) \<in> trm_ord\<close>
            and \<open>((snd pair, x) \<in> trm_ord \<longrightarrow> fst pair = trm_rep (snd pair) S)\<close>
[PROOF STATE]
proof (chain)
picking this:
(snd pair, x) \<in> trm_ord
(snd pair, x) \<in> trm_ord \<longrightarrow> fst pair = trm_rep (snd pair) S
[PROOF STEP]
have "fst pair = trm_rep (snd pair) S"
[PROOF STATE]
proof (prove)
using this:
(snd pair, x) \<in> trm_ord
(snd pair, x) \<in> trm_ord \<longrightarrow> fst pair = trm_rep (snd pair) S

goal (1 subgoal):
 1. fst pair = trm_rep (snd pair) S
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
fst pair = trm_rep (snd pair) S

goal (1 subgoal):
 1. trm_rep (trm_rep x S) S \<noteq> trm_rep x S \<Longrightarrow> False
[PROOF STEP]
from \<open>(snd pair,x) \<in> trm_ord\<close> and hyp_ind
[PROOF STATE]
proof (chain)
picking this:
(snd pair, x) \<in> trm_ord
\<forall>y. (y, x) \<in> trm_ord \<longrightarrow> trm_rep (trm_rep y S) S = trm_rep y S
[PROOF STEP]
have "(?P (snd pair))"
[PROOF STATE]
proof (prove)
using this:
(snd pair, x) \<in> trm_ord
\<forall>y. (y, x) \<in> trm_ord \<longrightarrow> trm_rep (trm_rep y S) S = trm_rep y S

goal (1 subgoal):
 1. trm_rep (trm_rep (snd pair) S) S = trm_rep (snd pair) S
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
trm_rep (trm_rep (snd pair) S) S = trm_rep (snd pair) S

goal (1 subgoal):
 1. trm_rep (trm_rep x S) S \<noteq> trm_rep x S \<Longrightarrow> False
[PROOF STEP]
from this and \<open>fst pair = (trm_rep (snd pair) S)\<close> and \<open>(trm_rep x S) = fst pair\<close>
            and \<open>(trm_rep (trm_rep x S) S) \<noteq> (trm_rep x S)\<close>
[PROOF STATE]
proof (chain)
picking this:
trm_rep (trm_rep (snd pair) S) S = trm_rep (snd pair) S
fst pair = trm_rep (snd pair) S
trm_rep x S = fst pair
trm_rep (trm_rep x S) S \<noteq> trm_rep x S
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
trm_rep (trm_rep (snd pair) S) S = trm_rep (snd pair) S
fst pair = trm_rep (snd pair) S
trm_rep x S = fst pair
trm_rep (trm_rep x S) S \<noteq> trm_rep x S

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
trm_rep (trm_rep x S) S = trm_rep x S

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
trm_rep (trm_rep x S) S = trm_rep x S

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma red_arg_implies_red_trm :
  assumes "st_red S t1"
  assumes "t = (Comb t1 t2) \<or> t = (Comb t2 t1)"
  shows "st_red S t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. st_red S t
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. st_red S t
[PROOF STEP]
from assms(1)
[PROOF STATE]
proof (chain)
picking this:
st_red S t1
[PROOF STEP]
obtain t' p where "subterm t1 p t'" and "root_term S t'" and "trm_rep t' S \<noteq> t'"
[PROOF STATE]
proof (prove)
using this:
st_red S t1

goal (1 subgoal):
 1. (\<And>p t'. \<lbrakk>subterm t1 p t'; root_term S t'; trm_rep t' S \<noteq> t'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding st_red_def
[PROOF STATE]
proof (prove)
using this:
\<exists>t' p. subterm t1 p t' \<and> root_term S t' \<and> trm_rep t' S \<noteq> t'

goal (1 subgoal):
 1. (\<And>p t'. \<lbrakk>subterm t1 p t'; root_term S t'; trm_rep t' S \<noteq> t'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
subterm t1 p t'
root_term S t'
trm_rep t' S \<noteq> t'

goal (1 subgoal):
 1. st_red S t
[PROOF STEP]
from \<open>subterm t1 p t'\<close> and assms(2)
[PROOF STATE]
proof (chain)
picking this:
subterm t1 p t'
t = t1 \<cdot> t2 \<or> t = t2 \<cdot> t1
[PROOF STEP]
obtain q where "subterm t q t'"
[PROOF STATE]
proof (prove)
using this:
subterm t1 p t'
t = t1 \<cdot> t2 \<or> t = t2 \<cdot> t1

goal (1 subgoal):
 1. (\<And>q. subterm t q t' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis subterm.simps(4) subterm.simps(5))
[PROOF STATE]
proof (state)
this:
subterm t q t'

goal (1 subgoal):
 1. st_red S t
[PROOF STEP]
from this and \<open>root_term S t'\<close> and \<open>trm_rep t' S \<noteq> t'\<close>
[PROOF STATE]
proof (chain)
picking this:
subterm t q t'
root_term S t'
trm_rep t' S \<noteq> t'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
subterm t q t'
root_term S t'
trm_rep t' S \<noteq> t'

goal (1 subgoal):
 1. st_red S t
[PROOF STEP]
unfolding st_red_def
[PROOF STATE]
proof (prove)
using this:
subterm t q t'
root_term S t'
trm_rep t' S \<noteq> t'

goal (1 subgoal):
 1. \<exists>t' p. subterm t p t' \<and> root_term S t' \<and> trm_rep t' S \<noteq> t'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
st_red S t

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma subterms_of_irred_trms_are_irred:
  "(trm_rep t S) \<noteq> t \<longrightarrow> st_red S t" (is "(?P t)")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trm_rep t S \<noteq> t \<longrightarrow> st_red S t
[PROOF STEP]
proof ((rule wf_induct [of "trm_ord" "?P" "t"]),(simp add: trm_ord_wf))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<forall>y. (y, x) \<in> trm_ord \<longrightarrow> trm_rep y S \<noteq> y \<longrightarrow> st_red S y \<Longrightarrow> trm_rep x S \<noteq> x \<longrightarrow> st_red S x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<forall>y. (y, x) \<in> trm_ord \<longrightarrow> trm_rep y S \<noteq> y \<longrightarrow> st_red S y \<Longrightarrow> trm_rep x S \<noteq> x \<longrightarrow> st_red S x
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<forall>y. (y, x) \<in> trm_ord \<longrightarrow> trm_rep y S \<noteq> y \<longrightarrow> st_red S y \<Longrightarrow> trm_rep x S \<noteq> x \<longrightarrow> st_red S x
[PROOF STEP]
assume hyp_ind: "\<forall>y. (y,x) \<in> trm_ord \<longrightarrow> (?P y)"
[PROOF STATE]
proof (state)
this:
\<forall>y. (y, x) \<in> trm_ord \<longrightarrow> trm_rep y S \<noteq> y \<longrightarrow> st_red S y

goal (1 subgoal):
 1. \<And>x. \<forall>y. (y, x) \<in> trm_ord \<longrightarrow> trm_rep y S \<noteq> y \<longrightarrow> st_red S y \<Longrightarrow> trm_rep x S \<noteq> x \<longrightarrow> st_red S x
[PROOF STEP]
show "(?P x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trm_rep x S \<noteq> x \<longrightarrow> st_red S x
[PROOF STEP]
proof (rule impI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. trm_rep x S \<noteq> x \<Longrightarrow> st_red S x
[PROOF STEP]
assume "(trm_rep x S) \<noteq> x"
[PROOF STATE]
proof (state)
this:
trm_rep x S \<noteq> x

goal (1 subgoal):
 1. trm_rep x S \<noteq> x \<Longrightarrow> st_red S x
[PROOF STEP]
show "st_red S x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. st_red S x
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> st_red S x \<Longrightarrow> False
[PROOF STEP]
assume neg_h: "\<not>st_red S x"
[PROOF STATE]
proof (state)
this:
\<not> st_red S x

goal (1 subgoal):
 1. \<not> st_red S x \<Longrightarrow> False
[PROOF STEP]
have i: " \<not>subterm_reduction_applicable S x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> subterm_reduction_applicable S x
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. subterm_reduction_applicable S x \<Longrightarrow> False
[PROOF STEP]
assume decomp_case: "subterm_reduction_applicable S x"
[PROOF STATE]
proof (state)
this:
subterm_reduction_applicable S x

goal (1 subgoal):
 1. subterm_reduction_applicable S x \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
subterm_reduction_applicable S x
[PROOF STEP]
obtain x1 x2 where "x = (Comb x1 x2)"
[PROOF STATE]
proof (prove)
using this:
subterm_reduction_applicable S x

goal (1 subgoal):
 1. (\<And>x1 x2. x = x1 \<cdot> x2 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using is_compound.elims(2)
[PROOF STATE]
proof (prove)
using this:
subterm_reduction_applicable S x
\<lbrakk>is_compound ?x; \<And>x y. ?x = x \<cdot> y \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

goal (1 subgoal):
 1. (\<And>x1 x2. x = x1 \<cdot> x2 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding subterm_reduction_applicable_def
[PROOF STATE]
proof (prove)
using this:
is_compound x \<and> (trm_rep (lhs x) S \<noteq> lhs x \<or> trm_rep (rhs x) S \<noteq> rhs x)
\<lbrakk>is_compound ?x; \<And>x y. ?x = x \<cdot> y \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

goal (1 subgoal):
 1. (\<And>x1 x2. x = x1 \<cdot> x2 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x = x1 \<cdot> x2

goal (1 subgoal):
 1. subterm_reduction_applicable S x \<Longrightarrow> False
[PROOF STEP]
from this and decomp_case
[PROOF STATE]
proof (chain)
picking this:
x = x1 \<cdot> x2
subterm_reduction_applicable S x
[PROOF STEP]
have "((trm_rep x1 S) \<noteq> x1 \<or> (trm_rep x2 S) \<noteq> x2)"
[PROOF STATE]
proof (prove)
using this:
x = x1 \<cdot> x2
subterm_reduction_applicable S x

goal (1 subgoal):
 1. trm_rep x1 S \<noteq> x1 \<or> trm_rep x2 S \<noteq> x2
[PROOF STEP]
using lhs.simps(1) rhs.simps(1)
[PROOF STATE]
proof (prove)
using this:
x = x1 \<cdot> x2
subterm_reduction_applicable S x
lhs (?t1.0 \<cdot> ?t2.0) = ?t1.0
rhs (?t1.0 \<cdot> ?t2.0) = ?t2.0

goal (1 subgoal):
 1. trm_rep x1 S \<noteq> x1 \<or> trm_rep x2 S \<noteq> x2
[PROOF STEP]
unfolding subterm_reduction_applicable_def
[PROOF STATE]
proof (prove)
using this:
x = x1 \<cdot> x2
is_compound x \<and> (trm_rep (lhs x) S \<noteq> lhs x \<or> trm_rep (rhs x) S \<noteq> rhs x)
lhs (?t1.0 \<cdot> ?t2.0) = ?t1.0
rhs (?t1.0 \<cdot> ?t2.0) = ?t2.0

goal (1 subgoal):
 1. trm_rep x1 S \<noteq> x1 \<or> trm_rep x2 S \<noteq> x2
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
trm_rep x1 S \<noteq> x1 \<or> trm_rep x2 S \<noteq> x2

goal (1 subgoal):
 1. subterm_reduction_applicable S x \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
trm_rep x1 S \<noteq> x1 \<or> trm_rep x2 S \<noteq> x2
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
trm_rep x1 S \<noteq> x1 \<or> trm_rep x2 S \<noteq> x2

goal (1 subgoal):
 1. False
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. trm_rep x1 S \<noteq> x1 \<Longrightarrow> False
 2. trm_rep x2 S \<noteq> x2 \<Longrightarrow> False
[PROOF STEP]
assume "(trm_rep x1 S) \<noteq> x1"
[PROOF STATE]
proof (state)
this:
trm_rep x1 S \<noteq> x1

goal (2 subgoals):
 1. trm_rep x1 S \<noteq> x1 \<Longrightarrow> False
 2. trm_rep x2 S \<noteq> x2 \<Longrightarrow> False
[PROOF STEP]
from \<open>x = (Comb x1 x2)\<close> and trm_ord_subterm
[PROOF STATE]
proof (chain)
picking this:
x = x1 \<cdot> x2
\<forall>x1 x2. (x1, x1 \<cdot> x2) \<in> trm_ord \<and> (x2, x1 \<cdot> x2) \<in> trm_ord
[PROOF STEP]
have "(x1,x) \<in> trm_ord"
[PROOF STATE]
proof (prove)
using this:
x = x1 \<cdot> x2
\<forall>x1 x2. (x1, x1 \<cdot> x2) \<in> trm_ord \<and> (x2, x1 \<cdot> x2) \<in> trm_ord

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

goal (2 subgoals):
 1. trm_rep x1 S \<noteq> x1 \<Longrightarrow> False
 2. trm_rep x2 S \<noteq> x2 \<Longrightarrow> False
[PROOF STEP]
from this and hyp_ind and \<open>(trm_rep x1 S) \<noteq> x1\<close>
[PROOF STATE]
proof (chain)
picking this:
(x1, x) \<in> trm_ord
\<forall>y. (y, x) \<in> trm_ord \<longrightarrow> trm_rep y S \<noteq> y \<longrightarrow> st_red S y
trm_rep x1 S \<noteq> x1
[PROOF STEP]
have "st_red S x1"
[PROOF STATE]
proof (prove)
using this:
(x1, x) \<in> trm_ord
\<forall>y. (y, x) \<in> trm_ord \<longrightarrow> trm_rep y S \<noteq> y \<longrightarrow> st_red S y
trm_rep x1 S \<noteq> x1

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

goal (2 subgoals):
 1. trm_rep x1 S \<noteq> x1 \<Longrightarrow> False
 2. trm_rep x2 S \<noteq> x2 \<Longrightarrow> False
[PROOF STEP]
from this and neg_h and \<open>x = (Comb x1 x2)\<close>
[PROOF STATE]
proof (chain)
picking this:
st_red S x1
\<not> st_red S x
x = x1 \<cdot> x2
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
st_red S x1
\<not> st_red S x
x = x1 \<cdot> x2

goal (1 subgoal):
 1. False
[PROOF STEP]
using red_arg_implies_red_trm [of S x1 x x2]
[PROOF STATE]
proof (prove)
using this:
st_red S x1
\<not> st_red S x
x = x1 \<cdot> x2
\<lbrakk>st_red S x1; x = x1 \<cdot> x2 \<or> x = x2 \<cdot> x1\<rbrakk> \<Longrightarrow> st_red S x

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

goal (1 subgoal):
 1. trm_rep x2 S \<noteq> x2 \<Longrightarrow> False
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. trm_rep x2 S \<noteq> x2 \<Longrightarrow> False
[PROOF STEP]
assume "(trm_rep x2 S) \<noteq> x2"
[PROOF STATE]
proof (state)
this:
trm_rep x2 S \<noteq> x2

goal (1 subgoal):
 1. trm_rep x2 S \<noteq> x2 \<Longrightarrow> False
[PROOF STEP]
from \<open>x = (Comb x1 x2)\<close> and trm_ord_subterm
[PROOF STATE]
proof (chain)
picking this:
x = x1 \<cdot> x2
\<forall>x1 x2. (x1, x1 \<cdot> x2) \<in> trm_ord \<and> (x2, x1 \<cdot> x2) \<in> trm_ord
[PROOF STEP]
have "(x2,x) \<in> trm_ord"
[PROOF STATE]
proof (prove)
using this:
x = x1 \<cdot> x2
\<forall>x1 x2. (x1, x1 \<cdot> x2) \<in> trm_ord \<and> (x2, x1 \<cdot> x2) \<in> trm_ord

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

goal (1 subgoal):
 1. trm_rep x2 S \<noteq> x2 \<Longrightarrow> False
[PROOF STEP]
from this and hyp_ind and \<open>(trm_rep x2 S) \<noteq> x2\<close>
[PROOF STATE]
proof (chain)
picking this:
(x2, x) \<in> trm_ord
\<forall>y. (y, x) \<in> trm_ord \<longrightarrow> trm_rep y S \<noteq> y \<longrightarrow> st_red S y
trm_rep x2 S \<noteq> x2
[PROOF STEP]
have "st_red S x2"
[PROOF STATE]
proof (prove)
using this:
(x2, x) \<in> trm_ord
\<forall>y. (y, x) \<in> trm_ord \<longrightarrow> trm_rep y S \<noteq> y \<longrightarrow> st_red S y
trm_rep x2 S \<noteq> x2

goal (1 subgoal):
 1. st_red S x2
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
st_red S x2

goal (1 subgoal):
 1. trm_rep x2 S \<noteq> x2 \<Longrightarrow> False
[PROOF STEP]
from this and neg_h and \<open>x = (Comb x1 x2)\<close>
[PROOF STATE]
proof (chain)
picking this:
st_red S x2
\<not> st_red S x
x = x1 \<cdot> x2
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
st_red S x2
\<not> st_red S x
x = x1 \<cdot> x2

goal (1 subgoal):
 1. False
[PROOF STEP]
using red_arg_implies_red_trm [of S x2 x x1]
[PROOF STATE]
proof (prove)
using this:
st_red S x2
\<not> st_red S x
x = x1 \<cdot> x2
\<lbrakk>st_red S x2; x = x2 \<cdot> x1 \<or> x = x1 \<cdot> x2\<rbrakk> \<Longrightarrow> st_red S x

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
[PROOF STATE]
proof (state)
this:
\<not> subterm_reduction_applicable S x

goal (1 subgoal):
 1. \<not> st_red S x \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> subterm_reduction_applicable S x
[PROOF STEP]
have "(trm_rep x S) = (get_min x (set_of_candidate_values S x))"
[PROOF STATE]
proof (prove)
using this:
\<not> subterm_reduction_applicable S x

goal (1 subgoal):
 1. trm_rep x S = get_min x (set_of_candidate_values S x)
[PROOF STEP]
using trm_rep_simp_def
[PROOF STATE]
proof (prove)
using this:
\<not> subterm_reduction_applicable S x
trm_rep ?t ?S = (if subterm_reduction_applicable ?S ?t then subterm_reduction ?S ?t else get_min ?t (set_of_candidate_values ?S ?t))

goal (1 subgoal):
 1. trm_rep x S = get_min x (set_of_candidate_values S x)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
trm_rep x S = get_min x (set_of_candidate_values S x)

goal (1 subgoal):
 1. \<not> st_red S x \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
trm_rep x S = get_min x (set_of_candidate_values S x)
[PROOF STEP]
have "root_term S x"
[PROOF STATE]
proof (prove)
using this:
trm_rep x S = get_min x (set_of_candidate_values S x)

goal (1 subgoal):
 1. root_term S x
[PROOF STEP]
unfolding root_term_def
[PROOF STATE]
proof (prove)
using this:
trm_rep x S = get_min x (set_of_candidate_values S x)

goal (1 subgoal):
 1. trm_rep x S = get_min x (set_of_candidate_values S x)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
root_term S x

goal (1 subgoal):
 1. \<not> st_red S x \<Longrightarrow> False
[PROOF STEP]
have "subterm x [] x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subterm x [] x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
subterm x [] x

goal (1 subgoal):
 1. \<not> st_red S x \<Longrightarrow> False
[PROOF STEP]
from this and \<open>root_term S x\<close> and \<open>(trm_rep x S) \<noteq> x\<close>
[PROOF STATE]
proof (chain)
picking this:
subterm x [] x
root_term S x
trm_rep x S \<noteq> x
[PROOF STEP]
have
          "st_red S x"
[PROOF STATE]
proof (prove)
using this:
subterm x [] x
root_term S x
trm_rep x S \<noteq> x

goal (1 subgoal):
 1. st_red S x
[PROOF STEP]
unfolding st_red_def
[PROOF STATE]
proof (prove)
using this:
subterm x [] x
root_term S x
trm_rep x S \<noteq> x

goal (1 subgoal):
 1. \<exists>t' p. subterm x p t' \<and> root_term S t' \<and> trm_rep t' S \<noteq> t'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
st_red S x

goal (1 subgoal):
 1. \<not> st_red S x \<Longrightarrow> False
[PROOF STEP]
from this and neg_h
[PROOF STATE]
proof (chain)
picking this:
st_red S x
\<not> st_red S x
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
st_red S x
\<not> st_red S x

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:
st_red S x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
trm_rep x S \<noteq> x \<longrightarrow> st_red S x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma trm_rep_compatible_with_structure:
  shows "value_is_compatible_with_structure (\<lambda>x. trm_rep x S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. value_is_compatible_with_structure (\<lambda>x. trm_rep x S)
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> value_is_compatible_with_structure (\<lambda>x. trm_rep x S) \<Longrightarrow> False
[PROOF STEP]
assume "\<not>value_is_compatible_with_structure (\<lambda>x. trm_rep x S)"
[PROOF STATE]
proof (state)
this:
\<not> value_is_compatible_with_structure (\<lambda>x. trm_rep x S)

goal (1 subgoal):
 1. \<not> value_is_compatible_with_structure (\<lambda>x. trm_rep x S) \<Longrightarrow> False
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
\<not> value_is_compatible_with_structure (\<lambda>x. trm_rep x S)
[PROOF STEP]
obtain t s
    where neg_h:"trm_rep (Comb t s) S \<noteq> (trm_rep (Comb (trm_rep t S) (trm_rep s S)) S)"
[PROOF STATE]
proof (prove)
using this:
\<not> value_is_compatible_with_structure (\<lambda>x. trm_rep x S)

goal (1 subgoal):
 1. (\<And>t s. trm_rep (t \<cdot> s) S \<noteq> trm_rep (trm_rep t S \<cdot> trm_rep s S) S \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding value_is_compatible_with_structure_def
[PROOF STATE]
proof (prove)
using this:
\<not> (\<forall>t s. trm_rep (t \<cdot> s) S = trm_rep (trm_rep t S \<cdot> trm_rep s S) S)

goal (1 subgoal):
 1. (\<And>t s. trm_rep (t \<cdot> s) S \<noteq> trm_rep (trm_rep t S \<cdot> trm_rep s S) S \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
trm_rep (t \<cdot> s) S \<noteq> trm_rep (trm_rep t S \<cdot> trm_rep s S) S

goal (1 subgoal):
 1. \<not> value_is_compatible_with_structure (\<lambda>x. trm_rep x S) \<Longrightarrow> False
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
trm_rep (t \<cdot> s) S \<noteq> trm_rep (trm_rep t S \<cdot> trm_rep s S) S
[PROOF STEP]
have "(trm_rep t S) \<noteq> t \<or> (trm_rep s S) \<noteq> s"
[PROOF STATE]
proof (prove)
using this:
trm_rep (t \<cdot> s) S \<noteq> trm_rep (trm_rep t S \<cdot> trm_rep s S) S

goal (1 subgoal):
 1. trm_rep t S \<noteq> t \<or> trm_rep s S \<noteq> s
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
trm_rep t S \<noteq> t \<or> trm_rep s S \<noteq> s

goal (1 subgoal):
 1. \<not> value_is_compatible_with_structure (\<lambda>x. trm_rep x S) \<Longrightarrow> False
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
trm_rep t S \<noteq> t \<or> trm_rep s S \<noteq> s
[PROOF STEP]
have "subterm_reduction_applicable S (Comb t s)"
[PROOF STATE]
proof (prove)
using this:
trm_rep t S \<noteq> t \<or> trm_rep s S \<noteq> s

goal (1 subgoal):
 1. subterm_reduction_applicable S (t \<cdot> s)
[PROOF STEP]
unfolding subterm_reduction_applicable_def
[PROOF STATE]
proof (prove)
using this:
trm_rep t S \<noteq> t \<or> trm_rep s S \<noteq> s

goal (1 subgoal):
 1. is_compound (t \<cdot> s) \<and> (trm_rep (lhs (t \<cdot> s)) S \<noteq> lhs (t \<cdot> s) \<or> trm_rep (rhs (t \<cdot> s)) S \<noteq> rhs (t \<cdot> s))
[PROOF STEP]
by (metis is_compound.simps(3) lhs.simps(1) rhs.simps(1))
[PROOF STATE]
proof (state)
this:
subterm_reduction_applicable S (t \<cdot> s)

goal (1 subgoal):
 1. \<not> value_is_compatible_with_structure (\<lambda>x. trm_rep x S) \<Longrightarrow> False
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
subterm_reduction_applicable S (t \<cdot> s)
[PROOF STEP]
have "(trm_rep (Comb t s) S) = (subterm_reduction S (Comb t s))"
[PROOF STATE]
proof (prove)
using this:
subterm_reduction_applicable S (t \<cdot> s)

goal (1 subgoal):
 1. trm_rep (t \<cdot> s) S = subterm_reduction S (t \<cdot> s)
[PROOF STEP]
using trm_rep_simp_def
[PROOF STATE]
proof (prove)
using this:
subterm_reduction_applicable S (t \<cdot> s)
trm_rep ?t ?S = (if subterm_reduction_applicable ?S ?t then subterm_reduction ?S ?t else get_min ?t (set_of_candidate_values ?S ?t))

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

goal (1 subgoal):
 1. \<not> value_is_compatible_with_structure (\<lambda>x. trm_rep x S) \<Longrightarrow> False
[PROOF STEP]
from this and neg_h
[PROOF STATE]
proof (chain)
picking this:
trm_rep (t \<cdot> s) S = subterm_reduction S (t \<cdot> s)
trm_rep (t \<cdot> s) S \<noteq> trm_rep (trm_rep t S \<cdot> trm_rep s S) S
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
trm_rep (t \<cdot> s) S = subterm_reduction S (t \<cdot> s)
trm_rep (t \<cdot> s) S \<noteq> trm_rep (trm_rep t S \<cdot> trm_rep s S) S

goal (1 subgoal):
 1. False
[PROOF STEP]
unfolding subterm_reduction_def
[PROOF STATE]
proof (prove)
using this:
trm_rep (t \<cdot> s) S = trm_rep (trm_rep (lhs (t \<cdot> s)) S \<cdot> trm_rep (rhs (t \<cdot> s)) S) S
trm_rep (t \<cdot> s) S \<noteq> trm_rep (trm_rep t S \<cdot> trm_rep s S) S

goal (1 subgoal):
 1. False
[PROOF STEP]
by (metis lhs.simps(1) rhs.simps(1))
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma maximal_literal_is_unique_lemma:
  assumes "\<not>equivalent_eq_exists t s C (int_clset S) \<sigma> L1"
  shows "maximal_literal_is_unique (subst t \<sigma>) (subst s \<sigma>) C L1 S \<sigma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. maximal_literal_is_unique (t \<lhd> \<sigma>) (s \<lhd> \<sigma>) C L1 S \<sigma>
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> maximal_literal_is_unique (t \<lhd> \<sigma>) (s \<lhd> \<sigma>) C L1 S \<sigma> \<Longrightarrow> False
[PROOF STEP]
let ?t = "(subst t \<sigma>)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> maximal_literal_is_unique (t \<lhd> \<sigma>) (s \<lhd> \<sigma>) C L1 S \<sigma> \<Longrightarrow> False
[PROOF STEP]
let ?s = "(subst s \<sigma>)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> maximal_literal_is_unique (t \<lhd> \<sigma>) (s \<lhd> \<sigma>) C L1 S \<sigma> \<Longrightarrow> False
[PROOF STEP]
let ?L = "(subst_lit L \<sigma>)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> maximal_literal_is_unique (t \<lhd> \<sigma>) (s \<lhd> \<sigma>) C L1 S \<sigma> \<Longrightarrow> False
[PROOF STEP]
let ?C = "(subst_cl C \<sigma>)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> maximal_literal_is_unique (t \<lhd> \<sigma>) (s \<lhd> \<sigma>) C L1 S \<sigma> \<Longrightarrow> False
[PROOF STEP]
assume "\<not>(maximal_literal_is_unique ?t ?s C L1 S \<sigma>)"
[PROOF STATE]
proof (state)
this:
\<not> maximal_literal_is_unique (t \<lhd> \<sigma>) (s \<lhd> \<sigma>) C L1 S \<sigma>

goal (1 subgoal):
 1. \<not> maximal_literal_is_unique (t \<lhd> \<sigma>) (s \<lhd> \<sigma>) C L1 S \<sigma> \<Longrightarrow> False
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
\<not> maximal_literal_is_unique (t \<lhd> \<sigma>) (s \<lhd> \<sigma>) C L1 S \<sigma>
[PROOF STEP]
obtain s'' where "(eq_occurs_in_cl ?t s'' (C- { L1 }) \<sigma>)"
    and "(trm_rep ?s  S) = (trm_rep s'' S)"
[PROOF STATE]
proof (prove)
using this:
\<not> maximal_literal_is_unique (t \<lhd> \<sigma>) (s \<lhd> \<sigma>) C L1 S \<sigma>

goal (1 subgoal):
 1. (\<And>s''. \<lbrakk>eq_occurs_in_cl (t \<lhd> \<sigma>) s'' (C - {L1}) \<sigma>; trm_rep (s \<lhd> \<sigma>) S = trm_rep s'' S\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding maximal_literal_is_unique_def
[PROOF STATE]
proof (prove)
using this:
\<not> (\<forall>s''. eq_occurs_in_cl (t \<lhd> \<sigma>) s'' (C - {L1}) \<sigma> \<longrightarrow> (s'', t \<lhd> \<sigma>) \<in> trm_ord \<longrightarrow> (s \<lhd> \<sigma>, t \<lhd> \<sigma>) \<in> trm_ord \<longrightarrow> trm_rep (s \<lhd> \<sigma>) S \<noteq> trm_rep s'' S)

goal (1 subgoal):
 1. (\<And>s''. \<lbrakk>eq_occurs_in_cl (t \<lhd> \<sigma>) s'' (C - {L1}) \<sigma>; trm_rep (s \<lhd> \<sigma>) S = trm_rep s'' S\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
eq_occurs_in_cl (t \<lhd> \<sigma>) s'' (C - {L1}) \<sigma>
trm_rep (s \<lhd> \<sigma>) S = trm_rep s'' S

goal (1 subgoal):
 1. \<not> maximal_literal_is_unique (t \<lhd> \<sigma>) (s \<lhd> \<sigma>) C L1 S \<sigma> \<Longrightarrow> False
[PROOF STEP]
from \<open>(eq_occurs_in_cl ?t s'' (C- { L1 }) \<sigma>)\<close>
[PROOF STATE]
proof (chain)
picking this:
eq_occurs_in_cl (t \<lhd> \<sigma>) s'' (C - {L1}) \<sigma>
[PROOF STEP]
obtain L' t' s' where "L' \<in> (C- { L1 })"
      and "orient_lit_inst L' t' s' pos \<sigma>" and "(subst t' \<sigma>) = ?t"
      and  "s'' = subst s' \<sigma>"
[PROOF STATE]
proof (prove)
using this:
eq_occurs_in_cl (t \<lhd> \<sigma>) s'' (C - {L1}) \<sigma>

goal (1 subgoal):
 1. (\<And>L' t' s'. \<lbrakk>L' \<in> C - {L1}; orient_lit_inst L' t' s' pos \<sigma>; t' \<lhd> \<sigma> = t \<lhd> \<sigma>; s'' = s' \<lhd> \<sigma>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding eq_occurs_in_cl_def
[PROOF STATE]
proof (prove)
using this:
\<exists>L t' s'. L \<in> C - {L1} \<and> orient_lit_inst L t' s' pos \<sigma> \<and> t \<lhd> \<sigma> = t' \<lhd> \<sigma> \<and> s'' = s' \<lhd> \<sigma>

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

goal (1 subgoal):
 1. \<not> maximal_literal_is_unique (t \<lhd> \<sigma>) (s \<lhd> \<sigma>) C L1 S \<sigma> \<Longrightarrow> False
[PROOF STEP]
from \<open>s'' = subst s' \<sigma>\<close> and \<open>(trm_rep ?s  S) = (trm_rep s'' S)\<close>
[PROOF STATE]
proof (chain)
picking this:
s'' = s' \<lhd> \<sigma>
trm_rep (s \<lhd> \<sigma>) S = trm_rep s'' S
[PROOF STEP]
have "(trm_rep ?s  S) = (trm_rep (subst s' \<sigma>) S)"
[PROOF STATE]
proof (prove)
using this:
s'' = s' \<lhd> \<sigma>
trm_rep (s \<lhd> \<sigma>) S = trm_rep s'' S

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

goal (1 subgoal):
 1. \<not> maximal_literal_is_unique (t \<lhd> \<sigma>) (s \<lhd> \<sigma>) C L1 S \<sigma> \<Longrightarrow> False
[PROOF STEP]
from \<open>L' \<in> (C- { L1 })\<close> \<open>orient_lit_inst L' t' s' pos \<sigma>\<close> \<open>(subst t' \<sigma>) = ?t\<close>
  \<open>(trm_rep ?s  S) = (trm_rep (subst s' \<sigma>) S)\<close>
[PROOF STATE]
proof (chain)
picking this:
L' \<in> C - {L1}
orient_lit_inst L' t' s' pos \<sigma>
t' \<lhd> \<sigma> = t \<lhd> \<sigma>
trm_rep (s \<lhd> \<sigma>) S = trm_rep (s' \<lhd> \<sigma>) S
[PROOF STEP]
have "equivalent_eq_exists t s C (int_clset S) \<sigma> L1"
[PROOF STATE]
proof (prove)
using this:
L' \<in> C - {L1}
orient_lit_inst L' t' s' pos \<sigma>
t' \<lhd> \<sigma> = t \<lhd> \<sigma>
trm_rep (s \<lhd> \<sigma>) S = trm_rep (s' \<lhd> \<sigma>) S

goal (1 subgoal):
 1. equivalent_eq_exists t s C (int_clset S) \<sigma> L1
[PROOF STEP]
unfolding equivalent_eq_exists_def same_values_def int_clset_def
[PROOF STATE]
proof (prove)
using this:
L' \<in> C - {L1}
orient_lit_inst L' t' s' pos \<sigma>
t' \<lhd> \<sigma> = t \<lhd> \<sigma>
trm_rep (s \<lhd> \<sigma>) S = trm_rep (s' \<lhd> \<sigma>) S

goal (1 subgoal):
 1. \<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
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
equivalent_eq_exists t s C (int_clset S) \<sigma> L1

goal (1 subgoal):
 1. \<not> maximal_literal_is_unique (t \<lhd> \<sigma>) (s \<lhd> \<sigma>) C L1 S \<sigma> \<Longrightarrow> False
[PROOF STEP]
from this and assms(1)
[PROOF STATE]
proof (chain)
picking this:
equivalent_eq_exists t s C (int_clset S) \<sigma> L1
\<not> equivalent_eq_exists t s C (int_clset S) \<sigma> L1
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
equivalent_eq_exists t s C (int_clset S) \<sigma> L1
\<not> equivalent_eq_exists t s C (int_clset S) \<sigma> L1

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

goal:
No subgoals!
[PROOF STEP]
qed