[STATEMENT]
lemma (in encoding) refl_trans_closure_of_indRelT:
  fixes TRel :: "('procT \<times> 'procT) set"
  assumes refl: "refl TRel"
  shows "indRelTEQ TRel = (indRelT TRel)\<^sup>*"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. indRelTEQ TRel = (indRelT TRel)\<^sup>*
[PROOF STEP]
proof auto
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>a b. a \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> b \<Longrightarrow> (a, b) \<in> (indRelT TRel)\<^sup>*
 2. \<And>a b. (a, b) \<in> (indRelT TRel)\<^sup>* \<Longrightarrow> a \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> b
[PROOF STEP]
fix P Q
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>a b. a \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> b \<Longrightarrow> (a, b) \<in> (indRelT TRel)\<^sup>*
 2. \<And>a b. (a, b) \<in> (indRelT TRel)\<^sup>* \<Longrightarrow> a \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> b
[PROOF STEP]
assume "P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q"
[PROOF STATE]
proof (state)
this:
P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q

goal (2 subgoals):
 1. \<And>a b. a \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> b \<Longrightarrow> (a, b) \<in> (indRelT TRel)\<^sup>*
 2. \<And>a b. (a, b) \<in> (indRelT TRel)\<^sup>* \<Longrightarrow> a \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> b
[PROOF STEP]
thus "(P, Q) \<in> (indRelT TRel)\<^sup>*"
[PROOF STATE]
proof (prove)
using this:
P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q

goal (1 subgoal):
 1. (P, Q) \<in> (indRelT TRel)\<^sup>*
[PROOF STEP]
proof induct
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> (indRelT TRel)\<^sup>*
 2. \<And>S. (TargetTerm (\<lbrakk>S\<rbrakk>), SourceTerm S) \<in> (indRelT TRel)\<^sup>*
 3. \<And>T1 T2. (T1, T2) \<in> TRel \<Longrightarrow> (TargetTerm T1, TargetTerm T2) \<in> (indRelT TRel)\<^sup>*
 4. \<And>P Q R. P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q \<and> (P, Q) \<in> (indRelT TRel)\<^sup>* \<and> Q \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> R \<and> (Q, R) \<in> (indRelT TRel)\<^sup>* \<Longrightarrow> (P, R) \<in> (indRelT TRel)\<^sup>*
[PROOF STEP]
case (encR S)
[PROOF STATE]
proof (state)
this:


goal (4 subgoals):
 1. \<And>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> (indRelT TRel)\<^sup>*
 2. \<And>S. (TargetTerm (\<lbrakk>S\<rbrakk>), SourceTerm S) \<in> (indRelT TRel)\<^sup>*
 3. \<And>T1 T2. (T1, T2) \<in> TRel \<Longrightarrow> (TargetTerm T1, TargetTerm T2) \<in> (indRelT TRel)\<^sup>*
 4. \<And>P Q R. P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q \<and> (P, Q) \<in> (indRelT TRel)\<^sup>* \<and> Q \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> R \<and> (Q, R) \<in> (indRelT TRel)\<^sup>* \<Longrightarrow> (P, R) \<in> (indRelT TRel)\<^sup>*
[PROOF STEP]
show "(SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> (indRelT TRel)\<^sup>*"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> (indRelT TRel)\<^sup>*
[PROOF STEP]
using indRelT.encR[of S TRel]
[PROOF STATE]
proof (prove)
using this:
SourceTerm S \<R>\<lbrakk>\<cdot>\<rbrakk>T<TRel> TargetTerm (\<lbrakk>S\<rbrakk>)

goal (1 subgoal):
 1. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> (indRelT TRel)\<^sup>*
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> (indRelT TRel)\<^sup>*

goal (3 subgoals):
 1. \<And>S. (TargetTerm (\<lbrakk>S\<rbrakk>), SourceTerm S) \<in> (indRelT TRel)\<^sup>*
 2. \<And>T1 T2. (T1, T2) \<in> TRel \<Longrightarrow> (TargetTerm T1, TargetTerm T2) \<in> (indRelT TRel)\<^sup>*
 3. \<And>P Q R. P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q \<and> (P, Q) \<in> (indRelT TRel)\<^sup>* \<and> Q \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> R \<and> (Q, R) \<in> (indRelT TRel)\<^sup>* \<Longrightarrow> (P, R) \<in> (indRelT TRel)\<^sup>*
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>S. (TargetTerm (\<lbrakk>S\<rbrakk>), SourceTerm S) \<in> (indRelT TRel)\<^sup>*
 2. \<And>T1 T2. (T1, T2) \<in> TRel \<Longrightarrow> (TargetTerm T1, TargetTerm T2) \<in> (indRelT TRel)\<^sup>*
 3. \<And>P Q R. P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q \<and> (P, Q) \<in> (indRelT TRel)\<^sup>* \<and> Q \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> R \<and> (Q, R) \<in> (indRelT TRel)\<^sup>* \<Longrightarrow> (P, R) \<in> (indRelT TRel)\<^sup>*
