[STATEMENT]
lemma project_sub:
  assumes inst_C:"C \<cdot>\<^sub>l\<^sub>s lmbd = C'"
  assumes L'sub: "L' \<subseteq> C'"
  shows "\<exists>L \<subseteq> C. L \<cdot>\<^sub>l\<^sub>s lmbd = L' \<and> (C-L) \<cdot>\<^sub>l\<^sub>s lmbd = C' - L'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>L\<subseteq>C. L \<cdot>\<^sub>l\<^sub>s lmbd = L' \<and> C - L \<cdot>\<^sub>l\<^sub>s lmbd = C' - L'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>L\<subseteq>C. L \<cdot>\<^sub>l\<^sub>s lmbd = L' \<and> C - L \<cdot>\<^sub>l\<^sub>s lmbd = C' - L'
[PROOF STEP]
let ?L = "{l \<in> C. \<exists>l' \<in> L'. l \<cdot>\<^sub>l lmbd = l'}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>L\<subseteq>C. L \<cdot>\<^sub>l\<^sub>s lmbd = L' \<and> C - L \<cdot>\<^sub>l\<^sub>s lmbd = C' - L'
[PROOF STEP]
have "?L \<subseteq> C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {l \<in> C. \<exists>l'\<in>L'. l \<cdot>\<^sub>l lmbd = l'} \<subseteq> C
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{l \<in> C. \<exists>l'\<in>L'. l \<cdot>\<^sub>l lmbd = l'} \<subseteq> C

goal (1 subgoal):
 1. \<exists>L\<subseteq>C. L \<cdot>\<^sub>l\<^sub>s lmbd = L' \<and> C - L \<cdot>\<^sub>l\<^sub>s lmbd = C' - L'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
{l \<in> C. \<exists>l'\<in>L'. l \<cdot>\<^sub>l lmbd = l'} \<subseteq> C

goal (1 subgoal):
 1. \<exists>L\<subseteq>C. L \<cdot>\<^sub>l\<^sub>s lmbd = L' \<and> C - L \<cdot>\<^sub>l\<^sub>s lmbd = C' - L'
[PROOF STEP]
have "?L \<cdot>\<^sub>l\<^sub>s lmbd = L'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {l \<in> C. \<exists>l'\<in>L'. l \<cdot>\<^sub>l lmbd = l'} \<cdot>\<^sub>l\<^sub>s lmbd = L'
[PROOF STEP]
proof (rule Orderings.order_antisym; rule Set.subsetI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in> {l \<in> C. \<exists>l'\<in>L'. l \<cdot>\<^sub>l lmbd = l'} \<cdot>\<^sub>l\<^sub>s lmbd \<Longrightarrow> x \<in> L'
 2. \<And>x. x \<in> L' \<Longrightarrow> x \<in> {l \<in> C. \<exists>l'\<in>L'. l \<cdot>\<^sub>l lmbd = l'} \<cdot>\<^sub>l\<^sub>s lmbd
[PROOF STEP]
fix l'
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in> {l \<in> C. \<exists>l'\<in>L'. l \<cdot>\<^sub>l lmbd = l'} \<cdot>\<^sub>l\<^sub>s lmbd \<Longrightarrow> x \<in> L'
 2. \<And>x. x \<in> L' \<Longrightarrow> x \<in> {l \<in> C. \<exists>l'\<in>L'. l \<cdot>\<^sub>l lmbd = l'} \<cdot>\<^sub>l\<^sub>s lmbd
[PROOF STEP]
assume l'L: "l' \<in> L'"
[PROOF STATE]
proof (state)
this:
l' \<in> L'

goal (2 subgoals):
 1. \<And>x. x \<in> {l \<in> C. \<exists>l'\<in>L'. l \<cdot>\<^sub>l lmbd = l'} \<cdot>\<^sub>l\<^sub>s lmbd \<Longrightarrow> x \<in> L'
 2. \<And>x. x \<in> L' \<Longrightarrow> x \<in> {l \<in> C. \<exists>l'\<in>L'. l \<cdot>\<^sub>l lmbd = l'} \<cdot>\<^sub>l\<^sub>s lmbd
[PROOF STEP]
from inst_C
[PROOF STATE]
proof (chain)
picking this:
C \<cdot>\<^sub>l\<^sub>s lmbd = C'
[PROOF STEP]
have "{l \<cdot>\<^sub>l lmbd|l. l \<in> C} = C'"
[PROOF STATE]
proof (prove)
using this:
C \<cdot>\<^sub>l\<^sub>s lmbd = C'

goal (1 subgoal):
 1. {l \<cdot>\<^sub>l lmbd |l. l \<in> C} = C'
[PROOF STEP]
unfolding subls_def2
[PROOF STATE]
proof (prove)
using this:
{l \<cdot>\<^sub>l lmbd |l. l \<in> C} = C'

goal (1 subgoal):
 1. {l \<cdot>\<^sub>l lmbd |l. l \<in> C} = C'
[PROOF STEP]
by -
[PROOF STATE]
proof (state)
this:
{l \<cdot>\<^sub>l lmbd |l. l \<in> C} = C'

goal (2 subgoals):
 1. \<And>x. x \<in> {l \<in> C. \<exists>l'\<in>L'. l \<cdot>\<^sub>l lmbd = l'} \<cdot>\<^sub>l\<^sub>s lmbd \<Longrightarrow> x \<in> L'
 2. \<And>x. x \<in> L' \<Longrightarrow> x \<in> {l \<in> C. \<exists>l'\<in>L'. l \<cdot>\<^sub>l lmbd = l'} \<cdot>\<^sub>l\<^sub>s lmbd
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
{l \<cdot>\<^sub>l lmbd |l. l \<in> C} = C'
[PROOF STEP]
have "\<exists>l. l' = l \<cdot>\<^sub>l lmbd \<and> l \<in> C \<and> l \<cdot>\<^sub>l lmbd \<in> L'"
[PROOF STATE]
proof (prove)
using this:
{l \<cdot>\<^sub>l lmbd |l. l \<in> C} = C'

goal (1 subgoal):
 1. \<exists>l. l' = l \<cdot>\<^sub>l lmbd \<and> l \<in> C \<and> l \<cdot>\<^sub>l lmbd \<in> L'
[PROOF STEP]
using L'sub l'L
[PROOF STATE]
proof (prove)
using this:
{l \<cdot>\<^sub>l lmbd |l. l \<in> C} = C'
L' \<subseteq> C'
l' \<in> L'

goal (1 subgoal):
 1. \<exists>l. l' = l \<cdot>\<^sub>l lmbd \<and> l \<in> C \<and> l \<cdot>\<^sub>l lmbd \<in> L'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>l. l' = l \<cdot>\<^sub>l lmbd \<and> l \<in> C \<and> l \<cdot>\<^sub>l lmbd \<in> L'

goal (2 subgoals):
 1. \<And>x. x \<in> {l \<in> C. \<exists>l'\<in>L'. l \<cdot>\<^sub>l lmbd = l'} \<cdot>\<^sub>l\<^sub>s lmbd \<Longrightarrow> x \<in> L'
 2. \<And>x. x \<in> L' \<Longrightarrow> x \<in> {l \<in> C. \<exists>l'\<in>L'. l \<cdot>\<^sub>l lmbd = l'} \<cdot>\<^sub>l\<^sub>s lmbd
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>l. l' = l \<cdot>\<^sub>l lmbd \<and> l \<in> C \<and> l \<cdot>\<^sub>l lmbd \<in> L'
[PROOF STEP]
have " l' \<in> {l \<in> C. l \<cdot>\<^sub>l lmbd \<in> L'} \<cdot>\<^sub>l\<^sub>s lmbd"
[PROOF STATE]
proof (prove)
using this:
\<exists>l. l' = l \<cdot>\<^sub>l lmbd \<and> l \<in> C \<and> l \<cdot>\<^sub>l lmbd \<in> L'

goal (1 subgoal):
 1. l' \<in> {l \<in> C. l \<cdot>\<^sub>l lmbd \<in> L'} \<cdot>\<^sub>l\<^sub>s lmbd
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
l' \<in> {l \<in> C. l \<cdot>\<^sub>l lmbd \<in> L'} \<cdot>\<^sub>l\<^sub>s lmbd

goal (2 subgoals):
 1. \<And>x. x \<in> {l \<in> C. \<exists>l'\<in>L'. l \<cdot>\<^sub>l lmbd = l'} \<cdot>\<^sub>l\<^sub>s lmbd \<Longrightarrow> x \<in> L'
 2. \<And>x. x \<in> L' \<Longrightarrow> x \<in> {l \<in> C. \<exists>l'\<in>L'. l \<cdot>\<^sub>l lmbd = l'} \<cdot>\<^sub>l\<^sub>s lmbd
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
l' \<in> {l \<in> C. l \<cdot>\<^sub>l lmbd \<in> L'} \<cdot>\<^sub>l\<^sub>s lmbd
[PROOF STEP]
show " l' \<in> {l \<in> C. \<exists>l'\<in>L'. l \<cdot>\<^sub>l lmbd = l'} \<cdot>\<^sub>l\<^sub>s lmbd"
[PROOF STATE]
proof (prove)
using this:
l' \<in> {l \<in> C. l \<cdot>\<^sub>l lmbd \<in> L'} \<cdot>\<^sub>l\<^sub>s lmbd

goal (1 subgoal):
 1. l' \<in> {l \<in> C. \<exists>l'\<in>L'. l \<cdot>\<^sub>l lmbd = l'} \<cdot>\<^sub>l\<^sub>s lmbd
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
l' \<in> {l \<in> C. \<exists>l'\<in>L'. l \<cdot>\<^sub>l lmbd = l'} \<cdot>\<^sub>l\<^sub>s lmbd

