[STATEMENT]
lemma timpl_closure'_inv:
  assumes "(s, t) \<in> timpl_closure' TI"
  shows "(\<exists>x. s = Var x \<and> t = Var x) \<or> (\<exists>f g S T. s = Fun f S \<and> t = Fun g T \<and> length S = length T)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>x. s = Var x \<and> t = Var x) \<or> (\<exists>f g S T. s = Fun f S \<and> t = Fun g T \<and> length S = length T)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(s, t) \<in> timpl_closure' TI

goal (1 subgoal):
 1. (\<exists>x. s = Var x \<and> t = Var x) \<or> (\<exists>f g S T. s = Fun f S \<and> t = Fun g T \<and> length S = length T)
[PROOF STEP]
unfolding timpl_closure'_def
[PROOF STATE]
proof (prove)
using this:
(s, t) \<in> (timpl_closure'_step TI)\<^sup>*

goal (1 subgoal):
 1. (\<exists>x. s = Var x \<and> t = Var x) \<or> (\<exists>f g S T. s = Fun f S \<and> t = Fun g T \<and> length S = length T)
[PROOF STEP]
proof (induction rule: rtrancl_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (\<exists>x. s = Var x \<and> s = Var x) \<or> (\<exists>f g S T. s = Fun f S \<and> s = Fun g T \<and> length S = length T)
 2. \<And>y z. \<lbrakk>(s, y) \<in> (timpl_closure'_step TI)\<^sup>*; (y, z) \<in> timpl_closure'_step TI; (\<exists>x. s = Var x \<and> y = Var x) \<or> (\<exists>f g S T. s = Fun f S \<and> y = Fun g T \<and> length S = length T)\<rbrakk> \<Longrightarrow> (\<exists>x. s = Var x \<and> z = Var x) \<or> (\<exists>f g S T. s = Fun f S \<and> z = Fun g T \<and> length S = length T)
[PROOF STEP]
case base
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. (\<exists>x. s = Var x \<and> s = Var x) \<or> (\<exists>f g S T. s = Fun f S \<and> s = Fun g T \<and> length S = length T)
 2. \<And>y z. \<lbrakk>(s, y) \<in> (timpl_closure'_step TI)\<^sup>*; (y, z) \<in> timpl_closure'_step TI; (\<exists>x. s = Var x \<and> y = Var x) \<or> (\<exists>f g S T. s = Fun f S \<and> y = Fun g T \<and> length S = length T)\<rbrakk> \<Longrightarrow> (\<exists>x. s = Var x \<and> z = Var x) \<or> (\<exists>f g S T. s = Fun f S \<and> z = Fun g T \<and> length S = length T)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>x. s = Var x \<and> s = Var x) \<or> (\<exists>f g S T. s = Fun f S \<and> s = Fun g T \<and> length S = length T)
[PROOF STEP]
by (cases s) auto
[PROOF STATE]
proof (state)
this:
(\<exists>x. s = Var x \<and> s = Var x) \<or> (\<exists>f g S T. s = Fun f S \<and> s = Fun g T \<and> length S = length T)

goal (1 subgoal):
 1. \<And>y z. \<lbrakk>(s, y) \<in> (timpl_closure'_step TI)\<^sup>*; (y, z) \<in> timpl_closure'_step TI; (\<exists>x. s = Var x \<and> y = Var x) \<or> (\<exists>f g S T. s = Fun f S \<and> y = Fun g T \<and> length S = length T)\<rbrakk> \<Longrightarrow> (\<exists>x. s = Var x \<and> z = Var x) \<or> (\<exists>f g S T. s = Fun f S \<and> z = Fun g T \<and> length S = length T)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>(s, y) \<in> (timpl_closure'_step TI)\<^sup>*; (y, z) \<in> timpl_closure'_step TI; (\<exists>x. s = Var x \<and> y = Var x) \<or> (\<exists>f g S T. s = Fun f S \<and> y = Fun g T \<and> length S = length T)\<rbrakk> \<Longrightarrow> (\<exists>x. s = Var x \<and> z = Var x) \<or> (\<exists>f g S T. s = Fun f S \<and> z = Fun g T \<and> length S = length T)
[PROOF STEP]
case (step t u)
[PROOF STATE]
proof (state)
this:
(s, t) \<in> (timpl_closure'_step TI)\<^sup>*
(t, u) \<in> timpl_closure'_step TI
(\<exists>x. s = Var x \<and> t = Var x) \<or> (\<exists>f g S T. s = Fun f S \<and> t = Fun g T \<and> length S = length T)

goal (1 subgoal):
 1. \<And>y z. \<lbrakk>(s, y) \<in> (timpl_closure'_step TI)\<^sup>*; (y, z) \<in> timpl_closure'_step TI; (\<exists>x. s = Var x \<and> y = Var x) \<or> (\<exists>f g S T. s = Fun f S \<and> y = Fun g T \<and> length S = length T)\<rbrakk> \<Longrightarrow> (\<exists>x. s = Var x \<and> z = Var x) \<or> (\<exists>f g S T. s = Fun f S \<and> z = Fun g T \<and> length S = length T)
[PROOF STEP]
obtain a b where ab: "(a, b) \<in> TI" "term_variants_pred ((\<lambda>_. [])(Abs a := [Abs b])) t u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>a b. \<lbrakk>(a, b) \<in> TI; term_variants_pred ((\<lambda>_. [])(Abs a := [Abs b])) t u\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using timpl_closure'_step_inv[OF step.hyps(2)]
[PROOF STATE]
proof (prove)
using this:
(\<And>a b. \<lbrakk>(a, b) \<in> TI; term_variants_pred ((\<lambda>_. [])(Abs a := [Abs b])) t u\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>a b. \<lbrakk>(a, b) \<in> TI; term_variants_pred ((\<lambda>_. [])(Abs a := [Abs b])) t u\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(a, b) \<in> TI
term_variants_pred ((\<lambda>_. [])(Abs a := [Abs b])) t u

goal (1 subgoal):
 1. \<And>y z. \<lbrakk>(s, y) \<in> (timpl_closure'_step TI)\<^sup>*; (y, z) \<in> timpl_closure'_step TI; (\<exists>x. s = Var x \<and> y = Var x) \<or> (\<exists>f g S T. s = Fun f S \<and> y = Fun g T \<and> length S = length T)\<rbrakk> \<Longrightarrow> (\<exists>x. s = Var x \<and> z = Var x) \<or> (\<exists>f g S T. s = Fun f S \<and> z = Fun g T \<and> length S = length T)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>x. s = Var x \<and> u = Var x) \<or> (\<exists>f g S T. s = Fun f S \<and> u = Fun g T \<and> length S = length T)
[PROOF STEP]
using step.IH
[PROOF STATE]
proof (prove)
using this:
(\<exists>x. s = Var x \<and> t = Var x) \<or> (\<exists>f g S T. s = Fun f S \<and> t = Fun g T \<and> length S = length T)

goal (1 subgoal):
 1. (\<exists>x. s = Var x \<and> u = Var x) \<or> (\<exists>f g S T. s = Fun f S \<and> u = Fun g T \<and> length S = length T)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<exists>x. s = Var x \<and> t = Var x \<Longrightarrow> (\<exists>x. s = Var x \<and> u = Var x) \<or> (\<exists>f g S T. s = Fun f S \<and> u = Fun g T \<and> length S = length T)
 2. \<exists>f g S T. s = Fun f S \<and> t = Fun g T \<and> length S = length T \<Longrightarrow> (\<exists>x. s = Var x \<and> u = Var x) \<or> (\<exists>f g S T. s = Fun f S \<and> u = Fun g T \<and> length S = length T)
[PROOF STEP]
assume "\<exists>x. s = Var x \<and> t = Var x"
[PROOF STATE]
proof (state)
this:
\<exists>x. s = Var x \<and> t = Var x

goal (2 subgoals):
 1. \<exists>x. s = Var x \<and> t = Var x \<Longrightarrow> (\<exists>x. s = Var x \<and> u = Var x) \<or> (\<exists>f g S T. s = Fun f S \<and> u = Fun g T \<and> length S = length T)
 2. \<exists>f g S T. s = Fun f S \<and> t = Fun g T \<and> length S = length T \<Longrightarrow> (\<exists>x. s = Var x \<and> u = Var x) \<or> (\<exists>f g S T. s = Fun f S \<and> u = Fun g T \<and> length S = length T)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<exists>x. s = Var x \<and> t = Var x

goal (1 subgoal):
 1. (\<exists>x. s = Var x \<and> u = Var x) \<or> (\<exists>f g S T. s = Fun f S \<and> u = Fun g T \<and> length S = length T)
[PROOF STEP]
using step.hyps(2) term_variants_pred_inv_Var ab
[PROOF STATE]
proof (prove)
using this:
\<exists>x. s = Var x \<and> t = Var x
(t, u) \<in> timpl_closure'_step TI
term_variants_pred ?P (Var ?x) ?t = (?t = Var ?x)
term_variants_pred ?P ?t (Var ?x) = (?t = Var ?x)
(a, b) \<in> TI
term_variants_pred ((\<lambda>_. [])(Abs a := [Abs b])) t u

goal (1 subgoal):
 1. (\<exists>x. s = Var x \<and> u = Var x) \<or> (\<exists>f g S T. s = Fun f S \<and> u = Fun g T \<and> length S = length T)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
(\<exists>x. s = Var x \<and> u = Var x) \<or> (\<exists>f g S T. s = Fun f S \<and> u = Fun g T \<and> length S = length T)

goal (1 subgoal):
 1. \<exists>f g S T. s = Fun f S \<and> t = Fun g T \<and> length S = length T \<Longrightarrow> (\<exists>x. s = Var x \<and> u = Var x) \<or> (\<exists>f g S T. s = Fun f S \<and> u = Fun g T \<and> length S = length T)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>f g S T. s = Fun f S \<and> t = Fun g T \<and> length S = length T \<Longrightarrow> (\<exists>x. s = Var x \<and> u = Var x) \<or> (\<exists>f g S T. s = Fun f S \<and> u = Fun g T \<and> length S = length T)
[PROOF STEP]
assume "\<exists>f g S T. s = Fun f S \<and> t = Fun g T \<and> length S = length T"
[PROOF STATE]
proof (state)
this:
\<exists>f g S T. s = Fun f S \<and> t = Fun g T \<and> length S = length T

goal (1 subgoal):
 1. \<exists>f g S T. s = Fun f S \<and> t = Fun g T \<and> length S = length T \<Longrightarrow> (\<exists>x. s = Var x \<and> u = Var x) \<or> (\<exists>f g S T. s = Fun f S \<and> u = Fun g T \<and> length S = length T)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>f g S T. s = Fun f S \<and> t = Fun g T \<and> length S = length T
[PROOF STEP]
obtain f g S T where st: "s = Fun f S" "t = Fun g T" "length S = length T"
[PROOF STATE]
proof (prove)
using this:
\<exists>f g S T. s = Fun f S \<and> t = Fun g T \<and> length S = length T

goal (1 subgoal):
 1. (\<And>f S g T. \<lbrakk>s = Fun f S; t = Fun g T; length S = length T\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by moura
[PROOF STATE]
proof (state)
this:
s = Fun f S
t = Fun g T
length S = length T

goal (1 subgoal):
 1. \<exists>f g S T. s = Fun f S \<and> t = Fun g T \<and> length S = length T \<Longrightarrow> (\<exists>x. s = Var x \<and> u = Var x) \<or> (\<exists>f g S T. s = Fun f S \<and> u = Fun g T \<and> length S = length T)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
s = Fun f S
t = Fun g T
length S = length T

goal (1 subgoal):
 1. (\<exists>x. s = Var x \<and> u = Var x) \<or> (\<exists>f g S T. s = Fun f S \<and> u = Fun g T \<and> length S = length T)
[PROOF STEP]
using ab step.hyps(2) term_variants_pred_inv'[of "(\<lambda>_. [])(Abs a := [Abs b])" g T u]
[PROOF STATE]
proof (prove)
using this:
s = Fun f S
t = Fun g T
length S = length T
(a, b) \<in> TI
term_variants_pred ((\<lambda>_. [])(Abs a := [Abs b])) t u
(t, u) \<in> timpl_closure'_step TI
term_variants_pred ((\<lambda>_. [])(Abs a := [Abs b])) (Fun g T) u \<Longrightarrow> is_Fun u
term_variants_pred ((\<lambda>_. [])(Abs a := [Abs b])) (Fun g T) u \<Longrightarrow> length T = length (args u)
\<lbrakk>term_variants_pred ((\<lambda>_. [])(Abs a := [Abs b])) (Fun g T) u; ?i < length T\<rbrakk> \<Longrightarrow> term_variants_pred ((\<lambda>_. [])(Abs a := [Abs b])) (T ! ?i) (args u ! ?i)
\<lbrakk>term_variants_pred ((\<lambda>_. [])(Abs a := [Abs b])) (Fun g T) u; g \<noteq> the_Fun u\<rbrakk> \<Longrightarrow> the_Fun u \<in> set (((\<lambda>_. [])(Abs a := [Abs b])) g)
\<lbrakk>term_variants_pred ((\<lambda>_. [])(Abs a := [Abs b])) (Fun g T) u; (\<lambda>_. [])(Abs a := [Abs b]) \<equiv> (\<lambda>_. [])(?g := [?h]); g \<noteq> the_Fun u\<rbrakk> \<Longrightarrow> g = ?g \<and> the_Fun u = ?h

goal (1 subgoal):
 1. (\<exists>x. s = Var x \<and> u = Var x) \<or> (\<exists>f g S T. s = Fun f S \<and> u = Fun g T \<and> length S = length T)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<exists>x. s = Var x \<and> u = Var x) \<or> (\<exists>f g S T. s = Fun f S \<and> u = Fun g T \<and> length S = length T)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<exists>x. s = Var x \<and> u = Var x) \<or> (\<exists>f g S T. s = Fun f S \<and> u = Fun g T \<and> length S = length T)

goal:
No subgoals!
[PROOF STEP]
qed