[STATEMENT]
theorem dist_induces_open:
  "open U \<longleftrightarrow> (\<forall>x\<in>U. \<exists>e>0. \<forall>y. dist x y < e \<longrightarrow> y \<in> U)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. open U = (\<forall>x\<in>U. \<exists>e>0. \<forall>y. local.dist x y < e \<longrightarrow> y \<in> U)
[PROOF STEP]
proof (transfer, safe)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>U x. \<lbrakk>\<forall>x\<in>U. \<exists>b>0. arith_prog x b \<subseteq> U; x \<in> U\<rbrakk> \<Longrightarrow> \<exists>e>0. \<forall>y. N (x - y) < e \<longrightarrow> y \<in> U
 2. \<And>U x. \<lbrakk>\<forall>x\<in>U. \<exists>e>0. \<forall>y. N (x - y) < e \<longrightarrow> y \<in> U; x \<in> U\<rbrakk> \<Longrightarrow> \<exists>b>0. arith_prog x b \<subseteq> U
[PROOF STEP]
fix U :: "int set" and x :: int
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>U x. \<lbrakk>\<forall>x\<in>U. \<exists>b>0. arith_prog x b \<subseteq> U; x \<in> U\<rbrakk> \<Longrightarrow> \<exists>e>0. \<forall>y. N (x - y) < e \<longrightarrow> y \<in> U
 2. \<And>U x. \<lbrakk>\<forall>x\<in>U. \<exists>e>0. \<forall>y. N (x - y) < e \<longrightarrow> y \<in> U; x \<in> U\<rbrakk> \<Longrightarrow> \<exists>b>0. arith_prog x b \<subseteq> U
[PROOF STEP]
assume *: "\<forall>x\<in>U. \<exists>b>0. arith_prog x b \<subseteq> U"
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>U. \<exists>b>0. arith_prog x b \<subseteq> U

goal (2 subgoals):
 1. \<And>U x. \<lbrakk>\<forall>x\<in>U. \<exists>b>0. arith_prog x b \<subseteq> U; x \<in> U\<rbrakk> \<Longrightarrow> \<exists>e>0. \<forall>y. N (x - y) < e \<longrightarrow> y \<in> U
 2. \<And>U x. \<lbrakk>\<forall>x\<in>U. \<exists>e>0. \<forall>y. N (x - y) < e \<longrightarrow> y \<in> U; x \<in> U\<rbrakk> \<Longrightarrow> \<exists>b>0. arith_prog x b \<subseteq> U
[PROOF STEP]
assume "x \<in> U"
[PROOF STATE]
proof (state)
this:
x \<in> U

goal (2 subgoals):
 1. \<And>U x. \<lbrakk>\<forall>x\<in>U. \<exists>b>0. arith_prog x b \<subseteq> U; x \<in> U\<rbrakk> \<Longrightarrow> \<exists>e>0. \<forall>y. N (x - y) < e \<longrightarrow> y \<in> U
 2. \<And>U x. \<lbrakk>\<forall>x\<in>U. \<exists>e>0. \<forall>y. N (x - y) < e \<longrightarrow> y \<in> U; x \<in> U\<rbrakk> \<Longrightarrow> \<exists>b>0. arith_prog x b \<subseteq> U
[PROOF STEP]
with *
[PROOF STATE]
proof (chain)
picking this:
\<forall>x\<in>U. \<exists>b>0. arith_prog x b \<subseteq> U
x \<in> U
[PROOF STEP]
obtain b where b: "b > 0" "arith_prog x b \<subseteq> U"
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>U. \<exists>b>0. arith_prog x b \<subseteq> U
x \<in> U