goal (1 subgoal):
 1. \<And>x. x \<in> {l \<in> C. \<exists>l'\<in>L'. l \<cdot>\<^sub>l lmbd = l'} \<cdot>\<^sub>l\<^sub>s lmbd \<Longrightarrow> x \<in> L'
[PROOF STEP]
qed auto
[PROOF STATE]
proof (state)
this:
{l \<in> C. \<exists>l'\<in>L'. l \<cdot>\<^sub>l lmbd = l'} \<cdot>\<^sub>l\<^sub>s lmbd = L'

goal (1 subgoal):
 1. \<exists>L\<subseteq>C. L \<cdot>\<^sub>l\<^sub>s lmbd = L' \<and> C - L \<cdot>\<^sub>l\<^sub>s lmbd = C' - L'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
{l \<in> C. \<exists>l'\<in>L'. l \<cdot>\<^sub>l lmbd = l'} \<cdot>\<^sub>l\<^sub>s lmbd = L'

goal (1 subgoal):
 1. \<exists>L\<subseteq>C. L \<cdot>\<^sub>l\<^sub>s lmbd = L' \<and> C - L \<cdot>\<^sub>l\<^sub>s lmbd = C' - L'
[PROOF STEP]
have "(C-?L) \<cdot>\<^sub>l\<^sub>s lmbd = C' - L'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C - {l \<in> C. \<exists>l'\<in>L'. l \<cdot>\<^sub>l lmbd = l'} \<cdot>\<^sub>l\<^sub>s lmbd = C' - L'
[PROOF STEP]
using inst_C
[PROOF STATE]
proof (prove)
using this:
C \<cdot>\<^sub>l\<^sub>s lmbd = C'

goal (1 subgoal):
 1. C - {l \<in> C. \<exists>l'\<in>L'. l \<cdot>\<^sub>l lmbd = l'} \<cdot>\<^sub>l\<^sub>s lmbd = C' - L'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
C - {l \<in> C. \<exists>l'\<in>L'. l \<cdot>\<^sub>l lmbd = l'} \<cdot>\<^sub>l\<^sub>s lmbd = C' - L'

goal (1 subgoal):
 1. \<exists>L\<subseteq>C. L \<cdot>\<^sub>l\<^sub>s lmbd = L' \<and> C - L \<cdot>\<^sub>l\<^sub>s lmbd = C' - L'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
{l \<in> C. \<exists>l'\<in>L'. l \<cdot>\<^sub>l lmbd = l'} \<subseteq> C
{l \<in> C. \<exists>l'\<in>L'. l \<cdot>\<^sub>l lmbd = l'} \<cdot>\<^sub>l\<^sub>s lmbd = L'
C - {l \<in> C. \<exists>l'\<in>L'. l \<cdot>\<^sub>l lmbd = l'} \<cdot>\<^sub>l\<^sub>s lmbd = C' - L'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
{l \<in> C. \<exists>l'\<in>L'. l \<cdot>\<^sub>l lmbd = l'} \<subseteq> C
{l \<in> C. \<exists>l'\<in>L'. l \<cdot>\<^sub>l lmbd = l'} \<cdot>\<^sub>l\<^sub>s lmbd = L'
C - {l \<in> C. \<exists>l'\<in>L'. l \<cdot>\<^sub>l lmbd = l'} \<cdot>\<^sub>l\<^sub>s lmbd = C' - L'

goal (1 subgoal):
 1. \<exists>L\<subseteq>C. L \<cdot>\<^sub>l\<^sub>s lmbd = L' \<and> C - L \<cdot>\<^sub>l\<^sub>s lmbd = C' - L'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>L\<subseteq>C. L \<cdot>\<^sub>l\<^sub>s lmbd = L' \<and> C - L \<cdot>\<^sub>l\<^sub>s lmbd = C' - L'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma relevant_vars_subt:
  assumes "\<forall>x \<in> vars\<^sub>t t. \<sigma>\<^sub>1 x = \<sigma>\<^sub>2 x"
  shows " t \<cdot>\<^sub>t \<sigma>\<^sub>1 = t \<cdot>\<^sub>t \<sigma>\<^sub>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t \<cdot>\<^sub>t \<sigma>\<^sub>1 = t \<cdot>\<^sub>t \<sigma>\<^sub>2
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>vars\<^sub>t t. \<sigma>\<^sub>1 x = \<sigma>\<^sub>2 x

goal (1 subgoal):
 1. t \<cdot>\<^sub>t \<sigma>\<^sub>1 = t \<cdot>\<^sub>t \<sigma>\<^sub>2
[PROOF STEP]
proof (induction t)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x1 x2a. \<lbrakk>\<And>x2aa. \<lbrakk>x2aa \<in> set x2a; \<forall>x\<in>vars\<^sub>t x2aa. \<sigma>\<^sub>1 x = \<sigma>\<^sub>2 x\<rbrakk> \<Longrightarrow> x2aa \<cdot>\<^sub>t \<sigma>\<^sub>1 = x2aa \<cdot>\<^sub>t \<sigma>\<^sub>2; \<forall>x\<in>vars\<^sub>t (Fun x1 x2a). \<sigma>\<^sub>1 x = \<sigma>\<^sub>2 x\<rbrakk> \<Longrightarrow> Fun x1 x2a \<cdot>\<^sub>t \<sigma>\<^sub>1 = Fun x1 x2a \<cdot>\<^sub>t \<sigma>\<^sub>2
 2. \<And>x. \<forall>x\<in>vars\<^sub>t (\<epsilon> x). \<sigma>\<^sub>1 x = \<sigma>\<^sub>2 x \<Longrightarrow> \<epsilon> x \<cdot>\<^sub>t \<sigma>\<^sub>1 = \<epsilon> x \<cdot>\<^sub>t \<sigma>\<^sub>2
[PROOF STEP]
case (Fun f ts)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?x2aa \<in> set ts; \<forall>x\<in>vars\<^sub>t ?x2aa. \<sigma>\<^sub>1 x = \<sigma>\<^sub>2 x\<rbrakk> \<Longrightarrow> ?x2aa \<cdot>\<^sub>t \<sigma>\<^sub>1 = ?x2aa \<cdot>\<^sub>t \<sigma>\<^sub>2
\<forall>x\<in>vars\<^sub>t (Fun f ts). \<sigma>\<^sub>1 x = \<sigma>\<^sub>2 x

goal (2 subgoals):
 1. \<And>x1 x2a. \<lbrakk>\<And>x2aa. \<lbrakk>x2aa \<in> set x2a; \<forall>x\<in>vars\<^sub>t x2aa. \<sigma>\<^sub>1 x = \<sigma>\<^sub>2 x\<rbrakk> \<Longrightarrow> x2aa \<cdot>\<^sub>t \<sigma>\<^sub>1 = x2aa \<cdot>\<^sub>t \<sigma>\<^sub>2; \<forall>x\<in>vars\<^sub>t (Fun x1 x2a). \<sigma>\<^sub>1 x = \<sigma>\<^sub>2 x\<rbrakk> \<Longrightarrow> Fun x1 x2a \<cdot>\<^sub>t \<sigma>\<^sub>1 = Fun x1 x2a \<cdot>\<^sub>t \<sigma>\<^sub>2
 2. \<And>x. \<forall>x\<in>vars\<^sub>t (\<epsilon> x). \<sigma>\<^sub>1 x = \<sigma>\<^sub>2 x \<Longrightarrow> \<epsilon> x \<cdot>\<^sub>t \<sigma>\<^sub>1 = \<epsilon> x \<cdot>\<^sub>t \<sigma>\<^sub>2
[PROOF STEP]
have f: "\<forall>t. t \<in> set ts \<longrightarrow> vars\<^sub>t t \<subseteq> vars\<^sub>t\<^sub>s ts"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>t. t \<in> set ts \<longrightarrow> vars\<^sub>t t \<subseteq> vars\<^sub>t\<^sub>s ts
[PROOF STEP]
by (induction ts) auto
[PROOF STATE]
proof (state)
this:
\<forall>t. t \<in> set ts \<longrightarrow> vars\<^sub>t t \<subseteq> vars\<^sub>t\<^sub>s ts

goal (2 subgoals):
 1. \<And>x1 x2a. \<lbrakk>\<And>x2aa. \<lbrakk>x2aa \<in> set x2a; \<forall>x\<in>vars\<^sub>t x2aa. \<sigma>\<^sub>1 x = \<sigma>\<^sub>2 x\<rbrakk> \<Longrightarrow> x2aa \<cdot>\<^sub>t \<sigma>\<^sub>1 = x2aa \<cdot>\<^sub>t \<sigma>\<^sub>2; \<forall>x\<in>vars\<^sub>t (Fun x1 x2a). \<sigma>\<^sub>1 x = \<sigma>\<^sub>2 x\<rbrakk> \<Longrightarrow> Fun x1 x2a \<cdot>\<^sub>t \<sigma>\<^sub>1 = Fun x1 x2a \<cdot>\<^sub>t \<sigma>\<^sub>2
 2. \<And>x. \<forall>x\<in>vars\<^sub>t (\<epsilon> x). \<sigma>\<^sub>1 x = \<sigma>\<^sub>2 x \<Longrightarrow> \<epsilon> x \<cdot>\<^sub>t \<sigma>\<^sub>1 = \<epsilon> x \<cdot>\<^sub>t \<sigma>\<^sub>2
[PROOF STEP]
have "\<forall>t\<in>set ts. t \<cdot>\<^sub>t \<sigma>\<^sub>1 = t \<cdot>\<^sub>t \<sigma>\<^sub>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>t\<in>set ts. t \<cdot>\<^sub>t \<sigma>\<^sub>1 = t \<cdot>\<^sub>t \<sigma>\<^sub>2
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>t. t \<in> set ts \<Longrightarrow> t \<cdot>\<^sub>t \<sigma>\<^sub>1 = t \<cdot>\<^sub>t \<sigma>\<^sub>2
[PROOF STEP]
fix t
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>t. t \<in> set ts \<Longrightarrow> t \<cdot>\<^sub>t \<sigma>\<^sub>1 = t \<cdot>\<^sub>t \<sigma>\<^sub>2
[PROOF STEP]
assume tints: "t \<in> set ts"
[PROOF STATE]
proof (state)
this:
t \<in> set ts

goal (1 subgoal):
 1. \<And>t. t \<in> set ts \<Longrightarrow> t \<cdot>\<^sub>t \<sigma>\<^sub>1 = t \<cdot>\<^sub>t \<sigma>\<^sub>2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
t \<in> set ts
[PROOF STEP]
have "\<forall>x \<in> vars\<^sub>t t. \<sigma>\<^sub>1 x = \<sigma>\<^sub>2 x"
[PROOF STATE]
proof (prove)
using this:
t \<in> set ts

goal (1 subgoal):
 1. \<forall>x\<in>vars\<^sub>t t. \<sigma>\<^sub>1 x = \<sigma>\<^sub>2 x
[PROOF STEP]
using f Fun(2)
[PROOF STATE]
proof (prove)
using this:
t \<in> set ts
\<forall>t. t \<in> set ts \<longrightarrow> vars\<^sub>t t \<subseteq> vars\<^sub>t\<^sub>s ts
\<forall>x\<in>vars\<^sub>t (Fun f ts). \<sigma>\<^sub>1 x = \<sigma>\<^sub>2 x

goal (1 subgoal):
 1. \<forall>x\<in>vars\<^sub>t t. \<sigma>\<^sub>1 x = \<sigma>\<^sub>2 x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>vars\<^sub>t t. \<sigma>\<^sub>1 x = \<sigma>\<^sub>2 x

goal (1 subgoal):
 1. \<And>t. t \<in> set ts \<Longrightarrow> t \<cdot>\<^sub>t \<sigma>\<^sub>1 = t \<cdot>\<^sub>t \<sigma>\<^sub>2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>x\<in>vars\<^sub>t t. \<sigma>\<^sub>1 x = \<sigma>\<^sub>2 x
[PROOF STEP]
show "t \<cdot>\<^sub>t \<sigma>\<^sub>1 = t \<cdot>\<^sub>t \<sigma>\<^sub>2"
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>vars\<^sub>t t. \<sigma>\<^sub>1 x = \<sigma>\<^sub>2 x

goal (1 subgoal):
 1. t \<cdot>\<^sub>t \<sigma>\<^sub>1 = t \<cdot>\<^sub>t \<sigma>\<^sub>2
[PROOF STEP]
using Fun tints
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>vars\<^sub>t t. \<sigma>\<^sub>1 x = \<sigma>\<^sub>2 x
\<lbrakk>?x2aa \<in> set ts; \<forall>x\<in>vars\<^sub>t ?x2aa. \<sigma>\<^sub>1 x = \<sigma>\<^sub>2 x\<rbrakk> \<Longrightarrow> ?x2aa \<cdot>\<^sub>t \<sigma>\<^sub>1 = ?x2aa \<cdot>\<^sub>t \<sigma>\<^sub>2
\<forall>x\<in>vars\<^sub>t (Fun f ts). \<sigma>\<^sub>1 x = \<sigma>\<^sub>2 x
t \<in> set ts

goal (1 subgoal):
 1. t \<cdot>\<^sub>t \<sigma>\<^sub>1 = t \<cdot>\<^sub>t \<sigma>\<^sub>2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
t \<cdot>\<^sub>t \<sigma>\<^sub>1 = t \<cdot>\<^sub>t \<sigma>\<^sub>2

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>t\<in>set ts. t \<cdot>\<^sub>t \<sigma>\<^sub>1 = t \<cdot>\<^sub>t \<sigma>\<^sub>2

goal (2 subgoals):
 1. \<And>x1 x2a. \<lbrakk>\<And>x2aa. \<lbrakk>x2aa \<in> set x2a; \<forall>x\<in>vars\<^sub>t x2aa. \<sigma>\<^sub>1 x = \<sigma>\<^sub>2 x\<rbrakk> \<Longrightarrow> x2aa \<cdot>\<^sub>t \<sigma>\<^sub>1 = x2aa \<cdot>\<^sub>t \<sigma>\<^sub>2; \<forall>x\<in>vars\<^sub>t (Fun x1 x2a). \<sigma>\<^sub>1 x = \<sigma>\<^sub>2 x\<rbrakk> \<Longrightarrow> Fun x1 x2a \<cdot>\<^sub>t \<sigma>\<^sub>1 = Fun x1 x2a \<cdot>\<^sub>t \<sigma>\<^sub>2
 2. \<And>x. \<forall>x\<in>vars\<^sub>t (\<epsilon> x). \<sigma>\<^sub>1 x = \<sigma>\<^sub>2 x \<Longrightarrow> \<epsilon> x \<cdot>\<^sub>t \<sigma>\<^sub>1 = \<epsilon> x \<cdot>\<^sub>t \<sigma>\<^sub>2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>t\<in>set ts. t \<cdot>\<^sub>t \<sigma>\<^sub>1 = t \<cdot>\<^sub>t \<sigma>\<^sub>2
[PROOF STEP]
have "ts \<cdot>\<^sub>t\<^sub>s \<sigma>\<^sub>1 = ts \<cdot>\<^sub>t\<^sub>s \<sigma>\<^sub>2"
[PROOF STATE]
proof (prove)
using this:
\<forall>t\<in>set ts. t \<cdot>\<^sub>t \<sigma>\<^sub>1 = t \<cdot>\<^sub>t \<sigma>\<^sub>2

goal (1 subgoal):
 1. ts \<cdot>\<^sub>t\<^sub>s \<sigma>\<^sub>1 = ts \<cdot>\<^sub>t\<^sub>s \<sigma>\<^sub>2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ts \<cdot>\<^sub>t\<^sub>s \<sigma>\<^sub>1 = ts \<cdot>\<^sub>t\<^sub>s \<sigma>\<^sub>2

goal (2 subgoals):
 1. \<And>x1 x2a. \<lbrakk>\<And>x2aa. \<lbrakk>x2aa \<in> set x2a; \<forall>x\<in>vars\<^sub>t x2aa. \<sigma>\<^sub>1 x = \<sigma>\<^sub>2 x\<rbrakk> \<Longrightarrow> x2aa \<cdot>\<^sub>t \<sigma>\<^sub>1 = x2aa \<cdot>\<^sub>t \<sigma>\<^sub>2; \<forall>x\<in>vars\<^sub>t (Fun x1 x2a). \<sigma>\<^sub>1 x = \<sigma>\<^sub>2 x\<rbrakk> \<Longrightarrow> Fun x1 x2a \<cdot>\<^sub>t \<sigma>\<^sub>1 = Fun x1 x2a \<cdot>\<^sub>t \<sigma>\<^sub>2
 2. \<And>x. \<forall>x\<in>vars\<^sub>t (\<epsilon> x). \<sigma>\<^sub>1 x = \<sigma>\<^sub>2 x \<Longrightarrow> \<epsilon> x \<cdot>\<^sub>t \<sigma>\<^sub>1 = \<epsilon> x \<cdot>\<^sub>t \<sigma>\<^sub>2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ts \<cdot>\<^sub>t\<^sub>s \<sigma>\<^sub>1 = ts \<cdot>\<^sub>t\<^sub>s \<sigma>\<^sub>2
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
ts \<cdot>\<^sub>t\<^sub>s \<sigma>\<^sub>1 = ts \<cdot>\<^sub>t\<^sub>s \<sigma>\<^sub>2

goal (1 subgoal):
 1. Fun f ts \<cdot>\<^sub>t \<sigma>\<^sub>1 = Fun f ts \<cdot>\<^sub>t \<sigma>\<^sub>2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Fun f ts \<cdot>\<^sub>t \<sigma>\<^sub>1 = Fun f ts \<cdot>\<^sub>t \<sigma>\<^sub>2

goal (1 subgoal):
 1. \<And>x. \<forall>x\<in>vars\<^sub>t (\<epsilon> x). \<sigma>\<^sub>1 x = \<sigma>\<^sub>2 x \<Longrightarrow> \<epsilon> x \<cdot>\<^sub>t \<sigma>\<^sub>1 = \<epsilon> x \<cdot>\<^sub>t \<sigma>\<^sub>2
[PROOF STEP]
qed auto


[STATEMENT]
lemma relevant_vars_subts: (* similar to above proof *)
  assumes asm: "\<forall>x \<in> vars\<^sub>t\<^sub>s ts. \<sigma>\<^sub>1 x = \<sigma>\<^sub>2 x"
  shows "ts \<cdot>\<^sub>t\<^sub>s \<sigma>\<^sub>1 = ts \<cdot>\<^sub>t\<^sub>s \<sigma>\<^sub>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ts \<cdot>\<^sub>t\<^sub>s \<sigma>\<^sub>1 = ts \<cdot>\<^sub>t\<^sub>s \<sigma>\<^sub>2
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ts \<cdot>\<^sub>t\<^sub>s \<sigma>\<^sub>1 = ts \<cdot>\<^sub>t\<^sub>s \<sigma>\<^sub>2
[PROOF STEP]
have f: "\<forall>t. t \<in> set ts \<longrightarrow> vars\<^sub>t t \<subseteq> vars\<^sub>t\<^sub>s ts"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>t. t \<in> set ts \<longrightarrow> vars\<^sub>t t \<subseteq> vars\<^sub>t\<^sub>s ts
[PROOF STEP]
by (induction ts) auto
[PROOF STATE]
proof (state)
this:
\<forall>t. t \<in> set ts \<longrightarrow> vars\<^sub>t t \<subseteq> vars\<^sub>t\<^sub>s ts

goal (1 subgoal):
 1. ts \<cdot>\<^sub>t\<^sub>s \<sigma>\<^sub>1 = ts \<cdot>\<^sub>t\<^sub>s \<sigma>\<^sub>2
[PROOF STEP]
have "\<forall>t\<in>set ts. t \<cdot>\<^sub>t \<sigma>\<^sub>1 = t \<cdot>\<^sub>t \<sigma>\<^sub>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>t\<in>set ts. t \<cdot>\<^sub>t \<sigma>\<^sub>1 = t \<cdot>\<^sub>t \<sigma>\<^sub>2
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>t. t \<in> set ts \<Longrightarrow> t \<cdot>\<^sub>t \<sigma>\<^sub>1 = t \<cdot>\<^sub>t \<sigma>\<^sub>2
[PROOF STEP]
fix t
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>t. t \<in> set ts \<Longrightarrow> t \<cdot>\<^sub>t \<sigma>\<^sub>1 = t \<cdot>\<^sub>t \<sigma>\<^sub>2
[PROOF STEP]
assume tints: "t \<in> set ts"
[PROOF STATE]
proof (state)
this:
t \<in> set ts

goal (1 subgoal):
 1. \<And>t. t \<in> set ts \<Longrightarrow> t \<cdot>\<^sub>t \<sigma>\<^sub>1 = t \<cdot>\<^sub>t \<sigma>\<^sub>2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
t \<in> set ts
[PROOF STEP]
have "\<forall>x \<in> vars\<^sub>t t. \<sigma>\<^sub>1 x = \<sigma>\<^sub>2 x"
[PROOF STATE]
proof (prove)
using this:
t \<in> set ts

goal (1 subgoal):
 1. \<forall>x\<in>vars\<^sub>t t. \<sigma>\<^sub>1 x = \<sigma>\<^sub>2 x
[PROOF STEP]
using f asm
[PROOF STATE]
proof (prove)
using this:
t \<in> set ts
\<forall>t. t \<in> set ts \<longrightarrow> vars\<^sub>t t \<subseteq> vars\<^sub>t\<^sub>s ts
\<forall>x\<in>vars\<^sub>t\<^sub>s ts. \<sigma>\<^sub>1 x = \<sigma>\<^sub>2 x

goal (1 subgoal):
 1. \<forall>x\<in>vars\<^sub>t t. \<sigma>\<^sub>1 x = \<sigma>\<^sub>2 x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>vars\<^sub>t t. \<sigma>\<^sub>1 x = \<sigma>\<^sub>2 x

goal (1 subgoal):
 1. \<And>t. t \<in> set ts \<Longrightarrow> t \<cdot>\<^sub>t \<sigma>\<^sub>1 = t \<cdot>\<^sub>t \<sigma>\<^sub>2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>x\<in>vars\<^sub>t t. \<sigma>\<^sub>1 x = \<sigma>\<^sub>2 x
[PROOF STEP]
show "t \<cdot>\<^sub>t \<sigma>\<^sub>1 = t \<cdot>\<^sub>t \<sigma>\<^sub>2"
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>vars\<^sub>t t. \<sigma>\<^sub>1 x = \<sigma>\<^sub>2 x

goal (1 subgoal):
 1. t \<cdot>\<^sub>t \<sigma>\<^sub>1 = t \<cdot>\<^sub>t \<sigma>\<^sub>2
[PROOF STEP]
using relevant_vars_subt tints
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>vars\<^sub>t t. \<sigma>\<^sub>1 x = \<sigma>\<^sub>2 x
\<forall>x\<in>vars\<^sub>t ?t. ?\<sigma>\<^sub>1 x = ?\<sigma>\<^sub>2 x \<Longrightarrow> ?t \<cdot>\<^sub>t ?\<sigma>\<^sub>1 = ?t \<cdot>\<^sub>t ?\<sigma>\<^sub>2
t \<in> set ts

goal (1 subgoal):
 1. t \<cdot>\<^sub>t \<sigma>\<^sub>1 = t \<cdot>\<^sub>t \<sigma>\<^sub>2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
t \<cdot>\<^sub>t \<sigma>\<^sub>1 = t \<cdot>\<^sub>t \<sigma>\<^sub>2

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>t\<in>set ts. t \<cdot>\<^sub>t \<sigma>\<^sub>1 = t \<cdot>\<^sub>t \<sigma>\<^sub>2

goal (1 subgoal):
 1. ts \<cdot>\<^sub>t\<^sub>s \<sigma>\<^sub>1 = ts \<cdot>\<^sub>t\<^sub>s \<sigma>\<^sub>2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>t\<in>set ts. t \<cdot>\<^sub>t \<sigma>\<^sub>1 = t \<cdot>\<^sub>t \<sigma>\<^sub>2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>t\<in>set ts. t \<cdot>\<^sub>t \<sigma>\<^sub>1 = t \<cdot>\<^sub>t \<sigma>\<^sub>2

goal (1 subgoal):
 1. ts \<cdot>\<^sub>t\<^sub>s \<sigma>\<^sub>1 = ts \<cdot>\<^sub>t\<^sub>s \<sigma>\<^sub>2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ts \<cdot>\<^sub>t\<^sub>s \<sigma>\<^sub>1 = ts \<cdot>\<^sub>t\<^sub>s \<sigma>\<^sub>2

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma relevant_vars_subls: (* in many ways a mirror of relevant_vars_subts  *)
  assumes asm: "\<forall>x \<in> vars\<^sub>l\<^sub>s L. \<sigma>\<^sub>1 x = \<sigma>\<^sub>2 x"
  shows "L \<cdot>\<^sub>l\<^sub>s \<sigma>\<^sub>1 = L \<cdot>\<^sub>l\<^sub>s \<sigma>\<^sub>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. L \<cdot>\<^sub>l\<^sub>s \<sigma>\<^sub>1 = L \<cdot>\<^sub>l\<^sub>s \<sigma>\<^sub>2
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. L \<cdot>\<^sub>l\<^sub>s \<sigma>\<^sub>1 = L \<cdot>\<^sub>l\<^sub>s \<sigma>\<^sub>2
[PROOF STEP]
have f: "\<forall>l. l \<in> L \<longrightarrow> vars\<^sub>l l \<subseteq> vars\<^sub>l\<^sub>s L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>l. l \<in> L \<longrightarrow> vars\<^sub>l l \<subseteq> vars\<^sub>l\<^sub>s L
[PROOF STEP]
unfolding vars\<^sub>l\<^sub>s_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>l. l \<in> L \<longrightarrow> vars\<^sub>l l \<subseteq> \<Union> (vars\<^sub>l ` L)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>l. l \<in> L \<longrightarrow> vars\<^sub>l l \<subseteq> vars\<^sub>l\<^sub>s L

goal (1 subgoal):
 1. L \<cdot>\<^sub>l\<^sub>s \<sigma>\<^sub>1 = L \<cdot>\<^sub>l\<^sub>s \<sigma>\<^sub>2
[PROOF STEP]
have "\<forall>l \<in> L. l \<cdot>\<^sub>l \<sigma>\<^sub>1 = l \<cdot>\<^sub>l \<sigma>\<^sub>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>l\<in>L. l \<cdot>\<^sub>l \<sigma>\<^sub>1 = l \<cdot>\<^sub>l \<sigma>\<^sub>2
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>l. l \<in> L \<Longrightarrow> l \<cdot>\<^sub>l \<sigma>\<^sub>1 = l \<cdot>\<^sub>l \<sigma>\<^sub>2
[PROOF STEP]
fix l
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>l. l \<in> L \<Longrightarrow> l \<cdot>\<^sub>l \<sigma>\<^sub>1 = l \<cdot>\<^sub>l \<sigma>\<^sub>2
[PROOF STEP]
assume linls: "l\<in>L"
[PROOF STATE]
proof (state)
this:
l \<in> L

goal (1 subgoal):
 1. \<And>l. l \<in> L \<Longrightarrow> l \<cdot>\<^sub>l \<sigma>\<^sub>1 = l \<cdot>\<^sub>l \<sigma>\<^sub>2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
l \<in> L
[PROOF STEP]
have "\<forall>x\<in>vars\<^sub>l l. \<sigma>\<^sub>1 x = \<sigma>\<^sub>2 x"
[PROOF STATE]
proof (prove)
using this:
l \<in> L

goal (1 subgoal):
 1. \<forall>x\<in>vars\<^sub>l l. \<sigma>\<^sub>1 x = \<sigma>\<^sub>2 x
[PROOF STEP]
using f asm
[PROOF STATE]
proof (prove)
using this:
l \<in> L
\<forall>l. l \<in> L \<longrightarrow> vars\<^sub>l l \<subseteq> vars\<^sub>l\<^sub>s L
\<forall>x\<in>vars\<^sub>l\<^sub>s L. \<sigma>\<^sub>1 x = \<sigma>\<^sub>2 x

goal (1 subgoal):
 1. \<forall>x\<in>vars\<^sub>l l. \<sigma>\<^sub>1 x = \<sigma>\<^sub>2 x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>vars\<^sub>l l. \<sigma>\<^sub>1 x = \<sigma>\<^sub>2 x

goal (1 subgoal):
 1. \<And>l. l \<in> L \<Longrightarrow> l \<cdot>\<^sub>l \<sigma>\<^sub>1 = l \<cdot>\<^sub>l \<sigma>\<^sub>2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>x\<in>vars\<^sub>l l. \<sigma>\<^sub>1 x = \<sigma>\<^sub>2 x
[PROOF STEP]
show "l \<cdot>\<^sub>l \<sigma>\<^sub>1 = l \<cdot>\<^sub>l \<sigma>\<^sub>2"
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>vars\<^sub>l l. \<sigma>\<^sub>1 x = \<sigma>\<^sub>2 x

goal (1 subgoal):
 1. l \<cdot>\<^sub>l \<sigma>\<^sub>1 = l \<cdot>\<^sub>l \<sigma>\<^sub>2
[PROOF STEP]
using relevant_vars_subl linls
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>vars\<^sub>l l. \<sigma>\<^sub>1 x = \<sigma>\<^sub>2 x
\<forall>x\<in>vars\<^sub>l ?l. ?\<sigma>\<^sub>1 x = ?\<sigma>\<^sub>2 x \<Longrightarrow> ?l \<cdot>\<^sub>l ?\<sigma>\<^sub>1 = ?l \<cdot>\<^sub>l ?\<sigma>\<^sub>2
l \<in> L

goal (1 subgoal):
 1. l \<cdot>\<^sub>l \<sigma>\<^sub>1 = l \<cdot>\<^sub>l \<sigma>\<^sub>2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
l \<cdot>\<^sub>l \<sigma>\<^sub>1 = l \<cdot>\<^sub>l \<sigma>\<^sub>2

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>l\<in>L. l \<cdot>\<^sub>l \<sigma>\<^sub>1 = l \<cdot>\<^sub>l \<sigma>\<^sub>2

goal (1 subgoal):
 1. L \<cdot>\<^sub>l\<^sub>s \<sigma>\<^sub>1 = L \<cdot>\<^sub>l\<^sub>s \<sigma>\<^sub>2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>l\<in>L. l \<cdot>\<^sub>l \<sigma>\<^sub>1 = l \<cdot>\<^sub>l \<sigma>\<^sub>2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>l\<in>L. l \<cdot>\<^sub>l \<sigma>\<^sub>1 = l \<cdot>\<^sub>l \<sigma>\<^sub>2

goal (1 subgoal):
 1. L \<cdot>\<^sub>l\<^sub>s \<sigma>\<^sub>1 = L \<cdot>\<^sub>l\<^sub>s \<sigma>\<^sub>2
[PROOF STEP]
by (meson image_cong)
[PROOF STATE]
proof (state)
this:
L \<cdot>\<^sub>l\<^sub>s \<sigma>\<^sub>1 = L \<cdot>\<^sub>l\<^sub>s \<sigma>\<^sub>2

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma merge_sub:
  assumes dist: "vars\<^sub>l\<^sub>s C \<inter> vars\<^sub>l\<^sub>s D = {}"
  assumes CC': "C \<cdot>\<^sub>l\<^sub>s lmbd = C'"
  assumes DD': "D \<cdot>\<^sub>l\<^sub>s \<mu> = D'"
  shows "\<exists>\<eta>. C \<cdot>\<^sub>l\<^sub>s \<eta> = C' \<and> D \<cdot>\<^sub>l\<^sub>s \<eta> = D'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>\<eta>. C \<cdot>\<^sub>l\<^sub>s \<eta> = C' \<and> D \<cdot>\<^sub>l\<^sub>s \<eta> = D'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>\<eta>. C \<cdot>\<^sub>l\<^sub>s \<eta> = C' \<and> D \<cdot>\<^sub>l\<^sub>s \<eta> = D'
[PROOF STEP]
let ?\<eta> = "\<lambda>x. if x \<in> vars\<^sub>l\<^sub>s C then lmbd x else \<mu> x"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>\<eta>. C \<cdot>\<^sub>l\<^sub>s \<eta> = C' \<and> D \<cdot>\<^sub>l\<^sub>s \<eta> = D'
[PROOF STEP]
have " \<forall>x\<in>vars\<^sub>l\<^sub>s C. ?\<eta> x = lmbd x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>vars\<^sub>l\<^sub>s C. (if x \<in> vars\<^sub>l\<^sub>s C then lmbd x else \<mu> x) = lmbd x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>vars\<^sub>l\<^sub>s C. (if x \<in> vars\<^sub>l\<^sub>s C then lmbd x else \<mu> x) = lmbd x

goal (1 subgoal):
 1. \<exists>\<eta>. C \<cdot>\<^sub>l\<^sub>s \<eta> = C' \<and> D \<cdot>\<^sub>l\<^sub>s \<eta> = D'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>x\<in>vars\<^sub>l\<^sub>s C. (if x \<in> vars\<^sub>l\<^sub>s C then lmbd x else \<mu> x) = lmbd x
[PROOF STEP]
have "C \<cdot>\<^sub>l\<^sub>s ?\<eta> = C \<cdot>\<^sub>l\<^sub>s lmbd"
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>vars\<^sub>l\<^sub>s C. (if x \<in> vars\<^sub>l\<^sub>s C then lmbd x else \<mu> x) = lmbd x

goal (1 subgoal):
 1. C \<cdot>\<^sub>l\<^sub>s (\<lambda>x. if x \<in> vars\<^sub>l\<^sub>s C then lmbd x else \<mu> x) = C \<cdot>\<^sub>l\<^sub>s lmbd
[PROOF STEP]
using relevant_vars_subls[of C ?\<eta> lmbd]
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>vars\<^sub>l\<^sub>s C. (if x \<in> vars\<^sub>l\<^sub>s C then lmbd x else \<mu> x) = lmbd x
\<forall>x\<in>vars\<^sub>l\<^sub>s C. (if x \<in> vars\<^sub>l\<^sub>s C then lmbd x else \<mu> x) = lmbd x \<Longrightarrow> C \<cdot>\<^sub>l\<^sub>s (\<lambda>x. if x \<in> vars\<^sub>l\<^sub>s C then lmbd x else \<mu> x) = C \<cdot>\<^sub>l\<^sub>s lmbd

goal (1 subgoal):
 1. C \<cdot>\<^sub>l\<^sub>s (\<lambda>x. if x \<in> vars\<^sub>l\<^sub>s C then lmbd x else \<mu> x) = C \<cdot>\<^sub>l\<^sub>s lmbd
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
C \<cdot>\<^sub>l\<^sub>s (\<lambda>x. if x \<in> vars\<^sub>l\<^sub>s C then lmbd x else \<mu> x) = C \<cdot>\<^sub>l\<^sub>s lmbd

goal (1 subgoal):
 1. \<exists>\<eta>. C \<cdot>\<^sub>l\<^sub>s \<eta> = C' \<and> D \<cdot>\<^sub>l\<^sub>s \<eta> = D'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
C \<cdot>\<^sub>l\<^sub>s (\<lambda>x. if x \<in> vars\<^sub>l\<^sub>s C then lmbd x else \<mu> x) = C \<cdot>\<^sub>l\<^sub>s lmbd
[PROOF STEP]
have "C \<cdot>\<^sub>l\<^sub>s ?\<eta> = C'"
[PROOF STATE]
proof (prove)
using this:
C \<cdot>\<^sub>l\<^sub>s (\<lambda>x. if x \<in> vars\<^sub>l\<^sub>s C then lmbd x else \<mu> x) = C \<cdot>\<^sub>l\<^sub>s lmbd

goal (1 subgoal):
 1. C \<cdot>\<^sub>l\<^sub>s (\<lambda>x. if x \<in> vars\<^sub>l\<^sub>s C then lmbd x else \<mu> x) = C'
[PROOF STEP]
using CC'
[PROOF STATE]
proof (prove)
using this:
C \<cdot>\<^sub>l\<^sub>s (\<lambda>x. if x \<in> vars\<^sub>l\<^sub>s C then lmbd x else \<mu> x) = C \<cdot>\<^sub>l\<^sub>s lmbd
C \<cdot>\<^sub>l\<^sub>s lmbd = C'

goal (1 subgoal):
 1. C \<cdot>\<^sub>l\<^sub>s (\<lambda>x. if x \<in> vars\<^sub>l\<^sub>s C then lmbd x else \<mu> x) = C'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
C \<cdot>\<^sub>l\<^sub>s (\<lambda>x. if x \<in> vars\<^sub>l\<^sub>s C then lmbd x else \<mu> x) = C'

goal (1 subgoal):
 1. \<exists>\<eta>. C \<cdot>\<^sub>l\<^sub>s \<eta> = C' \<and> D \<cdot>\<^sub>l\<^sub>s \<eta> = D'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
C \<cdot>\<^sub>l\<^sub>s (\<lambda>x. if x \<in> vars\<^sub>l\<^sub>s C then lmbd x else \<mu> x) = C'

goal (1 subgoal):
 1. \<exists>\<eta>. C \<cdot>\<^sub>l\<^sub>s \<eta> = C' \<and> D \<cdot>\<^sub>l\<^sub>s \<eta> = D'
[PROOF STEP]
have " \<forall>x \<in> vars\<^sub>l\<^sub>s D. ?\<eta> x = \<mu> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>vars\<^sub>l\<^sub>s D. (if x \<in> vars\<^sub>l\<^sub>s C then lmbd x else \<mu> x) = \<mu> x
[PROOF STEP]
using dist
[PROOF STATE]
proof (prove)
using this:
vars\<^sub>l\<^sub>s C \<inter> vars\<^sub>l\<^sub>s D = {}

goal (1 subgoal):
 1. \<forall>x\<in>vars\<^sub>l\<^sub>s D. (if x \<in> vars\<^sub>l\<^sub>s C then lmbd x else \<mu> x) = \<mu> x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>vars\<^sub>l\<^sub>s D. (if x \<in> vars\<^sub>l\<^sub>s C then lmbd x else \<mu> x) = \<mu> x

goal (1 subgoal):
 1. \<exists>\<eta>. C \<cdot>\<^sub>l\<^sub>s \<eta> = C' \<and> D \<cdot>\<^sub>l\<^sub>s \<eta> = D'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>x\<in>vars\<^sub>l\<^sub>s D. (if x \<in> vars\<^sub>l\<^sub>s C then lmbd x else \<mu> x) = \<mu> x
[PROOF STEP]
have "D \<cdot>\<^sub>l\<^sub>s ?\<eta> = D \<cdot>\<^sub>l\<^sub>s \<mu>"
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>vars\<^sub>l\<^sub>s D. (if x \<in> vars\<^sub>l\<^sub>s C then lmbd x else \<mu> x) = \<mu> x

goal (1 subgoal):
 1. D \<cdot>\<^sub>l\<^sub>s (\<lambda>x. if x \<in> vars\<^sub>l\<^sub>s C then lmbd x else \<mu> x) = D \<cdot>\<^sub>l\<^sub>s \<mu>
[PROOF STEP]
using relevant_vars_subls[of D ?\<eta> \<mu>]
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>vars\<^sub>l\<^sub>s D. (if x \<in> vars\<^sub>l\<^sub>s C then lmbd x else \<mu> x) = \<mu> x
\<forall>x\<in>vars\<^sub>l\<^sub>s D. (if x \<in> vars\<^sub>l\<^sub>s C then lmbd x else \<mu> x) = \<mu> x \<Longrightarrow> D \<cdot>\<^sub>l\<^sub>s (\<lambda>x. if x \<in> vars\<^sub>l\<^sub>s C then lmbd x else \<mu> x) = D \<cdot>\<^sub>l\<^sub>s \<mu>

goal (1 subgoal):
 1. D \<cdot>\<^sub>l\<^sub>s (\<lambda>x. if x \<in> vars\<^sub>l\<^sub>s C then lmbd x else \<mu> x) = D \<cdot>\<^sub>l\<^sub>s \<mu>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
D \<cdot>\<^sub>l\<^sub>s (\<lambda>x. if x \<in> vars\<^sub>l\<^sub>s C then lmbd x else \<mu> x) = D \<cdot>\<^sub>l\<^sub>s \<mu>

goal (1 subgoal):
 1. \<exists>\<eta>. C \<cdot>\<^sub>l\<^sub>s \<eta> = C' \<and> D \<cdot>\<^sub>l\<^sub>s \<eta> = D'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
D \<cdot>\<^sub>l\<^sub>s (\<lambda>x. if x \<in> vars\<^sub>l\<^sub>s C then lmbd x else \<mu> x) = D \<cdot>\<^sub>l\<^sub>s \<mu>
[PROOF STEP]
have "D \<cdot>\<^sub>l\<^sub>s ?\<eta> = D'"
[PROOF STATE]
proof (prove)
using this:
D \<cdot>\<^sub>l\<^sub>s (\<lambda>x. if x \<in> vars\<^sub>l\<^sub>s C then lmbd x else \<mu> x) = D \<cdot>\<^sub>l\<^sub>s \<mu>

goal (1 subgoal):
 1. D \<cdot>\<^sub>l\<^sub>s (\<lambda>x. if x \<in> vars\<^sub>l\<^sub>s C then lmbd x else \<mu> x) = D'
[PROOF STEP]
using DD'
[PROOF STATE]
proof (prove)
using this:
D \<cdot>\<^sub>l\<^sub>s (\<lambda>x. if x \<in> vars\<^sub>l\<^sub>s C then lmbd x else \<mu> x) = D \<cdot>\<^sub>l\<^sub>s \<mu>
D \<cdot>\<^sub>l\<^sub>s \<mu> = D'

goal (1 subgoal):
 1. D \<cdot>\<^sub>l\<^sub>s (\<lambda>x. if x \<in> vars\<^sub>l\<^sub>s C then lmbd x else \<mu> x) = D'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
D \<cdot>\<^sub>l\<^sub>s (\<lambda>x. if x \<in> vars\<^sub>l\<^sub>s C then lmbd x else \<mu> x) = D'

goal (1 subgoal):
 1. \<exists>\<eta>. C \<cdot>\<^sub>l\<^sub>s \<eta> = C' \<and> D \<cdot>\<^sub>l\<^sub>s \<eta> = D'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
C \<cdot>\<^sub>l\<^sub>s (\<lambda>x. if x \<in> vars\<^sub>l\<^sub>s C then lmbd x else \<mu> x) = C'
D \<cdot>\<^sub>l\<^sub>s (\<lambda>x. if x \<in> vars\<^sub>l\<^sub>s C then lmbd x else \<mu> x) = D'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
C \<cdot>\<^sub>l\<^sub>s (\<lambda>x. if x \<in> vars\<^sub>l\<^sub>s C then lmbd x else \<mu> x) = C'
D \<cdot>\<^sub>l\<^sub>s (\<lambda>x. if x \<in> vars\<^sub>l\<^sub>s C then lmbd x else \<mu> x) = D'

goal (1 subgoal):
 1. \<exists>\<eta>. C \<cdot>\<^sub>l\<^sub>s \<eta> = C' \<and> D \<cdot>\<^sub>l\<^sub>s \<eta> = D'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>\<eta>. C \<cdot>\<^sub>l\<^sub>s \<eta> = C' \<and> D \<cdot>\<^sub>l\<^sub>s \<eta> = D'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma std_apart_apart'':
  assumes "x \<in> vars\<^sub>t  (t \<cdot>\<^sub>t (\<lambda>x::char list. Var (y @ x)))"
  shows "\<exists>x'. x = y@x'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>x'. x = y @ x'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
x \<in> vars\<^sub>t (t \<cdot>\<^sub>t (\<lambda>x. \<epsilon> (y @ x)))

goal (1 subgoal):
 1. \<exists>x'. x = y @ x'
[PROOF STEP]
by (induction t) auto


[STATEMENT]
lemma std_apart_apart':
  assumes "x \<in> vars\<^sub>l (l \<cdot>\<^sub>l (\<lambda>x. Var  (y@x)))"
  shows "\<exists>x'. x = y@x'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>x'. x = y @ x'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
x \<in> vars\<^sub>l (l \<cdot>\<^sub>l (\<lambda>x. \<epsilon> (y @ x)))

goal (1 subgoal):
 1. \<exists>x'. x = y @ x'
[PROOF STEP]
unfolding vars\<^sub>l_def
[PROOF STATE]
proof (prove)
using this:
x \<in> vars\<^sub>t\<^sub>s (get_terms (l \<cdot>\<^sub>l (\<lambda>x. \<epsilon> (y @ x))))

goal (1 subgoal):
 1. \<exists>x'. x = y @ x'
[PROOF STEP]
using std_apart_apart''
[PROOF STATE]
proof (prove)
using this:
x \<in> vars\<^sub>t\<^sub>s (get_terms (l \<cdot>\<^sub>l (\<lambda>x. \<epsilon> (y @ x))))
?x \<in> vars\<^sub>t (?t \<cdot>\<^sub>t (\<lambda>x. \<epsilon> (?y @ x))) \<Longrightarrow> \<exists>x'. ?x = ?y @ x'

goal (1 subgoal):
 1. \<exists>x'. x = y @ x'
[PROOF STEP]
by (cases l) auto


[STATEMENT]
lemma std_apart_apart: "vars\<^sub>l\<^sub>s (std\<^sub>1 C\<^sub>1) \<inter> vars\<^sub>l\<^sub>s (std\<^sub>2 C\<^sub>2) = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vars\<^sub>l\<^sub>s (C\<^sub>1 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''1'' @ x))) \<inter> vars\<^sub>l\<^sub>s (C\<^sub>2 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''2'' @ x))) = {}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. vars\<^sub>l\<^sub>s (C\<^sub>1 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''1'' @ x))) \<inter> vars\<^sub>l\<^sub>s (C\<^sub>2 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''2'' @ x))) = {}
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. vars\<^sub>l\<^sub>s (C\<^sub>1 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''1'' @ x))) \<inter> vars\<^sub>l\<^sub>s (C\<^sub>2 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''2'' @ x))) = {}
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. vars\<^sub>l\<^sub>s (C\<^sub>1 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''1'' @ x))) \<inter> vars\<^sub>l\<^sub>s (C\<^sub>2 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''2'' @ x))) = {}
[PROOF STEP]
assume xin: "x \<in> vars\<^sub>l\<^sub>s (std\<^sub>1 C\<^sub>1) \<inter> vars\<^sub>l\<^sub>s (std\<^sub>2 C\<^sub>2)"
[PROOF STATE]
proof (state)
this:
x \<in> vars\<^sub>l\<^sub>s (C\<^sub>1 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''1'' @ x))) \<inter> vars\<^sub>l\<^sub>s (C\<^sub>2 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''2'' @ x)))

goal (1 subgoal):
 1. vars\<^sub>l\<^sub>s (C\<^sub>1 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''1'' @ x))) \<inter> vars\<^sub>l\<^sub>s (C\<^sub>2 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''2'' @ x))) = {}
[PROOF STEP]
from xin
[PROOF STATE]
proof (chain)
picking this:
x \<in> vars\<^sub>l\<^sub>s (C\<^sub>1 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''1'' @ x))) \<inter> vars\<^sub>l\<^sub>s (C\<^sub>2 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''2'' @ x)))
[PROOF STEP]
have "x \<in> vars\<^sub>l\<^sub>s (std\<^sub>1 C\<^sub>1)"
[PROOF STATE]
proof (prove)
using this:
x \<in> vars\<^sub>l\<^sub>s (C\<^sub>1 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''1'' @ x))) \<inter> vars\<^sub>l\<^sub>s (C\<^sub>2 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''2'' @ x)))

goal (1 subgoal):
 1. x \<in> vars\<^sub>l\<^sub>s (C\<^sub>1 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''1'' @ x)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> vars\<^sub>l\<^sub>s (C\<^sub>1 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''1'' @ x)))

goal (1 subgoal):
 1. vars\<^sub>l\<^sub>s (C\<^sub>1 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''1'' @ x))) \<inter> vars\<^sub>l\<^sub>s (C\<^sub>2 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''2'' @ x))) = {}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> vars\<^sub>l\<^sub>s (C\<^sub>1 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''1'' @ x)))
[PROOF STEP]
have "\<exists>x'. x=''1'' @ x'"
[PROOF STATE]
proof (prove)
using this:
x \<in> vars\<^sub>l\<^sub>s (C\<^sub>1 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''1'' @ x)))

goal (1 subgoal):
 1. \<exists>x'. x = ''1'' @ x'
[PROOF STEP]
using std_apart_apart'[of x _ "''1''"]
[PROOF STATE]
proof (prove)
using this:
x \<in> vars\<^sub>l\<^sub>s (C\<^sub>1 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''1'' @ x)))
x \<in> vars\<^sub>l (?l \<cdot>\<^sub>l (\<lambda>x. \<epsilon> (''1'' @ x))) \<Longrightarrow> \<exists>x'. x = ''1'' @ x'

goal (1 subgoal):
 1. \<exists>x'. x = ''1'' @ x'
[PROOF STEP]
unfolding vars\<^sub>l\<^sub>s_def
[PROOF STATE]
proof (prove)
using this:
x \<in> \<Union> (vars\<^sub>l ` (C\<^sub>1 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''1'' @ x))))
x \<in> vars\<^sub>l (?l \<cdot>\<^sub>l (\<lambda>x. \<epsilon> (''1'' @ x))) \<Longrightarrow> \<exists>x'. x = ''1'' @ x'

goal (1 subgoal):
 1. \<exists>x'. x = ''1'' @ x'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>x'. x = ''1'' @ x'

goal (1 subgoal):
 1. vars\<^sub>l\<^sub>s (C\<^sub>1 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''1'' @ x))) \<inter> vars\<^sub>l\<^sub>s (C\<^sub>2 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''2'' @ x))) = {}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<exists>x'. x = ''1'' @ x'

goal (1 subgoal):
 1. vars\<^sub>l\<^sub>s (C\<^sub>1 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''1'' @ x))) \<inter> vars\<^sub>l\<^sub>s (C\<^sub>2 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''2'' @ x))) = {}
[PROOF STEP]
from xin
[PROOF STATE]
proof (chain)
picking this:
x \<in> vars\<^sub>l\<^sub>s (C\<^sub>1 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''1'' @ x))) \<inter> vars\<^sub>l\<^sub>s (C\<^sub>2 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''2'' @ x)))
[PROOF STEP]
have "x \<in> vars\<^sub>l\<^sub>s (std\<^sub>2 C\<^sub>2)"
[PROOF STATE]
proof (prove)
using this:
x \<in> vars\<^sub>l\<^sub>s (C\<^sub>1 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''1'' @ x))) \<inter> vars\<^sub>l\<^sub>s (C\<^sub>2 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''2'' @ x)))