[PROOF STEP]
case (encL S)
[PROOF STATE]
proof (state)
this:


goal (3 subgoals):
 1. \<And>S. (TargetTerm (\<lbrakk>S\<rbrakk>), SourceTerm S) \<in> (indRelT TRel)\<^sup>*
 2. \<And>T1 T2. (T1, T2) \<in> TRel \<Longrightarrow> (TargetTerm T1, TargetTerm T2) \<in> (indRelT TRel)\<^sup>*
 3. \<And>P Q R. P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q \<and> (P, Q) \<in> (indRelT TRel)\<^sup>* \<and> Q \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> R \<and> (Q, R) \<in> (indRelT TRel)\<^sup>* \<Longrightarrow> (P, R) \<in> (indRelT TRel)\<^sup>*
[PROOF STEP]
show "(TargetTerm (\<lbrakk>S\<rbrakk>), SourceTerm S) \<in> (indRelT TRel)\<^sup>*"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (TargetTerm (\<lbrakk>S\<rbrakk>), SourceTerm S) \<in> (indRelT TRel)\<^sup>*
[PROOF STEP]
using indRelT.encL[of S TRel]
[PROOF STATE]
proof (prove)
using this:
TargetTerm (\<lbrakk>S\<rbrakk>) \<R>\<lbrakk>\<cdot>\<rbrakk>T<TRel> SourceTerm S

goal (1 subgoal):
 1. (TargetTerm (\<lbrakk>S\<rbrakk>), SourceTerm S) \<in> (indRelT TRel)\<^sup>*
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(TargetTerm (\<lbrakk>S\<rbrakk>), SourceTerm S) \<in> (indRelT TRel)\<^sup>*

goal (2 subgoals):
 1. \<And>T1 T2. (T1, T2) \<in> TRel \<Longrightarrow> (TargetTerm T1, TargetTerm T2) \<in> (indRelT TRel)\<^sup>*
 2. \<And>P Q R. P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q \<and> (P, Q) \<in> (indRelT TRel)\<^sup>* \<and> Q \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> R \<and> (Q, R) \<in> (indRelT TRel)\<^sup>* \<Longrightarrow> (P, R) \<in> (indRelT TRel)\<^sup>*
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>T1 T2. (T1, T2) \<in> TRel \<Longrightarrow> (TargetTerm T1, TargetTerm T2) \<in> (indRelT TRel)\<^sup>*
 2. \<And>P Q R. P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q \<and> (P, Q) \<in> (indRelT TRel)\<^sup>* \<and> Q \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> R \<and> (Q, R) \<in> (indRelT TRel)\<^sup>* \<Longrightarrow> (P, R) \<in> (indRelT TRel)\<^sup>*
[PROOF STEP]
case (target T1 T2)
[PROOF STATE]
proof (state)
this:
(T1, T2) \<in> TRel

goal (2 subgoals):
 1. \<And>T1 T2. (T1, T2) \<in> TRel \<Longrightarrow> (TargetTerm T1, TargetTerm T2) \<in> (indRelT TRel)\<^sup>*
 2. \<And>P Q R. P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q \<and> (P, Q) \<in> (indRelT TRel)\<^sup>* \<and> Q \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> R \<and> (Q, R) \<in> (indRelT TRel)\<^sup>* \<Longrightarrow> (P, R) \<in> (indRelT TRel)\<^sup>*
[PROOF STEP]
assume "(T1, T2) \<in> TRel"
[PROOF STATE]
proof (state)
this:
(T1, T2) \<in> TRel

goal (2 subgoals):
 1. \<And>T1 T2. (T1, T2) \<in> TRel \<Longrightarrow> (TargetTerm T1, TargetTerm T2) \<in> (indRelT TRel)\<^sup>*
 2. \<And>P Q R. P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q \<and> (P, Q) \<in> (indRelT TRel)\<^sup>* \<and> Q \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> R \<and> (Q, R) \<in> (indRelT TRel)\<^sup>* \<Longrightarrow> (P, R) \<in> (indRelT TRel)\<^sup>*