goal (1 subgoal):
 1. (\<And>b. \<lbrakk>0 < b; arith_prog x b \<subseteq> U\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
0 < b
arith_prog x b \<subseteq> U

goal (2 subgoals):
 1. \<And>U x. \<lbrakk>\<forall>x\<in>U. \<exists>b>0. arith_prog x b \<subseteq> U; x \<in> U\<rbrakk> \<Longrightarrow> \<exists>e>0. \<forall>y. N (x - y) < e \<longrightarrow> y \<in> U
 2. \<And>U x. \<lbrakk>\<forall>x\<in>U. \<exists>e>0. \<forall>y. N (x - y) < e \<longrightarrow> y \<in> U; x \<in> U\<rbrakk> \<Longrightarrow> \<exists>b>0. arith_prog x b \<subseteq> U
[PROOF STEP]
define e where "e = 1 / q ^ b"
[PROOF STATE]
proof (state)
this:
e = 1 / q ^ b

goal (2 subgoals):
 1. \<And>U x. \<lbrakk>\<forall>x\<in>U. \<exists>b>0. arith_prog x b \<subseteq> U; x \<in> U\<rbrakk> \<Longrightarrow> \<exists>e>0. \<forall>y. N (x - y) < e \<longrightarrow> y \<in> U
 2. \<And>U x. \<lbrakk>\<forall>x\<in>U. \<exists>e>0. \<forall>y. N (x - y) < e \<longrightarrow> y \<in> U; x \<in> U\<rbrakk> \<Longrightarrow> \<exists>b>0. arith_prog x b \<subseteq> U
[PROOF STEP]
show "\<exists>e>0. \<forall>y. N (x - y) < e \<longrightarrow> y \<in> U"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>e>0. \<forall>y. N (x - y) < e \<longrightarrow> y \<in> U
[PROOF STEP]
proof (rule exI; safe?)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. 0 < ?e1
 2. \<And>y. N (x - y) < ?e1 \<Longrightarrow> y \<in> U
[PROOF STEP]
show "e > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < e
[PROOF STEP]
using q_gt_1
[PROOF STATE]
proof (prove)
using this:
1 < q

goal (1 subgoal):
 1. 0 < e
[PROOF STEP]
by (simp add: e_def)
[PROOF STATE]
proof (state)
this:
0 < e

goal (1 subgoal):
 1. \<And>y. N (x - y) < e \<Longrightarrow> y \<in> U
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>y. N (x - y) < e \<Longrightarrow> y \<in> U
[PROOF STEP]
fix y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>y. N (x - y) < e \<Longrightarrow> y \<in> U
[PROOF STEP]
assume "N (x - y) < e"
[PROOF STATE]
proof (state)
this:
N (x - y) < e

goal (1 subgoal):
 1. \<And>y. N (x - y) < e \<Longrightarrow> y \<in> U
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
N (x - y) < e

goal (1 subgoal):
 1. \<And>y. N (x - y) < e \<Longrightarrow> y \<in> U
[PROOF STEP]
have "\<dots> = 1 / q ^ b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. e = 1 / q ^ b
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
e = 1 / q ^ b

goal (1 subgoal):
 1. \<And>y. N (x - y) < e \<Longrightarrow> y \<in> U
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
N (x - y) < 1 / q ^ b
[PROOF STEP]
have "b dvd (x - y)"
[PROOF STATE]
proof (prove)
using this:
N (x - y) < 1 / q ^ b

goal (1 subgoal):
 1. int b dvd x - y
[PROOF STEP]
by (rule N_lt_imp_dvd) fact
[PROOF STATE]
proof (state)
this:
int b dvd x - y

goal (1 subgoal):
 1. \<And>y. N (x - y) < e \<Longrightarrow> y \<in> U
[PROOF STEP]
hence "y \<in> arith_prog x b"
[PROOF STATE]
proof (prove)
using this:
int b dvd x - y

goal (1 subgoal):
 1. y \<in> arith_prog x b
[PROOF STEP]
by (auto simp: arith_prog_def cong_iff_dvd_diff dvd_diff_commute)
[PROOF STATE]
proof (state)
this:
y \<in> arith_prog x b

goal (1 subgoal):
 1. \<And>y. N (x - y) < e \<Longrightarrow> y \<in> U
[PROOF STEP]
with b
[PROOF STATE]
proof (chain)
picking this:
0 < b
arith_prog x b \<subseteq> U
y \<in> arith_prog x b
[PROOF STEP]
show "y \<in> U"
[PROOF STATE]
proof (prove)
using this:
0 < b
arith_prog x b \<subseteq> U
y \<in> arith_prog x b

goal (1 subgoal):
 1. y \<in> U
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
y \<in> U

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>e>0. \<forall>y. N (x - y) < e \<longrightarrow> y \<in> U

goal (1 subgoal):
 1. \<And>U x. \<lbrakk>\<forall>x\<in>U. \<exists>e>0. \<forall>y. N (x - y) < e \<longrightarrow> y \<in> U; x \<in> U\<rbrakk> \<Longrightarrow> \<exists>b>0. arith_prog x b \<subseteq> U
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>U x. \<lbrakk>\<forall>x\<in>U. \<exists>e>0. \<forall>y. N (x - y) < e \<longrightarrow> y \<in> U; x \<in> U\<rbrakk> \<Longrightarrow> \<exists>b>0. arith_prog x b \<subseteq> U
[PROOF STEP]
fix U :: "int set" and x :: int
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>U x. \<lbrakk>\<forall>x\<in>U. \<exists>e>0. \<forall>y. N (x - y) < e \<longrightarrow> y \<in> U; x \<in> U\<rbrakk> \<Longrightarrow> \<exists>b>0. arith_prog x b \<subseteq> U
[PROOF STEP]
assume *: "\<forall>x\<in>U. \<exists>e>0. \<forall>y. N (x - y) < e \<longrightarrow> y \<in> U"
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>U. \<exists>e>0. \<forall>y. N (x - y) < e \<longrightarrow> y \<in> U

goal (1 subgoal):
 1. \<And>U x. \<lbrakk>\<forall>x\<in>U. \<exists>e>0. \<forall>y. N (x - y) < e \<longrightarrow> y \<in> U; x \<in> U\<rbrakk> \<Longrightarrow> \<exists>b>0. arith_prog x b \<subseteq> U
[PROOF STEP]
assume "x \<in> U"
[PROOF STATE]
proof (state)
this:
x \<in> U

goal (1 subgoal):
 1. \<And>U x. \<lbrakk>\<forall>x\<in>U. \<exists>e>0. \<forall>y. N (x - y) < e \<longrightarrow> y \<in> U; x \<in> U\<rbrakk> \<Longrightarrow> \<exists>b>0. arith_prog x b \<subseteq> U
[PROOF STEP]
with *
[PROOF STATE]
proof (chain)
picking this:
\<forall>x\<in>U. \<exists>e>0. \<forall>y. N (x - y) < e \<longrightarrow> y \<in> U
x \<in> U
[PROOF STEP]
obtain e where e: "e > 0" "\<forall>y. N (x - y) < e \<longrightarrow> y \<in> U"
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>U. \<exists>e>0. \<forall>y. N (x - y) < e \<longrightarrow> y \<in> U
x \<in> U

goal (1 subgoal):
 1. (\<And>e. \<lbrakk>0 < e; \<forall>y. N (x - y) < e \<longrightarrow> y \<in> U\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
0 < e
\<forall>y. N (x - y) < e \<longrightarrow> y \<in> U

goal (1 subgoal):
 1. \<And>U x. \<lbrakk>\<forall>x\<in>U. \<exists>e>0. \<forall>y. N (x - y) < e \<longrightarrow> y \<in> U; x \<in> U\<rbrakk> \<Longrightarrow> \<exists>b>0. arith_prog x b \<subseteq> U
[PROOF STEP]
have "eventually (\<lambda>N. 1 / (q - 1) * 1 / q ^ N < e) at_top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<^sub>F N in sequentially. 1 / (q - 1) * 1 / q ^ N < e
[PROOF STEP]
using q_gt_1 \<open>e > 0\<close>
[PROOF STATE]
proof (prove)
using this:
1 < q
0 < e

goal (1 subgoal):
 1. \<forall>\<^sub>F N in sequentially. 1 / (q - 1) * 1 / q ^ N < e
[PROOF STEP]
by real_asymp
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F N in sequentially. 1 / (q - 1) * 1 / q ^ N < e

goal (1 subgoal):
 1. \<And>U x. \<lbrakk>\<forall>x\<in>U. \<exists>e>0. \<forall>y. N (x - y) < e \<longrightarrow> y \<in> U; x \<in> U\<rbrakk> \<Longrightarrow> \<exists>b>0. arith_prog x b \<subseteq> U
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>\<^sub>F N in sequentially. 1 / (q - 1) * 1 / q ^ N < e
[PROOF STEP]
obtain m where m: "1 / (q - 1) * 1 / q ^ m < e"
[PROOF STATE]
proof (prove)
using this:
\<forall>\<^sub>F N in sequentially. 1 / (q - 1) * 1 / q ^ N < e

goal (1 subgoal):
 1. (\<And>m. 1 / (q - 1) * 1 / q ^ m < e \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: eventually_at_top_linorder)
[PROOF STATE]
proof (state)
this:
1 / (q - 1) * 1 / q ^ m < e

goal (1 subgoal):
 1. \<And>U x. \<lbrakk>\<forall>x\<in>U. \<exists>e>0. \<forall>y. N (x - y) < e \<longrightarrow> y \<in> U; x \<in> U\<rbrakk> \<Longrightarrow> \<exists>b>0. arith_prog x b \<subseteq> U
[PROOF STEP]
define b :: nat where "b = fact m"
[PROOF STATE]
proof (state)
this:
b = fact m

goal (1 subgoal):
 1. \<And>U x. \<lbrakk>\<forall>x\<in>U. \<exists>e>0. \<forall>y. N (x - y) < e \<longrightarrow> y \<in> U; x \<in> U\<rbrakk> \<Longrightarrow> \<exists>b>0. arith_prog x b \<subseteq> U
[PROOF STEP]
have "arith_prog x b \<subseteq> U"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. arith_prog x b \<subseteq> U
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa. xa \<in> arith_prog x b \<Longrightarrow> xa \<in> U
[PROOF STEP]
fix y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa. xa \<in> arith_prog x b \<Longrightarrow> xa \<in> U
[PROOF STEP]
assume "y \<in> arith_prog x b"
[PROOF STATE]
proof (state)
this:
y \<in> arith_prog x b

goal (1 subgoal):
 1. \<And>xa. xa \<in> arith_prog x b \<Longrightarrow> xa \<in> U
[PROOF STEP]
show "y \<in> U"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y \<in> U
[PROOF STEP]
proof (cases "y = x")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. y = x \<Longrightarrow> y \<in> U
 2. y \<noteq> x \<Longrightarrow> y \<in> U
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
y \<noteq> x

goal (2 subgoals):
 1. y = x \<Longrightarrow> y \<in> U
 2. y \<noteq> x \<Longrightarrow> y \<in> U
[PROOF STEP]
from \<open>y \<in> arith_prog x b\<close>
[PROOF STATE]
proof (chain)
picking this:
y \<in> arith_prog x b
[PROOF STEP]
obtain n where y: "y = x + int b * n"
[PROOF STATE]
proof (prove)
using this:
y \<in> arith_prog x b

goal (1 subgoal):
 1. (\<And>n. y = x + int b * n \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: arith_prog_altdef)
[PROOF STATE]
proof (state)
this:
y = x + int b * n

goal (2 subgoals):
 1. y = x \<Longrightarrow> y \<in> U
 2. y \<noteq> x \<Longrightarrow> y \<in> U
[PROOF STEP]
from y and \<open>y \<noteq> x\<close>
[PROOF STATE]
proof (chain)
picking this:
y = x + int b * n
y \<noteq> x
[PROOF STEP]
have [simp]: "n \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
y = x + int b * n
y \<noteq> x

goal (1 subgoal):
 1. n \<noteq> 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
n \<noteq> 0

goal (2 subgoals):
 1. y = x \<Longrightarrow> y \<in> U
 2. y \<noteq> x \<Longrightarrow> y \<in> U
[PROOF STEP]
have "N (x - y) = N (int b * n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. N (x - y) = N (int b * n)
[PROOF STEP]
by (simp add: y)
[PROOF STATE]
proof (state)
this:
N (x - y) = N (int b * n)

goal (2 subgoals):
 1. y = x \<Longrightarrow> y \<in> U
 2. y \<noteq> x \<Longrightarrow> y \<in> U
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
N (x - y) = N (int b * n)

goal (2 subgoals):
 1. y = x \<Longrightarrow> y \<in> U
 2. y \<noteq> x \<Longrightarrow> y \<in> U
[PROOF STEP]
have "\<dots> \<le> N (int b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. N (int b * n) \<le> N (int b)
[PROOF STEP]
by (rule N_dvd_mono) auto
[PROOF STATE]
proof (state)
this:
N (int b * n) \<le> N (int b)

goal (2 subgoals):
 1. y = x \<Longrightarrow> y \<in> U
 2. y \<noteq> x \<Longrightarrow> y \<in> U
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
N (int b * n) \<le> N (int b)

goal (2 subgoals):
 1. y = x \<Longrightarrow> y \<in> U
 2. y \<noteq> x \<Longrightarrow> y \<in> U
[PROOF STEP]
have "\<dots> \<le> 1 / (q - 1) * 1 / q ^ m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. N (int b) \<le> 1 / (q - 1) * 1 / q ^ m
[PROOF STEP]
using N_fact_le
[PROOF STATE]
proof (prove)
using this:
N (fact ?m) \<le> 1 / (q - 1) * 1 / q ^ ?m

goal (1 subgoal):
 1. N (int b) \<le> 1 / (q - 1) * 1 / q ^ m
[PROOF STEP]
by (simp add: b_def)
[PROOF STATE]
proof (state)
this:
N (int b) \<le> 1 / (q - 1) * 1 / q ^ m

goal (2 subgoals):
 1. y = x \<Longrightarrow> y \<in> U
 2. y \<noteq> x \<Longrightarrow> y \<in> U
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
N (int b) \<le> 1 / (q - 1) * 1 / q ^ m

goal (2 subgoals):
 1. y = x \<Longrightarrow> y \<in> U
 2. y \<noteq> x \<Longrightarrow> y \<in> U
[PROOF STEP]
have "\<dots> < e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 / (q - 1) * 1 / q ^ m < e
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
1 / (q - 1) * 1 / q ^ m < e

goal (2 subgoals):
 1. y = x \<Longrightarrow> y \<in> U
 2. y \<noteq> x \<Longrightarrow> y \<in> U
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
N (x - y) < e
[PROOF STEP]
show "y \<in> U"
[PROOF STATE]
proof (prove)
using this:
N (x - y) < e

goal (1 subgoal):
 1. y \<in> U
[PROOF STEP]
using e
[PROOF STATE]
proof (prove)
using this:
N (x - y) < e
0 < e
\<forall>y. N (x - y) < e \<longrightarrow> y \<in> U

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

goal (1 subgoal):
 1. y = x \<Longrightarrow> y \<in> U
[PROOF STEP]
qed (use \<open>x \<in> U\<close> in auto)
[PROOF STATE]
proof (state)
this:
y \<in> U

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
arith_prog x b \<subseteq> U

goal (1 subgoal):
 1. \<And>U x. \<lbrakk>\<forall>x\<in>U. \<exists>e>0. \<forall>y. N (x - y) < e \<longrightarrow> y \<in> U; x \<in> U\<rbrakk> \<Longrightarrow> \<exists>b>0. arith_prog x b \<subseteq> U
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
arith_prog x b \<subseteq> U

goal (1 subgoal):
 1. \<And>U x. \<lbrakk>\<forall>x\<in>U. \<exists>e>0. \<forall>y. N (x - y) < e \<longrightarrow> y \<in> U; x \<in> U\<rbrakk> \<Longrightarrow> \<exists>b>0. arith_prog x b \<subseteq> U
[PROOF STEP]
have "b > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < b
[PROOF STEP]
by (auto simp: b_def)
[PROOF STATE]
proof (state)
this:
0 < b

goal (1 subgoal):
 1. \<And>U x. \<lbrakk>\<forall>x\<in>U. \<exists>e>0. \<forall>y. N (x - y) < e \<longrightarrow> y \<in> U; x \<in> U\<rbrakk> \<Longrightarrow> \<exists>b>0. arith_prog x b \<subseteq> U
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
arith_prog x b \<subseteq> U
0 < b
[PROOF STEP]
show "\<exists>b>0. arith_prog x b \<subseteq> U"
[PROOF STATE]
proof (prove)
using this:
arith_prog x b \<subseteq> U
0 < b

goal (1 subgoal):
 1. \<exists>b>0. arith_prog x b \<subseteq> U
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>b>0. arith_prog x b \<subseteq> U

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma tendsto_fbint_fact: "(\<lambda>n. fbint (fact n)) \<longlonglongrightarrow> fbint 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. fbint (fact n)) \<longlonglongrightarrow> fbint 0
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<lambda>n. fbint (fact n)) \<longlonglongrightarrow> fbint 0
[PROOF STEP]
have "(\<lambda>n. dist (fbint (fact n)) (fbint 0)) \<longlonglongrightarrow> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. dist (fbint (fact n)) (fbint 0)) \<longlonglongrightarrow> 0
[PROOF STEP]
proof (rule tendsto_sandwich[OF always_eventually always_eventually]; safe?)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>x. ?f1 x \<le> dist (fbint (fact x)) (fbint 0)
 2. \<And>x. dist (fbint (fact x)) (fbint 0) \<le> ?h1 x
 3. ?f1 \<longlonglongrightarrow> 0
 4. ?h1 \<longlonglongrightarrow> 0
[PROOF STEP]
fix n :: nat
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>x. ?f1 x \<le> dist (fbint (fact x)) (fbint 0)
 2. \<And>x. dist (fbint (fact x)) (fbint 0) \<le> ?h1 x
 3. ?f1 \<longlonglongrightarrow> 0
 4. ?h1 \<longlonglongrightarrow> 0
[PROOF STEP]
show "dist (fbint (fact n)) (fbint 0) \<le> 1 / 2 ^ n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (fbint (fact n)) (fbint 0) \<le> 1 / 2 ^ n
[PROOF STEP]
unfolding dist_fbint_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fb.dist (fbint (fact n)) (fbint 0) \<le> 1 / 2 ^ n
[PROOF STEP]
by (transfer fixing: n) (use fb.N_fact_le[of n] in simp)
[PROOF STATE]
proof (state)
this:
dist (fbint (fact n)) (fbint 0) \<le> 1 / 2 ^ n

goal (3 subgoals):
 1. \<And>x. ?f1 x \<le> dist (fbint (fact x)) (fbint 0)
 2. ?f1 \<longlonglongrightarrow> 0
 3. (\<lambda>x. 1 / 2 ^ x) \<longlonglongrightarrow> 0
[PROOF STEP]
show "dist (fbint (fact n)) (fbint 0) \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> dist (fbint (fact n)) (fbint 0)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 \<le> dist (fbint (fact n)) (fbint 0)

goal (2 subgoals):
 1. (\<lambda>x. 0) \<longlonglongrightarrow> 0
 2. (\<lambda>x. 1 / 2 ^ x) \<longlonglongrightarrow> 0
[PROOF STEP]
show "(\<lambda>n. 1 / 2 ^ n :: real) \<longlonglongrightarrow> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. 1 / 2 ^ n) \<longlonglongrightarrow> 0
[PROOF STEP]
by real_asymp
[PROOF STATE]
proof (state)
this:
(\<lambda>n. 1 / 2 ^ n) \<longlonglongrightarrow> 0

goal (1 subgoal):
 1. (\<lambda>x. 0) \<longlonglongrightarrow> 0
[PROOF STEP]
qed simp_all
[PROOF STATE]
proof (state)
this:
(\<lambda>n. dist (fbint (fact n)) (fbint 0)) \<longlonglongrightarrow> 0

goal (1 subgoal):
 1. (\<lambda>n. fbint (fact n)) \<longlonglongrightarrow> fbint 0
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<lambda>n. dist (fbint (fact n)) (fbint 0)) \<longlonglongrightarrow> 0

goal (1 subgoal):
 1. (\<lambda>n. fbint (fact n)) \<longlonglongrightarrow> fbint 0
[PROOF STEP]
using tendsto_dist_iff
[PROOF STATE]
proof (prove)
using this:
(\<lambda>n. dist (fbint (fact n)) (fbint 0)) \<longlonglongrightarrow> 0
(?f \<longlongrightarrow> ?l) ?F = ((\<lambda>x. dist (?f x) ?l) \<longlongrightarrow> 0) ?F

goal (1 subgoal):
 1. (\<lambda>n. fbint (fact n)) \<longlonglongrightarrow> fbint 0
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
(\<lambda>n. fbint (fact n)) \<longlonglongrightarrow> fbint 0

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cancel_comp1: "(l\<^sup>c)\<^sup>c = l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l\<^sup>c\<^sup>c = l
[PROOF STEP]
by (cases l) auto


[STATEMENT]
lemma cancel_comp2:
  assumes asm: "l\<^sub>1\<^sup>c = l\<^sub>2\<^sup>c"
  shows "l\<^sub>1 = l\<^sub>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l\<^sub>1 = l\<^sub>2
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. l\<^sub>1 = l\<^sub>2
[PROOF STEP]
from asm
[PROOF STATE]
proof (chain)
picking this:
l\<^sub>1\<^sup>c = l\<^sub>2\<^sup>c
[PROOF STEP]
have "(l\<^sub>1\<^sup>c)\<^sup>c = (l\<^sub>2\<^sup>c)\<^sup>c"
[PROOF STATE]
proof (prove)
using this:
l\<^sub>1\<^sup>c = l\<^sub>2\<^sup>c

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

goal (1 subgoal):
 1. l\<^sub>1 = l\<^sub>2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