goal (1 subgoal):
 1. x \<in> vars\<^sub>l\<^sub>s (C\<^sub>2 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''2'' @ x)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> vars\<^sub>l\<^sub>s (C\<^sub>2 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''2'' @ x)))

goal (1 subgoal):
 1. vars\<^sub>l\<^sub>s (C\<^sub>1 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''1'' @ x))) \<inter> vars\<^sub>l\<^sub>s (C\<^sub>2 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''2'' @ x))) = {}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> vars\<^sub>l\<^sub>s (C\<^sub>2 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''2'' @ x)))
[PROOF STEP]
have "\<exists>x'. x= ''2'' @x' "
[PROOF STATE]
proof (prove)
using this:
x \<in> vars\<^sub>l\<^sub>s (C\<^sub>2 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''2'' @ x)))

goal (1 subgoal):
 1. \<exists>x'. x = ''2'' @ x'
[PROOF STEP]
using std_apart_apart'[of x _ "''2''"]
[PROOF STATE]
proof (prove)
using this:
x \<in> vars\<^sub>l\<^sub>s (C\<^sub>2 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''2'' @ x)))
x \<in> vars\<^sub>l (?l \<cdot>\<^sub>l (\<lambda>x. \<epsilon> (''2'' @ x))) \<Longrightarrow> \<exists>x'. x = ''2'' @ x'

