[STATEMENT]
lemma lift_dom_trm:
  assumes "dom_trm (subst t \<theta>) (subst_cl C \<theta>)"
  assumes "\<sigma> \<doteq> \<theta> \<lozenge> \<eta>"
  shows "dom_trm (subst t \<sigma>) (subst_cl C \<sigma>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dom_trm (t \<lhd> \<sigma>) (subst_cl C \<sigma>)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. dom_trm (t \<lhd> \<sigma>) (subst_cl C \<sigma>)
[PROOF STEP]
let ?t = "(subst t \<theta>)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. dom_trm (t \<lhd> \<sigma>) (subst_cl C \<sigma>)
[PROOF STEP]
let ?t' = "(subst ?t \<eta>)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. dom_trm (t \<lhd> \<sigma>) (subst_cl C \<sigma>)
[PROOF STEP]
let ?t'' = "(subst t \<sigma>)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. dom_trm (t \<lhd> \<sigma>) (subst_cl C \<sigma>)
[PROOF STEP]
have "?t' = (subst t (\<theta> \<lozenge> \<eta>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t \<lhd> \<theta> \<lhd> \<eta> = t \<lhd> \<theta> \<lozenge> \<eta>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
t \<lhd> \<theta> \<lhd> \<eta> = t \<lhd> \<theta> \<lozenge> \<eta>

goal (1 subgoal):
 1. dom_trm (t \<lhd> \<sigma>) (subst_cl C \<sigma>)
[PROOF STEP]
from assms(2)
[PROOF STATE]
proof (chain)
picking this:
\<sigma> \<doteq> \<theta> \<lozenge> \<eta>
[PROOF STEP]
have "?t'' = (subst t (\<theta> \<lozenge> \<eta>))"
[PROOF STATE]
proof (prove)
using this:
\<sigma> \<doteq> \<theta> \<lozenge> \<eta>

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

goal (1 subgoal):
 1. dom_trm (t \<lhd> \<sigma>) (subst_cl C \<sigma>)
[PROOF STEP]
from this and \<open>?t' = (subst t (\<theta> \<lozenge> \<eta>))\<close>
[PROOF STATE]
proof (chain)
picking this:
t \<lhd> \<sigma> = t \<lhd> \<theta> \<lozenge> \<eta>
t \<lhd> \<theta> \<lhd> \<eta> = t \<lhd> \<theta> \<lozenge> \<eta>
[PROOF STEP]
have "?t' = ?t''"
[PROOF STATE]
proof (prove)
using this:
t \<lhd> \<sigma> = t \<lhd> \<theta> \<lozenge> \<eta>
t \<lhd> \<theta> \<lhd> \<eta> = t \<lhd> \<theta> \<lozenge> \<eta>

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

goal (1 subgoal):
 1. dom_trm (t \<lhd> \<sigma>) (subst_cl C \<sigma>)
[PROOF STEP]
from assms(1)
[PROOF STATE]
proof (chain)
picking this:
dom_trm (t \<lhd> \<theta>) (subst_cl C \<theta>)
[PROOF STEP]
have "(\<exists> L u v p. (L \<in> (subst_cl C \<theta>) \<and> (decompose_literal L u v p)
        \<and> (( (p = neg \<and> ?t = u) \<or> (?t,u) \<in> trm_ord))))"
[PROOF STATE]
proof (prove)
using this:
dom_trm (t \<lhd> \<theta>) (subst_cl C \<theta>)

goal (1 subgoal):
 1. \<exists>L u v p. L \<in> subst_cl C \<theta> \<and> decompose_literal L u v p \<and> (p = neg \<and> t \<lhd> \<theta> = u \<or> (t \<lhd> \<theta>, u) \<in> trm_ord)
[PROOF STEP]
unfolding dom_trm_def
[PROOF STATE]
proof (prove)
using this:
\<exists>L u v p. L \<in> subst_cl C \<theta> \<and> decompose_literal L u v p \<and> (p = neg \<and> t \<lhd> \<theta> = u \<or> (t \<lhd> \<theta>, u) \<in> trm_ord)

goal (1 subgoal):
 1. \<exists>L u v p. L \<in> subst_cl C \<theta> \<and> decompose_literal L u v p \<and> (p = neg \<and> t \<lhd> \<theta> = u \<or> (t \<lhd> \<theta>, u) \<in> trm_ord)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>L u v p. L \<in> subst_cl C \<theta> \<and> decompose_literal L u v p \<and> (p = neg \<and> t \<lhd> \<theta> = u \<or> (t \<lhd> \<theta>, u) \<in> trm_ord)

goal (1 subgoal):
 1. dom_trm (t \<lhd> \<sigma>) (subst_cl C \<sigma>)
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
\<exists>L u v p. L \<in> subst_cl C \<theta> \<and> decompose_literal L u v p \<and> (p = neg \<and> t \<lhd> \<theta> = u \<or> (t \<lhd> \<theta>, u) \<in> trm_ord)
[PROOF STEP]
obtain L u v p where  "L \<in> (subst_cl C \<theta>)"
    "decompose_literal L u v p" "(( (p = neg \<and> ?t = u) \<or> (?t,u) \<in> trm_ord))"
[PROOF STATE]
proof (prove)
using this:
\<exists>L u v p. L \<in> subst_cl C \<theta> \<and> decompose_literal L u v p \<and> (p = neg \<and> t \<lhd> \<theta> = u \<or> (t \<lhd> \<theta>, u) \<in> trm_ord)

goal (1 subgoal):
 1. (\<And>L u v p. \<lbrakk>L \<in> subst_cl C \<theta>; decompose_literal L u v p; p = neg \<and> t \<lhd> \<theta> = u \<or> (t \<lhd> \<theta>, u) \<in> trm_ord\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding dom_trm_def
[PROOF STATE]
proof (prove)
using this:
\<exists>L u v p. L \<in> subst_cl C \<theta> \<and> decompose_literal L u v p \<and> (p = neg \<and> t \<lhd> \<theta> = u \<or> (t \<lhd> \<theta>, u) \<in> trm_ord)

goal (1 subgoal):
 1. (\<And>L u v p. \<lbrakk>L \<in> subst_cl C \<theta>; decompose_literal L u v p; p = neg \<and> t \<lhd> \<theta> = u \<or> (t \<lhd> \<theta>, u) \<in> trm_ord\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
L \<in> subst_cl C \<theta>
decompose_literal L u v p
p = neg \<and> t \<lhd> \<theta> = u \<or> (t \<lhd> \<theta>, u) \<in> trm_ord

goal (1 subgoal):
 1. dom_trm (t \<lhd> \<sigma>) (subst_cl C \<sigma>)
[PROOF STEP]
from \<open>L \<in> (subst_cl C \<theta>)\<close>
[PROOF STATE]
proof (chain)
picking this:
L \<in> subst_cl C \<theta>
[PROOF STEP]
obtain L' where "L' \<in> C"
    "L = (subst_lit L' \<theta>)"
[PROOF STATE]
proof (prove)
using this:
L \<in> subst_cl C \<theta>

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

goal (1 subgoal):
 1. dom_trm (t \<lhd> \<sigma>) (subst_cl C \<sigma>)
[PROOF STEP]
from this and \<open>decompose_literal L u v p\<close>
[PROOF STATE]
proof (chain)
picking this:
L' \<in> C
L = subst_lit L' \<theta>
decompose_literal L u v p
[PROOF STEP]
have "decompose_literal (subst_lit L' \<theta>) u v p"
[PROOF STATE]
proof (prove)
using this:
L' \<in> C
L = subst_lit L' \<theta>
decompose_literal L u v p

goal (1 subgoal):
 1. decompose_literal (subst_lit L' \<theta>) u v p
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
decompose_literal (subst_lit L' \<theta>) u v p

goal (1 subgoal):
 1. dom_trm (t \<lhd> \<sigma>) (subst_cl C \<sigma>)
[PROOF STEP]
from this assms(2)  \<open>L = (subst_lit L' \<theta>)\<close>
[PROOF STATE]
proof (chain)
picking this:
decompose_literal (subst_lit L' \<theta>) u v p
\<sigma> \<doteq> \<theta> \<lozenge> \<eta>
L = subst_lit L' \<theta>
[PROOF STEP]
have "decompose_literal (subst_lit L' \<sigma>) (subst u \<eta>) (subst v \<eta>) p"
[PROOF STATE]
proof (prove)
using this:
decompose_literal (subst_lit L' \<theta>) u v p
\<sigma> \<doteq> \<theta> \<lozenge> \<eta>
L = subst_lit L' \<theta>

goal (1 subgoal):
 1. decompose_literal (subst_lit L' \<sigma>) (u \<lhd> \<eta>) (v \<lhd> \<eta>) p
[PROOF STEP]
using lift_decompose_literal [of L' \<theta> u v p \<sigma> \<eta>]
[PROOF STATE]
proof (prove)
using this:
decompose_literal (subst_lit L' \<theta>) u v p
\<sigma> \<doteq> \<theta> \<lozenge> \<eta>
L = subst_lit L' \<theta>
\<lbrakk>decompose_literal (subst_lit L' \<theta>) u v p; \<sigma> \<doteq> \<theta> \<lozenge> \<eta>\<rbrakk> \<Longrightarrow> decompose_literal (subst_lit L' \<sigma>) (u \<lhd> \<eta>) (v \<lhd> \<eta>) p

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

goal (1 subgoal):
 1. dom_trm (t \<lhd> \<sigma>) (subst_cl C \<sigma>)
[PROOF STEP]
let ?u = "(subst u \<eta>)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. dom_trm (t \<lhd> \<sigma>) (subst_cl C \<sigma>)
[PROOF STEP]
from \<open>L' \<in> C\<close>
[PROOF STATE]
proof (chain)
picking this:
L' \<in> C
[PROOF STEP]
have "(subst_lit L' \<sigma>) \<in> (subst_cl C \<sigma>)"
[PROOF STATE]
proof (prove)
using this:
L' \<in> C

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

goal (1 subgoal):
 1. dom_trm (t \<lhd> \<sigma>) (subst_cl C \<sigma>)
[PROOF STEP]
from \<open>(( (p = neg \<and> ?t = u) \<or> (?t,u) \<in> trm_ord))\<close>
[PROOF STATE]
proof (chain)
picking this:
p = neg \<and> t \<lhd> \<theta> = u \<or> (t \<lhd> \<theta>, u) \<in> trm_ord
[PROOF STEP]
have "(( (p = neg \<and> ?t' = ?u) \<or> (?t',?u) \<in> trm_ord))"
[PROOF STATE]
proof (prove)
using this:
p = neg \<and> t \<lhd> \<theta> = u \<or> (t \<lhd> \<theta>, u) \<in> trm_ord

goal (1 subgoal):
 1. p = neg \<and> t \<lhd> \<theta> \<lhd> \<eta> = u \<lhd> \<eta> \<or> (t \<lhd> \<theta> \<lhd> \<eta>, u \<lhd> \<eta>) \<in> trm_ord
[PROOF STEP]
using trm_ord_subst
[PROOF STATE]
proof (prove)
using this:
p = neg \<and> t \<lhd> \<theta> = u \<or> (t \<lhd> \<theta>, u) \<in> trm_ord
\<forall>s x y. (x, y) \<in> trm_ord \<longrightarrow> (x \<lhd> s, y \<lhd> s) \<in> trm_ord

goal (1 subgoal):
 1. p = neg \<and> t \<lhd> \<theta> \<lhd> \<eta> = u \<lhd> \<eta> \<or> (t \<lhd> \<theta> \<lhd> \<eta>, u \<lhd> \<eta>) \<in> trm_ord
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p = neg \<and> t \<lhd> \<theta> \<lhd> \<eta> = u \<lhd> \<eta> \<or> (t \<lhd> \<theta> \<lhd> \<eta>, u \<lhd> \<eta>) \<in> trm_ord

goal (1 subgoal):
 1. dom_trm (t \<lhd> \<sigma>) (subst_cl C \<sigma>)
[PROOF STEP]
from this and \<open>?t' = ?t''\<close>
[PROOF STATE]
proof (chain)
picking this:
p = neg \<and> t \<lhd> \<theta> \<lhd> \<eta> = u \<lhd> \<eta> \<or> (t \<lhd> \<theta> \<lhd> \<eta>, u \<lhd> \<eta>) \<in> trm_ord
t \<lhd> \<theta> \<lhd> \<eta> = t \<lhd> \<sigma>
[PROOF STEP]
have "(( (p = neg \<and> ?t'' = ?u) \<or> (?t'',?u) \<in> trm_ord))"
[PROOF STATE]
proof (prove)
using this:
p = neg \<and> t \<lhd> \<theta> \<lhd> \<eta> = u \<lhd> \<eta> \<or> (t \<lhd> \<theta> \<lhd> \<eta>, u \<lhd> \<eta>) \<in> trm_ord
t \<lhd> \<theta> \<lhd> \<eta> = t \<lhd> \<sigma>

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

goal (1 subgoal):
 1. dom_trm (t \<lhd> \<sigma>) (subst_cl C \<sigma>)
[PROOF STEP]
from this \<open>(subst_lit L' \<sigma>) \<in> (subst_cl C \<sigma>)\<close>
    \<open>decompose_literal (subst_lit L' \<sigma>) (subst u \<eta>) (subst v \<eta>) p\<close>
[PROOF STATE]
proof (chain)
picking this:
p = neg \<and> t \<lhd> \<sigma> = u \<lhd> \<eta> \<or> (t \<lhd> \<sigma>, u \<lhd> \<eta>) \<in> trm_ord
subst_lit L' \<sigma> \<in> subst_cl C \<sigma>
decompose_literal (subst_lit L' \<sigma>) (u \<lhd> \<eta>) (v \<lhd> \<eta>) p
[PROOF STEP]
show "dom_trm (subst t \<sigma>) (subst_cl C \<sigma>)"
[PROOF STATE]
proof (prove)
using this:
p = neg \<and> t \<lhd> \<sigma> = u \<lhd> \<eta> \<or> (t \<lhd> \<sigma>, u \<lhd> \<eta>) \<in> trm_ord
subst_lit L' \<sigma> \<in> subst_cl C \<sigma>
decompose_literal (subst_lit L' \<sigma>) (u \<lhd> \<eta>) (v \<lhd> \<eta>) p

goal (1 subgoal):
 1. dom_trm (t \<lhd> \<sigma>) (subst_cl C \<sigma>)
[PROOF STEP]
unfolding dom_trm_def
[PROOF STATE]
proof (prove)
using this:
p = neg \<and> t \<lhd> \<sigma> = u \<lhd> \<eta> \<or> (t \<lhd> \<sigma>, u \<lhd> \<eta>) \<in> trm_ord
subst_lit L' \<sigma> \<in> subst_cl C \<sigma>
decompose_literal (subst_lit L' \<sigma>) (u \<lhd> \<eta>) (v \<lhd> \<eta>) p

goal (1 subgoal):
 1. \<exists>L u v p. L \<in> subst_cl C \<sigma> \<and> decompose_literal L u v p \<and> (p = neg \<and> t \<lhd> \<sigma> = u \<or> (t \<lhd> \<sigma>, u) \<in> trm_ord)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dom_trm (t \<lhd> \<sigma>) (subst_cl C \<sigma>)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma lift_irreducible_terms:
  assumes "T = get_trms C (dom_trms (subst_cl D \<sigma>) (subst_set E \<sigma>)) Ground"
  assumes "\<sigma> \<doteq> \<theta> \<lozenge> \<eta>"
  shows "\<exists>T'. ( (subst_set T' \<eta>) \<subseteq> T \<and> T' = get_trms C'
    (dom_trms (subst_cl D \<theta>) (subst_set E \<theta>)) FirstOrder)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>T'. subst_set T' \<eta> \<subseteq> T \<and> T' = get_trms C' (dom_trms (subst_cl D \<theta>) (subst_set E \<theta>)) FirstOrder
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>T'. subst_set T' \<eta> \<subseteq> T \<and> T' = get_trms C' (dom_trms (subst_cl D \<theta>) (subst_set E \<theta>)) FirstOrder
[PROOF STEP]
let ?E = "(dom_trms (subst_cl D \<theta>) (subst_set E \<theta>))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>T'. subst_set T' \<eta> \<subseteq> T \<and> T' = get_trms C' (dom_trms (subst_cl D \<theta>) (subst_set E \<theta>)) FirstOrder
[PROOF STEP]
let ?E' = "(dom_trms (subst_cl D \<sigma>) (subst_set E \<sigma>))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>T'. subst_set T' \<eta> \<subseteq> T \<and> T' = get_trms C' (dom_trms (subst_cl D \<theta>) (subst_set E \<theta>)) FirstOrder
[PROOF STEP]
let ?T' = "(filter_trms C' ?E)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>T'. subst_set T' \<eta> \<subseteq> T \<and> T' = get_trms C' (dom_trms (subst_cl D \<theta>) (subst_set E \<theta>)) FirstOrder
[PROOF STEP]
have "?T' = get_trms C' ?E FirstOrder"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. filter_trms C' (dom_trms (subst_cl D \<theta>) (subst_set E \<theta>)) = get_trms C' (dom_trms (subst_cl D \<theta>) (subst_set E \<theta>)) FirstOrder
[PROOF STEP]
unfolding get_trms_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. filter_trms C' (dom_trms (subst_cl D \<theta>) (subst_set E \<theta>)) = (if FirstOrder = FirstOrder then filter_trms C' (dom_trms (subst_cl D \<theta>) (subst_set E \<theta>)) else dom_trms (subst_cl D \<theta>) (subst_set E \<theta>))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
filter_trms C' (dom_trms (subst_cl D \<theta>) (subst_set E \<theta>)) = get_trms C' (dom_trms (subst_cl D \<theta>) (subst_set E \<theta>)) FirstOrder

goal (1 subgoal):
 1. \<exists>T'. subst_set T' \<eta> \<subseteq> T \<and> T' = get_trms C' (dom_trms (subst_cl D \<theta>) (subst_set E \<theta>)) FirstOrder
[PROOF STEP]
from assms(1)
[PROOF STATE]
proof (chain)
picking this:
T = get_trms C (dom_trms (subst_cl D \<sigma>) (subst_set E \<sigma>)) Ground
[PROOF STEP]
have "T = ?E'"
[PROOF STATE]
proof (prove)
using this:
T = get_trms C (dom_trms (subst_cl D \<sigma>) (subst_set E \<sigma>)) Ground

goal (1 subgoal):
 1. T = dom_trms (subst_cl D \<sigma>) (subst_set E \<sigma>)
[PROOF STEP]
unfolding get_trms_def
[PROOF STATE]
proof (prove)
using this:
T = (if Ground = FirstOrder then filter_trms C (dom_trms (subst_cl D \<sigma>) (subst_set E \<sigma>)) else dom_trms (subst_cl D \<sigma>) (subst_set E \<sigma>))

goal (1 subgoal):
 1. T = dom_trms (subst_cl D \<sigma>) (subst_set E \<sigma>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
T = dom_trms (subst_cl D \<sigma>) (subst_set E \<sigma>)

goal (1 subgoal):
 1. \<exists>T'. subst_set T' \<eta> \<subseteq> T \<and> T' = get_trms C' (dom_trms (subst_cl D \<theta>) (subst_set E \<theta>)) FirstOrder
[PROOF STEP]
have "(subst_set ?T' \<eta>) \<subseteq> ?E'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subst_set (filter_trms C' (dom_trms (subst_cl D \<theta>) (subst_set E \<theta>))) \<eta> \<subseteq> dom_trms (subst_cl D \<sigma>) (subst_set E \<sigma>)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> subst_set (filter_trms C' (dom_trms (subst_cl D \<theta>) (subst_set E \<theta>))) \<eta> \<Longrightarrow> x \<in> dom_trms (subst_cl D \<sigma>) (subst_set E \<sigma>)
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> subst_set (filter_trms C' (dom_trms (subst_cl D \<theta>) (subst_set E \<theta>))) \<eta> \<Longrightarrow> x \<in> dom_trms (subst_cl D \<sigma>) (subst_set E \<sigma>)
[PROOF STEP]
assume "x \<in> (subst_set ?T' \<eta>)"
[PROOF STATE]
proof (state)
this:
x \<in> subst_set (filter_trms C' (dom_trms (subst_cl D \<theta>) (subst_set E \<theta>))) \<eta>

goal (1 subgoal):
 1. \<And>x. x \<in> subst_set (filter_trms C' (dom_trms (subst_cl D \<theta>) (subst_set E \<theta>))) \<eta> \<Longrightarrow> x \<in> dom_trms (subst_cl D \<sigma>) (subst_set E \<sigma>)
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
x \<in> subst_set (filter_trms C' (dom_trms (subst_cl D \<theta>) (subst_set E \<theta>))) \<eta>
[PROOF STEP]
obtain x' where "x = (subst x' \<eta>)" and "x' \<in> ?T'"
[PROOF STATE]
proof (prove)
using this:
x \<in> subst_set (filter_trms C' (dom_trms (subst_cl D \<theta>) (subst_set E \<theta>))) \<eta>

goal (1 subgoal):
 1. (\<And>x'. \<lbrakk>x = x' \<lhd> \<eta>; x' \<in> filter_trms C' (dom_trms (subst_cl D \<theta>) (subst_set E \<theta>))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x = x' \<lhd> \<eta>
x' \<in> filter_trms C' (dom_trms (subst_cl D \<theta>) (subst_set E \<theta>))

goal (1 subgoal):
 1. \<And>x. x \<in> subst_set (filter_trms C' (dom_trms (subst_cl D \<theta>) (subst_set E \<theta>))) \<eta> \<Longrightarrow> x \<in> dom_trms (subst_cl D \<sigma>) (subst_set E \<sigma>)
[PROOF STEP]
from \<open>x' \<in> ?T'\<close>
[PROOF STATE]
proof (chain)
picking this:
x' \<in> filter_trms C' (dom_trms (subst_cl D \<theta>) (subst_set E \<theta>))
[PROOF STEP]
have "x' \<in> ?E"
[PROOF STATE]
proof (prove)
using this:
x' \<in> filter_trms C' (dom_trms (subst_cl D \<theta>) (subst_set E \<theta>))

goal (1 subgoal):
 1. x' \<in> dom_trms (subst_cl D \<theta>) (subst_set E \<theta>)
[PROOF STEP]
using filter_trms_inclusion
[PROOF STATE]
proof (prove)
using this:
x' \<in> filter_trms C' (dom_trms (subst_cl D \<theta>) (subst_set E \<theta>))
filter_trms ?C ?E \<subseteq> ?E

goal (1 subgoal):
 1. x' \<in> dom_trms (subst_cl D \<theta>) (subst_set E \<theta>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x' \<in> dom_trms (subst_cl D \<theta>) (subst_set E \<theta>)

goal (1 subgoal):
 1. \<And>x. x \<in> subst_set (filter_trms C' (dom_trms (subst_cl D \<theta>) (subst_set E \<theta>))) \<eta> \<Longrightarrow> x \<in> dom_trms (subst_cl D \<sigma>) (subst_set E \<sigma>)
[PROOF STEP]
from \<open>x' \<in> ?E\<close>
[PROOF STATE]
proof (chain)
picking this:
x' \<in> dom_trms (subst_cl D \<theta>) (subst_set E \<theta>)
[PROOF STEP]
have "x' \<in> (subst_set E \<theta>)"
      and "dom_trm x' (subst_cl D \<theta>)"
[PROOF STATE]
proof (prove)
using this:
x' \<in> dom_trms (subst_cl D \<theta>) (subst_set E \<theta>)

goal (1 subgoal):
 1. x' \<in> subst_set E \<theta> &&& dom_trm x' (subst_cl D \<theta>)
[PROOF STEP]
unfolding dom_trms_def
[PROOF STATE]
proof (prove)
using this:
x' \<in> {x \<in> subst_set E \<theta>. dom_trm x (subst_cl D \<theta>)}

goal (1 subgoal):
 1. x' \<in> subst_set E \<theta> &&& dom_trm x' (subst_cl D \<theta>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x' \<in> subst_set E \<theta>
dom_trm x' (subst_cl D \<theta>)

goal (1 subgoal):
 1. \<And>x. x \<in> subst_set (filter_trms C' (dom_trms (subst_cl D \<theta>) (subst_set E \<theta>))) \<eta> \<Longrightarrow> x \<in> dom_trms (subst_cl D \<sigma>) (subst_set E \<sigma>)
[PROOF STEP]
from \<open>x' \<in> (subst_set E \<theta>)\<close>
[PROOF STATE]
proof (chain)
picking this:
x' \<in> subst_set E \<theta>
[PROOF STEP]
obtain y where "y \<in> E"
      and "x' = (subst y \<theta>)"
[PROOF STATE]
proof (prove)
using this:
x' \<in> subst_set E \<theta>

goal (1 subgoal):
 1. (\<And>y. \<lbrakk>y \<in> E; x' = y \<lhd> \<theta>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
y \<in> E
x' = y \<lhd> \<theta>

goal (1 subgoal):
 1. \<And>x. x \<in> subst_set (filter_trms C' (dom_trms (subst_cl D \<theta>) (subst_set E \<theta>))) \<eta> \<Longrightarrow> x \<in> dom_trms (subst_cl D \<sigma>) (subst_set E \<sigma>)
[PROOF STEP]
from \<open>x' = (subst y \<theta>)\<close> and \<open>dom_trm x' (subst_cl D \<theta>)\<close>
[PROOF STATE]
proof (chain)
picking this:
x' = y \<lhd> \<theta>
dom_trm x' (subst_cl D \<theta>)
[PROOF STEP]
have "dom_trm (subst y \<theta>) (subst_cl D \<theta>)"
[PROOF STATE]
proof (prove)
using this:
x' = y \<lhd> \<theta>
dom_trm x' (subst_cl D \<theta>)

goal (1 subgoal):
 1. dom_trm (y \<lhd> \<theta>) (subst_cl D \<theta>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dom_trm (y \<lhd> \<theta>) (subst_cl D \<theta>)

goal (1 subgoal):
 1. \<And>x. x \<in> subst_set (filter_trms C' (dom_trms (subst_cl D \<theta>) (subst_set E \<theta>))) \<eta> \<Longrightarrow> x \<in> dom_trms (subst_cl D \<sigma>) (subst_set E \<sigma>)
[PROOF STEP]
from this assms(2)
[PROOF STATE]
proof (chain)
picking this:
dom_trm (y \<lhd> \<theta>) (subst_cl D \<theta>)
\<sigma> \<doteq> \<theta> \<lozenge> \<eta>
[PROOF STEP]
have "dom_trm (subst y \<sigma>) (subst_cl D \<sigma>)"
[PROOF STATE]
proof (prove)
using this:
dom_trm (y \<lhd> \<theta>) (subst_cl D \<theta>)
\<sigma> \<doteq> \<theta> \<lozenge> \<eta>

goal (1 subgoal):
 1. dom_trm (y \<lhd> \<sigma>) (subst_cl D \<sigma>)
[PROOF STEP]
using lift_dom_trm
[PROOF STATE]
proof (prove)
using this:
dom_trm (y \<lhd> \<theta>) (subst_cl D \<theta>)
\<sigma> \<doteq> \<theta> \<lozenge> \<eta>
\<lbrakk>dom_trm (?t \<lhd> ?\<theta>) (subst_cl ?C ?\<theta>); ?\<sigma> \<doteq> ?\<theta> \<lozenge> ?\<eta>\<rbrakk> \<Longrightarrow> dom_trm (?t \<lhd> ?\<sigma>) (subst_cl ?C ?\<sigma>)

goal (1 subgoal):
 1. dom_trm (y \<lhd> \<sigma>) (subst_cl D \<sigma>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dom_trm (y \<lhd> \<sigma>) (subst_cl D \<sigma>)

goal (1 subgoal):
 1. \<And>x. x \<in> subst_set (filter_trms C' (dom_trms (subst_cl D \<theta>) (subst_set E \<theta>))) \<eta> \<Longrightarrow> x \<in> dom_trms (subst_cl D \<sigma>) (subst_set E \<sigma>)
[PROOF STEP]
from \<open>y \<in> E\<close>
[PROOF STATE]
proof (chain)
picking this:
y \<in> E
[PROOF STEP]
have "(subst y \<sigma>) \<in> (subst_set E \<sigma>)"
[PROOF STATE]
proof (prove)
using this:
y \<in> E

goal (1 subgoal):
 1. y \<lhd> \<sigma> \<in> subst_set E \<sigma>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
y \<lhd> \<sigma> \<in> subst_set E \<sigma>

goal (1 subgoal):
 1. \<And>x. x \<in> subst_set (filter_trms C' (dom_trms (subst_cl D \<theta>) (subst_set E \<theta>))) \<eta> \<Longrightarrow> x \<in> dom_trms (subst_cl D \<sigma>) (subst_set E \<sigma>)
[PROOF STEP]
from this and \<open>dom_trm (subst y \<sigma>) (subst_cl D \<sigma>)\<close>
[PROOF STATE]
proof (chain)
picking this:
y \<lhd> \<sigma> \<in> subst_set E \<sigma>
dom_trm (y \<lhd> \<sigma>) (subst_cl D \<sigma>)
[PROOF STEP]
have "(subst y \<sigma>) \<in> ?E'"
[PROOF STATE]
proof (prove)
using this:
y \<lhd> \<sigma> \<in> subst_set E \<sigma>
dom_trm (y \<lhd> \<sigma>) (subst_cl D \<sigma>)

goal (1 subgoal):
 1. y \<lhd> \<sigma> \<in> dom_trms (subst_cl D \<sigma>) (subst_set E \<sigma>)
[PROOF STEP]
unfolding dom_trms_def
[PROOF STATE]
proof (prove)
using this:
y \<lhd> \<sigma> \<in> subst_set E \<sigma>
dom_trm (y \<lhd> \<sigma>) (subst_cl D \<sigma>)

goal (1 subgoal):
 1. y \<lhd> \<sigma> \<in> {x \<in> subst_set E \<sigma>. dom_trm x (subst_cl D \<sigma>)}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
y \<lhd> \<sigma> \<in> dom_trms (subst_cl D \<sigma>) (subst_set E \<sigma>)

goal (1 subgoal):
 1. \<And>x. x \<in> subst_set (filter_trms C' (dom_trms (subst_cl D \<theta>) (subst_set E \<theta>))) \<eta> \<Longrightarrow> x \<in> dom_trms (subst_cl D \<sigma>) (subst_set E \<sigma>)
[PROOF STEP]
from assms(2)
[PROOF STATE]
proof (chain)
picking this:
\<sigma> \<doteq> \<theta> \<lozenge> \<eta>
[PROOF STEP]
have "(subst y \<sigma>) = (subst y (\<theta> \<lozenge> \<eta>))"
[PROOF STATE]
proof (prove)
using this:
\<sigma> \<doteq> \<theta> \<lozenge> \<eta>

goal (1 subgoal):
 1. y \<lhd> \<sigma> = y \<lhd> \<theta> \<lozenge> \<eta>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
y \<lhd> \<sigma> = y \<lhd> \<theta> \<lozenge> \<eta>

goal (1 subgoal):
 1. \<And>x. x \<in> subst_set (filter_trms C' (dom_trms (subst_cl D \<theta>) (subst_set E \<theta>))) \<eta> \<Longrightarrow> x \<in> dom_trms (subst_cl D \<sigma>) (subst_set E \<sigma>)
[PROOF STEP]
from this \<open>x = (subst x' \<eta>)\<close> and \<open>x' = (subst y \<theta>)\<close>
[PROOF STATE]
proof (chain)
picking this:
y \<lhd> \<sigma> = y \<lhd> \<theta> \<lozenge> \<eta>
x = x' \<lhd> \<eta>
x' = y \<lhd> \<theta>
[PROOF STEP]
have "x = (subst y \<sigma>)"
[PROOF STATE]
proof (prove)
using this:
y \<lhd> \<sigma> = y \<lhd> \<theta> \<lozenge> \<eta>
x = x' \<lhd> \<eta>
x' = y \<lhd> \<theta>

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

goal (1 subgoal):
 1. \<And>x. x \<in> subst_set (filter_trms C' (dom_trms (subst_cl D \<theta>) (subst_set E \<theta>))) \<eta> \<Longrightarrow> x \<in> dom_trms (subst_cl D \<sigma>) (subst_set E \<sigma>)
[PROOF STEP]
from this and \<open>(subst y \<sigma>) \<in> ?E'\<close>
[PROOF STATE]
proof (chain)
picking this:
x = y \<lhd> \<sigma>
y \<lhd> \<sigma> \<in> dom_trms (subst_cl D \<sigma>) (subst_set E \<sigma>)
[PROOF STEP]
show "x \<in> ?E'"
[PROOF STATE]
proof (prove)
using this:
x = y \<lhd> \<sigma>
y \<lhd> \<sigma> \<in> dom_trms (subst_cl D \<sigma>) (subst_set E \<sigma>)

goal (1 subgoal):
 1. x \<in> dom_trms (subst_cl D \<sigma>) (subst_set E \<sigma>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> dom_trms (subst_cl D \<sigma>) (subst_set E \<sigma>)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
subst_set (filter_trms C' (dom_trms (subst_cl D \<theta>) (subst_set E \<theta>))) \<eta> \<subseteq> dom_trms (subst_cl D \<sigma>) (subst_set E \<sigma>)

goal (1 subgoal):
 1. \<exists>T'. subst_set T' \<eta> \<subseteq> T \<and> T' = get_trms C' (dom_trms (subst_cl D \<theta>) (subst_set E \<theta>)) FirstOrder
[PROOF STEP]
from this and \<open>T = ?E'\<close> \<open>?T' = get_trms C' ?E FirstOrder\<close>
[PROOF STATE]
proof (chain)
picking this:
subst_set (filter_trms C' (dom_trms (subst_cl D \<theta>) (subst_set E \<theta>))) \<eta> \<subseteq> dom_trms (subst_cl D \<sigma>) (subst_set E \<sigma>)
T = dom_trms (subst_cl D \<sigma>) (subst_set E \<sigma>)
filter_trms C' (dom_trms (subst_cl D \<theta>) (subst_set E \<theta>)) = get_trms C' (dom_trms (subst_cl D \<theta>) (subst_set E \<theta>)) FirstOrder
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
subst_set (filter_trms C' (dom_trms (subst_cl D \<theta>) (subst_set E \<theta>))) \<eta> \<subseteq> dom_trms (subst_cl D \<sigma>) (subst_set E \<sigma>)
T = dom_trms (subst_cl D \<sigma>) (subst_set E \<sigma>)
filter_trms C' (dom_trms (subst_cl D \<theta>) (subst_set E \<theta>)) = get_trms C' (dom_trms (subst_cl D \<theta>) (subst_set E \<theta>)) FirstOrder

goal (1 subgoal):
 1. \<exists>T'. subst_set T' \<eta> \<subseteq> T \<and> T' = get_trms C' (dom_trms (subst_cl D \<theta>) (subst_set E \<theta>)) FirstOrder
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>T'. subst_set T' \<eta> \<subseteq> T \<and> T' = get_trms C' (dom_trms (subst_cl D \<theta>) (subst_set E \<theta>)) FirstOrder

goal:
No subgoals!
[PROOF STEP]
qed