l\<^sub>1\<^sup>c\<^sup>c = l\<^sub>2\<^sup>c\<^sup>c
[PROOF STEP]
have "l\<^sub>1 = (l\<^sub>2\<^sup>c)\<^sup>c"
[PROOF STATE]
proof (prove)
using this:
l\<^sub>1\<^sup>c\<^sup>c = l\<^sub>2\<^sup>c\<^sup>c

goal (1 subgoal):
 1. l\<^sub>1 = l\<^sub>2\<^sup>c\<^sup>c
[PROOF STEP]
using cancel_comp1[of l\<^sub>1]
[PROOF STATE]
proof (prove)
using this:
l\<^sub>1\<^sup>c\<^sup>c = l\<^sub>2\<^sup>c\<^sup>c
l\<^sub>1\<^sup>c\<^sup>c = l\<^sub>1

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

goal (1 subgoal):
 1. l\<^sub>1 = l\<^sub>2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
l\<^sub>1 = l\<^sub>2\<^sup>c\<^sup>c
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
l\<^sub>1 = l\<^sub>2\<^sup>c\<^sup>c

goal (1 subgoal):
 1. l\<^sub>1 = l\<^sub>2
[PROOF STEP]
using cancel_comp1[of l\<^sub>2]
[PROOF STATE]
proof (prove)
using this:
l\<^sub>1 = l\<^sub>2\<^sup>c\<^sup>c
l\<^sub>2\<^sup>c\<^sup>c = l\<^sub>2

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma comp_exi1: "\<exists>l'. l' = l\<^sup>c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>l'. l' = l\<^sup>c
[PROOF STEP]
by (cases l) auto


[STATEMENT]
lemma comp_swap: "l\<^sub>1\<^sup>c = l\<^sub>2 \<longleftrightarrow> l\<^sub>1 = l\<^sub>2\<^sup>c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (l\<^sub>1\<^sup>c = l\<^sub>2) = (l\<^sub>1 = l\<^sub>2\<^sup>c)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (l\<^sub>1\<^sup>c = l\<^sub>2) = (l\<^sub>1 = l\<^sub>2\<^sup>c)
[PROOF STEP]
have "l\<^sub>1\<^sup>c = l\<^sub>2 \<longrightarrow> l\<^sub>1 = l\<^sub>2\<^sup>c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l\<^sub>1\<^sup>c = l\<^sub>2 \<longrightarrow> l\<^sub>1 = l\<^sub>2\<^sup>c
[PROOF STEP]
using cancel_comp1[of l\<^sub>1]
[PROOF STATE]
proof (prove)
using this:
l\<^sub>1\<^sup>c\<^sup>c = l\<^sub>1

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

goal (1 subgoal):
 1. (l\<^sub>1\<^sup>c = l\<^sub>2) = (l\<^sub>1 = l\<^sub>2\<^sup>c)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
l\<^sub>1\<^sup>c = l\<^sub>2 \<longrightarrow> l\<^sub>1 = l\<^sub>2\<^sup>c

goal (1 subgoal):
 1. (l\<^sub>1\<^sup>c = l\<^sub>2) = (l\<^sub>1 = l\<^sub>2\<^sup>c)
[PROOF STEP]
have "l\<^sub>1 = l\<^sub>2\<^sup>c \<longrightarrow> l\<^sub>1\<^sup>c = l\<^sub>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l\<^sub>1 = l\<^sub>2\<^sup>c \<longrightarrow> l\<^sub>1\<^sup>c = l\<^sub>2
[PROOF STEP]
using cancel_comp1
[PROOF STATE]
proof (prove)
using this:
?l\<^sup>c\<^sup>c = ?l

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

goal (1 subgoal):
 1. (l\<^sub>1\<^sup>c = l\<^sub>2) = (l\<^sub>1 = l\<^sub>2\<^sup>c)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
l\<^sub>1\<^sup>c = l\<^sub>2 \<longrightarrow> l\<^sub>1 = l\<^sub>2\<^sup>c
l\<^sub>1 = l\<^sub>2\<^sup>c \<longrightarrow> l\<^sub>1\<^sup>c = l\<^sub>2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
l\<^sub>1\<^sup>c = l\<^sub>2 \<longrightarrow> l\<^sub>1 = l\<^sub>2\<^sup>c
l\<^sub>1 = l\<^sub>2\<^sup>c \<longrightarrow> l\<^sub>1\<^sup>c = l\<^sub>2

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sign_comp: "sign l\<^sub>1 \<noteq> sign l\<^sub>2 \<and> get_pred l\<^sub>1 = get_pred l\<^sub>2 \<and> get_terms l\<^sub>1 = get_terms l\<^sub>2 \<longleftrightarrow> l\<^sub>2 = l\<^sub>1\<^sup>c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (sign l\<^sub>1 \<noteq> sign l\<^sub>2 \<and> get_pred l\<^sub>1 = get_pred l\<^sub>2 \<and> get_terms l\<^sub>1 = get_terms l\<^sub>2) = (l\<^sub>2 = l\<^sub>1\<^sup>c)
[PROOF STEP]
by (cases l\<^sub>1; cases l\<^sub>2) auto


[STATEMENT]
lemma sign_comp_atom: "sign l\<^sub>1 \<noteq> sign l\<^sub>2 \<and> get_atom l\<^sub>1 = get_atom l\<^sub>2 \<longleftrightarrow> l\<^sub>2 = l\<^sub>1\<^sup>c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (sign l\<^sub>1 \<noteq> sign l\<^sub>2 \<and> get_atom l\<^sub>1 = get_atom l\<^sub>2) = (l\<^sub>2 = l\<^sub>1\<^sup>c)
[PROOF STEP]
by (cases l\<^sub>1; cases l\<^sub>2) auto