goal (1 subgoal):
 1. \<exists>x'. x = ''2'' @ x'
[PROOF STEP]
unfolding vars\<^sub>l\<^sub>s_def
[PROOF STATE]
proof (prove)
using this:
x \<in> \<Union> (vars\<^sub>l ` (C\<^sub>2 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''2'' @ x))))
x \<in> vars\<^sub>l (?l \<cdot>\<^sub>l (\<lambda>x. \<epsilon> (''2'' @ x))) \<Longrightarrow> \<exists>x'. x = ''2'' @ x'

goal (1 subgoal):
 1. \<exists>x'. x = ''2'' @ x'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>x'. x = ''2'' @ x'

goal (1 subgoal):
 1. vars\<^sub>l\<^sub>s (C\<^sub>1 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''1'' @ x))) \<inter> vars\<^sub>l\<^sub>s (C\<^sub>2 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''2'' @ x))) = {}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<exists>x'. x = ''1'' @ x'
\<exists>x'. x = ''2'' @ x'
[PROOF STEP]
have "False"
[PROOF STATE]
proof (prove)
using this:
\<exists>x'. x = ''1'' @ x'
\<exists>x'. x = ''2'' @ x'

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

goal (1 subgoal):
 1. vars\<^sub>l\<^sub>s (C\<^sub>1 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''1'' @ x))) \<inter> vars\<^sub>l\<^sub>s (C\<^sub>2 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''2'' @ x))) = {}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
False
[PROOF STEP]
have "x \<in> {}"
[PROOF STATE]
proof (prove)
using this:
False

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

goal (1 subgoal):
 1. vars\<^sub>l\<^sub>s (C\<^sub>1 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''1'' @ x))) \<inter> vars\<^sub>l\<^sub>s (C\<^sub>2 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''2'' @ x))) = {}
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?x2 \<in> vars\<^sub>l\<^sub>s (C\<^sub>1 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''1'' @ x))) \<inter> vars\<^sub>l\<^sub>s (C\<^sub>2 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''2'' @ x))) \<Longrightarrow> ?x2 \<in> {}

goal (1 subgoal):
 1. vars\<^sub>l\<^sub>s (C\<^sub>1 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''1'' @ x))) \<inter> vars\<^sub>l\<^sub>s (C\<^sub>2 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''2'' @ x))) = {}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?x2 \<in> vars\<^sub>l\<^sub>s (C\<^sub>1 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''1'' @ x))) \<inter> vars\<^sub>l\<^sub>s (C\<^sub>2 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''2'' @ x))) \<Longrightarrow> ?x2 \<in> {}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
?x2 \<in> vars\<^sub>l\<^sub>s (C\<^sub>1 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''1'' @ x))) \<inter> vars\<^sub>l\<^sub>s (C\<^sub>2 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''2'' @ x))) \<Longrightarrow> ?x2 \<in> {}

goal (1 subgoal):
 1. vars\<^sub>l\<^sub>s (C\<^sub>1 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''1'' @ x))) \<inter> vars\<^sub>l\<^sub>s (C\<^sub>2 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''2'' @ x))) = {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vars\<^sub>l\<^sub>s (C\<^sub>1 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''1'' @ x))) \<inter> vars\<^sub>l\<^sub>s (C\<^sub>2 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''2'' @ x))) = {}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma std_apart_instance_of\<^sub>l\<^sub>s1: "instance_of\<^sub>l\<^sub>s C\<^sub>1 (std\<^sub>1 C\<^sub>1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. instance_of\<^sub>l\<^sub>s C\<^sub>1 (C\<^sub>1 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''1'' @ x)))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. instance_of\<^sub>l\<^sub>s C\<^sub>1 (C\<^sub>1 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''1'' @ x)))
[PROOF STEP]
have empty: "(\<lambda>x. Var (''1''@x)) \<cdot> (\<lambda>x. Var (tl x)) = \<epsilon>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. \<epsilon> (''1'' @ x)) \<cdot> (\<lambda>x. \<epsilon> (tl x)) = \<epsilon>
[PROOF STEP]
using composition_def
[PROOF STATE]
proof (prove)
using this:
(?\<sigma>\<^sub>1 \<cdot> ?\<sigma>\<^sub>2) ?x = ?\<sigma>\<^sub>1 ?x \<cdot>\<^sub>t ?\<sigma>\<^sub>2

goal (1 subgoal):
 1. (\<lambda>x. \<epsilon> (''1'' @ x)) \<cdot> (\<lambda>x. \<epsilon> (tl x)) = \<epsilon>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<lambda>x. \<epsilon> (''1'' @ x)) \<cdot> (\<lambda>x. \<epsilon> (tl x)) = \<epsilon>

goal (1 subgoal):
 1. instance_of\<^sub>l\<^sub>s C\<^sub>1 (C\<^sub>1 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''1'' @ x)))
[PROOF STEP]
have "C\<^sub>1 \<cdot>\<^sub>l\<^sub>s \<epsilon> = C\<^sub>1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C\<^sub>1 \<cdot>\<^sub>l\<^sub>s \<epsilon> = C\<^sub>1
[PROOF STEP]
using empty_subls
[PROOF STATE]
proof (prove)
using this:
?L \<cdot>\<^sub>l\<^sub>s \<epsilon> = ?L

goal (1 subgoal):
 1. C\<^sub>1 \<cdot>\<^sub>l\<^sub>s \<epsilon> = C\<^sub>1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
C\<^sub>1 \<cdot>\<^sub>l\<^sub>s \<epsilon> = C\<^sub>1

goal (1 subgoal):
 1. instance_of\<^sub>l\<^sub>s C\<^sub>1 (C\<^sub>1 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''1'' @ x)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
C\<^sub>1 \<cdot>\<^sub>l\<^sub>s \<epsilon> = C\<^sub>1
[PROOF STEP]
have "C\<^sub>1 \<cdot>\<^sub>l\<^sub>s ((\<lambda>x. Var (''1''@x)) \<cdot> (\<lambda>x. Var (tl x))) = C\<^sub>1"
[PROOF STATE]
proof (prove)
using this:
C\<^sub>1 \<cdot>\<^sub>l\<^sub>s \<epsilon> = C\<^sub>1

goal (1 subgoal):
 1. C\<^sub>1 \<cdot>\<^sub>l\<^sub>s ((\<lambda>x. \<epsilon> (''1'' @ x)) \<cdot> (\<lambda>x. \<epsilon> (tl x))) = C\<^sub>1
[PROOF STEP]
using empty
[PROOF STATE]
proof (prove)
using this:
C\<^sub>1 \<cdot>\<^sub>l\<^sub>s \<epsilon> = C\<^sub>1
(\<lambda>x. \<epsilon> (''1'' @ x)) \<cdot> (\<lambda>x. \<epsilon> (tl x)) = \<epsilon>

goal (1 subgoal):
 1. C\<^sub>1 \<cdot>\<^sub>l\<^sub>s ((\<lambda>x. \<epsilon> (''1'' @ x)) \<cdot> (\<lambda>x. \<epsilon> (tl x))) = C\<^sub>1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
C\<^sub>1 \<cdot>\<^sub>l\<^sub>s ((\<lambda>x. \<epsilon> (''1'' @ x)) \<cdot> (\<lambda>x. \<epsilon> (tl x))) = C\<^sub>1

goal (1 subgoal):
 1. instance_of\<^sub>l\<^sub>s C\<^sub>1 (C\<^sub>1 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''1'' @ x)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
C\<^sub>1 \<cdot>\<^sub>l\<^sub>s ((\<lambda>x. \<epsilon> (''1'' @ x)) \<cdot> (\<lambda>x. \<epsilon> (tl x))) = C\<^sub>1
[PROOF STEP]
have "(C\<^sub>1 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. Var (''1''@x))) \<cdot>\<^sub>l\<^sub>s (\<lambda>x. Var (tl x)) = C\<^sub>1"
[PROOF STATE]
proof (prove)
using this:
C\<^sub>1 \<cdot>\<^sub>l\<^sub>s ((\<lambda>x. \<epsilon> (''1'' @ x)) \<cdot> (\<lambda>x. \<epsilon> (tl x))) = C\<^sub>1

goal (1 subgoal):
 1. C\<^sub>1 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''1'' @ x)) \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (tl x)) = C\<^sub>1
[PROOF STEP]
using composition_conseq2ls
[PROOF STATE]
proof (prove)
using this:
C\<^sub>1 \<cdot>\<^sub>l\<^sub>s ((\<lambda>x. \<epsilon> (''1'' @ x)) \<cdot> (\<lambda>x. \<epsilon> (tl x))) = C\<^sub>1
?L \<cdot>\<^sub>l\<^sub>s ?\<sigma>\<^sub>1 \<cdot>\<^sub>l\<^sub>s ?\<sigma>\<^sub>2 = ?L \<cdot>\<^sub>l\<^sub>s (?\<sigma>\<^sub>1 \<cdot> ?\<sigma>\<^sub>2)

goal (1 subgoal):
 1. C\<^sub>1 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''1'' @ x)) \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (tl x)) = C\<^sub>1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
C\<^sub>1 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''1'' @ x)) \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (tl x)) = C\<^sub>1

goal (1 subgoal):
 1. instance_of\<^sub>l\<^sub>s C\<^sub>1 (C\<^sub>1 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''1'' @ x)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
C\<^sub>1 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''1'' @ x)) \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (tl x)) = C\<^sub>1
[PROOF STEP]
have "C\<^sub>1 = (std\<^sub>1 C\<^sub>1) \<cdot>\<^sub>l\<^sub>s (\<lambda>x. Var (tl x))"
[PROOF STATE]
proof (prove)
using this:
C\<^sub>1 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''1'' @ x)) \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (tl x)) = C\<^sub>1

goal (1 subgoal):
 1. C\<^sub>1 = C\<^sub>1 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''1'' @ x)) \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (tl x))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
C\<^sub>1 = C\<^sub>1 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''1'' @ x)) \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (tl x))

goal (1 subgoal):
 1. instance_of\<^sub>l\<^sub>s C\<^sub>1 (C\<^sub>1 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''1'' @ x)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
C\<^sub>1 = C\<^sub>1 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''1'' @ x)) \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (tl x))
[PROOF STEP]
show "instance_of\<^sub>l\<^sub>s C\<^sub>1 (std\<^sub>1 C\<^sub>1)"
[PROOF STATE]
proof (prove)
using this:
C\<^sub>1 = C\<^sub>1 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''1'' @ x)) \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (tl x))

goal (1 subgoal):
 1. instance_of\<^sub>l\<^sub>s C\<^sub>1 (C\<^sub>1 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''1'' @ x)))
[PROOF STEP]
unfolding instance_of\<^sub>l\<^sub>s_def
[PROOF STATE]
proof (prove)
using this:
C\<^sub>1 = C\<^sub>1 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''1'' @ x)) \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (tl x))

goal (1 subgoal):
 1. \<exists>\<sigma>. C\<^sub>1 = C\<^sub>1 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''1'' @ x)) \<cdot>\<^sub>l\<^sub>s \<sigma>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
instance_of\<^sub>l\<^sub>s C\<^sub>1 (C\<^sub>1 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''1'' @ x)))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma std_apart_instance_of\<^sub>l\<^sub>s2: "instance_of\<^sub>l\<^sub>s C2 (std\<^sub>2 C2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. instance_of\<^sub>l\<^sub>s C2 (C2 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''2'' @ x)))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. instance_of\<^sub>l\<^sub>s C2 (C2 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''2'' @ x)))
[PROOF STEP]
have empty: "(\<lambda>x. Var (''2''@x)) \<cdot> (\<lambda>x. Var (tl x)) = \<epsilon>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. \<epsilon> (''2'' @ x)) \<cdot> (\<lambda>x. \<epsilon> (tl x)) = \<epsilon>
[PROOF STEP]
using composition_def
[PROOF STATE]
proof (prove)
using this:
(?\<sigma>\<^sub>1 \<cdot> ?\<sigma>\<^sub>2) ?x = ?\<sigma>\<^sub>1 ?x \<cdot>\<^sub>t ?\<sigma>\<^sub>2

goal (1 subgoal):
 1. (\<lambda>x. \<epsilon> (''2'' @ x)) \<cdot> (\<lambda>x. \<epsilon> (tl x)) = \<epsilon>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<lambda>x. \<epsilon> (''2'' @ x)) \<cdot> (\<lambda>x. \<epsilon> (tl x)) = \<epsilon>

goal (1 subgoal):
 1. instance_of\<^sub>l\<^sub>s C2 (C2 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''2'' @ x)))
[PROOF STEP]
have "C2 \<cdot>\<^sub>l\<^sub>s \<epsilon> = C2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C2 \<cdot>\<^sub>l\<^sub>s \<epsilon> = C2
[PROOF STEP]
using empty_subls
[PROOF STATE]
proof (prove)
using this:
?L \<cdot>\<^sub>l\<^sub>s \<epsilon> = ?L

goal (1 subgoal):
 1. C2 \<cdot>\<^sub>l\<^sub>s \<epsilon> = C2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
C2 \<cdot>\<^sub>l\<^sub>s \<epsilon> = C2

goal (1 subgoal):
 1. instance_of\<^sub>l\<^sub>s C2 (C2 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''2'' @ x)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
C2 \<cdot>\<^sub>l\<^sub>s \<epsilon> = C2
[PROOF STEP]
have "C2 \<cdot>\<^sub>l\<^sub>s ((\<lambda>x. Var (''2''@x)) \<cdot> (\<lambda>x. Var (tl x))) = C2"
[PROOF STATE]
proof (prove)
using this:
C2 \<cdot>\<^sub>l\<^sub>s \<epsilon> = C2

goal (1 subgoal):
 1. C2 \<cdot>\<^sub>l\<^sub>s ((\<lambda>x. \<epsilon> (''2'' @ x)) \<cdot> (\<lambda>x. \<epsilon> (tl x))) = C2
[PROOF STEP]
using empty
[PROOF STATE]
proof (prove)
using this:
C2 \<cdot>\<^sub>l\<^sub>s \<epsilon> = C2
(\<lambda>x. \<epsilon> (''2'' @ x)) \<cdot> (\<lambda>x. \<epsilon> (tl x)) = \<epsilon>

goal (1 subgoal):
 1. C2 \<cdot>\<^sub>l\<^sub>s ((\<lambda>x. \<epsilon> (''2'' @ x)) \<cdot> (\<lambda>x. \<epsilon> (tl x))) = C2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
C2 \<cdot>\<^sub>l\<^sub>s ((\<lambda>x. \<epsilon> (''2'' @ x)) \<cdot> (\<lambda>x. \<epsilon> (tl x))) = C2

goal (1 subgoal):
 1. instance_of\<^sub>l\<^sub>s C2 (C2 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''2'' @ x)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
C2 \<cdot>\<^sub>l\<^sub>s ((\<lambda>x. \<epsilon> (''2'' @ x)) \<cdot> (\<lambda>x. \<epsilon> (tl x))) = C2
[PROOF STEP]
have "(C2 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. Var (''2''@x))) \<cdot>\<^sub>l\<^sub>s (\<lambda>x. Var (tl x)) = C2"
[PROOF STATE]
proof (prove)
using this:
C2 \<cdot>\<^sub>l\<^sub>s ((\<lambda>x. \<epsilon> (''2'' @ x)) \<cdot> (\<lambda>x. \<epsilon> (tl x))) = C2

goal (1 subgoal):
 1. C2 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''2'' @ x)) \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (tl x)) = C2
[PROOF STEP]
using composition_conseq2ls
[PROOF STATE]
proof (prove)
using this:
C2 \<cdot>\<^sub>l\<^sub>s ((\<lambda>x. \<epsilon> (''2'' @ x)) \<cdot> (\<lambda>x. \<epsilon> (tl x))) = C2
?L \<cdot>\<^sub>l\<^sub>s ?\<sigma>\<^sub>1 \<cdot>\<^sub>l\<^sub>s ?\<sigma>\<^sub>2 = ?L \<cdot>\<^sub>l\<^sub>s (?\<sigma>\<^sub>1 \<cdot> ?\<sigma>\<^sub>2)

goal (1 subgoal):
 1. C2 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''2'' @ x)) \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (tl x)) = C2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
C2 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''2'' @ x)) \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (tl x)) = C2

goal (1 subgoal):
 1. instance_of\<^sub>l\<^sub>s C2 (C2 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''2'' @ x)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
C2 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''2'' @ x)) \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (tl x)) = C2
[PROOF STEP]
have "C2 = (std\<^sub>2 C2) \<cdot>\<^sub>l\<^sub>s (\<lambda>x. Var (tl x))"
[PROOF STATE]
proof (prove)
using this:
C2 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''2'' @ x)) \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (tl x)) = C2

goal (1 subgoal):
 1. C2 = C2 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''2'' @ x)) \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (tl x))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
C2 = C2 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''2'' @ x)) \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (tl x))

goal (1 subgoal):
 1. instance_of\<^sub>l\<^sub>s C2 (C2 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''2'' @ x)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
C2 = C2 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''2'' @ x)) \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (tl x))
[PROOF STEP]
show "instance_of\<^sub>l\<^sub>s C2 (std\<^sub>2 C2)"
[PROOF STATE]
proof (prove)
using this:
C2 = C2 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''2'' @ x)) \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (tl x))

goal (1 subgoal):
 1. instance_of\<^sub>l\<^sub>s C2 (C2 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''2'' @ x)))
[PROOF STEP]
unfolding instance_of\<^sub>l\<^sub>s_def
[PROOF STATE]
proof (prove)
using this:
C2 = C2 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''2'' @ x)) \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (tl x))

goal (1 subgoal):
 1. \<exists>\<sigma>. C2 = C2 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''2'' @ x)) \<cdot>\<^sub>l\<^sub>s \<sigma>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
instance_of\<^sub>l\<^sub>s C2 (C2 \<cdot>\<^sub>l\<^sub>s (\<lambda>x. \<epsilon> (''2'' @ x)))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma unif_sub:
  assumes unif: "unifier\<^sub>l\<^sub>s \<sigma> L"
  assumes nonempty: "L \<noteq> {}"
  shows "\<exists>l. subls L \<sigma> = {subl l \<sigma>}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>l. L \<cdot>\<^sub>l\<^sub>s \<sigma> = {l \<cdot>\<^sub>l \<sigma>}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>l. L \<cdot>\<^sub>l\<^sub>s \<sigma> = {l \<cdot>\<^sub>l \<sigma>}
[PROOF STEP]
from nonempty
[PROOF STATE]
proof (chain)
picking this:
L \<noteq> {}
[PROOF STEP]
obtain l where "l \<in> L"
[PROOF STATE]
proof (prove)
using this:
L \<noteq> {}

goal (1 subgoal):
 1. (\<And>l. l \<in> L \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
l \<in> L

goal (1 subgoal):
 1. \<exists>l. L \<cdot>\<^sub>l\<^sub>s \<sigma> = {l \<cdot>\<^sub>l \<sigma>}
[PROOF STEP]
from unif this
[PROOF STATE]
proof (chain)
picking this:
unifier\<^sub>l\<^sub>s \<sigma> L
l \<in> L
[PROOF STEP]
have "L \<cdot>\<^sub>l\<^sub>s \<sigma> = {l \<cdot>\<^sub>l \<sigma>}"
[PROOF STATE]
proof (prove)
using this:
unifier\<^sub>l\<^sub>s \<sigma> L
l \<in> L

goal (1 subgoal):
 1. L \<cdot>\<^sub>l\<^sub>s \<sigma> = {l \<cdot>\<^sub>l \<sigma>}
[PROOF STEP]
unfolding unifier\<^sub>l\<^sub>s_def
[PROOF STATE]
proof (prove)
using this:
\<exists>l'. \<forall>l\<in>L. l \<cdot>\<^sub>l \<sigma> = l'
l \<in> L

goal (1 subgoal):
 1. L \<cdot>\<^sub>l\<^sub>s \<sigma> = {l \<cdot>\<^sub>l \<sigma>}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
L \<cdot>\<^sub>l\<^sub>s \<sigma> = {l \<cdot>\<^sub>l \<sigma>}

goal (1 subgoal):
 1. \<exists>l. L \<cdot>\<^sub>l\<^sub>s \<sigma> = {l \<cdot>\<^sub>l \<sigma>}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
L \<cdot>\<^sub>l\<^sub>s \<sigma> = {l \<cdot>\<^sub>l \<sigma>}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
L \<cdot>\<^sub>l\<^sub>s \<sigma> = {l \<cdot>\<^sub>l \<sigma>}

goal (1 subgoal):
 1. \<exists>l. L \<cdot>\<^sub>l\<^sub>s \<sigma> = {l \<cdot>\<^sub>l \<sigma>}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>l. L \<cdot>\<^sub>l\<^sub>s \<sigma> = {l \<cdot>\<^sub>l \<sigma>}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma unifiert_def2: (*  (\<lambda>t. sub t \<sigma>) ` ts could have some nice notation maybe *)
  assumes L_elem: "ts \<noteq> {}"
  shows "unifier\<^sub>t\<^sub>s \<sigma> ts \<longleftrightarrow> (\<exists>l. (\<lambda>t. sub t \<sigma>) ` ts ={l})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unifier\<^sub>t\<^sub>s \<sigma> ts = (\<exists>l. (\<lambda>t. t \<cdot>\<^sub>t \<sigma>) ` ts = {l})
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. unifier\<^sub>t\<^sub>s \<sigma> ts \<Longrightarrow> \<exists>l. (\<lambda>t. t \<cdot>\<^sub>t \<sigma>) ` ts = {l}
 2. \<exists>l. (\<lambda>t. t \<cdot>\<^sub>t \<sigma>) ` ts = {l} \<Longrightarrow> unifier\<^sub>t\<^sub>s \<sigma> ts
[PROOF STEP]
assume unif: "unifier\<^sub>t\<^sub>s \<sigma> ts"
[PROOF STATE]
proof (state)
this:
unifier\<^sub>t\<^sub>s \<sigma> ts

goal (2 subgoals):
 1. unifier\<^sub>t\<^sub>s \<sigma> ts \<Longrightarrow> \<exists>l. (\<lambda>t. t \<cdot>\<^sub>t \<sigma>) ` ts = {l}
 2. \<exists>l. (\<lambda>t. t \<cdot>\<^sub>t \<sigma>) ` ts = {l} \<Longrightarrow> unifier\<^sub>t\<^sub>s \<sigma> ts
[PROOF STEP]
from L_elem
[PROOF STATE]
proof (chain)
picking this:
ts \<noteq> {}
[PROOF STEP]
obtain t where "t \<in> ts"
[PROOF STATE]
proof (prove)
using this:
ts \<noteq> {}

goal (1 subgoal):
 1. (\<And>t. t \<in> ts \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
t \<in> ts

goal (2 subgoals):
 1. unifier\<^sub>t\<^sub>s \<sigma> ts \<Longrightarrow> \<exists>l. (\<lambda>t. t \<cdot>\<^sub>t \<sigma>) ` ts = {l}
 2. \<exists>l. (\<lambda>t. t \<cdot>\<^sub>t \<sigma>) ` ts = {l} \<Longrightarrow> unifier\<^sub>t\<^sub>s \<sigma> ts
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
t \<in> ts
[PROOF STEP]
have "(\<lambda>t. sub t \<sigma>) ` ts = {t \<cdot>\<^sub>t \<sigma>}"
[PROOF STATE]
proof (prove)
using this:
t \<in> ts

goal (1 subgoal):
 1. (\<lambda>t. t \<cdot>\<^sub>t \<sigma>) ` ts = {t \<cdot>\<^sub>t \<sigma>}
[PROOF STEP]
using unif
[PROOF STATE]
proof (prove)
using this:
t \<in> ts
unifier\<^sub>t\<^sub>s \<sigma> ts

goal (1 subgoal):
 1. (\<lambda>t. t \<cdot>\<^sub>t \<sigma>) ` ts = {t \<cdot>\<^sub>t \<sigma>}
[PROOF STEP]
unfolding unifier\<^sub>t\<^sub>s_def
[PROOF STATE]
proof (prove)
using this:
t \<in> ts
\<exists>t'. \<forall>t\<in>ts. t \<cdot>\<^sub>t \<sigma> = t'

goal (1 subgoal):
 1. (\<lambda>t. t \<cdot>\<^sub>t \<sigma>) ` ts = {t \<cdot>\<^sub>t \<sigma>}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<lambda>t. t \<cdot>\<^sub>t \<sigma>) ` ts = {t \<cdot>\<^sub>t \<sigma>}

goal (2 subgoals):
 1. unifier\<^sub>t\<^sub>s \<sigma> ts \<Longrightarrow> \<exists>l. (\<lambda>t. t \<cdot>\<^sub>t \<sigma>) ` ts = {l}
 2. \<exists>l. (\<lambda>t. t \<cdot>\<^sub>t \<sigma>) ` ts = {l} \<Longrightarrow> unifier\<^sub>t\<^sub>s \<sigma> ts
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>t. t \<cdot>\<^sub>t \<sigma>) ` ts = {t \<cdot>\<^sub>t \<sigma>}
[PROOF STEP]
show "\<exists>l. (\<lambda>t. sub t \<sigma>) ` ts = {l}"
[PROOF STATE]
proof (prove)
using this:
(\<lambda>t. t \<cdot>\<^sub>t \<sigma>) ` ts = {t \<cdot>\<^sub>t \<sigma>}

goal (1 subgoal):
 1. \<exists>l. (\<lambda>t. t \<cdot>\<^sub>t \<sigma>) ` ts = {l}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>l. (\<lambda>t. t \<cdot>\<^sub>t \<sigma>) ` ts = {l}

goal (1 subgoal):
 1. \<exists>l. (\<lambda>t. t \<cdot>\<^sub>t \<sigma>) ` ts = {l} \<Longrightarrow> unifier\<^sub>t\<^sub>s \<sigma> ts
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>l. (\<lambda>t. t \<cdot>\<^sub>t \<sigma>) ` ts = {l} \<Longrightarrow> unifier\<^sub>t\<^sub>s \<sigma> ts
[PROOF STEP]
assume "\<exists>l. (\<lambda>t. sub t \<sigma>) ` ts ={l}"
[PROOF STATE]
proof (state)
this:
\<exists>l. (\<lambda>t. t \<cdot>\<^sub>t \<sigma>) ` ts = {l}

goal (1 subgoal):
 1. \<exists>l. (\<lambda>t. t \<cdot>\<^sub>t \<sigma>) ` ts = {l} \<Longrightarrow> unifier\<^sub>t\<^sub>s \<sigma> ts
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>l. (\<lambda>t. t \<cdot>\<^sub>t \<sigma>) ` ts = {l}
[PROOF STEP]
obtain l where "(\<lambda>t. sub t \<sigma>) ` ts = {l}"
[PROOF STATE]
proof (prove)
using this:
\<exists>l. (\<lambda>t. t \<cdot>\<^sub>t \<sigma>) ` ts = {l}

goal (1 subgoal):
 1. (\<And>l. (\<lambda>t. t \<cdot>\<^sub>t \<sigma>) ` ts = {l} \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<lambda>t. t \<cdot>\<^sub>t \<sigma>) ` ts = {l}

goal (1 subgoal):
 1. \<exists>l. (\<lambda>t. t \<cdot>\<^sub>t \<sigma>) ` ts = {l} \<Longrightarrow> unifier\<^sub>t\<^sub>s \<sigma> ts
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>t. t \<cdot>\<^sub>t \<sigma>) ` ts = {l}
[PROOF STEP]
have "\<forall>l' \<in> ts. l' \<cdot>\<^sub>t \<sigma> = l"
[PROOF STATE]
proof (prove)
using this:
(\<lambda>t. t \<cdot>\<^sub>t \<sigma>) ` ts = {l}

goal (1 subgoal):
 1. \<forall>l'\<in>ts. l' \<cdot>\<^sub>t \<sigma> = l
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>l'\<in>ts. l' \<cdot>\<^sub>t \<sigma> = l

goal (1 subgoal):
 1. \<exists>l. (\<lambda>t. t \<cdot>\<^sub>t \<sigma>) ` ts = {l} \<Longrightarrow> unifier\<^sub>t\<^sub>s \<sigma> ts
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>l'\<in>ts. l' \<cdot>\<^sub>t \<sigma> = l
[PROOF STEP]
show "unifier\<^sub>t\<^sub>s \<sigma> ts"
[PROOF STATE]
proof (prove)
using this:
\<forall>l'\<in>ts. l' \<cdot>\<^sub>t \<sigma> = l

goal (1 subgoal):
 1. unifier\<^sub>t\<^sub>s \<sigma> ts
[PROOF STEP]
unfolding unifier\<^sub>t\<^sub>s_def
[PROOF STATE]
proof (prove)
using this:
\<forall>l'\<in>ts. l' \<cdot>\<^sub>t \<sigma> = l

goal (1 subgoal):
 1. \<exists>t'. \<forall>t\<in>ts. t \<cdot>\<^sub>t \<sigma> = t'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
unifier\<^sub>t\<^sub>s \<sigma> ts

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma unifier\<^sub>l\<^sub>s_def2:
  assumes L_elem: "L \<noteq> {}"
  shows "unifier\<^sub>l\<^sub>s \<sigma> L \<longleftrightarrow> (\<exists>l. L \<cdot>\<^sub>l\<^sub>s \<sigma> = {l})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unifier\<^sub>l\<^sub>s \<sigma> L = (\<exists>l. L \<cdot>\<^sub>l\<^sub>s \<sigma> = {l})
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. unifier\<^sub>l\<^sub>s \<sigma> L \<Longrightarrow> \<exists>l. L \<cdot>\<^sub>l\<^sub>s \<sigma> = {l}
 2. \<exists>l. L \<cdot>\<^sub>l\<^sub>s \<sigma> = {l} \<Longrightarrow> unifier\<^sub>l\<^sub>s \<sigma> L
[PROOF STEP]
assume unif: "unifier\<^sub>l\<^sub>s \<sigma> L"
[PROOF STATE]
proof (state)
this:
unifier\<^sub>l\<^sub>s \<sigma> L

goal (2 subgoals):
 1. unifier\<^sub>l\<^sub>s \<sigma> L \<Longrightarrow> \<exists>l. L \<cdot>\<^sub>l\<^sub>s \<sigma> = {l}
 2. \<exists>l. L \<cdot>\<^sub>l\<^sub>s \<sigma> = {l} \<Longrightarrow> unifier\<^sub>l\<^sub>s \<sigma> L
[PROOF STEP]
from L_elem
[PROOF STATE]
proof (chain)
picking this:
L \<noteq> {}
[PROOF STEP]
obtain l where "l \<in> L"
[PROOF STATE]
proof (prove)
using this:
L \<noteq> {}

goal (1 subgoal):
 1. (\<And>l. l \<in> L \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
l \<in> L

goal (2 subgoals):
 1. unifier\<^sub>l\<^sub>s \<sigma> L \<Longrightarrow> \<exists>l. L \<cdot>\<^sub>l\<^sub>s \<sigma> = {l}
 2. \<exists>l. L \<cdot>\<^sub>l\<^sub>s \<sigma> = {l} \<Longrightarrow> unifier\<^sub>l\<^sub>s \<sigma> L
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
l \<in> L
[PROOF STEP]
have "L \<cdot>\<^sub>l\<^sub>s \<sigma> = {l \<cdot>\<^sub>l \<sigma>}"
[PROOF STATE]
proof (prove)
using this:
l \<in> L

goal (1 subgoal):
 1. L \<cdot>\<^sub>l\<^sub>s \<sigma> = {l \<cdot>\<^sub>l \<sigma>}
[PROOF STEP]
using unif
[PROOF STATE]
proof (prove)
using this:
l \<in> L
unifier\<^sub>l\<^sub>s \<sigma> L

goal (1 subgoal):
 1. L \<cdot>\<^sub>l\<^sub>s \<sigma> = {l \<cdot>\<^sub>l \<sigma>}
[PROOF STEP]
unfolding unifier\<^sub>l\<^sub>s_def
[PROOF STATE]
proof (prove)
using this:
l \<in> L
\<exists>l'. \<forall>l\<in>L. l \<cdot>\<^sub>l \<sigma> = l'

goal (1 subgoal):
 1. L \<cdot>\<^sub>l\<^sub>s \<sigma> = {l \<cdot>\<^sub>l \<sigma>}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
L \<cdot>\<^sub>l\<^sub>s \<sigma> = {l \<cdot>\<^sub>l \<sigma>}

goal (2 subgoals):
 1. unifier\<^sub>l\<^sub>s \<sigma> L \<Longrightarrow> \<exists>l. L \<cdot>\<^sub>l\<^sub>s \<sigma> = {l}
 2. \<exists>l. L \<cdot>\<^sub>l\<^sub>s \<sigma> = {l} \<Longrightarrow> unifier\<^sub>l\<^sub>s \<sigma> L
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
L \<cdot>\<^sub>l\<^sub>s \<sigma> = {l \<cdot>\<^sub>l \<sigma>}
[PROOF STEP]
show "\<exists>l. L \<cdot>\<^sub>l\<^sub>s \<sigma> = {l}"
[PROOF STATE]
proof (prove)
using this:
L \<cdot>\<^sub>l\<^sub>s \<sigma> = {l \<cdot>\<^sub>l \<sigma>}

goal (1 subgoal):
 1. \<exists>l. L \<cdot>\<^sub>l\<^sub>s \<sigma> = {l}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>l. L \<cdot>\<^sub>l\<^sub>s \<sigma> = {l}

goal (1 subgoal):
 1. \<exists>l. L \<cdot>\<^sub>l\<^sub>s \<sigma> = {l} \<Longrightarrow> unifier\<^sub>l\<^sub>s \<sigma> L
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>l. L \<cdot>\<^sub>l\<^sub>s \<sigma> = {l} \<Longrightarrow> unifier\<^sub>l\<^sub>s \<sigma> L
[PROOF STEP]
assume "\<exists>l. L \<cdot>\<^sub>l\<^sub>s \<sigma> ={l}"
[PROOF STATE]
proof (state)
this:
\<exists>l. L \<cdot>\<^sub>l\<^sub>s \<sigma> = {l}

goal (1 subgoal):
 1. \<exists>l. L \<cdot>\<^sub>l\<^sub>s \<sigma> = {l} \<Longrightarrow> unifier\<^sub>l\<^sub>s \<sigma> L
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>l. L \<cdot>\<^sub>l\<^sub>s \<sigma> = {l}
[PROOF STEP]
obtain l where "L \<cdot>\<^sub>l\<^sub>s \<sigma> = {l}"
[PROOF STATE]
proof (prove)
using this:
\<exists>l. L \<cdot>\<^sub>l\<^sub>s \<sigma> = {l}

goal (1 subgoal):
 1. (\<And>l. L \<cdot>\<^sub>l\<^sub>s \<sigma> = {l} \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
L \<cdot>\<^sub>l\<^sub>s \<sigma> = {l}

goal (1 subgoal):
 1. \<exists>l. L \<cdot>\<^sub>l\<^sub>s \<sigma> = {l} \<Longrightarrow> unifier\<^sub>l\<^sub>s \<sigma> L
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
L \<cdot>\<^sub>l\<^sub>s \<sigma> = {l}
[PROOF STEP]
have "\<forall>l' \<in> L. l' \<cdot>\<^sub>l \<sigma> = l"
[PROOF STATE]
proof (prove)
using this:
L \<cdot>\<^sub>l\<^sub>s \<sigma> = {l}

goal (1 subgoal):
 1. \<forall>l'\<in>L. l' \<cdot>\<^sub>l \<sigma> = l
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>l'\<in>L. l' \<cdot>\<^sub>l \<sigma> = l

goal (1 subgoal):
 1. \<exists>l. L \<cdot>\<^sub>l\<^sub>s \<sigma> = {l} \<Longrightarrow> unifier\<^sub>l\<^sub>s \<sigma> L
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>l'\<in>L. l' \<cdot>\<^sub>l \<sigma> = l
[PROOF STEP]
show "unifier\<^sub>l\<^sub>s \<sigma> L"
[PROOF STATE]
proof (prove)
using this:
\<forall>l'\<in>L. l' \<cdot>\<^sub>l \<sigma> = l

goal (1 subgoal):
 1. unifier\<^sub>l\<^sub>s \<sigma> L
[PROOF STEP]
unfolding unifier\<^sub>l\<^sub>s_def
[PROOF STATE]
proof (prove)
using this:
\<forall>l'\<in>L. l' \<cdot>\<^sub>l \<sigma> = l

goal (1 subgoal):
 1. \<exists>l'. \<forall>l\<in>L. l \<cdot>\<^sub>l \<sigma> = l'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
unifier\<^sub>l\<^sub>s \<sigma> L

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ground\<^sub>l\<^sub>s_unif_singleton:
  assumes ground\<^sub>l\<^sub>s: "ground\<^sub>l\<^sub>s L"
  assumes unif: "unifier\<^sub>l\<^sub>s \<sigma>' L"
  assumes empt: "L \<noteq> {}"
  shows "\<exists>l. L = {l}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>l. L = {l}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>l. L = {l}
[PROOF STEP]
from unif empt
[PROOF STATE]
proof (chain)
picking this:
unifier\<^sub>l\<^sub>s \<sigma>' L
L \<noteq> {}
[PROOF STEP]
have "\<exists>l. L \<cdot>\<^sub>l\<^sub>s \<sigma>' = {l}"
[PROOF STATE]
proof (prove)
using this:
unifier\<^sub>l\<^sub>s \<sigma>' L
L \<noteq> {}

goal (1 subgoal):
 1. \<exists>l. L \<cdot>\<^sub>l\<^sub>s \<sigma>' = {l}
[PROOF STEP]
using unif_sub
[PROOF STATE]
proof (prove)
using this:
unifier\<^sub>l\<^sub>s \<sigma>' L
L \<noteq> {}
\<lbrakk>unifier\<^sub>l\<^sub>s ?\<sigma> ?L; ?L \<noteq> {}\<rbrakk> \<Longrightarrow> \<exists>l. ?L \<cdot>\<^sub>l\<^sub>s ?\<sigma> = {l \<cdot>\<^sub>l ?\<sigma>}

goal (1 subgoal):
 1. \<exists>l. L \<cdot>\<^sub>l\<^sub>s \<sigma>' = {l}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>l. L \<cdot>\<^sub>l\<^sub>s \<sigma>' = {l}

goal (1 subgoal):
 1. \<exists>l. L = {l}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>l. L \<cdot>\<^sub>l\<^sub>s \<sigma>' = {l}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<exists>l. L \<cdot>\<^sub>l\<^sub>s \<sigma>' = {l}

goal (1 subgoal):
 1. \<exists>l. L = {l}
[PROOF STEP]
using ground\<^sub>l\<^sub>s_subls ground\<^sub>l\<^sub>s
[PROOF STATE]
proof (prove)
using this:
\<exists>l. L \<cdot>\<^sub>l\<^sub>s \<sigma>' = {l}
ground\<^sub>l\<^sub>s ?L \<Longrightarrow> ?L \<cdot>\<^sub>l\<^sub>s ?\<sigma> = ?L
ground\<^sub>l\<^sub>s L

goal (1 subgoal):
 1. \<exists>l. L = {l}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>l. L = {l}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma unifier_comp[simp]: "unifier\<^sub>l\<^sub>s \<sigma> (L\<^sup>C) \<longleftrightarrow> unifier\<^sub>l\<^sub>s \<sigma> L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unifier\<^sub>l\<^sub>s \<sigma> (L\<^sup>C) = unifier\<^sub>l\<^sub>s \<sigma> L
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. unifier\<^sub>l\<^sub>s \<sigma> (L\<^sup>C) \<Longrightarrow> unifier\<^sub>l\<^sub>s \<sigma> L
 2. unifier\<^sub>l\<^sub>s \<sigma> L \<Longrightarrow> unifier\<^sub>l\<^sub>s \<sigma> (L\<^sup>C)
[PROOF STEP]
assume "unifier\<^sub>l\<^sub>s \<sigma> (L\<^sup>C)"
[PROOF STATE]
proof (state)
this:
unifier\<^sub>l\<^sub>s \<sigma> (L\<^sup>C)

goal (2 subgoals):
 1. unifier\<^sub>l\<^sub>s \<sigma> (L\<^sup>C) \<Longrightarrow> unifier\<^sub>l\<^sub>s \<sigma> L
 2. unifier\<^sub>l\<^sub>s \<sigma> L \<Longrightarrow> unifier\<^sub>l\<^sub>s \<sigma> (L\<^sup>C)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
unifier\<^sub>l\<^sub>s \<sigma> (L\<^sup>C)
[PROOF STEP]
obtain l'' where l''_p: "\<forall>l \<in> L\<^sup>C. l \<cdot>\<^sub>l \<sigma> = l''"
[PROOF STATE]
proof (prove)
using this:
unifier\<^sub>l\<^sub>s \<sigma> (L\<^sup>C)

goal (1 subgoal):
 1. (\<And>l''. \<forall>l\<in>L\<^sup>C. l \<cdot>\<^sub>l \<sigma> = l'' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding unifier\<^sub>l\<^sub>s_def
[PROOF STATE]
proof (prove)
using this:
\<exists>l'. \<forall>l\<in>L\<^sup>C. l \<cdot>\<^sub>l \<sigma> = l'

goal (1 subgoal):
 1. (\<And>l''. \<forall>l\<in>L\<^sup>C. l \<cdot>\<^sub>l \<sigma> = l'' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>l\<in>L\<^sup>C. l \<cdot>\<^sub>l \<sigma> = l''

goal (2 subgoals):
 1. unifier\<^sub>l\<^sub>s \<sigma> (L\<^sup>C) \<Longrightarrow> unifier\<^sub>l\<^sub>s \<sigma> L
 2. unifier\<^sub>l\<^sub>s \<sigma> L \<Longrightarrow> unifier\<^sub>l\<^sub>s \<sigma> (L\<^sup>C)
[PROOF STEP]
obtain l' where "(l')\<^sup>c = l''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>l'. l'\<^sup>c = l'' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using comp_exi2[of l'']
[PROOF STATE]
proof (prove)
using this:
\<exists>l. l'' = l\<^sup>c

goal (1 subgoal):
 1. (\<And>l'. l'\<^sup>c = l'' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
l'\<^sup>c = l''

goal (2 subgoals):
 1. unifier\<^sub>l\<^sub>s \<sigma> (L\<^sup>C) \<Longrightarrow> unifier\<^sub>l\<^sub>s \<sigma> L
 2. unifier\<^sub>l\<^sub>s \<sigma> L \<Longrightarrow> unifier\<^sub>l\<^sub>s \<sigma> (L\<^sup>C)
[PROOF STEP]
from this l''_p
[PROOF STATE]
proof (chain)
picking this:
l'\<^sup>c = l''
\<forall>l\<in>L\<^sup>C. l \<cdot>\<^sub>l \<sigma> = l''
[PROOF STEP]
have l'_p:"\<forall>l \<in> L\<^sup>C. l \<cdot>\<^sub>l \<sigma> = (l')\<^sup>c"
[PROOF STATE]
proof (prove)
using this:
l'\<^sup>c = l''
\<forall>l\<in>L\<^sup>C. l \<cdot>\<^sub>l \<sigma> = l''

goal (1 subgoal):
 1. \<forall>l\<in>L\<^sup>C. l \<cdot>\<^sub>l \<sigma> = l'\<^sup>c
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>l\<in>L\<^sup>C. l \<cdot>\<^sub>l \<sigma> = l'\<^sup>c

goal (2 subgoals):
 1. unifier\<^sub>l\<^sub>s \<sigma> (L\<^sup>C) \<Longrightarrow> unifier\<^sub>l\<^sub>s \<sigma> L
 2. unifier\<^sub>l\<^sub>s \<sigma> L \<Longrightarrow> unifier\<^sub>l\<^sub>s \<sigma> (L\<^sup>C)
[PROOF STEP]
have "\<forall>l \<in> L. l \<cdot>\<^sub>l \<sigma> = l'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>l\<in>L. l \<cdot>\<^sub>l \<sigma> = l'
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>l. l \<in> L \<Longrightarrow> l \<cdot>\<^sub>l \<sigma> = l'
[PROOF STEP]
fix l
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>l. l \<in> L \<Longrightarrow> l \<cdot>\<^sub>l \<sigma> = l'
[PROOF STEP]
assume "l\<in>L"
[PROOF STATE]
proof (state)
this:
l \<in> L

goal (1 subgoal):
 1. \<And>l. l \<in> L \<Longrightarrow> l \<cdot>\<^sub>l \<sigma> = l'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
l \<in> L
[PROOF STEP]
have "l\<^sup>c \<in> L\<^sup>C"
[PROOF STATE]
proof (prove)
using this:
l \<in> L

goal (1 subgoal):
 1. l\<^sup>c \<in> L\<^sup>C
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
l\<^sup>c \<in> L\<^sup>C

goal (1 subgoal):
 1. \<And>l. l \<in> L \<Longrightarrow> l \<cdot>\<^sub>l \<sigma> = l'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
l\<^sup>c \<in> L\<^sup>C
[PROOF STEP]
have "(l\<^sup>c) \<cdot>\<^sub>l \<sigma> = (l')\<^sup>c"
[PROOF STATE]
proof (prove)
using this:
l\<^sup>c \<in> L\<^sup>C

goal (1 subgoal):
 1. l\<^sup>c \<cdot>\<^sub>l \<sigma> = l'\<^sup>c
[PROOF STEP]
using l'_p
[PROOF STATE]
proof (prove)
using this:
l\<^sup>c \<in> L\<^sup>C
\<forall>l\<in>L\<^sup>C. l \<cdot>\<^sub>l \<sigma> = l'\<^sup>c

goal (1 subgoal):
 1. l\<^sup>c \<cdot>\<^sub>l \<sigma> = l'\<^sup>c
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
l\<^sup>c \<cdot>\<^sub>l \<sigma> = l'\<^sup>c

goal (1 subgoal):
 1. \<And>l. l \<in> L \<Longrightarrow> l \<cdot>\<^sub>l \<sigma> = l'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
l\<^sup>c \<cdot>\<^sub>l \<sigma> = l'\<^sup>c
[PROOF STEP]
have "(l \<cdot>\<^sub>l \<sigma>)\<^sup>c = (l')\<^sup>c"
[PROOF STATE]
proof (prove)
using this:
l\<^sup>c \<cdot>\<^sub>l \<sigma> = l'\<^sup>c

goal (1 subgoal):
 1. (l \<cdot>\<^sub>l \<sigma>)\<^sup>c = l'\<^sup>c
[PROOF STEP]
by (cases l) auto
[PROOF STATE]
proof (state)
this:
(l \<cdot>\<^sub>l \<sigma>)\<^sup>c = l'\<^sup>c

goal (1 subgoal):
 1. \<And>l. l \<in> L \<Longrightarrow> l \<cdot>\<^sub>l \<sigma> = l'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(l \<cdot>\<^sub>l \<sigma>)\<^sup>c = l'\<^sup>c
[PROOF STEP]
show "l \<cdot>\<^sub>l \<sigma> = l'"
[PROOF STATE]
proof (prove)
using this:
(l \<cdot>\<^sub>l \<sigma>)\<^sup>c = l'\<^sup>c

goal (1 subgoal):
 1. l \<cdot>\<^sub>l \<sigma> = l'
[PROOF STEP]
using cancel_comp2
[PROOF STATE]
proof (prove)
using this:
(l \<cdot>\<^sub>l \<sigma>)\<^sup>c = l'\<^sup>c
?l\<^sub>1\<^sup>c = ?l\<^sub>2\<^sup>c \<Longrightarrow> ?l\<^sub>1 = ?l\<^sub>2

goal (1 subgoal):
 1. l \<cdot>\<^sub>l \<sigma> = l'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
l \<cdot>\<^sub>l \<sigma> = l'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>l\<in>L. l \<cdot>\<^sub>l \<sigma> = l'

goal (2 subgoals):
 1. unifier\<^sub>l\<^sub>s \<sigma> (L\<^sup>C) \<Longrightarrow> unifier\<^sub>l\<^sub>s \<sigma> L
 2. unifier\<^sub>l\<^sub>s \<sigma> L \<Longrightarrow> unifier\<^sub>l\<^sub>s \<sigma> (L\<^sup>C)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>l\<in>L. l \<cdot>\<^sub>l \<sigma> = l'
[PROOF STEP]
show "unifier\<^sub>l\<^sub>s \<sigma> L"
[PROOF STATE]
proof (prove)
using this:
\<forall>l\<in>L. l \<cdot>\<^sub>l \<sigma> = l'

goal (1 subgoal):
 1. unifier\<^sub>l\<^sub>s \<sigma> L
[PROOF STEP]
unfolding unifier\<^sub>l\<^sub>s_def
[PROOF STATE]
proof (prove)
using this:
\<forall>l\<in>L. l \<cdot>\<^sub>l \<sigma> = l'

goal (1 subgoal):
 1. \<exists>l'. \<forall>l\<in>L. l \<cdot>\<^sub>l \<sigma> = l'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
unifier\<^sub>l\<^sub>s \<sigma> L

goal (1 subgoal):
 1. unifier\<^sub>l\<^sub>s \<sigma> L \<Longrightarrow> unifier\<^sub>l\<^sub>s \<sigma> (L\<^sup>C)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. unifier\<^sub>l\<^sub>s \<sigma> L \<Longrightarrow> unifier\<^sub>l\<^sub>s \<sigma> (L\<^sup>C)
[PROOF STEP]
assume "unifier\<^sub>l\<^sub>s \<sigma> L"
[PROOF STATE]
proof (state)
this:
unifier\<^sub>l\<^sub>s \<sigma> L

goal (1 subgoal):
 1. unifier\<^sub>l\<^sub>s \<sigma> L \<Longrightarrow> unifier\<^sub>l\<^sub>s \<sigma> (L\<^sup>C)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
unifier\<^sub>l\<^sub>s \<sigma> L
[PROOF STEP]
obtain l' where l'_p: "\<forall>l \<in> L. l \<cdot>\<^sub>l \<sigma> = l'"
[PROOF STATE]
proof (prove)
using this:
unifier\<^sub>l\<^sub>s \<sigma> L

goal (1 subgoal):
 1. (\<And>l'. \<forall>l\<in>L. l \<cdot>\<^sub>l \<sigma> = l' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding unifier\<^sub>l\<^sub>s_def
[PROOF STATE]
proof (prove)
using this:
\<exists>l'. \<forall>l\<in>L. l \<cdot>\<^sub>l \<sigma> = l'

goal (1 subgoal):
 1. (\<And>l'. \<forall>l\<in>L. l \<cdot>\<^sub>l \<sigma> = l' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>l\<in>L. l \<cdot>\<^sub>l \<sigma> = l'

goal (1 subgoal):
 1. unifier\<^sub>l\<^sub>s \<sigma> L \<Longrightarrow> unifier\<^sub>l\<^sub>s \<sigma> (L\<^sup>C)
[PROOF STEP]
have "\<forall>l \<in> L\<^sup>C. l \<cdot>\<^sub>l \<sigma> = (l')\<^sup>c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>l\<in>L\<^sup>C. l \<cdot>\<^sub>l \<sigma> = l'\<^sup>c
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>l. l \<in> L\<^sup>C \<Longrightarrow> l \<cdot>\<^sub>l \<sigma> = l'\<^sup>c
[PROOF STEP]
fix l
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>l. l \<in> L\<^sup>C \<Longrightarrow> l \<cdot>\<^sub>l \<sigma> = l'\<^sup>c
[PROOF STEP]
assume "l \<in> L\<^sup>C"
[PROOF STATE]
proof (state)
this:
l \<in> L\<^sup>C

goal (1 subgoal):
 1. \<And>l. l \<in> L\<^sup>C \<Longrightarrow> l \<cdot>\<^sub>l \<sigma> = l'\<^sup>c
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
l \<in> L\<^sup>C
[PROOF STEP]
have "l\<^sup>c \<in> L"
[PROOF STATE]
proof (prove)
using this:
l \<in> L\<^sup>C

goal (1 subgoal):
 1. l\<^sup>c \<in> L
[PROOF STEP]
using cancel_comp1
[PROOF STATE]
proof (prove)
using this:
l \<in> L\<^sup>C
?l\<^sup>c\<^sup>c = ?l

goal (1 subgoal):
 1. l\<^sup>c \<in> L
[PROOF STEP]
by (metis image_iff)
[PROOF STATE]
proof (state)
this:
l\<^sup>c \<in> L

goal (1 subgoal):
 1. \<And>l. l \<in> L\<^sup>C \<Longrightarrow> l \<cdot>\<^sub>l \<sigma> = l'\<^sup>c
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
l\<^sup>c \<in> L
[PROOF STEP]
show "l \<cdot>\<^sub>l \<sigma> = (l')\<^sup>c"
[PROOF STATE]
proof (prove)
using this:
l\<^sup>c \<in> L

goal (1 subgoal):
 1. l \<cdot>\<^sub>l \<sigma> = l'\<^sup>c
[PROOF STEP]
using l'_p comp_sub cancel_comp1
[PROOF STATE]
proof (prove)
using this:
l\<^sup>c \<in> L
\<forall>l\<in>L. l \<cdot>\<^sub>l \<sigma> = l'
?l\<^sup>c \<cdot>\<^sub>l ?\<sigma> = (?l \<cdot>\<^sub>l ?\<sigma>)\<^sup>c
?l\<^sup>c\<^sup>c = ?l

goal (1 subgoal):
 1. l \<cdot>\<^sub>l \<sigma> = l'\<^sup>c
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
l \<cdot>\<^sub>l \<sigma> = l'\<^sup>c

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>l\<in>L\<^sup>C. l \<cdot>\<^sub>l \<sigma> = l'\<^sup>c

goal (1 subgoal):
 1. unifier\<^sub>l\<^sub>s \<sigma> L \<Longrightarrow> unifier\<^sub>l\<^sub>s \<sigma> (L\<^sup>C)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>l\<in>L\<^sup>C. l \<cdot>\<^sub>l \<sigma> = l'\<^sup>c
[PROOF STEP]
show "unifier\<^sub>l\<^sub>s \<sigma> (L\<^sup>C)"
[PROOF STATE]
proof (prove)
using this:
\<forall>l\<in>L\<^sup>C. l \<cdot>\<^sub>l \<sigma> = l'\<^sup>c

goal (1 subgoal):
 1. unifier\<^sub>l\<^sub>s \<sigma> (L\<^sup>C)
[PROOF STEP]
unfolding unifier\<^sub>l\<^sub>s_def
[PROOF STATE]
proof (prove)
using this:
\<forall>l\<in>L\<^sup>C. l \<cdot>\<^sub>l \<sigma> = l'\<^sup>c

goal (1 subgoal):
 1. \<exists>l'. \<forall>l\<in>L\<^sup>C. l \<cdot>\<^sub>l \<sigma> = l'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
unifier\<^sub>l\<^sub>s \<sigma> (L\<^sup>C)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma unifier_sub1:
  assumes "unifier\<^sub>l\<^sub>s \<sigma> L"
  assumes "L' \<subseteq> L"
  shows "unifier\<^sub>l\<^sub>s \<sigma> L' "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unifier\<^sub>l\<^sub>s \<sigma> L'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
unifier\<^sub>l\<^sub>s \<sigma> L
L' \<subseteq> L

goal (1 subgoal):
 1. unifier\<^sub>l\<^sub>s \<sigma> L'
[PROOF STEP]
unfolding unifier\<^sub>l\<^sub>s_def
[PROOF STATE]
proof (prove)
using this:
\<exists>l'. \<forall>l\<in>L. l \<cdot>\<^sub>l \<sigma> = l'
L' \<subseteq> L

goal (1 subgoal):
 1. \<exists>l'. \<forall>l\<in>L'. l \<cdot>\<^sub>l \<sigma> = l'
[PROOF STEP]
by auto


[STATEMENT]
lemma unifier_sub2:
  assumes asm: "unifier\<^sub>l\<^sub>s \<sigma> (L\<^sub>1 \<union> L\<^sub>2)"
  shows "unifier\<^sub>l\<^sub>s \<sigma> L\<^sub>1 \<and> unifier\<^sub>l\<^sub>s \<sigma> L\<^sub>2 "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unifier\<^sub>l\<^sub>s \<sigma> L\<^sub>1 \<and> unifier\<^sub>l\<^sub>s \<sigma> L\<^sub>2
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. unifier\<^sub>l\<^sub>s \<sigma> L\<^sub>1 \<and> unifier\<^sub>l\<^sub>s \<sigma> L\<^sub>2
[PROOF STEP]
have "L\<^sub>1 \<subseteq> (L\<^sub>1 \<union> L\<^sub>2) \<and> L\<^sub>2 \<subseteq> (L\<^sub>1 \<union> L\<^sub>2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. L\<^sub>1 \<subseteq> L\<^sub>1 \<union> L\<^sub>2 \<and> L\<^sub>2 \<subseteq> L\<^sub>1 \<union> L\<^sub>2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
L\<^sub>1 \<subseteq> L\<^sub>1 \<union> L\<^sub>2 \<and> L\<^sub>2 \<subseteq> L\<^sub>1 \<union> L\<^sub>2

goal (1 subgoal):
 1. unifier\<^sub>l\<^sub>s \<sigma> L\<^sub>1 \<and> unifier\<^sub>l\<^sub>s \<sigma> L\<^sub>2
[PROOF STEP]
from this asm
[PROOF STATE]
proof (chain)
picking this:
L\<^sub>1 \<subseteq> L\<^sub>1 \<union> L\<^sub>2 \<and> L\<^sub>2 \<subseteq> L\<^sub>1 \<union> L\<^sub>2
unifier\<^sub>l\<^sub>s \<sigma> (L\<^sub>1 \<union> L\<^sub>2)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
L\<^sub>1 \<subseteq> L\<^sub>1 \<union> L\<^sub>2 \<and> L\<^sub>2 \<subseteq> L\<^sub>1 \<union> L\<^sub>2
unifier\<^sub>l\<^sub>s \<sigma> (L\<^sub>1 \<union> L\<^sub>2)

goal (1 subgoal):
 1. unifier\<^sub>l\<^sub>s \<sigma> L\<^sub>1 \<and> unifier\<^sub>l\<^sub>s \<sigma> L\<^sub>2
[PROOF STEP]
using unifier_sub1
[PROOF STATE]
proof (prove)
using this:
L\<^sub>1 \<subseteq> L\<^sub>1 \<union> L\<^sub>2 \<and> L\<^sub>2 \<subseteq> L\<^sub>1 \<union> L\<^sub>2
unifier\<^sub>l\<^sub>s \<sigma> (L\<^sub>1 \<union> L\<^sub>2)
\<lbrakk>unifier\<^sub>l\<^sub>s ?\<sigma> ?L; ?L' \<subseteq> ?L\<rbrakk> \<Longrightarrow> unifier\<^sub>l\<^sub>s ?\<sigma> ?L'

goal (1 subgoal):
 1. unifier\<^sub>l\<^sub>s \<sigma> L\<^sub>1 \<and> unifier\<^sub>l\<^sub>s \<sigma> L\<^sub>2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
unifier\<^sub>l\<^sub>s \<sigma> L\<^sub>1 \<and> unifier\<^sub>l\<^sub>s \<sigma> L\<^sub>2

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma substitutiont: "eval\<^sub>t E F (t \<cdot>\<^sub>t \<sigma>) = eval\<^sub>t (evalsub E F \<sigma>) F t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval\<^sub>t E F (t \<cdot>\<^sub>t \<sigma>) = eval\<^sub>t (evalsub E F \<sigma>) F t
[PROOF STEP]
apply (induction t)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x1 x2a. (\<And>x2aa. x2aa \<in> set x2a \<Longrightarrow> eval\<^sub>t E F (x2aa \<cdot>\<^sub>t \<sigma>) = eval\<^sub>t (evalsub E F \<sigma>) F x2aa) \<Longrightarrow> eval\<^sub>t E F (Fun x1 x2a \<cdot>\<^sub>t \<sigma>) = eval\<^sub>t (evalsub E F \<sigma>) F (Fun x1 x2a)
 2. \<And>x. eval\<^sub>t E F (\<epsilon> x \<cdot>\<^sub>t \<sigma>) = eval\<^sub>t (evalsub E F \<sigma>) F (\<epsilon> x)
[PROOF STEP]
unfolding evalsub_def
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x1 x2a. (\<And>x2aa. x2aa \<in> set x2a \<Longrightarrow> eval\<^sub>t E F (x2aa \<cdot>\<^sub>t \<sigma>) = eval\<^sub>t (eval\<^sub>t E F \<circ> \<sigma>) F x2aa) \<Longrightarrow> eval\<^sub>t E F (Fun x1 x2a \<cdot>\<^sub>t \<sigma>) = eval\<^sub>t (eval\<^sub>t E F \<circ> \<sigma>) F (Fun x1 x2a)
 2. \<And>x. eval\<^sub>t E F (\<epsilon> x \<cdot>\<^sub>t \<sigma>) = eval\<^sub>t (eval\<^sub>t E F \<circ> \<sigma>) F (\<epsilon> x)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2a. (\<And>x2aa. x2aa \<in> set x2a \<Longrightarrow> eval\<^sub>t E F (x2aa \<cdot>\<^sub>t \<sigma>) = eval\<^sub>t (\<lambda>a. eval\<^sub>t E F (\<sigma> a)) F x2aa) \<Longrightarrow> F x1 (map (eval\<^sub>t E F \<circ> (\<lambda>t. t \<cdot>\<^sub>t \<sigma>)) x2a) = F x1 (eval\<^sub>t\<^sub>s (\<lambda>a. eval\<^sub>t E F (\<sigma> a)) F x2a)
[PROOF STEP]
apply (metis (mono_tags, lifting) comp_apply map_cong)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma substitutionts: "eval\<^sub>t\<^sub>s E F (ts \<cdot>\<^sub>t\<^sub>s \<sigma>) = eval\<^sub>t\<^sub>s (evalsub E F \<sigma>) F ts"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval\<^sub>t\<^sub>s E F (ts \<cdot>\<^sub>t\<^sub>s \<sigma>) = eval\<^sub>t\<^sub>s (evalsub E F \<sigma>) F ts
[PROOF STEP]
using substitutiont
[PROOF STATE]
proof (prove)
using this:
eval\<^sub>t ?E ?F (?t \<cdot>\<^sub>t ?\<sigma>) = eval\<^sub>t (evalsub ?E ?F ?\<sigma>) ?F ?t

goal (1 subgoal):
 1. eval\<^sub>t\<^sub>s E F (ts \<cdot>\<^sub>t\<^sub>s \<sigma>) = eval\<^sub>t\<^sub>s (evalsub E F \<sigma>) F ts
[PROOF STEP]
by auto


[STATEMENT]
lemma substitution: "eval\<^sub>l E F G (l \<cdot>\<^sub>l \<sigma>) \<longleftrightarrow> eval\<^sub>l (evalsub E F \<sigma>) F G l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval\<^sub>l E F G (l \<cdot>\<^sub>l \<sigma>) = eval\<^sub>l (evalsub E F \<sigma>) F G l
[PROOF STEP]
apply (induction l)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x1 x2. eval\<^sub>l E F G (Pos x1 x2 \<cdot>\<^sub>l \<sigma>) = eval\<^sub>l (evalsub E F \<sigma>) F G (Pos x1 x2)
 2. \<And>x1 x2. eval\<^sub>l E F G (Neg x1 x2 \<cdot>\<^sub>l \<sigma>) = eval\<^sub>l (evalsub E F \<sigma>) F G (Neg x1 x2)
[PROOF STEP]
using substitutionts
[PROOF STATE]
proof (prove)
using this:
eval\<^sub>t\<^sub>s ?E ?F (?ts \<cdot>\<^sub>t\<^sub>s ?\<sigma>) = eval\<^sub>t\<^sub>s (evalsub ?E ?F ?\<sigma>) ?F ?ts

goal (2 subgoals):
 1. \<And>x1 x2. eval\<^sub>l E F G (Pos x1 x2 \<cdot>\<^sub>l \<sigma>) = eval\<^sub>l (evalsub E F \<sigma>) F G (Pos x1 x2)
 2. \<And>x1 x2. eval\<^sub>l E F G (Neg x1 x2 \<cdot>\<^sub>l \<sigma>) = eval\<^sub>l (evalsub E F \<sigma>) F G (Neg x1 x2)
[PROOF STEP]
apply (metis eval\<^sub>l.simps(1) subl.simps(1))
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2. eval\<^sub>l E F G (Neg x1 x2 \<cdot>\<^sub>l \<sigma>) = eval\<^sub>l (evalsub E F \<sigma>) F G (Neg x1 x2)
[PROOF STEP]
using substitutionts
[PROOF STATE]
proof (prove)
using this:
eval\<^sub>t\<^sub>s ?E ?F (?ts \<cdot>\<^sub>t\<^sub>s ?\<sigma>) = eval\<^sub>t\<^sub>s (evalsub ?E ?F ?\<sigma>) ?F ?ts

goal (1 subgoal):
 1. \<And>x1 x2. eval\<^sub>l E F G (Neg x1 x2 \<cdot>\<^sub>l \<sigma>) = eval\<^sub>l (evalsub E F \<sigma>) F G (Neg x1 x2)
[PROOF STEP]
apply (metis eval\<^sub>l.simps(2) subl.simps(2))
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma subst_sound:
 assumes asm: "eval\<^sub>c F G C"
 shows "eval\<^sub>c F G (C \<cdot>\<^sub>l\<^sub>s \<sigma>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval\<^sub>c F G (C \<cdot>\<^sub>l\<^sub>s \<sigma>)
[PROOF STEP]
unfolding eval\<^sub>c_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>E. Bex (C \<cdot>\<^sub>l\<^sub>s \<sigma>) (eval\<^sub>l E F G)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>E. Bex (C \<cdot>\<^sub>l\<^sub>s \<sigma>) (eval\<^sub>l E F G)
[PROOF STEP]
fix E
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>E. Bex (C \<cdot>\<^sub>l\<^sub>s \<sigma>) (eval\<^sub>l E F G)
[PROOF STEP]
from asm
[PROOF STATE]
proof (chain)
picking this:
eval\<^sub>c F G C
[PROOF STEP]
have "\<forall>E'. \<exists>l \<in> C. eval\<^sub>l E' F G l"
[PROOF STATE]
proof (prove)
using this:
eval\<^sub>c F G C

goal (1 subgoal):
 1. \<forall>E'. \<exists>l\<in>C. eval\<^sub>l E' F G l
[PROOF STEP]
using eval\<^sub>c_def
[PROOF STATE]
proof (prove)
using this:
eval\<^sub>c F G C
eval\<^sub>c ?F ?G ?C = (\<forall>E. \<exists>l\<in>?C. eval\<^sub>l E ?F ?G l)

goal (1 subgoal):
 1. \<forall>E'. \<exists>l\<in>C. eval\<^sub>l E' F G l
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>E'. \<exists>l\<in>C. eval\<^sub>l E' F G l

goal (1 subgoal):
 1. \<And>E. Bex (C \<cdot>\<^sub>l\<^sub>s \<sigma>) (eval\<^sub>l E F G)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>E'. \<exists>l\<in>C. eval\<^sub>l E' F G l
[PROOF STEP]
have "\<exists>l \<in> C. eval\<^sub>l (evalsub E F \<sigma>) F G l"
[PROOF STATE]
proof (prove)
using this:
\<forall>E'. \<exists>l\<in>C. eval\<^sub>l E' F G l

goal (1 subgoal):
 1. \<exists>l\<in>C. eval\<^sub>l (evalsub E F \<sigma>) F G l
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>l\<in>C. eval\<^sub>l (evalsub E F \<sigma>) F G l

goal (1 subgoal):
 1. \<And>E. Bex (C \<cdot>\<^sub>l\<^sub>s \<sigma>) (eval\<^sub>l E F G)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>l\<in>C. eval\<^sub>l (evalsub E F \<sigma>) F G l
[PROOF STEP]
show "\<exists>l \<in> C \<cdot>\<^sub>l\<^sub>s \<sigma>. eval\<^sub>l E F G l"
[PROOF STATE]
proof (prove)
using this:
\<exists>l\<in>C. eval\<^sub>l (evalsub E F \<sigma>) F G l

goal (1 subgoal):
 1. \<exists>l\<in>C \<cdot>\<^sub>l\<^sub>s \<sigma>. eval\<^sub>l E F G l
[PROOF STEP]
using substitution
[PROOF STATE]
proof (prove)
using this:
\<exists>l\<in>C. eval\<^sub>l (evalsub E F \<sigma>) F G l
eval\<^sub>l ?E ?F ?G (?l \<cdot>\<^sub>l ?\<sigma>) = eval\<^sub>l (evalsub ?E ?F ?\<sigma>) ?F ?G ?l

goal (1 subgoal):
 1. \<exists>l\<in>C \<cdot>\<^sub>l\<^sub>s \<sigma>. eval\<^sub>l E F G l
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>l\<in>C \<cdot>\<^sub>l\<^sub>s \<sigma>. eval\<^sub>l E F G l

goal:
No subgoals!
[PROOF STEP]
qed