[PROOF STEP]
thus "(TargetTerm T1, TargetTerm T2) \<in> (indRelT TRel)\<^sup>*"
[PROOF STATE]
proof (prove)
using this:
(T1, T2) \<in> TRel

goal (1 subgoal):
 1. (TargetTerm T1, TargetTerm T2) \<in> (indRelT TRel)\<^sup>*
[PROOF STEP]
using indRelT.target[of T1 T2 TRel]
[PROOF STATE]
proof (prove)
using this:
(T1, T2) \<in> TRel
(T1, T2) \<in> TRel \<Longrightarrow> TargetTerm T1 \<R>\<lbrakk>\<cdot>\<rbrakk>T<TRel> TargetTerm T2

goal (1 subgoal):
 1. (TargetTerm T1, TargetTerm T2) \<in> (indRelT TRel)\<^sup>*
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(TargetTerm T1, TargetTerm T2) \<in> (indRelT TRel)\<^sup>*

goal (1 subgoal):
 1. \<And>P Q R. P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q \<and> (P, Q) \<in> (indRelT TRel)\<^sup>* \<and> Q \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> R \<and> (Q, R) \<in> (indRelT TRel)\<^sup>* \<Longrightarrow> (P, R) \<in> (indRelT TRel)\<^sup>*
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>P Q R. P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q \<and> (P, Q) \<in> (indRelT TRel)\<^sup>* \<and> Q \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> R \<and> (Q, R) \<in> (indRelT TRel)\<^sup>* \<Longrightarrow> (P, R) \<in> (indRelT TRel)\<^sup>*
[PROOF STEP]
case (trans P Q R)
[PROOF STATE]
proof (state)
this:
P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q
(P, Q) \<in> (indRelT TRel)\<^sup>*
Q \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> R
(Q, R) \<in> (indRelT TRel)\<^sup>*

goal (1 subgoal):
 1. \<And>P Q R. P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q \<and> (P, Q) \<in> (indRelT TRel)\<^sup>* \<and> Q \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> R \<and> (Q, R) \<in> (indRelT TRel)\<^sup>* \<Longrightarrow> (P, R) \<in> (indRelT TRel)\<^sup>*
[PROOF STEP]
assume "(P, Q) \<in> (indRelT TRel)\<^sup>*" and "(Q, R) \<in> (indRelT TRel)\<^sup>*"
[PROOF STATE]
proof (state)
this:
(P, Q) \<in> (indRelT TRel)\<^sup>*
(Q, R) \<in> (indRelT TRel)\<^sup>*

goal (1 subgoal):
 1. \<And>P Q R. P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q \<and> (P, Q) \<in> (indRelT TRel)\<^sup>* \<and> Q \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> R \<and> (Q, R) \<in> (indRelT TRel)\<^sup>* \<Longrightarrow> (P, R) \<in> (indRelT TRel)\<^sup>*
[PROOF STEP]
thus "(P, R) \<in> (indRelT TRel)\<^sup>*"
[PROOF STATE]
proof (prove)
using this:
(P, Q) \<in> (indRelT TRel)\<^sup>*
(Q, R) \<in> (indRelT TRel)\<^sup>*

goal (1 subgoal):
 1. (P, R) \<in> (indRelT TRel)\<^sup>*
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(P, R) \<in> (indRelT TRel)\<^sup>*

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(P, Q) \<in> (indRelT TRel)\<^sup>*

goal (1 subgoal):
 1. \<And>a b. (a, b) \<in> (indRelT TRel)\<^sup>* \<Longrightarrow> a \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> b
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b. (a, b) \<in> (indRelT TRel)\<^sup>* \<Longrightarrow> a \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> b
[PROOF STEP]
fix P Q
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b. (a, b) \<in> (indRelT TRel)\<^sup>* \<Longrightarrow> a \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> b
[PROOF STEP]
assume "(P, Q) \<in> (indRelT TRel)\<^sup>*"
[PROOF STATE]
proof (state)
this:
(P, Q) \<in> (indRelT TRel)\<^sup>*

goal (1 subgoal):
 1. \<And>a b. (a, b) \<in> (indRelT TRel)\<^sup>* \<Longrightarrow> a \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> b
[PROOF STEP]
thus "P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q"
[PROOF STATE]
proof (prove)
using this:
(P, Q) \<in> (indRelT TRel)\<^sup>*

goal (1 subgoal):
 1. P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q
[PROOF STEP]
proof induct
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> P
 2. \<And>y z. (P, y) \<in> (indRelT TRel)\<^sup>* \<and> y \<R>\<lbrakk>\<cdot>\<rbrakk>T<TRel> z \<and> P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> y \<Longrightarrow> P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> z
[PROOF STEP]
from refl
[PROOF STATE]
proof (chain)
picking this:
refl TRel
[PROOF STEP]
show "P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> P"
[PROOF STATE]
proof (prove)
using this:
refl TRel

goal (1 subgoal):
 1. P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> P
[PROOF STEP]
using indRelTEQ_refl[of TRel]
[PROOF STATE]
proof (prove)
using this:
refl TRel
refl TRel \<Longrightarrow> refl (indRelTEQ TRel)

goal (1 subgoal):
 1. P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> P
[PROOF STEP]
unfolding refl_on_def
[PROOF STATE]
proof (prove)
using this:
TRel \<subseteq> UNIV \<times> UNIV \<and> (\<forall>x\<in>UNIV. (x, x) \<in> TRel)
TRel \<subseteq> UNIV \<times> UNIV \<and> (\<forall>x\<in>UNIV. (x, x) \<in> TRel) \<Longrightarrow> indRelTEQ TRel \<subseteq> UNIV \<times> UNIV \<and> (\<forall>x\<in>UNIV. x \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> x)

goal (1 subgoal):
 1. P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> P
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> P

goal (1 subgoal):
 1. \<And>y z. (P, y) \<in> (indRelT TRel)\<^sup>* \<and> y \<R>\<lbrakk>\<cdot>\<rbrakk>T<TRel> z \<and> P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> y \<Longrightarrow> P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> z
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>y z. (P, y) \<in> (indRelT TRel)\<^sup>* \<and> y \<R>\<lbrakk>\<cdot>\<rbrakk>T<TRel> z \<and> P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> y \<Longrightarrow> P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> z
[PROOF STEP]
case (step Q R)
[PROOF STATE]
proof (state)
this:
(P, Q) \<in> (indRelT TRel)\<^sup>*
Q \<R>\<lbrakk>\<cdot>\<rbrakk>T<TRel> R
P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q

goal (1 subgoal):
 1. \<And>y z. (P, y) \<in> (indRelT TRel)\<^sup>* \<and> y \<R>\<lbrakk>\<cdot>\<rbrakk>T<TRel> z \<and> P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> y \<Longrightarrow> P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> z
[PROOF STEP]
assume "P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q"
[PROOF STATE]
proof (state)
this:
P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q

goal (1 subgoal):
 1. \<And>y z. (P, y) \<in> (indRelT TRel)\<^sup>* \<and> y \<R>\<lbrakk>\<cdot>\<rbrakk>T<TRel> z \<and> P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> y \<Longrightarrow> P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> z
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q

goal (1 subgoal):
 1. \<And>y z. (P, y) \<in> (indRelT TRel)\<^sup>* \<and> y \<R>\<lbrakk>\<cdot>\<rbrakk>T<TRel> z \<and> P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> y \<Longrightarrow> P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> z
[PROOF STEP]
assume "Q \<R>\<lbrakk>\<cdot>\<rbrakk>T<TRel> R"
[PROOF STATE]
proof (state)
this:
Q \<R>\<lbrakk>\<cdot>\<rbrakk>T<TRel> R

goal (1 subgoal):
 1. \<And>y z. (P, y) \<in> (indRelT TRel)\<^sup>* \<and> y \<R>\<lbrakk>\<cdot>\<rbrakk>T<TRel> z \<and> P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> y \<Longrightarrow> P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> z
[PROOF STEP]
hence "Q \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> R"
[PROOF STATE]
proof (prove)
using this:
Q \<R>\<lbrakk>\<cdot>\<rbrakk>T<TRel> R

goal (1 subgoal):
 1. Q \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> R
[PROOF STEP]
by (induct, simp_all add: indRelTEQ.encR indRelTEQ.encL indRelTEQ.target)
[PROOF STATE]
proof (state)
this:
Q \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> R

goal (1 subgoal):
 1. \<And>y z. (P, y) \<in> (indRelT TRel)\<^sup>* \<and> y \<R>\<lbrakk>\<cdot>\<rbrakk>T<TRel> z \<and> P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> y \<Longrightarrow> P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> z
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q
Q \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> R
[PROOF STEP]
show "P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> R"
[PROOF STATE]
proof (prove)
using this:
P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q
Q \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> R

goal (1 subgoal):
 1. P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> R
[PROOF STEP]
by (rule indRelTEQ.trans)
[PROOF STATE]
proof (state)
this:
P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> R

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q

goal:
No subgoals!
[PROOF STEP]
qed