[STATEMENT]
lemma cancel_compls1: "(L\<^sup>C)\<^sup>C = L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. L\<^sup>C\<^sup>C = L
[PROOF STEP]
apply (auto simp add: cancel_comp1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> L \<Longrightarrow> x \<in> L\<^sup>C\<^sup>C
[PROOF STEP]
apply (metis imageI cancel_comp1)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma cancel_compls2:
  assumes asm: "L\<^sub>1\<^sup>C = L\<^sub>2\<^sup>C"
  shows "L\<^sub>1 = L\<^sub>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. L\<^sub>1 = L\<^sub>2
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. L\<^sub>1 = L\<^sub>2
[PROOF STEP]
from asm
[PROOF STATE]
proof (chain)
picking this:
L\<^sub>1\<^sup>C = L\<^sub>2\<^sup>C
[PROOF STEP]
have "(L\<^sub>1\<^sup>C)\<^sup>C = (L\<^sub>2\<^sup>C)\<^sup>C"
[PROOF STATE]
proof (prove)
using this:
L\<^sub>1\<^sup>C = L\<^sub>2\<^sup>C

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

goal (1 subgoal):
 1. L\<^sub>1 = L\<^sub>2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
L\<^sub>1\<^sup>C\<^sup>C = L\<^sub>2\<^sup>C\<^sup>C
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
L\<^sub>1\<^sup>C\<^sup>C = L\<^sub>2\<^sup>C\<^sup>C

goal (1 subgoal):
 1. L\<^sub>1 = L\<^sub>2
[PROOF STEP]
using cancel_compls1[of L\<^sub>1] cancel_compls1[of L\<^sub>2]
[PROOF STATE]
proof (prove)
using this:
L\<^sub>1\<^sup>C\<^sup>C = L\<^sub>2\<^sup>C\<^sup>C
L\<^sub>1\<^sup>C\<^sup>C = L\<^sub>1
L\<^sub>2\<^sup>C\<^sup>C = L\<^sub>2

goal (1 subgoal):
 1. L\<^sub>1 = L\<^sub>2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
L\<^sub>1 = L\<^sub>2

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ground_vars\<^sub>t:
  assumes "ground\<^sub>t t"
  shows "vars\<^sub>t t = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vars\<^sub>t t = {}
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
ground\<^sub>t t

goal (1 subgoal):
 1. vars\<^sub>t t = {}
[PROOF STEP]
by (induction t) auto


[STATEMENT]
lemma ground\<^sub>t\<^sub>s_vars\<^sub>t\<^sub>s:
  assumes "ground\<^sub>t\<^sub>s ts"
  shows "vars\<^sub>t\<^sub>s ts = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vars\<^sub>t\<^sub>s ts = {}
[PROOF STEP]
using assms ground_vars\<^sub>t
[PROOF STATE]
proof (prove)
using this:
ground\<^sub>t\<^sub>s ts
ground\<^sub>t ?t \<Longrightarrow> vars\<^sub>t ?t = {}

goal (1 subgoal):
 1. vars\<^sub>t\<^sub>s ts = {}
[PROOF STEP]
by auto


[STATEMENT]
lemma ground\<^sub>l_vars\<^sub>l:
  assumes "ground\<^sub>l l"
  shows "vars\<^sub>l l = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vars\<^sub>l l = {}
[PROOF STEP]
unfolding vars\<^sub>l_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vars\<^sub>t\<^sub>s (get_terms l) = {}
[PROOF STEP]
using assms ground_vars\<^sub>t
[PROOF STATE]
proof (prove)
using this:
ground\<^sub>l l
ground\<^sub>t ?t \<Longrightarrow> vars\<^sub>t ?t = {}

goal (1 subgoal):
 1. vars\<^sub>t\<^sub>s (get_terms l) = {}
[PROOF STEP]
by auto


[STATEMENT]
lemma ground\<^sub>l\<^sub>s_vars\<^sub>l\<^sub>s:
  assumes "ground\<^sub>l\<^sub>s L"
  shows "vars\<^sub>l\<^sub>s L = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vars\<^sub>l\<^sub>s L = {}
[PROOF STEP]
unfolding vars\<^sub>l\<^sub>s_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Union> (vars\<^sub>l ` L) = {}
[PROOF STEP]
using assms ground\<^sub>l_vars\<^sub>l
[PROOF STATE]
proof (prove)
using this:
ground\<^sub>l\<^sub>s L
ground\<^sub>l ?l \<Longrightarrow> vars\<^sub>l ?l = {}

goal (1 subgoal):
 1. \<Union> (vars\<^sub>l ` L) = {}
[PROOF STEP]
by auto


[STATEMENT]
lemma ground_comp: "ground\<^sub>l (l\<^sup>c) \<longleftrightarrow> ground\<^sub>l l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ground\<^sub>l (l\<^sup>c) = ground\<^sub>l l
[PROOF STEP]
by (cases l) auto


[STATEMENT]
lemma  ground_compls: "ground\<^sub>l\<^sub>s (L\<^sup>C) \<longleftrightarrow> ground\<^sub>l\<^sub>s L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ground\<^sub>l\<^sub>s (L\<^sup>C) = ground\<^sub>l\<^sub>s L
[PROOF STEP]
using ground_comp
[PROOF STATE]
proof (prove)
using this:
ground\<^sub>l (?l\<^sup>c) = ground\<^sub>l ?l

goal (1 subgoal):
 1. ground\<^sub>l\<^sub>s (L\<^sup>C) = ground\<^sub>l\<^sub>s L
[PROOF STEP]
by auto


[STATEMENT]
lemma ground_var_denott:
  assumes "ground\<^sub>t t"
  shows "eval\<^sub>t E F t = eval\<^sub>t E' F t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval\<^sub>t E F t = eval\<^sub>t E' F t
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
ground\<^sub>t t

goal (1 subgoal):
 1. eval\<^sub>t E F t = eval\<^sub>t E' F t
[PROOF STEP]
proof (induction t)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x1 x2a. \<lbrakk>\<And>x2aa. \<lbrakk>x2aa \<in> set x2a; ground\<^sub>t x2aa\<rbrakk> \<Longrightarrow> eval\<^sub>t E F x2aa = eval\<^sub>t E' F x2aa; ground\<^sub>t (Fun x1 x2a)\<rbrakk> \<Longrightarrow> eval\<^sub>t E F (Fun x1 x2a) = eval\<^sub>t E' F (Fun x1 x2a)
 2. \<And>x. ground\<^sub>t (Var x) \<Longrightarrow> eval\<^sub>t E F (Var x) = eval\<^sub>t E' F (Var x)
[PROOF STEP]
case (Var x)
[PROOF STATE]
proof (state)
this:
ground\<^sub>t (Var x)

goal (2 subgoals):
 1. \<And>x1 x2a. \<lbrakk>\<And>x2aa. \<lbrakk>x2aa \<in> set x2a; ground\<^sub>t x2aa\<rbrakk> \<Longrightarrow> eval\<^sub>t E F x2aa = eval\<^sub>t E' F x2aa; ground\<^sub>t (Fun x1 x2a)\<rbrakk> \<Longrightarrow> eval\<^sub>t E F (Fun x1 x2a) = eval\<^sub>t E' F (Fun x1 x2a)
 2. \<And>x. ground\<^sub>t (Var x) \<Longrightarrow> eval\<^sub>t E F (Var x) = eval\<^sub>t E' F (Var x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ground\<^sub>t (Var x)
[PROOF STEP]
have "False"
[PROOF STATE]
proof (prove)
using this:
ground\<^sub>t (Var x)

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

goal (2 subgoals):
 1. \<And>x1 x2a. \<lbrakk>\<And>x2aa. \<lbrakk>x2aa \<in> set x2a; ground\<^sub>t x2aa\<rbrakk> \<Longrightarrow> eval\<^sub>t E F x2aa = eval\<^sub>t E' F x2aa; ground\<^sub>t (Fun x1 x2a)\<rbrakk> \<Longrightarrow> eval\<^sub>t E F (Fun x1 x2a) = eval\<^sub>t E' F (Fun x1 x2a)
 2. \<And>x. ground\<^sub>t (Var x) \<Longrightarrow> eval\<^sub>t E F (Var x) = eval\<^sub>t E' F (Var x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
False
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
False

goal (1 subgoal):
 1. eval\<^sub>t E F (Var x) = eval\<^sub>t E' F (Var x)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
eval\<^sub>t E F (Var x) = eval\<^sub>t E' F (Var x)

goal (1 subgoal):
 1. \<And>x1 x2a. \<lbrakk>\<And>x2aa. \<lbrakk>x2aa \<in> set x2a; ground\<^sub>t x2aa\<rbrakk> \<Longrightarrow> eval\<^sub>t E F x2aa = eval\<^sub>t E' F x2aa; ground\<^sub>t (Fun x1 x2a)\<rbrakk> \<Longrightarrow> eval\<^sub>t E F (Fun x1 x2a) = eval\<^sub>t E' F (Fun x1 x2a)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x1 x2a. \<lbrakk>\<And>x2aa. \<lbrakk>x2aa \<in> set x2a; ground\<^sub>t x2aa\<rbrakk> \<Longrightarrow> eval\<^sub>t E F x2aa = eval\<^sub>t E' F x2aa; ground\<^sub>t (Fun x1 x2a)\<rbrakk> \<Longrightarrow> eval\<^sub>t E F (Fun x1 x2a) = eval\<^sub>t E' F (Fun x1 x2a)
[PROOF STEP]
case (Fun f ts)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?x2aa \<in> set ts; ground\<^sub>t ?x2aa\<rbrakk> \<Longrightarrow> eval\<^sub>t E F ?x2aa = eval\<^sub>t E' F ?x2aa
ground\<^sub>t (Fun f ts)

goal (1 subgoal):
 1. \<And>x1 x2a. \<lbrakk>\<And>x2aa. \<lbrakk>x2aa \<in> set x2a; ground\<^sub>t x2aa\<rbrakk> \<Longrightarrow> eval\<^sub>t E F x2aa = eval\<^sub>t E' F x2aa; ground\<^sub>t (Fun x1 x2a)\<rbrakk> \<Longrightarrow> eval\<^sub>t E F (Fun x1 x2a) = eval\<^sub>t E' F (Fun x1 x2a)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?x2aa \<in> set ts; ground\<^sub>t ?x2aa\<rbrakk> \<Longrightarrow> eval\<^sub>t E F ?x2aa = eval\<^sub>t E' F ?x2aa
ground\<^sub>t (Fun f ts)
[PROOF STEP]
have "\<forall>t \<in> set ts. ground\<^sub>t t"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x2aa \<in> set ts; ground\<^sub>t ?x2aa\<rbrakk> \<Longrightarrow> eval\<^sub>t E F ?x2aa = eval\<^sub>t E' F ?x2aa
ground\<^sub>t (Fun f ts)

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

goal (1 subgoal):
 1. \<And>x1 x2a. \<lbrakk>\<And>x2aa. \<lbrakk>x2aa \<in> set x2a; ground\<^sub>t x2aa\<rbrakk> \<Longrightarrow> eval\<^sub>t E F x2aa = eval\<^sub>t E' F x2aa; ground\<^sub>t (Fun x1 x2a)\<rbrakk> \<Longrightarrow> eval\<^sub>t E F (Fun x1 x2a) = eval\<^sub>t E' F (Fun x1 x2a)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ground\<^sub>t\<^sub>s ts
[PROOF STEP]
have "\<forall>t \<in> set ts. eval\<^sub>t E F t = eval\<^sub>t E' F t"
[PROOF STATE]
proof (prove)
using this:
ground\<^sub>t\<^sub>s ts

goal (1 subgoal):
 1. \<forall>t\<in>set ts. eval\<^sub>t E F t = eval\<^sub>t E' F t
[PROOF STEP]
using Fun
[PROOF STATE]
proof (prove)
using this:
ground\<^sub>t\<^sub>s ts
\<lbrakk>?x2aa \<in> set ts; ground\<^sub>t ?x2aa\<rbrakk> \<Longrightarrow> eval\<^sub>t E F ?x2aa = eval\<^sub>t E' F ?x2aa
ground\<^sub>t (Fun f ts)

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

goal (1 subgoal):
 1. \<And>x1 x2a. \<lbrakk>\<And>x2aa. \<lbrakk>x2aa \<in> set x2a; ground\<^sub>t x2aa\<rbrakk> \<Longrightarrow> eval\<^sub>t E F x2aa = eval\<^sub>t E' F x2aa; ground\<^sub>t (Fun x1 x2a)\<rbrakk> \<Longrightarrow> eval\<^sub>t E F (Fun x1 x2a) = eval\<^sub>t E' F (Fun x1 x2a)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>t\<in>set ts. eval\<^sub>t E F t = eval\<^sub>t E' F t
[PROOF STEP]
have "eval\<^sub>t\<^sub>s E F ts = eval\<^sub>t\<^sub>s E' F ts"
[PROOF STATE]
proof (prove)
using this:
\<forall>t\<in>set ts. eval\<^sub>t E F t = eval\<^sub>t E' F t

goal (1 subgoal):
 1. eval\<^sub>t\<^sub>s E F ts = eval\<^sub>t\<^sub>s E' F ts
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
eval\<^sub>t\<^sub>s E F ts = eval\<^sub>t\<^sub>s E' F ts

goal (1 subgoal):
 1. \<And>x1 x2a. \<lbrakk>\<And>x2aa. \<lbrakk>x2aa \<in> set x2a; ground\<^sub>t x2aa\<rbrakk> \<Longrightarrow> eval\<^sub>t E F x2aa = eval\<^sub>t E' F x2aa; ground\<^sub>t (Fun x1 x2a)\<rbrakk> \<Longrightarrow> eval\<^sub>t E F (Fun x1 x2a) = eval\<^sub>t E' F (Fun x1 x2a)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
eval\<^sub>t\<^sub>s E F ts = eval\<^sub>t\<^sub>s E' F ts
[PROOF STEP]
have "F f (map (eval\<^sub>t E F) ts) = F f (map (eval\<^sub>t E' F) ts)"
[PROOF STATE]
proof (prove)
using this:
eval\<^sub>t\<^sub>s E F ts = eval\<^sub>t\<^sub>s E' F ts

goal (1 subgoal):
 1. F f (eval\<^sub>t\<^sub>s E F ts) = F f (eval\<^sub>t\<^sub>s E' F ts)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
F f (eval\<^sub>t\<^sub>s E F ts) = F f (eval\<^sub>t\<^sub>s E' F ts)

goal (1 subgoal):
 1. \<And>x1 x2a. \<lbrakk>\<And>x2aa. \<lbrakk>x2aa \<in> set x2a; ground\<^sub>t x2aa\<rbrakk> \<Longrightarrow> eval\<^sub>t E F x2aa = eval\<^sub>t E' F x2aa; ground\<^sub>t (Fun x1 x2a)\<rbrakk> \<Longrightarrow> eval\<^sub>t E F (Fun x1 x2a) = eval\<^sub>t E' F (Fun x1 x2a)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
F f (eval\<^sub>t\<^sub>s E F ts) = F f (eval\<^sub>t\<^sub>s E' F ts)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
F f (eval\<^sub>t\<^sub>s E F ts) = F f (eval\<^sub>t\<^sub>s E' F ts)

goal (1 subgoal):
 1. eval\<^sub>t E F (Fun f ts) = eval\<^sub>t E' F (Fun f ts)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
eval\<^sub>t E F (Fun f ts) = eval\<^sub>t E' F (Fun f ts)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ground_var_denotts:
  assumes "ground\<^sub>t\<^sub>s ts"
  shows "eval\<^sub>t\<^sub>s E F ts = eval\<^sub>t\<^sub>s E' F ts"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval\<^sub>t\<^sub>s E F ts = eval\<^sub>t\<^sub>s E' F ts
[PROOF STEP]
using assms ground_var_denott
[PROOF STATE]
proof (prove)
using this:
ground\<^sub>t\<^sub>s ts
ground\<^sub>t ?t \<Longrightarrow> eval\<^sub>t ?E ?F ?t = eval\<^sub>t ?E' ?F ?t

goal (1 subgoal):
 1. eval\<^sub>t\<^sub>s E F ts = eval\<^sub>t\<^sub>s E' F ts
[PROOF STEP]
by (metis map_eq_conv)


[STATEMENT]
lemma ground_var_denot:
  assumes "ground\<^sub>l l"
  shows "eval\<^sub>l E F G l = eval\<^sub>l E' F G l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval\<^sub>l E F G l = eval\<^sub>l E' F G l
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
ground\<^sub>l l

goal (1 subgoal):
 1. eval\<^sub>l E F G l = eval\<^sub>l E' F G l
[PROOF STEP]
proof (induction l)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x1 x2. ground\<^sub>l (Pos x1 x2) \<Longrightarrow> eval\<^sub>l E F G (Pos x1 x2) = eval\<^sub>l E' F G (Pos x1 x2)
 2. \<And>x1 x2. ground\<^sub>l (Neg x1 x2) \<Longrightarrow> eval\<^sub>l E F G (Neg x1 x2) = eval\<^sub>l E' F G (Neg x1 x2)
[PROOF STEP]
case Pos
[PROOF STATE]
proof (state)
this:
ground\<^sub>l (Pos x1_ x2_)

goal (2 subgoals):
 1. \<And>x1 x2. ground\<^sub>l (Pos x1 x2) \<Longrightarrow> eval\<^sub>l E F G (Pos x1 x2) = eval\<^sub>l E' F G (Pos x1 x2)
 2. \<And>x1 x2. ground\<^sub>l (Neg x1 x2) \<Longrightarrow> eval\<^sub>l E F G (Neg x1 x2) = eval\<^sub>l E' F G (Neg x1 x2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ground\<^sub>l (Pos x1_ x2_)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
ground\<^sub>l (Pos x1_ x2_)

goal (1 subgoal):
 1. eval\<^sub>l E F G (Pos x1_ x2_) = eval\<^sub>l E' F G (Pos x1_ x2_)
[PROOF STEP]
using ground_var_denotts
[PROOF STATE]
proof (prove)
using this:
ground\<^sub>l (Pos x1_ x2_)
ground\<^sub>t\<^sub>s ?ts \<Longrightarrow> eval\<^sub>t\<^sub>s ?E ?F ?ts = eval\<^sub>t\<^sub>s ?E' ?F ?ts

goal (1 subgoal):
 1. eval\<^sub>l E F G (Pos x1_ x2_) = eval\<^sub>l E' F G (Pos x1_ x2_)
[PROOF STEP]
by (metis eval\<^sub>l.simps(1) literal.sel(3))
[PROOF STATE]
proof (state)
this:
eval\<^sub>l E F G (Pos x1_ x2_) = eval\<^sub>l E' F G (Pos x1_ x2_)

goal (1 subgoal):
 1. \<And>x1 x2. ground\<^sub>l (Neg x1 x2) \<Longrightarrow> eval\<^sub>l E F G (Neg x1 x2) = eval\<^sub>l E' F G (Neg x1 x2)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x1 x2. ground\<^sub>l (Neg x1 x2) \<Longrightarrow> eval\<^sub>l E F G (Neg x1 x2) = eval\<^sub>l E' F G (Neg x1 x2)
[PROOF STEP]
case Neg
[PROOF STATE]
proof (state)
this:
ground\<^sub>l (Neg x1_ x2_)

goal (1 subgoal):
 1. \<And>x1 x2. ground\<^sub>l (Neg x1 x2) \<Longrightarrow> eval\<^sub>l E F G (Neg x1 x2) = eval\<^sub>l E' F G (Neg x1 x2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ground\<^sub>l (Neg x1_ x2_)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
ground\<^sub>l (Neg x1_ x2_)

goal (1 subgoal):
 1. eval\<^sub>l E F G (Neg x1_ x2_) = eval\<^sub>l E' F G (Neg x1_ x2_)
[PROOF STEP]
using ground_var_denotts
[PROOF STATE]
proof (prove)
using this:
ground\<^sub>l (Neg x1_ x2_)
ground\<^sub>t\<^sub>s ?ts \<Longrightarrow> eval\<^sub>t\<^sub>s ?E ?F ?ts = eval\<^sub>t\<^sub>s ?E' ?F ?ts

goal (1 subgoal):
 1. eval\<^sub>l E F G (Neg x1_ x2_) = eval\<^sub>l E' F G (Neg x1_ x2_)
[PROOF STEP]
by (metis eval\<^sub>l.simps(2) literal.sel(4))
[PROOF STATE]
proof (state)
this:
eval\<^sub>l E F G (Neg x1_ x2_) = eval\<^sub>l E' F G (Neg x1_ x2_)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma subls_def2: "L \<cdot>\<^sub>l\<^sub>s \<sigma> = {l \<cdot>\<^sub>l \<sigma>|l. l \<in> L}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. L \<cdot>\<^sub>l\<^sub>s \<sigma> = {l \<cdot>\<^sub>l \<sigma> |l. l \<in> L}
[PROOF STEP]
by auto


[STATEMENT]
lemma comp_sub: "(l\<^sup>c) \<cdot>\<^sub>l \<sigma>=(l \<cdot>\<^sub>l \<sigma>)\<^sup>c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l\<^sup>c \<cdot>\<^sub>l \<sigma> = (l \<cdot>\<^sub>l \<sigma>)\<^sup>c
[PROOF STEP]
by (cases l) auto


[STATEMENT]
lemma compls_subls: "(L\<^sup>C) \<cdot>\<^sub>l\<^sub>s \<sigma>=(L \<cdot>\<^sub>l\<^sub>s \<sigma>)\<^sup>C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. L\<^sup>C \<cdot>\<^sub>l\<^sub>s \<sigma> = (L \<cdot>\<^sub>l\<^sub>s \<sigma>)\<^sup>C
[PROOF STEP]
using comp_sub
[PROOF STATE]
proof (prove)
using this:
?l\<^sup>c \<cdot>\<^sub>l ?\<sigma> = (?l \<cdot>\<^sub>l ?\<sigma>)\<^sup>c

goal (1 subgoal):
 1. L\<^sup>C \<cdot>\<^sub>l\<^sub>s \<sigma> = (L \<cdot>\<^sub>l\<^sub>s \<sigma>)\<^sup>C
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>l. \<lbrakk>\<And>l \<sigma>. l\<^sup>c \<cdot>\<^sub>l \<sigma> = (l \<cdot>\<^sub>l \<sigma>)\<^sup>c; l \<in> L\<rbrakk> \<Longrightarrow> (l \<cdot>\<^sub>l \<sigma>)\<^sup>c \<in> L\<^sup>C \<cdot>\<^sub>l\<^sub>s \<sigma>
[PROOF STEP]
apply (metis image_eqI)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma subls_union: "(L\<^sub>1 \<union> L\<^sub>2) \<cdot>\<^sub>l\<^sub>s \<sigma> = (L\<^sub>1 \<cdot>\<^sub>l\<^sub>s \<sigma>) \<union> (L\<^sub>2 \<cdot>\<^sub>l\<^sub>s \<sigma>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. L\<^sub>1 \<union> L\<^sub>2 \<cdot>\<^sub>l\<^sub>s \<sigma> = (L\<^sub>1 \<cdot>\<^sub>l\<^sub>s \<sigma>) \<union> (L\<^sub>2 \<cdot>\<^sub>l\<^sub>s \<sigma>)
[PROOF STEP]
by auto


[STATEMENT]
lemma empty_subt: "(t :: fterm) \<cdot>\<^sub>t \<epsilon> = t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t \<cdot>\<^sub>t \<epsilon> = t
[PROOF STEP]
by (induction t) (auto simp add: map_idI)


[STATEMENT]
lemma empty_subts: "ts \<cdot>\<^sub>t\<^sub>s \<epsilon> = ts"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ts \<cdot>\<^sub>t\<^sub>s \<epsilon> = ts
[PROOF STEP]
using empty_subt
[PROOF STATE]
proof (prove)
using this:
?t \<cdot>\<^sub>t \<epsilon> = ?t

goal (1 subgoal):
 1. ts \<cdot>\<^sub>t\<^sub>s \<epsilon> = ts
[PROOF STEP]
by auto


[STATEMENT]
lemma empty_subl: "l \<cdot>\<^sub>l \<epsilon> = l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l \<cdot>\<^sub>l \<epsilon> = l
[PROOF STEP]
using empty_subts
[PROOF STATE]
proof (prove)
using this:
?ts \<cdot>\<^sub>t\<^sub>s \<epsilon> = ?ts

goal (1 subgoal):
 1. l \<cdot>\<^sub>l \<epsilon> = l
[PROOF STEP]
by (cases l) auto


[STATEMENT]
lemma empty_subls: "L \<cdot>\<^sub>l\<^sub>s \<epsilon> = L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. L \<cdot>\<^sub>l\<^sub>s \<epsilon> = L
[PROOF STEP]
using empty_subl
[PROOF STATE]
proof (prove)
using this:
?l \<cdot>\<^sub>l \<epsilon> = ?l

goal (1 subgoal):
 1. L \<cdot>\<^sub>l\<^sub>s \<epsilon> = L
[PROOF STEP]
by auto


[STATEMENT]
lemma instance_of\<^sub>t_self: "instance_of\<^sub>t t t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. instance_of\<^sub>t t t
[PROOF STEP]
unfolding instance_of\<^sub>t_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>\<sigma>. t = t \<cdot>\<^sub>t \<sigma>
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. t = t \<cdot>\<^sub>t ?\<sigma>
[PROOF STEP]
show "t = t \<cdot>\<^sub>t \<epsilon>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t = t \<cdot>\<^sub>t \<epsilon>
[PROOF STEP]
using empty_subt
[PROOF STATE]
proof (prove)
using this:
?t \<cdot>\<^sub>t \<epsilon> = ?t

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma instance_of\<^sub>t\<^sub>s_self: "instance_of\<^sub>t\<^sub>s ts ts"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. instance_of\<^sub>t\<^sub>s ts ts
[PROOF STEP]
unfolding instance_of\<^sub>t\<^sub>s_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>\<sigma>. ts = ts \<cdot>\<^sub>t\<^sub>s \<sigma>
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ts = ts \<cdot>\<^sub>t\<^sub>s ?\<sigma>
[PROOF STEP]
show "ts = ts \<cdot>\<^sub>t\<^sub>s \<epsilon>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ts = ts \<cdot>\<^sub>t\<^sub>s \<epsilon>
[PROOF STEP]
using empty_subts
[PROOF STATE]
proof (prove)
using this:
?ts \<cdot>\<^sub>t\<^sub>s \<epsilon> = ?ts

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma instance_of\<^sub>l_self: "instance_of\<^sub>l l l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. instance_of\<^sub>l l l
[PROOF STEP]
unfolding instance_of\<^sub>l_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>\<sigma>. l = l \<cdot>\<^sub>l \<sigma>
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. l = l \<cdot>\<^sub>l ?\<sigma>
[PROOF STEP]
show "l = l \<cdot>\<^sub>l \<epsilon>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l = l \<cdot>\<^sub>l \<epsilon>
[PROOF STEP]
using empty_subl
[PROOF STATE]
proof (prove)
using this:
?l \<cdot>\<^sub>l \<epsilon> = ?l

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma instance_of\<^sub>l\<^sub>s_self: "instance_of\<^sub>l\<^sub>s L L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. instance_of\<^sub>l\<^sub>s L L
[PROOF STEP]
unfolding instance_of\<^sub>l\<^sub>s_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>\<sigma>. L = L \<cdot>\<^sub>l\<^sub>s \<sigma>
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. L = L \<cdot>\<^sub>l\<^sub>s ?\<sigma>
[PROOF STEP]
show "L = L \<cdot>\<^sub>l\<^sub>s \<epsilon>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. L = L \<cdot>\<^sub>l\<^sub>s \<epsilon>
[PROOF STEP]
using empty_subls
[PROOF STATE]
proof (prove)
using this:
?L \<cdot>\<^sub>l\<^sub>s \<epsilon> = ?L

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ground_sub:
  assumes "ground\<^sub>t t"
  shows "t \<cdot>\<^sub>t \<sigma> = t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t \<cdot>\<^sub>t \<sigma> = t
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
ground\<^sub>t t

goal (1 subgoal):
 1. t \<cdot>\<^sub>t \<sigma> = t
[PROOF STEP]
by (induction t) (auto simp add: map_idI)


[STATEMENT]
lemma ground_subs:
  assumes "ground\<^sub>t\<^sub>s ts "
  shows " ts \<cdot>\<^sub>t\<^sub>s \<sigma> = ts"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ts \<cdot>\<^sub>t\<^sub>s \<sigma> = ts
[PROOF STEP]
using assms ground_sub
[PROOF STATE]
proof (prove)
using this:
ground\<^sub>t\<^sub>s ts
ground\<^sub>t ?t \<Longrightarrow> ?t \<cdot>\<^sub>t ?\<sigma> = ?t

goal (1 subgoal):
 1. ts \<cdot>\<^sub>t\<^sub>s \<sigma> = ts
[PROOF STEP]
by (simp add: map_idI)


[STATEMENT]
lemma ground\<^sub>l_subs:
  assumes "ground\<^sub>l l "
  shows " l \<cdot>\<^sub>l \<sigma> = l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l \<cdot>\<^sub>l \<sigma> = l
[PROOF STEP]
using assms ground_subs
[PROOF STATE]
proof (prove)
using this:
ground\<^sub>l l
ground\<^sub>t\<^sub>s ?ts \<Longrightarrow> ?ts \<cdot>\<^sub>t\<^sub>s ?\<sigma> = ?ts

goal (1 subgoal):
 1. l \<cdot>\<^sub>l \<sigma> = l
[PROOF STEP]
by (cases l) auto


[STATEMENT]
lemma ground\<^sub>l\<^sub>s_subls:
  assumes ground: "ground\<^sub>l\<^sub>s L"
  shows "L \<cdot>\<^sub>l\<^sub>s \<sigma> = L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. L \<cdot>\<^sub>l\<^sub>s \<sigma> = L
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. L \<cdot>\<^sub>l\<^sub>s \<sigma> = L
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. L \<cdot>\<^sub>l\<^sub>s \<sigma> = L
[PROOF STEP]
fix l
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. L \<cdot>\<^sub>l\<^sub>s \<sigma> = L
[PROOF STEP]
assume l_L: "l \<in> L"
[PROOF STATE]
proof (state)
this:
l \<in> L

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

goal (1 subgoal):
 1. ground\<^sub>l l
[PROOF STEP]
using ground
[PROOF STATE]
proof (prove)
using this:
l \<in> L
ground\<^sub>l\<^sub>s L

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

goal (1 subgoal):
 1. L \<cdot>\<^sub>l\<^sub>s \<sigma> = L
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ground\<^sub>l l
[PROOF STEP]
have "l = l \<cdot>\<^sub>l \<sigma>"
[PROOF STATE]
proof (prove)
using this:
ground\<^sub>l l

goal (1 subgoal):
 1. l = l \<cdot>\<^sub>l \<sigma>
[PROOF STEP]
using ground\<^sub>l_subs
[PROOF STATE]
proof (prove)
using this:
ground\<^sub>l l
ground\<^sub>l ?l \<Longrightarrow> ?l \<cdot>\<^sub>l ?\<sigma> = ?l

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

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

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

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

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

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

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

goal (1 subgoal):
 1. L \<cdot>\<^sub>l\<^sub>s \<sigma> = L
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?l2 \<in> L \<Longrightarrow> ?l2 \<in> L \<cdot>\<^sub>l\<^sub>s \<sigma>

goal (1 subgoal):
 1. L \<cdot>\<^sub>l\<^sub>s \<sigma> = L
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
?l2 \<in> L \<Longrightarrow> ?l2 \<in> L \<cdot>\<^sub>l\<^sub>s \<sigma>

goal (1 subgoal):
 1. L \<cdot>\<^sub>l\<^sub>s \<sigma> = L
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
?l2 \<in> L \<Longrightarrow> ?l2 \<in> L \<cdot>\<^sub>l\<^sub>s \<sigma>

goal (1 subgoal):
 1. L \<cdot>\<^sub>l\<^sub>s \<sigma> = L
[PROOF STEP]
fix l
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. L \<cdot>\<^sub>l\<^sub>s \<sigma> = L
[PROOF STEP]
assume l_L: "l \<in> L \<cdot>\<^sub>l\<^sub>s \<sigma>"
[PROOF STATE]
proof (state)
this:
l \<in> L \<cdot>\<^sub>l\<^sub>s \<sigma>

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

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

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

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

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

goal (1 subgoal):
 1. L \<cdot>\<^sub>l\<^sub>s \<sigma> = L
[PROOF STEP]
from l_L l'_p this
[PROOF STATE]
proof (chain)
picking this:
l \<in> L \<cdot>\<^sub>l\<^sub>s \<sigma>
l' \<in> L \<and> l' \<cdot>\<^sub>l \<sigma> = l
l' = l
[PROOF STEP]
have "l \<in> L"
[PROOF STATE]
proof (prove)
using this:
l \<in> L \<cdot>\<^sub>l\<^sub>s \<sigma>
l' \<in> L \<and> l' \<cdot>\<^sub>l \<sigma> = l
l' = l

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

goal (1 subgoal):
 1. L \<cdot>\<^sub>l\<^sub>s \<sigma> = L
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?l2 \<in> L \<cdot>\<^sub>l\<^sub>s \<sigma> \<Longrightarrow> ?l2 \<in> L

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma composition_conseq2t:  "(t \<cdot>\<^sub>t \<sigma>\<^sub>1) \<cdot>\<^sub>t \<sigma>\<^sub>2 = t \<cdot>\<^sub>t (\<sigma>\<^sub>1 \<cdot> \<sigma>\<^sub>2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t \<cdot>\<^sub>t \<sigma>\<^sub>1 \<cdot>\<^sub>t \<sigma>\<^sub>2 = t \<cdot>\<^sub>t (\<sigma>\<^sub>1 \<cdot> \<sigma>\<^sub>2)
[PROOF STEP]
proof (induction t)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x1 x2a. (\<And>x2aa. x2aa \<in> set x2a \<Longrightarrow> x2aa \<cdot>\<^sub>t \<sigma>\<^sub>1 \<cdot>\<^sub>t \<sigma>\<^sub>2 = x2aa \<cdot>\<^sub>t (\<sigma>\<^sub>1 \<cdot> \<sigma>\<^sub>2)) \<Longrightarrow> Fun x1 x2a \<cdot>\<^sub>t \<sigma>\<^sub>1 \<cdot>\<^sub>t \<sigma>\<^sub>2 = Fun x1 x2a \<cdot>\<^sub>t (\<sigma>\<^sub>1 \<cdot> \<sigma>\<^sub>2)
 2. \<And>x. \<epsilon> x \<cdot>\<^sub>t \<sigma>\<^sub>1 \<cdot>\<^sub>t \<sigma>\<^sub>2 = \<epsilon> x \<cdot>\<^sub>t (\<sigma>\<^sub>1 \<cdot> \<sigma>\<^sub>2)
[PROOF STEP]
case (Var x)
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. \<And>x1 x2a. (\<And>x2aa. x2aa \<in> set x2a \<Longrightarrow> x2aa \<cdot>\<^sub>t \<sigma>\<^sub>1 \<cdot>\<^sub>t \<sigma>\<^sub>2 = x2aa \<cdot>\<^sub>t (\<sigma>\<^sub>1 \<cdot> \<sigma>\<^sub>2)) \<Longrightarrow> Fun x1 x2a \<cdot>\<^sub>t \<sigma>\<^sub>1 \<cdot>\<^sub>t \<sigma>\<^sub>2 = Fun x1 x2a \<cdot>\<^sub>t (\<sigma>\<^sub>1 \<cdot> \<sigma>\<^sub>2)
 2. \<And>x. \<epsilon> x \<cdot>\<^sub>t \<sigma>\<^sub>1 \<cdot>\<^sub>t \<sigma>\<^sub>2 = \<epsilon> x \<cdot>\<^sub>t (\<sigma>\<^sub>1 \<cdot> \<sigma>\<^sub>2)
[PROOF STEP]
have "((Var x) \<cdot>\<^sub>t \<sigma>\<^sub>1) \<cdot>\<^sub>t \<sigma>\<^sub>2 = (\<sigma>\<^sub>1 x) \<cdot>\<^sub>t \<sigma>\<^sub>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<epsilon> x \<cdot>\<^sub>t \<sigma>\<^sub>1 \<cdot>\<^sub>t \<sigma>\<^sub>2 = \<sigma>\<^sub>1 x \<cdot>\<^sub>t \<sigma>\<^sub>2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<epsilon> x \<cdot>\<^sub>t \<sigma>\<^sub>1 \<cdot>\<^sub>t \<sigma>\<^sub>2 = \<sigma>\<^sub>1 x \<cdot>\<^sub>t \<sigma>\<^sub>2

goal (2 subgoals):
 1. \<And>x1 x2a. (\<And>x2aa. x2aa \<in> set x2a \<Longrightarrow> x2aa \<cdot>\<^sub>t \<sigma>\<^sub>1 \<cdot>\<^sub>t \<sigma>\<^sub>2 = x2aa \<cdot>\<^sub>t (\<sigma>\<^sub>1 \<cdot> \<sigma>\<^sub>2)) \<Longrightarrow> Fun x1 x2a \<cdot>\<^sub>t \<sigma>\<^sub>1 \<cdot>\<^sub>t \<sigma>\<^sub>2 = Fun x1 x2a \<cdot>\<^sub>t (\<sigma>\<^sub>1 \<cdot> \<sigma>\<^sub>2)
 2. \<And>x. \<epsilon> x \<cdot>\<^sub>t \<sigma>\<^sub>1 \<cdot>\<^sub>t \<sigma>\<^sub>2 = \<epsilon> x \<cdot>\<^sub>t (\<sigma>\<^sub>1 \<cdot> \<sigma>\<^sub>2)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<epsilon> x \<cdot>\<^sub>t \<sigma>\<^sub>1 \<cdot>\<^sub>t \<sigma>\<^sub>2 = \<sigma>\<^sub>1 x \<cdot>\<^sub>t \<sigma>\<^sub>2

goal (2 subgoals):
 1. \<And>x1 x2a. (\<And>x2aa. x2aa \<in> set x2a \<Longrightarrow> x2aa \<cdot>\<^sub>t \<sigma>\<^sub>1 \<cdot>\<^sub>t \<sigma>\<^sub>2 = x2aa \<cdot>\<^sub>t (\<sigma>\<^sub>1 \<cdot> \<sigma>\<^sub>2)) \<Longrightarrow> Fun x1 x2a \<cdot>\<^sub>t \<sigma>\<^sub>1 \<cdot>\<^sub>t \<sigma>\<^sub>2 = Fun x1 x2a \<cdot>\<^sub>t (\<sigma>\<^sub>1 \<cdot> \<sigma>\<^sub>2)
 2. \<And>x. \<epsilon> x \<cdot>\<^sub>t \<sigma>\<^sub>1 \<cdot>\<^sub>t \<sigma>\<^sub>2 = \<epsilon> x \<cdot>\<^sub>t (\<sigma>\<^sub>1 \<cdot> \<sigma>\<^sub>2)
[PROOF STEP]
have " ... = (\<sigma>\<^sub>1 \<cdot> \<sigma>\<^sub>2) x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<sigma>\<^sub>1 x \<cdot>\<^sub>t \<sigma>\<^sub>2 = (\<sigma>\<^sub>1 \<cdot> \<sigma>\<^sub>2) x
[PROOF STEP]
unfolding composition_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<sigma>\<^sub>1 x \<cdot>\<^sub>t \<sigma>\<^sub>2 = \<sigma>\<^sub>1 x \<cdot>\<^sub>t \<sigma>\<^sub>2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<sigma>\<^sub>1 x \<cdot>\<^sub>t \<sigma>\<^sub>2 = (\<sigma>\<^sub>1 \<cdot> \<sigma>\<^sub>2) x

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

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

goal (1 subgoal):
 1. \<And>x1 x2a. (\<And>x2aa. x2aa \<in> set x2a \<Longrightarrow> x2aa \<cdot>\<^sub>t \<sigma>\<^sub>1 \<cdot>\<^sub>t \<sigma>\<^sub>2 = x2aa \<cdot>\<^sub>t (\<sigma>\<^sub>1 \<cdot> \<sigma>\<^sub>2)) \<Longrightarrow> Fun x1 x2a \<cdot>\<^sub>t \<sigma>\<^sub>1 \<cdot>\<^sub>t \<sigma>\<^sub>2 = Fun x1 x2a \<cdot>\<^sub>t (\<sigma>\<^sub>1 \<cdot> \<sigma>\<^sub>2)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x1 x2a. (\<And>x2aa. x2aa \<in> set x2a \<Longrightarrow> x2aa \<cdot>\<^sub>t \<sigma>\<^sub>1 \<cdot>\<^sub>t \<sigma>\<^sub>2 = x2aa \<cdot>\<^sub>t (\<sigma>\<^sub>1 \<cdot> \<sigma>\<^sub>2)) \<Longrightarrow> Fun x1 x2a \<cdot>\<^sub>t \<sigma>\<^sub>1 \<cdot>\<^sub>t \<sigma>\<^sub>2 = Fun x1 x2a \<cdot>\<^sub>t (\<sigma>\<^sub>1 \<cdot> \<sigma>\<^sub>2)
[PROOF STEP]
case (Fun t ts)
[PROOF STATE]
proof (state)
this:
?x2aa \<in> set ts \<Longrightarrow> ?x2aa \<cdot>\<^sub>t \<sigma>\<^sub>1 \<cdot>\<^sub>t \<sigma>\<^sub>2 = ?x2aa \<cdot>\<^sub>t (\<sigma>\<^sub>1 \<cdot> \<sigma>\<^sub>2)

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

goal (1 subgoal):
 1. Fun t ts \<cdot>\<^sub>t \<sigma>\<^sub>1 \<cdot>\<^sub>t \<sigma>\<^sub>2 = Fun t ts \<cdot>\<^sub>t (\<sigma>\<^sub>1 \<cdot> \<sigma>\<^sub>2)
[PROOF STEP]
unfolding composition_def
[PROOF STATE]
proof (prove)
using this:
?x2aa \<in> set ts \<Longrightarrow> ?x2aa \<cdot>\<^sub>t \<sigma>\<^sub>1 \<cdot>\<^sub>t \<sigma>\<^sub>2 = ?x2aa \<cdot>\<^sub>t (\<lambda>a. \<sigma>\<^sub>1 a \<cdot>\<^sub>t \<sigma>\<^sub>2)

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma composition_conseq2ts: "(ts \<cdot>\<^sub>t\<^sub>s \<sigma>\<^sub>1) \<cdot>\<^sub>t\<^sub>s \<sigma>\<^sub>2 = ts \<cdot>\<^sub>t\<^sub>s (\<sigma>\<^sub>1 \<cdot> \<sigma>\<^sub>2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ts \<cdot>\<^sub>t\<^sub>s \<sigma>\<^sub>1 \<cdot>\<^sub>t\<^sub>s \<sigma>\<^sub>2 = ts \<cdot>\<^sub>t\<^sub>s (\<sigma>\<^sub>1 \<cdot> \<sigma>\<^sub>2)
[PROOF STEP]
using composition_conseq2t
[PROOF STATE]
proof (prove)
using this:
?t \<cdot>\<^sub>t ?\<sigma>\<^sub>1 \<cdot>\<^sub>t ?\<sigma>\<^sub>2 = ?t \<cdot>\<^sub>t (?\<sigma>\<^sub>1 \<cdot> ?\<sigma>\<^sub>2)

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


[STATEMENT]
lemma composition_conseq2l: "(l \<cdot>\<^sub>l \<sigma>\<^sub>1) \<cdot>\<^sub>l \<sigma>\<^sub>2 = l \<cdot>\<^sub>l (\<sigma>\<^sub>1 \<cdot> \<sigma>\<^sub>2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l \<cdot>\<^sub>l \<sigma>\<^sub>1 \<cdot>\<^sub>l \<sigma>\<^sub>2 = l \<cdot>\<^sub>l (\<sigma>\<^sub>1 \<cdot> \<sigma>\<^sub>2)
[PROOF STEP]
using composition_conseq2t
[PROOF STATE]
proof (prove)
using this:
?t \<cdot>\<^sub>t ?\<sigma>\<^sub>1 \<cdot>\<^sub>t ?\<sigma>\<^sub>2 = ?t \<cdot>\<^sub>t (?\<sigma>\<^sub>1 \<cdot> ?\<sigma>\<^sub>2)

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


[STATEMENT]
lemma composition_assoc: "\<sigma>\<^sub>1 \<cdot> (\<sigma>\<^sub>2 \<cdot> \<sigma>\<^sub>3) = (\<sigma>\<^sub>1 \<cdot> \<sigma>\<^sub>2) \<cdot> \<sigma>\<^sub>3"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<sigma>\<^sub>1 \<cdot> (\<sigma>\<^sub>2 \<cdot> \<sigma>\<^sub>3) = \<sigma>\<^sub>1 \<cdot> \<sigma>\<^sub>2 \<cdot> \<sigma>\<^sub>3
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. (\<sigma>\<^sub>1 \<cdot> (\<sigma>\<^sub>2 \<cdot> \<sigma>\<^sub>3)) x = (\<sigma>\<^sub>1 \<cdot> \<sigma>\<^sub>2 \<cdot> \<sigma>\<^sub>3) x
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. (\<sigma>\<^sub>1 \<cdot> (\<sigma>\<^sub>2 \<cdot> \<sigma>\<^sub>3)) x = (\<sigma>\<^sub>1 \<cdot> \<sigma>\<^sub>2 \<cdot> \<sigma>\<^sub>3) x
[PROOF STEP]
show "(\<sigma>\<^sub>1 \<cdot> (\<sigma>\<^sub>2 \<cdot> \<sigma>\<^sub>3)) x = ((\<sigma>\<^sub>1 \<cdot> \<sigma>\<^sub>2) \<cdot> \<sigma>\<^sub>3) x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<sigma>\<^sub>1 \<cdot> (\<sigma>\<^sub>2 \<cdot> \<sigma>\<^sub>3)) x = (\<sigma>\<^sub>1 \<cdot> \<sigma>\<^sub>2 \<cdot> \<sigma>\<^sub>3) x
[PROOF STEP]
by (simp only: composition_def composition_conseq2t)
[PROOF STATE]
proof (state)
this:
(\<sigma>\<^sub>1 \<cdot> (\<sigma>\<^sub>2 \<cdot> \<sigma>\<^sub>3)) x = (\<sigma>\<^sub>1 \<cdot> \<sigma>\<^sub>2 \<cdot> \<sigma>\<^sub>3) x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma empty_comp1: "(\<sigma> \<cdot> \<epsilon>) = \<sigma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<sigma> \<cdot> \<epsilon> = \<sigma>
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. (\<sigma> \<cdot> \<epsilon>) x = \<sigma> x
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. (\<sigma> \<cdot> \<epsilon>) x = \<sigma> x
[PROOF STEP]
show "(\<sigma> \<cdot> \<epsilon>) x = \<sigma> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<sigma> \<cdot> \<epsilon>) x = \<sigma> x
[PROOF STEP]
unfolding composition_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<sigma> x \<cdot>\<^sub>t \<epsilon> = \<sigma> x
[PROOF STEP]
using empty_subt
[PROOF STATE]
proof (prove)
using this:
?t \<cdot>\<^sub>t \<epsilon> = ?t

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma empty_comp2: "(\<epsilon> \<cdot> \<sigma>) = \<sigma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<epsilon> \<cdot> \<sigma> = \<sigma>
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. (\<epsilon> \<cdot> \<sigma>) x = \<sigma> x
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. (\<epsilon> \<cdot> \<sigma>) x = \<sigma> x
[PROOF STEP]
show "(\<epsilon> \<cdot> \<sigma>) x = \<sigma> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<epsilon> \<cdot> \<sigma>) x = \<sigma> x
[PROOF STEP]
unfolding composition_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<epsilon> x \<cdot>\<^sub>t \<sigma> = \<sigma> x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<epsilon> \<cdot> \<sigma>) x = \<sigma> x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma instance_of\<^sub>t_trans :
  assumes t\<^sub>1\<^sub>2: "instance_of\<^sub>t t\<^sub>1 t\<^sub>2"
  assumes t\<^sub>2\<^sub>3: "instance_of\<^sub>t t\<^sub>2 t\<^sub>3"
  shows "instance_of\<^sub>t t\<^sub>1 t\<^sub>3"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. instance_of\<^sub>t t\<^sub>1 t\<^sub>3
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. instance_of\<^sub>t t\<^sub>1 t\<^sub>3
[PROOF STEP]
from t\<^sub>1\<^sub>2
[PROOF STATE]
proof (chain)
picking this:
instance_of\<^sub>t t\<^sub>1 t\<^sub>2
[PROOF STEP]
obtain \<sigma>\<^sub>1\<^sub>2 where "t\<^sub>1 = t\<^sub>2 \<cdot>\<^sub>t \<sigma>\<^sub>1\<^sub>2"
[PROOF STATE]
proof (prove)
using this:
instance_of\<^sub>t t\<^sub>1 t\<^sub>2

goal (1 subgoal):
 1. (\<And>\<sigma>\<^sub>1\<^sub>2. t\<^sub>1 = t\<^sub>2 \<cdot>\<^sub>t \<sigma>\<^sub>1\<^sub>2 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding instance_of\<^sub>t_def
[PROOF STATE]
proof (prove)
using this:
\<exists>\<sigma>. t\<^sub>1 = t\<^sub>2 \<cdot>\<^sub>t \<sigma>

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

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

goal (1 subgoal):
 1. instance_of\<^sub>t t\<^sub>1 t\<^sub>3
[PROOF STEP]
from t\<^sub>2\<^sub>3
[PROOF STATE]
proof (chain)
picking this:
instance_of\<^sub>t t\<^sub>2 t\<^sub>3
[PROOF STEP]
obtain \<sigma>\<^sub>2\<^sub>3 where "t\<^sub>2 = t\<^sub>3 \<cdot>\<^sub>t \<sigma>\<^sub>2\<^sub>3"
[PROOF STATE]
proof (prove)
using this:
instance_of\<^sub>t t\<^sub>2 t\<^sub>3

goal (1 subgoal):
 1. (\<And>\<sigma>\<^sub>2\<^sub>3. t\<^sub>2 = t\<^sub>3 \<cdot>\<^sub>t \<sigma>\<^sub>2\<^sub>3 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding instance_of\<^sub>t_def
[PROOF STATE]
proof (prove)
using this:
\<exists>\<sigma>. t\<^sub>2 = t\<^sub>3 \<cdot>\<^sub>t \<sigma>

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

goal (1 subgoal):
 1. instance_of\<^sub>t t\<^sub>1 t\<^sub>3
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
t\<^sub>1 = t\<^sub>2 \<cdot>\<^sub>t \<sigma>\<^sub>1\<^sub>2
t\<^sub>2 = t\<^sub>3 \<cdot>\<^sub>t \<sigma>\<^sub>2\<^sub>3
[PROOF STEP]
have "t\<^sub>1 = (t\<^sub>3 \<cdot>\<^sub>t \<sigma>\<^sub>2\<^sub>3) \<cdot>\<^sub>t \<sigma>\<^sub>1\<^sub>2"
[PROOF STATE]
proof (prove)
using this:
t\<^sub>1 = t\<^sub>2 \<cdot>\<^sub>t \<sigma>\<^sub>1\<^sub>2
t\<^sub>2 = t\<^sub>3 \<cdot>\<^sub>t \<sigma>\<^sub>2\<^sub>3

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

goal (1 subgoal):
 1. instance_of\<^sub>t t\<^sub>1 t\<^sub>3
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
t\<^sub>1 = t\<^sub>3 \<cdot>\<^sub>t \<sigma>\<^sub>2\<^sub>3 \<cdot>\<^sub>t \<sigma>\<^sub>1\<^sub>2
[PROOF STEP]
have "t\<^sub>1 = t\<^sub>3 \<cdot>\<^sub>t (\<sigma>\<^sub>2\<^sub>3 \<cdot> \<sigma>\<^sub>1\<^sub>2)"
[PROOF STATE]
proof (prove)
using this:
t\<^sub>1 = t\<^sub>3 \<cdot>\<^sub>t \<sigma>\<^sub>2\<^sub>3 \<cdot>\<^sub>t \<sigma>\<^sub>1\<^sub>2

goal (1 subgoal):
 1. t\<^sub>1 = t\<^sub>3 \<cdot>\<^sub>t (\<sigma>\<^sub>2\<^sub>3 \<cdot> \<sigma>\<^sub>1\<^sub>2)
[PROOF STEP]
using composition_conseq2t
[PROOF STATE]
proof (prove)
using this:
t\<^sub>1 = t\<^sub>3 \<cdot>\<^sub>t \<sigma>\<^sub>2\<^sub>3 \<cdot>\<^sub>t \<sigma>\<^sub>1\<^sub>2
?t \<cdot>\<^sub>t ?\<sigma>\<^sub>1 \<cdot>\<^sub>t ?\<sigma>\<^sub>2 = ?t \<cdot>\<^sub>t (?\<sigma>\<^sub>1 \<cdot> ?\<sigma>\<^sub>2)

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

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

goal (1 subgoal):
 1. instance_of\<^sub>t t\<^sub>1 t\<^sub>3
[PROOF STEP]
unfolding instance_of\<^sub>t_def
[PROOF STATE]
proof (prove)
using this:
t\<^sub>1 = t\<^sub>3 \<cdot>\<^sub>t (\<sigma>\<^sub>2\<^sub>3 \<cdot> \<sigma>\<^sub>1\<^sub>2)

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma instance_of\<^sub>t\<^sub>s_trans :
  assumes ts\<^sub>1\<^sub>2: "instance_of\<^sub>t\<^sub>s ts\<^sub>1 ts\<^sub>2"
  assumes ts\<^sub>2\<^sub>3: "instance_of\<^sub>t\<^sub>s ts\<^sub>2 ts\<^sub>3"
  shows "instance_of\<^sub>t\<^sub>s ts\<^sub>1 ts\<^sub>3"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. instance_of\<^sub>t\<^sub>s ts\<^sub>1 ts\<^sub>3
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. instance_of\<^sub>t\<^sub>s ts\<^sub>1 ts\<^sub>3
[PROOF STEP]
from ts\<^sub>1\<^sub>2
[PROOF STATE]
proof (chain)
picking this:
instance_of\<^sub>t\<^sub>s ts\<^sub>1 ts\<^sub>2
[PROOF STEP]
obtain \<sigma>\<^sub>1\<^sub>2 where "ts\<^sub>1 = ts\<^sub>2 \<cdot>\<^sub>t\<^sub>s \<sigma>\<^sub>1\<^sub>2"
[PROOF STATE]
proof (prove)
using this:
instance_of\<^sub>t\<^sub>s ts\<^sub>1 ts\<^sub>2

goal (1 subgoal):
 1. (\<And>\<sigma>\<^sub>1\<^sub>2. ts\<^sub>1 = ts\<^sub>2 \<cdot>\<^sub>t\<^sub>s \<sigma>\<^sub>1\<^sub>2 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding instance_of\<^sub>t\<^sub>s_def
[PROOF STATE]
proof (prove)
using this:
\<exists>\<sigma>. ts\<^sub>1 = ts\<^sub>2 \<cdot>\<^sub>t\<^sub>s \<sigma>

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

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

goal (1 subgoal):
 1. instance_of\<^sub>t\<^sub>s ts\<^sub>1 ts\<^sub>3
[PROOF STEP]
from ts\<^sub>2\<^sub>3
[PROOF STATE]
proof (chain)
picking this:
instance_of\<^sub>t\<^sub>s ts\<^sub>2 ts\<^sub>3
[PROOF STEP]
obtain \<sigma>\<^sub>2\<^sub>3 where "ts\<^sub>2 = ts\<^sub>3 \<cdot>\<^sub>t\<^sub>s \<sigma>\<^sub>2\<^sub>3"
[PROOF STATE]
proof (prove)
using this:
instance_of\<^sub>t\<^sub>s ts\<^sub>2 ts\<^sub>3

goal (1 subgoal):
 1. (\<And>\<sigma>\<^sub>2\<^sub>3. ts\<^sub>2 = ts\<^sub>3 \<cdot>\<^sub>t\<^sub>s \<sigma>\<^sub>2\<^sub>3 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding instance_of\<^sub>t\<^sub>s_def
[PROOF STATE]
proof (prove)
using this:
\<exists>\<sigma>. ts\<^sub>2 = ts\<^sub>3 \<cdot>\<^sub>t\<^sub>s \<sigma>

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

goal (1 subgoal):
 1. instance_of\<^sub>t\<^sub>s ts\<^sub>1 ts\<^sub>3
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
ts\<^sub>1 = ts\<^sub>2 \<cdot>\<^sub>t\<^sub>s \<sigma>\<^sub>1\<^sub>2
ts\<^sub>2 = ts\<^sub>3 \<cdot>\<^sub>t\<^sub>s \<sigma>\<^sub>2\<^sub>3
[PROOF STEP]
have "ts\<^sub>1 = (ts\<^sub>3 \<cdot>\<^sub>t\<^sub>s \<sigma>\<^sub>2\<^sub>3) \<cdot>\<^sub>t\<^sub>s \<sigma>\<^sub>1\<^sub>2"
[PROOF STATE]
proof (prove)
using this:
ts\<^sub>1 = ts\<^sub>2 \<cdot>\<^sub>t\<^sub>s \<sigma>\<^sub>1\<^sub>2
ts\<^sub>2 = ts\<^sub>3 \<cdot>\<^sub>t\<^sub>s \<sigma>\<^sub>2\<^sub>3

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

goal (1 subgoal):
 1. instance_of\<^sub>t\<^sub>s ts\<^sub>1 ts\<^sub>3
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ts\<^sub>1 = ts\<^sub>3 \<cdot>\<^sub>t\<^sub>s \<sigma>\<^sub>2\<^sub>3 \<cdot>\<^sub>t\<^sub>s \<sigma>\<^sub>1\<^sub>2
[PROOF STEP]
have "ts\<^sub>1 = ts\<^sub>3 \<cdot>\<^sub>t\<^sub>s (\<sigma>\<^sub>2\<^sub>3 \<cdot> \<sigma>\<^sub>1\<^sub>2)"
[PROOF STATE]
proof (prove)
using this:
ts\<^sub>1 = ts\<^sub>3 \<cdot>\<^sub>t\<^sub>s \<sigma>\<^sub>2\<^sub>3 \<cdot>\<^sub>t\<^sub>s \<sigma>\<^sub>1\<^sub>2

goal (1 subgoal):
 1. ts\<^sub>1 = ts\<^sub>3 \<cdot>\<^sub>t\<^sub>s (\<sigma>\<^sub>2\<^sub>3 \<cdot> \<sigma>\<^sub>1\<^sub>2)
[PROOF STEP]
using composition_conseq2ts
[PROOF STATE]
proof (prove)
using this:
ts\<^sub>1 = ts\<^sub>3 \<cdot>\<^sub>t\<^sub>s \<sigma>\<^sub>2\<^sub>3 \<cdot>\<^sub>t\<^sub>s \<sigma>\<^sub>1\<^sub>2
?ts \<cdot>\<^sub>t\<^sub>s ?\<sigma>\<^sub>1 \<cdot>\<^sub>t\<^sub>s ?\<sigma>\<^sub>2 = ?ts \<cdot>\<^sub>t\<^sub>s (?\<sigma>\<^sub>1 \<cdot> ?\<sigma>\<^sub>2)

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

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

goal (1 subgoal):
 1. instance_of\<^sub>t\<^sub>s ts\<^sub>1 ts\<^sub>3
[PROOF STEP]
unfolding instance_of\<^sub>t\<^sub>s_def
[PROOF STATE]
proof (prove)
using this:
ts\<^sub>1 = ts\<^sub>3 \<cdot>\<^sub>t\<^sub>s (\<sigma>\<^sub>2\<^sub>3 \<cdot> \<sigma>\<^sub>1\<^sub>2)

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma instance_of\<^sub>l_trans :
  assumes l\<^sub>1\<^sub>2: "instance_of\<^sub>l l\<^sub>1 l\<^sub>2"
  assumes l\<^sub>2\<^sub>3: "instance_of\<^sub>l l\<^sub>2 l\<^sub>3"
  shows "instance_of\<^sub>l l\<^sub>1 l\<^sub>3"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. instance_of\<^sub>l l\<^sub>1 l\<^sub>3
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. instance_of\<^sub>l l\<^sub>1 l\<^sub>3
[PROOF STEP]
from l\<^sub>1\<^sub>2
[PROOF STATE]
proof (chain)
picking this:
instance_of\<^sub>l l\<^sub>1 l\<^sub>2
[PROOF STEP]
obtain \<sigma>\<^sub>1\<^sub>2 where "l\<^sub>1 = l\<^sub>2 \<cdot>\<^sub>l \<sigma>\<^sub>1\<^sub>2"
[PROOF STATE]
proof (prove)
using this:
instance_of\<^sub>l l\<^sub>1 l\<^sub>2

goal (1 subgoal):
 1. (\<And>\<sigma>\<^sub>1\<^sub>2. l\<^sub>1 = l\<^sub>2 \<cdot>\<^sub>l \<sigma>\<^sub>1\<^sub>2 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding instance_of\<^sub>l_def
[PROOF STATE]
proof (prove)
using this:
\<exists>\<sigma>. l\<^sub>1 = l\<^sub>2 \<cdot>\<^sub>l \<sigma>

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

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

goal (1 subgoal):
 1. instance_of\<^sub>l l\<^sub>1 l\<^sub>3
[PROOF STEP]
from l\<^sub>2\<^sub>3
[PROOF STATE]
proof (chain)
picking this:
instance_of\<^sub>l l\<^sub>2 l\<^sub>3
[PROOF STEP]
obtain \<sigma>\<^sub>2\<^sub>3 where "l\<^sub>2 = l\<^sub>3 \<cdot>\<^sub>l \<sigma>\<^sub>2\<^sub>3"
[PROOF STATE]
proof (prove)
using this:
instance_of\<^sub>l l\<^sub>2 l\<^sub>3

goal (1 subgoal):
 1. (\<And>\<sigma>\<^sub>2\<^sub>3. l\<^sub>2 = l\<^sub>3 \<cdot>\<^sub>l \<sigma>\<^sub>2\<^sub>3 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding instance_of\<^sub>l_def
[PROOF STATE]
proof (prove)
using this:
\<exists>\<sigma>. l\<^sub>2 = l\<^sub>3 \<cdot>\<^sub>l \<sigma>

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

goal (1 subgoal):
 1. instance_of\<^sub>l l\<^sub>1 l\<^sub>3
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
l\<^sub>1 = l\<^sub>2 \<cdot>\<^sub>l \<sigma>\<^sub>1\<^sub>2
l\<^sub>2 = l\<^sub>3 \<cdot>\<^sub>l \<sigma>\<^sub>2\<^sub>3
[PROOF STEP]
have "l\<^sub>1 = (l\<^sub>3 \<cdot>\<^sub>l \<sigma>\<^sub>2\<^sub>3) \<cdot>\<^sub>l \<sigma>\<^sub>1\<^sub>2"
[PROOF STATE]
proof (prove)
using this:
l\<^sub>1 = l\<^sub>2 \<cdot>\<^sub>l \<sigma>\<^sub>1\<^sub>2
l\<^sub>2 = l\<^sub>3 \<cdot>\<^sub>l \<sigma>\<^sub>2\<^sub>3

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

goal (1 subgoal):
 1. instance_of\<^sub>l l\<^sub>1 l\<^sub>3
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
l\<^sub>1 = l\<^sub>3 \<cdot>\<^sub>l \<sigma>\<^sub>2\<^sub>3 \<cdot>\<^sub>l \<sigma>\<^sub>1\<^sub>2
[PROOF STEP]
have "l\<^sub>1 = l\<^sub>3 \<cdot>\<^sub>l (\<sigma>\<^sub>2\<^sub>3 \<cdot> \<sigma>\<^sub>1\<^sub>2)"
[PROOF STATE]
proof (prove)
using this:
l\<^sub>1 = l\<^sub>3 \<cdot>\<^sub>l \<sigma>\<^sub>2\<^sub>3 \<cdot>\<^sub>l \<sigma>\<^sub>1\<^sub>2

goal (1 subgoal):
 1. l\<^sub>1 = l\<^sub>3 \<cdot>\<^sub>l (\<sigma>\<^sub>2\<^sub>3 \<cdot> \<sigma>\<^sub>1\<^sub>2)
[PROOF STEP]
using composition_conseq2l
[PROOF STATE]
proof (prove)
using this:
l\<^sub>1 = l\<^sub>3 \<cdot>\<^sub>l \<sigma>\<^sub>2\<^sub>3 \<cdot>\<^sub>l \<sigma>\<^sub>1\<^sub>2
?l \<cdot>\<^sub>l ?\<sigma>\<^sub>1 \<cdot>\<^sub>l ?\<sigma>\<^sub>2 = ?l \<cdot>\<^sub>l (?\<sigma>\<^sub>1 \<cdot> ?\<sigma>\<^sub>2)

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

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

goal (1 subgoal):
 1. instance_of\<^sub>l l\<^sub>1 l\<^sub>3
[PROOF STEP]
unfolding instance_of\<^sub>l_def
[PROOF STATE]
proof (prove)
using this:
l\<^sub>1 = l\<^sub>3 \<cdot>\<^sub>l (\<sigma>\<^sub>2\<^sub>3 \<cdot> \<sigma>\<^sub>1\<^sub>2)

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma instance_of\<^sub>l\<^sub>s_trans :
  assumes L\<^sub>1\<^sub>2: "instance_of\<^sub>l\<^sub>s L\<^sub>1 L\<^sub>2"
  assumes L\<^sub>2\<^sub>3: "instance_of\<^sub>l\<^sub>s L\<^sub>2 L\<^sub>3"
  shows "instance_of\<^sub>l\<^sub>s L\<^sub>1 L\<^sub>3"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. instance_of\<^sub>l\<^sub>s L\<^sub>1 L\<^sub>3
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. instance_of\<^sub>l\<^sub>s L\<^sub>1 L\<^sub>3
[PROOF STEP]
from L\<^sub>1\<^sub>2
[PROOF STATE]
proof (chain)
picking this:
instance_of\<^sub>l\<^sub>s L\<^sub>1 L\<^sub>2
[PROOF STEP]
obtain \<sigma>\<^sub>1\<^sub>2 where "L\<^sub>1 = L\<^sub>2 \<cdot>\<^sub>l\<^sub>s \<sigma>\<^sub>1\<^sub>2"
[PROOF STATE]
proof (prove)
using this:
instance_of\<^sub>l\<^sub>s L\<^sub>1 L\<^sub>2

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

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

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

goal (1 subgoal):
 1. instance_of\<^sub>l\<^sub>s L\<^sub>1 L\<^sub>3
[PROOF STEP]
from L\<^sub>2\<^sub>3
[PROOF STATE]
proof (chain)
picking this:
instance_of\<^sub>l\<^sub>s L\<^sub>2 L\<^sub>3
[PROOF STEP]
obtain \<sigma>\<^sub>2\<^sub>3 where "L\<^sub>2 = L\<^sub>3 \<cdot>\<^sub>l\<^sub>s \<sigma>\<^sub>2\<^sub>3"
[PROOF STATE]
proof (prove)
using this:
instance_of\<^sub>l\<^sub>s L\<^sub>2 L\<^sub>3

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

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

goal (1 subgoal):
 1. instance_of\<^sub>l\<^sub>s L\<^sub>1 L\<^sub>3
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
L\<^sub>1 = L\<^sub>2 \<cdot>\<^sub>l\<^sub>s \<sigma>\<^sub>1\<^sub>2
L\<^sub>2 = L\<^sub>3 \<cdot>\<^sub>l\<^sub>s \<sigma>\<^sub>2\<^sub>3
[PROOF STEP]
have "L\<^sub>1 = (L\<^sub>3 \<cdot>\<^sub>l\<^sub>s \<sigma>\<^sub>2\<^sub>3) \<cdot>\<^sub>l\<^sub>s \<sigma>\<^sub>1\<^sub>2"
[PROOF STATE]
proof (prove)
using this:
L\<^sub>1 = L\<^sub>2 \<cdot>\<^sub>l\<^sub>s \<sigma>\<^sub>1\<^sub>2
L\<^sub>2 = L\<^sub>3 \<cdot>\<^sub>l\<^sub>s \<sigma>\<^sub>2\<^sub>3

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

goal (1 subgoal):
 1. instance_of\<^sub>l\<^sub>s L\<^sub>1 L\<^sub>3
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
L\<^sub>1 = L\<^sub>3 \<cdot>\<^sub>l\<^sub>s \<sigma>\<^sub>2\<^sub>3 \<cdot>\<^sub>l\<^sub>s \<sigma>\<^sub>1\<^sub>2
[PROOF STEP]
have "L\<^sub>1 = L\<^sub>3 \<cdot>\<^sub>l\<^sub>s (\<sigma>\<^sub>2\<^sub>3 \<cdot> \<sigma>\<^sub>1\<^sub>2)"
[PROOF STATE]
proof (prove)
using this:
L\<^sub>1 = L\<^sub>3 \<cdot>\<^sub>l\<^sub>s \<sigma>\<^sub>2\<^sub>3 \<cdot>\<^sub>l\<^sub>s \<sigma>\<^sub>1\<^sub>2

goal (1 subgoal):
 1. L\<^sub>1 = L\<^sub>3 \<cdot>\<^sub>l\<^sub>s (\<sigma>\<^sub>2\<^sub>3 \<cdot> \<sigma>\<^sub>1\<^sub>2)
[PROOF STEP]
using composition_conseq2ls
[PROOF STATE]
proof (prove)
using this:
L\<^sub>1 = L\<^sub>3 \<cdot>\<^sub>l\<^sub>s \<sigma>\<^sub>2\<^sub>3 \<cdot>\<^sub>l\<^sub>s \<sigma>\<^sub>1\<^sub>2
?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. L\<^sub>1 = L\<^sub>3 \<cdot>\<^sub>l\<^sub>s (\<sigma>\<^sub>2\<^sub>3 \<cdot> \<sigma>\<^sub>1\<^sub>2)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
L\<^sub>1 = L\<^sub>3 \<cdot>\<^sub>l\<^sub>s (\<sigma>\<^sub>2\<^sub>3 \<cdot> \<sigma>\<^sub>1\<^sub>2)

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed