[STATEMENT]
lemma (in encoding) SOCom_iff_indRelRTPO_is_strong_reduction_simulation:
  fixes TRel :: "('procT \<times> 'procT) set"
  shows "(strongly_operational_complete (TRel\<^sup>*)
         \<and> strong_reduction_simulation (TRel\<^sup>+) Target)
         = strong_reduction_simulation (indRelRTPO TRel) (STCal Source Target)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<forall>S S'. S \<longmapsto>Source S' \<longrightarrow> (\<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*)) \<and> strong_reduction_simulation (TRel\<^sup>+) Target) = (\<forall>P Q P'. P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q \<and> P \<longmapsto>STCal Source Target P' \<longrightarrow> (\<exists>Q'. Q \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'))
[PROOF STEP]
proof (rule iffI, erule conjE)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (\<forall>S S'. S \<longmapsto>Source S' \<longrightarrow> (\<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*)) \<and> strong_reduction_simulation (TRel\<^sup>+) Target \<Longrightarrow> \<forall>P Q P'. P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q \<and> P \<longmapsto>STCal Source Target P' \<longrightarrow> (\<exists>Q'. Q \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q')
 2. \<forall>P Q P'. P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q \<and> P \<longmapsto>STCal Source Target P' \<longrightarrow> (\<exists>Q'. Q \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q') \<Longrightarrow> (\<forall>S S'. S \<longmapsto>Source S' \<longrightarrow> (\<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*)) \<and> strong_reduction_simulation (TRel\<^sup>+) Target
[PROOF STEP]
assume soc: "strongly_operational_complete (TRel\<^sup>*)"
     and sim: "strong_reduction_simulation (TRel\<^sup>+) Target"
[PROOF STATE]
proof (state)
this:
\<forall>S S'. S \<longmapsto>Source S' \<longrightarrow> (\<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*)
strong_reduction_simulation (TRel\<^sup>+) Target

goal (2 subgoals):
 1. (\<forall>S S'. S \<longmapsto>Source S' \<longrightarrow> (\<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*)) \<and> strong_reduction_simulation (TRel\<^sup>+) Target \<Longrightarrow> \<forall>P Q P'. P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q \<and> P \<longmapsto>STCal Source Target P' \<longrightarrow> (\<exists>Q'. Q \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q')
 2. \<forall>P Q P'. P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q \<and> P \<longmapsto>STCal Source Target P' \<longrightarrow> (\<exists>Q'. Q \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q') \<Longrightarrow> (\<forall>S S'. S \<longmapsto>Source S' \<longrightarrow> (\<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*)) \<and> strong_reduction_simulation (TRel\<^sup>+) Target
[PROOF STEP]
show "strong_reduction_simulation (indRelRTPO TRel) (STCal Source Target)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>P Q P'. P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q \<and> P \<longmapsto>STCal Source Target P' \<longrightarrow> (\<exists>Q'. Q \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q')
[PROOF STEP]
proof clarify
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>P Q P'. P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q \<and> P \<longmapsto>STCal Source Target P' \<Longrightarrow> \<exists>Q'. Q \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'
[PROOF STEP]
fix P Q P'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>P Q P'. P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q \<and> P \<longmapsto>STCal Source Target P' \<Longrightarrow> \<exists>Q'. Q \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'
[PROOF STEP]
assume "P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q" and "P \<longmapsto>(STCal Source Target) P'"
[PROOF STATE]
proof (state)
this:
P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q
P \<longmapsto>STCal Source Target P'

goal (1 subgoal):
 1. \<And>P Q P'. P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q \<and> P \<longmapsto>STCal Source Target P' \<Longrightarrow> \<exists>Q'. Q \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'
[PROOF STEP]
thus "\<exists>Q'. Q \<longmapsto>(STCal Source Target) Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'"
[PROOF STATE]
proof (prove)
using this:
P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q
P \<longmapsto>STCal Source Target P'

goal (1 subgoal):
 1. \<exists>Q'. Q \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'
[PROOF STEP]
proof (induct arbitrary: P')
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>S P'. SourceTerm S \<longmapsto>STCal Source Target P' \<Longrightarrow> \<exists>Q'. TargetTerm (\<lbrakk>S\<rbrakk>) \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'
 2. \<And>S P'. SourceTerm S \<longmapsto>STCal Source Target P' \<Longrightarrow> \<exists>Q'. SourceTerm S \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'
 3. \<And>T1 T2 P'. (T1, T2) \<in> TRel \<and> TargetTerm T1 \<longmapsto>STCal Source Target P' \<Longrightarrow> \<exists>Q'. TargetTerm T2 \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'
 4. \<And>P Q R P'. \<lbrakk>P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q; \<And>P'. P \<longmapsto>STCal Source Target P' \<Longrightarrow> \<exists>Q'. Q \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'; Q \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> R; \<And>P'. Q \<longmapsto>STCal Source Target P' \<Longrightarrow> \<exists>Q'. R \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'; P \<longmapsto>STCal Source Target P'\<rbrakk> \<Longrightarrow> \<exists>Q'. R \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'
[PROOF STEP]
case (encR S)
[PROOF STATE]
proof (state)
this:
SourceTerm S \<longmapsto>STCal Source Target P'

goal (4 subgoals):
 1. \<And>S P'. SourceTerm S \<longmapsto>STCal Source Target P' \<Longrightarrow> \<exists>Q'. TargetTerm (\<lbrakk>S\<rbrakk>) \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'
 2. \<And>S P'. SourceTerm S \<longmapsto>STCal Source Target P' \<Longrightarrow> \<exists>Q'. SourceTerm S \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'
 3. \<And>T1 T2 P'. (T1, T2) \<in> TRel \<and> TargetTerm T1 \<longmapsto>STCal Source Target P' \<Longrightarrow> \<exists>Q'. TargetTerm T2 \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'
 4. \<And>P Q R P'. \<lbrakk>P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q; \<And>P'. P \<longmapsto>STCal Source Target P' \<Longrightarrow> \<exists>Q'. Q \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'; Q \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> R; \<And>P'. Q \<longmapsto>STCal Source Target P' \<Longrightarrow> \<exists>Q'. R \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'; P \<longmapsto>STCal Source Target P'\<rbrakk> \<Longrightarrow> \<exists>Q'. R \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'
[PROOF STEP]
assume "SourceTerm S \<longmapsto>(STCal Source Target) P'"
[PROOF STATE]
proof (state)
this:
SourceTerm S \<longmapsto>STCal Source Target P'

goal (4 subgoals):
 1. \<And>S P'. SourceTerm S \<longmapsto>STCal Source Target P' \<Longrightarrow> \<exists>Q'. TargetTerm (\<lbrakk>S\<rbrakk>) \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'
 2. \<And>S P'. SourceTerm S \<longmapsto>STCal Source Target P' \<Longrightarrow> \<exists>Q'. SourceTerm S \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'
 3. \<And>T1 T2 P'. (T1, T2) \<in> TRel \<and> TargetTerm T1 \<longmapsto>STCal Source Target P' \<Longrightarrow> \<exists>Q'. TargetTerm T2 \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'
 4. \<And>P Q R P'. \<lbrakk>P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q; \<And>P'. P \<longmapsto>STCal Source Target P' \<Longrightarrow> \<exists>Q'. Q \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'; Q \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> R; \<And>P'. Q \<longmapsto>STCal Source Target P' \<Longrightarrow> \<exists>Q'. R \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'; P \<longmapsto>STCal Source Target P'\<rbrakk> \<Longrightarrow> \<exists>Q'. R \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
SourceTerm S \<longmapsto>STCal Source Target P'
[PROOF STEP]
obtain S' where A1: "S' \<in>S P'" and A2: "S \<longmapsto>Source S'"
[PROOF STATE]
proof (prove)
using this:
SourceTerm S \<longmapsto>STCal Source Target P'

goal (1 subgoal):
 1. (\<And>S'. S' \<in>S P' \<and> S \<longmapsto>Source S' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp add: STCal_step(1))
[PROOF STATE]
proof (state)
this:
S' \<in>S P'
S \<longmapsto>Source S'

goal (4 subgoals):
 1. \<And>S P'. SourceTerm S \<longmapsto>STCal Source Target P' \<Longrightarrow> \<exists>Q'. TargetTerm (\<lbrakk>S\<rbrakk>) \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'
 2. \<And>S P'. SourceTerm S \<longmapsto>STCal Source Target P' \<Longrightarrow> \<exists>Q'. SourceTerm S \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'
 3. \<And>T1 T2 P'. (T1, T2) \<in> TRel \<and> TargetTerm T1 \<longmapsto>STCal Source Target P' \<Longrightarrow> \<exists>Q'. TargetTerm T2 \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'
 4. \<And>P Q R P'. \<lbrakk>P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q; \<And>P'. P \<longmapsto>STCal Source Target P' \<Longrightarrow> \<exists>Q'. Q \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'; Q \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> R; \<And>P'. Q \<longmapsto>STCal Source Target P' \<Longrightarrow> \<exists>Q'. R \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'; P \<longmapsto>STCal Source Target P'\<rbrakk> \<Longrightarrow> \<exists>Q'. R \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'
[PROOF STEP]
from soc A2
[PROOF STATE]
proof (chain)
picking this:
\<forall>S S'. S \<longmapsto>Source S' \<longrightarrow> (\<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*)
S \<longmapsto>Source S'
[PROOF STEP]
obtain T where A3: "\<lbrakk>S\<rbrakk> \<longmapsto>Target T" and A4: "(\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*"
[PROOF STATE]
proof (prove)
using this:
\<forall>S S'. S \<longmapsto>Source S' \<longrightarrow> (\<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*)
S \<longmapsto>Source S'

goal (1 subgoal):
 1. (\<And>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>* \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<lbrakk>S\<rbrakk> \<longmapsto>Target T
(\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*

goal (4 subgoals):
 1. \<And>S P'. SourceTerm S \<longmapsto>STCal Source Target P' \<Longrightarrow> \<exists>Q'. TargetTerm (\<lbrakk>S\<rbrakk>) \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'
 2. \<And>S P'. SourceTerm S \<longmapsto>STCal Source Target P' \<Longrightarrow> \<exists>Q'. SourceTerm S \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'
 3. \<And>T1 T2 P'. (T1, T2) \<in> TRel \<and> TargetTerm T1 \<longmapsto>STCal Source Target P' \<Longrightarrow> \<exists>Q'. TargetTerm T2 \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'
 4. \<And>P Q R P'. \<lbrakk>P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q; \<And>P'. P \<longmapsto>STCal Source Target P' \<Longrightarrow> \<exists>Q'. Q \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'; Q \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> R; \<And>P'. Q \<longmapsto>STCal Source Target P' \<Longrightarrow> \<exists>Q'. R \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'; P \<longmapsto>STCal Source Target P'\<rbrakk> \<Longrightarrow> \<exists>Q'. R \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'
[PROOF STEP]
from A3
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>S\<rbrakk> \<longmapsto>Target T
[PROOF STEP]
have "TargetTerm (\<lbrakk>S\<rbrakk>) \<longmapsto>(STCal Source Target) (TargetTerm T)"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>S\<rbrakk> \<longmapsto>Target T

goal (1 subgoal):
 1. TargetTerm (\<lbrakk>S\<rbrakk>) \<longmapsto>STCal Source Target TargetTerm T
[PROOF STEP]
by (simp add: STCal_step(2))
[PROOF STATE]
proof (state)
this:
TargetTerm (\<lbrakk>S\<rbrakk>) \<longmapsto>STCal Source Target TargetTerm T

goal (4 subgoals):
 1. \<And>S P'. SourceTerm S \<longmapsto>STCal Source Target P' \<Longrightarrow> \<exists>Q'. TargetTerm (\<lbrakk>S\<rbrakk>) \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'
 2. \<And>S P'. SourceTerm S \<longmapsto>STCal Source Target P' \<Longrightarrow> \<exists>Q'. SourceTerm S \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'
 3. \<And>T1 T2 P'. (T1, T2) \<in> TRel \<and> TargetTerm T1 \<longmapsto>STCal Source Target P' \<Longrightarrow> \<exists>Q'. TargetTerm T2 \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'
 4. \<And>P Q R P'. \<lbrakk>P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q; \<And>P'. P \<longmapsto>STCal Source Target P' \<Longrightarrow> \<exists>Q'. Q \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'; Q \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> R; \<And>P'. Q \<longmapsto>STCal Source Target P' \<Longrightarrow> \<exists>Q'. R \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'; P \<longmapsto>STCal Source Target P'\<rbrakk> \<Longrightarrow> \<exists>Q'. R \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
TargetTerm (\<lbrakk>S\<rbrakk>) \<longmapsto>STCal Source Target TargetTerm T

goal (4 subgoals):
 1. \<And>S P'. SourceTerm S \<longmapsto>STCal Source Target P' \<Longrightarrow> \<exists>Q'. TargetTerm (\<lbrakk>S\<rbrakk>) \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'
 2. \<And>S P'. SourceTerm S \<longmapsto>STCal Source Target P' \<Longrightarrow> \<exists>Q'. SourceTerm S \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'
 3. \<And>T1 T2 P'. (T1, T2) \<in> TRel \<and> TargetTerm T1 \<longmapsto>STCal Source Target P' \<Longrightarrow> \<exists>Q'. TargetTerm T2 \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'
 4. \<And>P Q R P'. \<lbrakk>P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q; \<And>P'. P \<longmapsto>STCal Source Target P' \<Longrightarrow> \<exists>Q'. Q \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'; Q \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> R; \<And>P'. Q \<longmapsto>STCal Source Target P' \<Longrightarrow> \<exists>Q'. R \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'; P \<longmapsto>STCal Source Target P'\<rbrakk> \<Longrightarrow> \<exists>Q'. R \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'
[PROOF STEP]
have "P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm T
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm T
[PROOF STEP]
from A4
[PROOF STATE]
proof (chain)
picking this:
(\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*
[PROOF STEP]
have "\<lbrakk>S'\<rbrakk> = T \<or> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>+"
[PROOF STATE]
proof (prove)
using this:
(\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*

goal (1 subgoal):
 1. \<lbrakk>S'\<rbrakk> = T \<or> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>+
[PROOF STEP]
using rtrancl_eq_or_trancl[of "\<lbrakk>S'\<rbrakk>" T TRel]
[PROOF STATE]
proof (prove)
using this:
(\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*
((\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*) = (\<lbrakk>S'\<rbrakk> = T \<or> \<lbrakk>S'\<rbrakk> \<noteq> T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>+)

goal (1 subgoal):
 1. \<lbrakk>S'\<rbrakk> = T \<or> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>+
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<lbrakk>S'\<rbrakk> = T \<or> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>+

goal (1 subgoal):
 1. P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm T
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<lbrakk>S'\<rbrakk> = T \<or> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>+

goal (1 subgoal):
 1. P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm T
[PROOF STEP]
from A1
[PROOF STATE]
proof (chain)
picking this:
S' \<in>S P'
[PROOF STEP]
have A5: "P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm (\<lbrakk>S'\<rbrakk>)"
[PROOF STATE]
proof (prove)
using this:
S' \<in>S P'

goal (1 subgoal):
 1. P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm (\<lbrakk>S'\<rbrakk>)
[PROOF STEP]
by (simp add: indRelRTPO.encR)
[PROOF STATE]
proof (state)
this:
P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm (\<lbrakk>S'\<rbrakk>)

goal (1 subgoal):
 1. P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm T
[PROOF STEP]
hence "\<lbrakk>S'\<rbrakk> = T \<Longrightarrow> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm T"
[PROOF STATE]
proof (prove)
using this:
P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm (\<lbrakk>S'\<rbrakk>)

goal (1 subgoal):
 1. \<lbrakk>S'\<rbrakk> = T \<Longrightarrow> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm T
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<lbrakk>S'\<rbrakk> = T \<Longrightarrow> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm T

goal (1 subgoal):
 1. P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm T
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<lbrakk>S'\<rbrakk> = T \<Longrightarrow> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm T

goal (1 subgoal):
 1. P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm T
[PROOF STEP]
have "(\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>+ \<Longrightarrow> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>+ \<Longrightarrow> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm T
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>+ \<Longrightarrow> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm T
[PROOF STEP]
assume "(\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>+"
[PROOF STATE]
proof (state)
this:
(\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>+

goal (1 subgoal):
 1. (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>+ \<Longrightarrow> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm T
[PROOF STEP]
hence "TargetTerm (\<lbrakk>S'\<rbrakk>) \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm T"
[PROOF STATE]
proof (prove)
using this:
(\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>+

goal (1 subgoal):
 1. TargetTerm (\<lbrakk>S'\<rbrakk>) \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm T
[PROOF STEP]
proof induct
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>y. (\<lbrakk>S'\<rbrakk>, y) \<in> TRel \<Longrightarrow> TargetTerm (\<lbrakk>S'\<rbrakk>) \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm y
 2. \<And>y z. (\<lbrakk>S'\<rbrakk>, y) \<in> TRel\<^sup>+ \<and> (y, z) \<in> TRel \<and> TargetTerm (\<lbrakk>S'\<rbrakk>) \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm y \<Longrightarrow> TargetTerm (\<lbrakk>S'\<rbrakk>) \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm z
[PROOF STEP]
fix TQ
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>y. (\<lbrakk>S'\<rbrakk>, y) \<in> TRel \<Longrightarrow> TargetTerm (\<lbrakk>S'\<rbrakk>) \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm y
 2. \<And>y z. (\<lbrakk>S'\<rbrakk>, y) \<in> TRel\<^sup>+ \<and> (y, z) \<in> TRel \<and> TargetTerm (\<lbrakk>S'\<rbrakk>) \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm y \<Longrightarrow> TargetTerm (\<lbrakk>S'\<rbrakk>) \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm z
[PROOF STEP]
assume "(\<lbrakk>S'\<rbrakk>, TQ) \<in> TRel"
[PROOF STATE]
proof (state)
this:
(\<lbrakk>S'\<rbrakk>, TQ) \<in> TRel

goal (2 subgoals):
 1. \<And>y. (\<lbrakk>S'\<rbrakk>, y) \<in> TRel \<Longrightarrow> TargetTerm (\<lbrakk>S'\<rbrakk>) \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm y
 2. \<And>y z. (\<lbrakk>S'\<rbrakk>, y) \<in> TRel\<^sup>+ \<and> (y, z) \<in> TRel \<and> TargetTerm (\<lbrakk>S'\<rbrakk>) \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm y \<Longrightarrow> TargetTerm (\<lbrakk>S'\<rbrakk>) \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm z
[PROOF STEP]
thus "TargetTerm (\<lbrakk>S'\<rbrakk>) \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm TQ"
[PROOF STATE]
proof (prove)
using this:
(\<lbrakk>S'\<rbrakk>, TQ) \<in> TRel

goal (1 subgoal):
 1. TargetTerm (\<lbrakk>S'\<rbrakk>) \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm TQ
[PROOF STEP]
by (rule indRelRTPO.target)
[PROOF STATE]
proof (state)
this:
TargetTerm (\<lbrakk>S'\<rbrakk>) \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm TQ

goal (1 subgoal):
 1. \<And>y z. (\<lbrakk>S'\<rbrakk>, y) \<in> TRel\<^sup>+ \<and> (y, z) \<in> TRel \<and> TargetTerm (\<lbrakk>S'\<rbrakk>) \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm y \<Longrightarrow> TargetTerm (\<lbrakk>S'\<rbrakk>) \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm z
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>y z. (\<lbrakk>S'\<rbrakk>, y) \<in> TRel\<^sup>+ \<and> (y, z) \<in> TRel \<and> TargetTerm (\<lbrakk>S'\<rbrakk>) \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm y \<Longrightarrow> TargetTerm (\<lbrakk>S'\<rbrakk>) \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm z
[PROOF STEP]
case (step TQ TR)
[PROOF STATE]
proof (state)
this:
(\<lbrakk>S'\<rbrakk>, TQ) \<in> TRel\<^sup>+
(TQ, TR) \<in> TRel
TargetTerm (\<lbrakk>S'\<rbrakk>) \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm TQ

goal (1 subgoal):
 1. \<And>y z. (\<lbrakk>S'\<rbrakk>, y) \<in> TRel\<^sup>+ \<and> (y, z) \<in> TRel \<and> TargetTerm (\<lbrakk>S'\<rbrakk>) \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm y \<Longrightarrow> TargetTerm (\<lbrakk>S'\<rbrakk>) \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm z
[PROOF STEP]
assume "TargetTerm (\<lbrakk>S'\<rbrakk>) \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm TQ"
[PROOF STATE]
proof (state)
this:
TargetTerm (\<lbrakk>S'\<rbrakk>) \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm TQ

goal (1 subgoal):
 1. \<And>y z. (\<lbrakk>S'\<rbrakk>, y) \<in> TRel\<^sup>+ \<and> (y, z) \<in> TRel \<and> TargetTerm (\<lbrakk>S'\<rbrakk>) \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm y \<Longrightarrow> TargetTerm (\<lbrakk>S'\<rbrakk>) \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm z
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
TargetTerm (\<lbrakk>S'\<rbrakk>) \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm TQ

goal (1 subgoal):
 1. \<And>y z. (\<lbrakk>S'\<rbrakk>, y) \<in> TRel\<^sup>+ \<and> (y, z) \<in> TRel \<and> TargetTerm (\<lbrakk>S'\<rbrakk>) \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm y \<Longrightarrow> TargetTerm (\<lbrakk>S'\<rbrakk>) \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm z
[PROOF STEP]
assume "(TQ, TR) \<in> TRel"
[PROOF STATE]
proof (state)
this:
(TQ, TR) \<in> TRel

goal (1 subgoal):
 1. \<And>y z. (\<lbrakk>S'\<rbrakk>, y) \<in> TRel\<^sup>+ \<and> (y, z) \<in> TRel \<and> TargetTerm (\<lbrakk>S'\<rbrakk>) \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm y \<Longrightarrow> TargetTerm (\<lbrakk>S'\<rbrakk>) \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm z
[PROOF STEP]
hence "TargetTerm TQ \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm TR"
[PROOF STATE]
proof (prove)
using this:
(TQ, TR) \<in> TRel

goal (1 subgoal):
 1. TargetTerm TQ \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm TR
[PROOF STEP]
by (rule indRelRTPO.target)
[PROOF STATE]
proof (state)
this:
TargetTerm TQ \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm TR

goal (1 subgoal):
 1. \<And>y z. (\<lbrakk>S'\<rbrakk>, y) \<in> TRel\<^sup>+ \<and> (y, z) \<in> TRel \<and> TargetTerm (\<lbrakk>S'\<rbrakk>) \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm y \<Longrightarrow> TargetTerm (\<lbrakk>S'\<rbrakk>) \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm z
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
TargetTerm (\<lbrakk>S'\<rbrakk>) \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm TQ
TargetTerm TQ \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm TR
[PROOF STEP]
show "TargetTerm (\<lbrakk>S'\<rbrakk>) \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm TR"
[PROOF STATE]
proof (prove)
using this:
TargetTerm (\<lbrakk>S'\<rbrakk>) \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm TQ
TargetTerm TQ \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm TR

goal (1 subgoal):
 1. TargetTerm (\<lbrakk>S'\<rbrakk>) \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm TR
[PROOF STEP]
by (rule indRelRTPO.trans)
[PROOF STATE]
proof (state)
this:
TargetTerm (\<lbrakk>S'\<rbrakk>) \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm TR

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
TargetTerm (\<lbrakk>S'\<rbrakk>) \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm T

goal (1 subgoal):
 1. (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>+ \<Longrightarrow> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm T
[PROOF STEP]
with A5
[PROOF STATE]
proof (chain)
picking this:
P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm (\<lbrakk>S'\<rbrakk>)
TargetTerm (\<lbrakk>S'\<rbrakk>) \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm T
[PROOF STEP]
show "P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm T"
[PROOF STATE]
proof (prove)
using this:
P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm (\<lbrakk>S'\<rbrakk>)
TargetTerm (\<lbrakk>S'\<rbrakk>) \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm T

goal (1 subgoal):
 1. P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm T
[PROOF STEP]
by (rule indRelRTPO.trans)
[PROOF STATE]
proof (state)
this:
P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm T

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>+ \<Longrightarrow> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm T

goal (1 subgoal):
 1. P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm T
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>S'\<rbrakk> = T \<or> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>+
\<lbrakk>S'\<rbrakk> = T \<Longrightarrow> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm T
(\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>+ \<Longrightarrow> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm T
[PROOF STEP]
show "P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm T"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>S'\<rbrakk> = T \<or> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>+
\<lbrakk>S'\<rbrakk> = T \<Longrightarrow> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm T
(\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>+ \<Longrightarrow> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm T

goal (1 subgoal):
 1. P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm T
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm T

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

goal (4 subgoals):
 1. \<And>S P'. SourceTerm S \<longmapsto>STCal Source Target P' \<Longrightarrow> \<exists>Q'. TargetTerm (\<lbrakk>S\<rbrakk>) \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'
 2. \<And>S P'. SourceTerm S \<longmapsto>STCal Source Target P' \<Longrightarrow> \<exists>Q'. SourceTerm S \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'
 3. \<And>T1 T2 P'. (T1, T2) \<in> TRel \<and> TargetTerm T1 \<longmapsto>STCal Source Target P' \<Longrightarrow> \<exists>Q'. TargetTerm T2 \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'
 4. \<And>P Q R P'. \<lbrakk>P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q; \<And>P'. P \<longmapsto>STCal Source Target P' \<Longrightarrow> \<exists>Q'. Q \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'; Q \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> R; \<And>P'. Q \<longmapsto>STCal Source Target P' \<Longrightarrow> \<exists>Q'. R \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'; P \<longmapsto>STCal Source Target P'\<rbrakk> \<Longrightarrow> \<exists>Q'. R \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
TargetTerm (\<lbrakk>S\<rbrakk>) \<longmapsto>STCal Source Target TargetTerm T
P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm T
[PROOF STEP]
show "\<exists>Q'. TargetTerm (\<lbrakk>S\<rbrakk>) \<longmapsto>(STCal Source Target) Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'"
[PROOF STATE]
proof (prove)
using this:
TargetTerm (\<lbrakk>S\<rbrakk>) \<longmapsto>STCal Source Target TargetTerm T
P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm T

goal (1 subgoal):
 1. \<exists>Q'. TargetTerm (\<lbrakk>S\<rbrakk>) \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>Q'. TargetTerm (\<lbrakk>S\<rbrakk>) \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'

goal (3 subgoals):
 1. \<And>S P'. SourceTerm S \<longmapsto>STCal Source Target P' \<Longrightarrow> \<exists>Q'. SourceTerm S \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'
 2. \<And>T1 T2 P'. (T1, T2) \<in> TRel \<and> TargetTerm T1 \<longmapsto>STCal Source Target P' \<Longrightarrow> \<exists>Q'. TargetTerm T2 \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'
 3. \<And>P Q R P'. \<lbrakk>P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q; \<And>P'. P \<longmapsto>STCal Source Target P' \<Longrightarrow> \<exists>Q'. Q \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'; Q \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> R; \<And>P'. Q \<longmapsto>STCal Source Target P' \<Longrightarrow> \<exists>Q'. R \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'; P \<longmapsto>STCal Source Target P'\<rbrakk> \<Longrightarrow> \<exists>Q'. R \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>S P'. SourceTerm S \<longmapsto>STCal Source Target P' \<Longrightarrow> \<exists>Q'. SourceTerm S \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'
 2. \<And>T1 T2 P'. (T1, T2) \<in> TRel \<and> TargetTerm T1 \<longmapsto>STCal Source Target P' \<Longrightarrow> \<exists>Q'. TargetTerm T2 \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'
 3. \<And>P Q R P'. \<lbrakk>P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q; \<And>P'. P \<longmapsto>STCal Source Target P' \<Longrightarrow> \<exists>Q'. Q \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'; Q \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> R; \<And>P'. Q \<longmapsto>STCal Source Target P' \<Longrightarrow> \<exists>Q'. R \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'; P \<longmapsto>STCal Source Target P'\<rbrakk> \<Longrightarrow> \<exists>Q'. R \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'
[PROOF STEP]
case (source S)
[PROOF STATE]
proof (state)
this:
SourceTerm S \<longmapsto>STCal Source Target P'

goal (3 subgoals):
 1. \<And>S P'. SourceTerm S \<longmapsto>STCal Source Target P' \<Longrightarrow> \<exists>Q'. SourceTerm S \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'
 2. \<And>T1 T2 P'. (T1, T2) \<in> TRel \<and> TargetTerm T1 \<longmapsto>STCal Source Target P' \<Longrightarrow> \<exists>Q'. TargetTerm T2 \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'
 3. \<And>P Q R P'. \<lbrakk>P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q; \<And>P'. P \<longmapsto>STCal Source Target P' \<Longrightarrow> \<exists>Q'. Q \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'; Q \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> R; \<And>P'. Q \<longmapsto>STCal Source Target P' \<Longrightarrow> \<exists>Q'. R \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'; P \<longmapsto>STCal Source Target P'\<rbrakk> \<Longrightarrow> \<exists>Q'. R \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
SourceTerm S \<longmapsto>STCal Source Target P'
[PROOF STEP]
obtain S' where B1: "S' \<in>S P'"
[PROOF STATE]
proof (prove)
using this:
SourceTerm S \<longmapsto>STCal Source Target P'

goal (1 subgoal):
 1. (\<And>S'. S' \<in>S P' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp add: STCal_step(1))
[PROOF STATE]
proof (state)
this:
S' \<in>S P'

goal (3 subgoals):
 1. \<And>S P'. SourceTerm S \<longmapsto>STCal Source Target P' \<Longrightarrow> \<exists>Q'. SourceTerm S \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'
 2. \<And>T1 T2 P'. (T1, T2) \<in> TRel \<and> TargetTerm T1 \<longmapsto>STCal Source Target P' \<Longrightarrow> \<exists>Q'. TargetTerm T2 \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'
 3. \<And>P Q R P'. \<lbrakk>P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q; \<And>P'. P \<longmapsto>STCal Source Target P' \<Longrightarrow> \<exists>Q'. Q \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'; Q \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> R; \<And>P'. Q \<longmapsto>STCal Source Target P' \<Longrightarrow> \<exists>Q'. R \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'; P \<longmapsto>STCal Source Target P'\<rbrakk> \<Longrightarrow> \<exists>Q'. R \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'
[PROOF STEP]
hence "P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> P'"
[PROOF STATE]
proof (prove)
using this:
S' \<in>S P'

goal (1 subgoal):
 1. P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> P'
[PROOF STEP]
by (simp add: indRelRTPO.source)
[PROOF STATE]
proof (state)
this:
P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> P'

goal (3 subgoals):
 1. \<And>S P'. SourceTerm S \<longmapsto>STCal Source Target P' \<Longrightarrow> \<exists>Q'. SourceTerm S \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'
 2. \<And>T1 T2 P'. (T1, T2) \<in> TRel \<and> TargetTerm T1 \<longmapsto>STCal Source Target P' \<Longrightarrow> \<exists>Q'. TargetTerm T2 \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'
 3. \<And>P Q R P'. \<lbrakk>P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q; \<And>P'. P \<longmapsto>STCal Source Target P' \<Longrightarrow> \<exists>Q'. Q \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'; Q \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> R; \<And>P'. Q \<longmapsto>STCal Source Target P' \<Longrightarrow> \<exists>Q'. R \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'; P \<longmapsto>STCal Source Target P'\<rbrakk> \<Longrightarrow> \<exists>Q'. R \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'
[PROOF STEP]
with source
[PROOF STATE]
proof (chain)
picking this:
SourceTerm S \<longmapsto>STCal Source Target P'
P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> P'
[PROOF STEP]
show "\<exists>Q'. SourceTerm S \<longmapsto>(STCal Source Target) Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'"
[PROOF STATE]
proof (prove)
using this:
SourceTerm S \<longmapsto>STCal Source Target P'
P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> P'

goal (1 subgoal):
 1. \<exists>Q'. SourceTerm S \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>Q'. SourceTerm S \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'

goal (2 subgoals):
 1. \<And>T1 T2 P'. (T1, T2) \<in> TRel \<and> TargetTerm T1 \<longmapsto>STCal Source Target P' \<Longrightarrow> \<exists>Q'. TargetTerm T2 \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'
 2. \<And>P Q R P'. \<lbrakk>P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q; \<And>P'. P \<longmapsto>STCal Source Target P' \<Longrightarrow> \<exists>Q'. Q \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'; Q \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> R; \<And>P'. Q \<longmapsto>STCal Source Target P' \<Longrightarrow> \<exists>Q'. R \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'; P \<longmapsto>STCal Source Target P'\<rbrakk> \<Longrightarrow> \<exists>Q'. R \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>T1 T2 P'. (T1, T2) \<in> TRel \<and> TargetTerm T1 \<longmapsto>STCal Source Target P' \<Longrightarrow> \<exists>Q'. TargetTerm T2 \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'
 2. \<And>P Q R P'. \<lbrakk>P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q; \<And>P'. P \<longmapsto>STCal Source Target P' \<Longrightarrow> \<exists>Q'. Q \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'; Q \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> R; \<And>P'. Q \<longmapsto>STCal Source Target P' \<Longrightarrow> \<exists>Q'. R \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'; P \<longmapsto>STCal Source Target P'\<rbrakk> \<Longrightarrow> \<exists>Q'. R \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'
[PROOF STEP]
case (target T1 T2)
[PROOF STATE]
proof (state)
this:
(T1, T2) \<in> TRel
TargetTerm T1 \<longmapsto>STCal Source Target P'

goal (2 subgoals):
 1. \<And>T1 T2 P'. (T1, T2) \<in> TRel \<and> TargetTerm T1 \<longmapsto>STCal Source Target P' \<Longrightarrow> \<exists>Q'. TargetTerm T2 \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'
 2. \<And>P Q R P'. \<lbrakk>P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q; \<And>P'. P \<longmapsto>STCal Source Target P' \<Longrightarrow> \<exists>Q'. Q \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'; Q \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> R; \<And>P'. Q \<longmapsto>STCal Source Target P' \<Longrightarrow> \<exists>Q'. R \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'; P \<longmapsto>STCal Source Target P'\<rbrakk> \<Longrightarrow> \<exists>Q'. R \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'
[PROOF STEP]
assume "TargetTerm T1 \<longmapsto>(STCal Source Target) P'"
[PROOF STATE]
proof (state)
this:
TargetTerm T1 \<longmapsto>STCal Source Target P'

goal (2 subgoals):
 1. \<And>T1 T2 P'. (T1, T2) \<in> TRel \<and> TargetTerm T1 \<longmapsto>STCal Source Target P' \<Longrightarrow> \<exists>Q'. TargetTerm T2 \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'
 2. \<And>P Q R P'. \<lbrakk>P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q; \<And>P'. P \<longmapsto>STCal Source Target P' \<Longrightarrow> \<exists>Q'. Q \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'; Q \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> R; \<And>P'. Q \<longmapsto>STCal Source Target P' \<Longrightarrow> \<exists>Q'. R \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'; P \<longmapsto>STCal Source Target P'\<rbrakk> \<Longrightarrow> \<exists>Q'. R \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
TargetTerm T1 \<longmapsto>STCal Source Target P'
[PROOF STEP]
obtain T1' where C1: "T1' \<in>T P'" and C2: "T1 \<longmapsto>Target T1'"
[PROOF STATE]
proof (prove)
using this:
TargetTerm T1 \<longmapsto>STCal Source Target P'

goal (1 subgoal):
 1. (\<And>T1'. T1' \<in>T P' \<and> T1 \<longmapsto>Target T1' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp add: STCal_step(2))
[PROOF STATE]
proof (state)
this:
T1' \<in>T P'
T1 \<longmapsto>Target T1'

goal (2 subgoals):
 1. \<And>T1 T2 P'. (T1, T2) \<in> TRel \<and> TargetTerm T1 \<longmapsto>STCal Source Target P' \<Longrightarrow> \<exists>Q'. TargetTerm T2 \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'
 2. \<And>P Q R P'. \<lbrakk>P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q; \<And>P'. P \<longmapsto>STCal Source Target P' \<Longrightarrow> \<exists>Q'. Q \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'; Q \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> R; \<And>P'. Q \<longmapsto>STCal Source Target P' \<Longrightarrow> \<exists>Q'. R \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'; P \<longmapsto>STCal Source Target P'\<rbrakk> \<Longrightarrow> \<exists>Q'. R \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'
[PROOF STEP]
assume "(T1, T2) \<in> TRel"
[PROOF STATE]
proof (state)
this:
(T1, T2) \<in> TRel

goal (2 subgoals):
 1. \<And>T1 T2 P'. (T1, T2) \<in> TRel \<and> TargetTerm T1 \<longmapsto>STCal Source Target P' \<Longrightarrow> \<exists>Q'. TargetTerm T2 \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'
 2. \<And>P Q R P'. \<lbrakk>P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q; \<And>P'. P \<longmapsto>STCal Source Target P' \<Longrightarrow> \<exists>Q'. Q \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'; Q \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> R; \<And>P'. Q \<longmapsto>STCal Source Target P' \<Longrightarrow> \<exists>Q'. R \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'; P \<longmapsto>STCal Source Target P'\<rbrakk> \<Longrightarrow> \<exists>Q'. R \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'
[PROOF STEP]
hence "(T1, T2) \<in> TRel\<^sup>+"
[PROOF STATE]
proof (prove)
using this:
(T1, T2) \<in> TRel

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

goal (2 subgoals):
 1. \<And>T1 T2 P'. (T1, T2) \<in> TRel \<and> TargetTerm T1 \<longmapsto>STCal Source Target P' \<Longrightarrow> \<exists>Q'. TargetTerm T2 \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'
 2. \<And>P Q R P'. \<lbrakk>P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q; \<And>P'. P \<longmapsto>STCal Source Target P' \<Longrightarrow> \<exists>Q'. Q \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'; Q \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> R; \<And>P'. Q \<longmapsto>STCal Source Target P' \<Longrightarrow> \<exists>Q'. R \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'; P \<longmapsto>STCal Source Target P'\<rbrakk> \<Longrightarrow> \<exists>Q'. R \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'
[PROOF STEP]
with C2 sim
[PROOF STATE]
proof (chain)
picking this:
T1 \<longmapsto>Target T1'
strong_reduction_simulation (TRel\<^sup>+) Target
(T1, T2) \<in> TRel\<^sup>+
[PROOF STEP]
obtain T2' where C3: "T2 \<longmapsto>Target T2'" and C4: "(T1', T2') \<in> TRel\<^sup>+"
[PROOF STATE]
proof (prove)
using this:
T1 \<longmapsto>Target T1'
strong_reduction_simulation (TRel\<^sup>+) Target
(T1, T2) \<in> TRel\<^sup>+

goal (1 subgoal):
 1. (\<And>T2'. T2 \<longmapsto>Target T2' \<and> (T1', T2') \<in> TRel\<^sup>+ \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
T2 \<longmapsto>Target T2'
(T1', T2') \<in> TRel\<^sup>+

goal (2 subgoals):
 1. \<And>T1 T2 P'. (T1, T2) \<in> TRel \<and> TargetTerm T1 \<longmapsto>STCal Source Target P' \<Longrightarrow> \<exists>Q'. TargetTerm T2 \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'
 2. \<And>P Q R P'. \<lbrakk>P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q; \<And>P'. P \<longmapsto>STCal Source Target P' \<Longrightarrow> \<exists>Q'. Q \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'; Q \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> R; \<And>P'. Q \<longmapsto>STCal Source Target P' \<Longrightarrow> \<exists>Q'. R \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'; P \<longmapsto>STCal Source Target P'\<rbrakk> \<Longrightarrow> \<exists>Q'. R \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'
[PROOF STEP]
from C3
[PROOF STATE]
proof (chain)
picking this:
T2 \<longmapsto>Target T2'
[PROOF STEP]
have "TargetTerm T2 \<longmapsto>(STCal Source Target) (TargetTerm T2')"
[PROOF STATE]
proof (prove)
using this:
T2 \<longmapsto>Target T2'

goal (1 subgoal):
 1. TargetTerm T2 \<longmapsto>STCal Source Target TargetTerm T2'
[PROOF STEP]
by (simp add: STCal_step(2))
[PROOF STATE]
proof (state)
this:
TargetTerm T2 \<longmapsto>STCal Source Target TargetTerm T2'

goal (2 subgoals):
 1. \<And>T1 T2 P'. (T1, T2) \<in> TRel \<and> TargetTerm T1 \<longmapsto>STCal Source Target P' \<Longrightarrow> \<exists>Q'. TargetTerm T2 \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'
 2. \<And>P Q R P'. \<lbrakk>P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q; \<And>P'. P \<longmapsto>STCal Source Target P' \<Longrightarrow> \<exists>Q'. Q \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'; Q \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> R; \<And>P'. Q \<longmapsto>STCal Source Target P' \<Longrightarrow> \<exists>Q'. R \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'; P \<longmapsto>STCal Source Target P'\<rbrakk> \<Longrightarrow> \<exists>Q'. R \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
TargetTerm T2 \<longmapsto>STCal Source Target TargetTerm T2'

goal (2 subgoals):
 1. \<And>T1 T2 P'. (T1, T2) \<in> TRel \<and> TargetTerm T1 \<longmapsto>STCal Source Target P' \<Longrightarrow> \<exists>Q'. TargetTerm T2 \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'
 2. \<And>P Q R P'. \<lbrakk>P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q; \<And>P'. P \<longmapsto>STCal Source Target P' \<Longrightarrow> \<exists>Q'. Q \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'; Q \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> R; \<And>P'. Q \<longmapsto>STCal Source Target P' \<Longrightarrow> \<exists>Q'. R \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'; P \<longmapsto>STCal Source Target P'\<rbrakk> \<Longrightarrow> \<exists>Q'. R \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'
[PROOF STEP]
from C4
[PROOF STATE]
proof (chain)
picking this:
(T1', T2') \<in> TRel\<^sup>+
[PROOF STEP]
have "TargetTerm T1' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm T2'"
[PROOF STATE]
proof (prove)
using this:
(T1', T2') \<in> TRel\<^sup>+

goal (1 subgoal):
 1. TargetTerm T1' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm T2'
[PROOF STEP]
proof induct
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>y. (T1', y) \<in> TRel \<Longrightarrow> TargetTerm T1' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm y
 2. \<And>y z. (T1', y) \<in> TRel\<^sup>+ \<and> (y, z) \<in> TRel \<and> TargetTerm T1' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm y \<Longrightarrow> TargetTerm T1' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm z
[PROOF STEP]
fix T2'
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>y. (T1', y) \<in> TRel \<Longrightarrow> TargetTerm T1' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm y
 2. \<And>y z. (T1', y) \<in> TRel\<^sup>+ \<and> (y, z) \<in> TRel \<and> TargetTerm T1' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm y \<Longrightarrow> TargetTerm T1' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm z
[PROOF STEP]
assume "(T1', T2') \<in> TRel"
[PROOF STATE]
proof (state)
this:
(T1', T2') \<in> TRel

goal (2 subgoals):
 1. \<And>y. (T1', y) \<in> TRel \<Longrightarrow> TargetTerm T1' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm y
 2. \<And>y z. (T1', y) \<in> TRel\<^sup>+ \<and> (y, z) \<in> TRel \<and> TargetTerm T1' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm y \<Longrightarrow> TargetTerm T1' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm z
[PROOF STEP]
thus "TargetTerm T1' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm T2'"
[PROOF STATE]
proof (prove)
using this:
(T1', T2') \<in> TRel

goal (1 subgoal):
 1. TargetTerm T1' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm T2'
[PROOF STEP]
by (rule indRelRTPO.target)
[PROOF STATE]
proof (state)
this:
TargetTerm T1' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm T2'

goal (1 subgoal):
 1. \<And>y z. (T1', y) \<in> TRel\<^sup>+ \<and> (y, z) \<in> TRel \<and> TargetTerm T1' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm y \<Longrightarrow> TargetTerm T1' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm z
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>y z. (T1', y) \<in> TRel\<^sup>+ \<and> (y, z) \<in> TRel \<and> TargetTerm T1' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm y \<Longrightarrow> TargetTerm T1' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm z
[PROOF STEP]
case (step TQ TR)
[PROOF STATE]
proof (state)
this:
(T1', TQ) \<in> TRel\<^sup>+
(TQ, TR) \<in> TRel
TargetTerm T1' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm TQ

goal (1 subgoal):
 1. \<And>y z. (T1', y) \<in> TRel\<^sup>+ \<and> (y, z) \<in> TRel \<and> TargetTerm T1' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm y \<Longrightarrow> TargetTerm T1' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm z
[PROOF STEP]
assume "TargetTerm T1' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm TQ"
[PROOF STATE]
proof (state)
this:
TargetTerm T1' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm TQ

goal (1 subgoal):
 1. \<And>y z. (T1', y) \<in> TRel\<^sup>+ \<and> (y, z) \<in> TRel \<and> TargetTerm T1' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm y \<Longrightarrow> TargetTerm T1' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm z
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
TargetTerm T1' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm TQ

goal (1 subgoal):
 1. \<And>y z. (T1', y) \<in> TRel\<^sup>+ \<and> (y, z) \<in> TRel \<and> TargetTerm T1' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm y \<Longrightarrow> TargetTerm T1' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm z
[PROOF STEP]
assume "(TQ, TR) \<in> TRel"
[PROOF STATE]
proof (state)
this:
(TQ, TR) \<in> TRel

goal (1 subgoal):
 1. \<And>y z. (T1', y) \<in> TRel\<^sup>+ \<and> (y, z) \<in> TRel \<and> TargetTerm T1' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm y \<Longrightarrow> TargetTerm T1' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm z
[PROOF STEP]
hence "TargetTerm TQ \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm TR"
[PROOF STATE]
proof (prove)
using this:
(TQ, TR) \<in> TRel

goal (1 subgoal):
 1. TargetTerm TQ \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm TR
[PROOF STEP]
by (rule indRelRTPO.target)
[PROOF STATE]
proof (state)
this:
TargetTerm TQ \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm TR

goal (1 subgoal):
 1. \<And>y z. (T1', y) \<in> TRel\<^sup>+ \<and> (y, z) \<in> TRel \<and> TargetTerm T1' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm y \<Longrightarrow> TargetTerm T1' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm z
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
TargetTerm T1' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm TQ
TargetTerm TQ \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm TR
[PROOF STEP]
show "TargetTerm T1' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm TR"
[PROOF STATE]
proof (prove)
using this:
TargetTerm T1' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm TQ
TargetTerm TQ \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm TR

goal (1 subgoal):
 1. TargetTerm T1' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm TR
[PROOF STEP]
by (rule indRelRTPO.trans)
[PROOF STATE]
proof (state)
this:
TargetTerm T1' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm TR

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
TargetTerm T1' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm T2'

goal (2 subgoals):
 1. \<And>T1 T2 P'. (T1, T2) \<in> TRel \<and> TargetTerm T1 \<longmapsto>STCal Source Target P' \<Longrightarrow> \<exists>Q'. TargetTerm T2 \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'
 2. \<And>P Q R P'. \<lbrakk>P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q; \<And>P'. P \<longmapsto>STCal Source Target P' \<Longrightarrow> \<exists>Q'. Q \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'; Q \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> R; \<And>P'. Q \<longmapsto>STCal Source Target P' \<Longrightarrow> \<exists>Q'. R \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'; P \<longmapsto>STCal Source Target P'\<rbrakk> \<Longrightarrow> \<exists>Q'. R \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'
[PROOF STEP]
with C1
[PROOF STATE]
proof (chain)
picking this:
T1' \<in>T P'
TargetTerm T1' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm T2'
[PROOF STEP]
have "P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm T2'"
[PROOF STATE]
proof (prove)
using this:
T1' \<in>T P'
TargetTerm T1' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm T2'

goal (1 subgoal):
 1. P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm T2'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm T2'

goal (2 subgoals):
 1. \<And>T1 T2 P'. (T1, T2) \<in> TRel \<and> TargetTerm T1 \<longmapsto>STCal Source Target P' \<Longrightarrow> \<exists>Q'. TargetTerm T2 \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'
 2. \<And>P Q R P'. \<lbrakk>P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q; \<And>P'. P \<longmapsto>STCal Source Target P' \<Longrightarrow> \<exists>Q'. Q \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'; Q \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> R; \<And>P'. Q \<longmapsto>STCal Source Target P' \<Longrightarrow> \<exists>Q'. R \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'; P \<longmapsto>STCal Source Target P'\<rbrakk> \<Longrightarrow> \<exists>Q'. R \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
TargetTerm T2 \<longmapsto>STCal Source Target TargetTerm T2'
P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm T2'
[PROOF STEP]
show "\<exists>Q'. TargetTerm T2 \<longmapsto>(STCal Source Target) Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'"
[PROOF STATE]
proof (prove)
using this:
TargetTerm T2 \<longmapsto>STCal Source Target TargetTerm T2'
P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm T2'

goal (1 subgoal):
 1. \<exists>Q'. TargetTerm T2 \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>Q'. TargetTerm T2 \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'

goal (1 subgoal):
 1. \<And>P Q R P'. \<lbrakk>P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q; \<And>P'. P \<longmapsto>STCal Source Target P' \<Longrightarrow> \<exists>Q'. Q \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'; Q \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> R; \<And>P'. Q \<longmapsto>STCal Source Target P' \<Longrightarrow> \<exists>Q'. R \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'; P \<longmapsto>STCal Source Target P'\<rbrakk> \<Longrightarrow> \<exists>Q'. R \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>P Q R P'. \<lbrakk>P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q; \<And>P'. P \<longmapsto>STCal Source Target P' \<Longrightarrow> \<exists>Q'. Q \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'; Q \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> R; \<And>P'. Q \<longmapsto>STCal Source Target P' \<Longrightarrow> \<exists>Q'. R \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'; P \<longmapsto>STCal Source Target P'\<rbrakk> \<Longrightarrow> \<exists>Q'. R \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'
[PROOF STEP]
case (trans P Q R)
[PROOF STATE]
proof (state)
this:
P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q
P \<longmapsto>STCal Source Target ?P'3 \<Longrightarrow> \<exists>Q'. Q \<longmapsto>STCal Source Target Q' \<and> ?P'3 \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'
Q \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> R
Q \<longmapsto>STCal Source Target ?P'3 \<Longrightarrow> \<exists>Q'. R \<longmapsto>STCal Source Target Q' \<and> ?P'3 \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'
P \<longmapsto>STCal Source Target P'

goal (1 subgoal):
 1. \<And>P Q R P'. \<lbrakk>P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q; \<And>P'. P \<longmapsto>STCal Source Target P' \<Longrightarrow> \<exists>Q'. Q \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'; Q \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> R; \<And>P'. Q \<longmapsto>STCal Source Target P' \<Longrightarrow> \<exists>Q'. R \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'; P \<longmapsto>STCal Source Target P'\<rbrakk> \<Longrightarrow> \<exists>Q'. R \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'
[PROOF STEP]
assume "P \<longmapsto>(STCal Source Target) P'"
         and "\<And>P'. P \<longmapsto>(STCal Source Target) P'
              \<Longrightarrow> \<exists>Q'. Q \<longmapsto>(STCal Source Target) Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'"
[PROOF STATE]
proof (state)
this:
P \<longmapsto>STCal Source Target P'
P \<longmapsto>STCal Source Target ?P'3 \<Longrightarrow> \<exists>Q'. Q \<longmapsto>STCal Source Target Q' \<and> ?P'3 \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'

goal (1 subgoal):
 1. \<And>P Q R P'. \<lbrakk>P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q; \<And>P'. P \<longmapsto>STCal Source Target P' \<Longrightarrow> \<exists>Q'. Q \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'; Q \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> R; \<And>P'. Q \<longmapsto>STCal Source Target P' \<Longrightarrow> \<exists>Q'. R \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'; P \<longmapsto>STCal Source Target P'\<rbrakk> \<Longrightarrow> \<exists>Q'. R \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
P \<longmapsto>STCal Source Target P'
P \<longmapsto>STCal Source Target ?P'3 \<Longrightarrow> \<exists>Q'. Q \<longmapsto>STCal Source Target Q' \<and> ?P'3 \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'
[PROOF STEP]
obtain Q' where D1: "Q \<longmapsto>(STCal Source Target) Q'"
                            and D2: "P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'"
[PROOF STATE]
proof (prove)
using this:
P \<longmapsto>STCal Source Target P'
P \<longmapsto>STCal Source Target ?P'3 \<Longrightarrow> \<exists>Q'. Q \<longmapsto>STCal Source Target Q' \<and> ?P'3 \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'

goal (1 subgoal):
 1. (\<And>Q'. Q \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Q \<longmapsto>STCal Source Target Q'
P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'

goal (1 subgoal):
 1. \<And>P Q R P'. \<lbrakk>P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q; \<And>P'. P \<longmapsto>STCal Source Target P' \<Longrightarrow> \<exists>Q'. Q \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'; Q \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> R; \<And>P'. Q \<longmapsto>STCal Source Target P' \<Longrightarrow> \<exists>Q'. R \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'; P \<longmapsto>STCal Source Target P'\<rbrakk> \<Longrightarrow> \<exists>Q'. R \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'
[PROOF STEP]
assume "\<And>Q'. Q \<longmapsto>(STCal Source Target) Q'
              \<Longrightarrow> \<exists>R'. R \<longmapsto>(STCal Source Target) R' \<and> Q' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> R'"
[PROOF STATE]
proof (state)
this:
Q \<longmapsto>STCal Source Target ?Q'3 \<Longrightarrow> \<exists>R'. R \<longmapsto>STCal Source Target R' \<and> ?Q'3 \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> R'

goal (1 subgoal):
 1. \<And>P Q R P'. \<lbrakk>P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q; \<And>P'. P \<longmapsto>STCal Source Target P' \<Longrightarrow> \<exists>Q'. Q \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'; Q \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> R; \<And>P'. Q \<longmapsto>STCal Source Target P' \<Longrightarrow> \<exists>Q'. R \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'; P \<longmapsto>STCal Source Target P'\<rbrakk> \<Longrightarrow> \<exists>Q'. R \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'
[PROOF STEP]
with D1
[PROOF STATE]
proof (chain)
picking this:
Q \<longmapsto>STCal Source Target Q'
Q \<longmapsto>STCal Source Target ?Q'3 \<Longrightarrow> \<exists>R'. R \<longmapsto>STCal Source Target R' \<and> ?Q'3 \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> R'
[PROOF STEP]
obtain R' where D3: "R \<longmapsto>(STCal Source Target) R'"
                          and D4: "Q' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> R'"
[PROOF STATE]
proof (prove)
using this:
Q \<longmapsto>STCal Source Target Q'
Q \<longmapsto>STCal Source Target ?Q'3 \<Longrightarrow> \<exists>R'. R \<longmapsto>STCal Source Target R' \<and> ?Q'3 \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> R'

goal (1 subgoal):
 1. (\<And>R'. R \<longmapsto>STCal Source Target R' \<and> Q' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> R' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
R \<longmapsto>STCal Source Target R'
Q' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> R'

goal (1 subgoal):
 1. \<And>P Q R P'. \<lbrakk>P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q; \<And>P'. P \<longmapsto>STCal Source Target P' \<Longrightarrow> \<exists>Q'. Q \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'; Q \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> R; \<And>P'. Q \<longmapsto>STCal Source Target P' \<Longrightarrow> \<exists>Q'. R \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'; P \<longmapsto>STCal Source Target P'\<rbrakk> \<Longrightarrow> \<exists>Q'. R \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'
[PROOF STEP]
from D2 D4
[PROOF STATE]
proof (chain)
picking this:
P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'
Q' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> R'
[PROOF STEP]
have "P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> R'"
[PROOF STATE]
proof (prove)
using this:
P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'
Q' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> R'

goal (1 subgoal):
 1. P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> R'
[PROOF STEP]
by (rule indRelRTPO.trans)
[PROOF STATE]
proof (state)
this:
P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> R'

goal (1 subgoal):
 1. \<And>P Q R P'. \<lbrakk>P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q; \<And>P'. P \<longmapsto>STCal Source Target P' \<Longrightarrow> \<exists>Q'. Q \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'; Q \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> R; \<And>P'. Q \<longmapsto>STCal Source Target P' \<Longrightarrow> \<exists>Q'. R \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'; P \<longmapsto>STCal Source Target P'\<rbrakk> \<Longrightarrow> \<exists>Q'. R \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'
[PROOF STEP]
with D3
[PROOF STATE]
proof (chain)
picking this:
R \<longmapsto>STCal Source Target R'
P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> R'
[PROOF STEP]
show "\<exists>R'. R \<longmapsto>(STCal Source Target) R' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> R'"
[PROOF STATE]
proof (prove)
using this:
R \<longmapsto>STCal Source Target R'
P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> R'

goal (1 subgoal):
 1. \<exists>R'. R \<longmapsto>STCal Source Target R' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> R'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>R'. R \<longmapsto>STCal Source Target R' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> R'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>Q'. Q \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>P Q P'. P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q \<and> P \<longmapsto>STCal Source Target P' \<longrightarrow> (\<exists>Q'. Q \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q')

goal (1 subgoal):
 1. \<forall>P Q P'. P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q \<and> P \<longmapsto>STCal Source Target P' \<longrightarrow> (\<exists>Q'. Q \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q') \<Longrightarrow> (\<forall>S S'. S \<longmapsto>Source S' \<longrightarrow> (\<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*)) \<and> strong_reduction_simulation (TRel\<^sup>+) Target
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>P Q P'. P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q \<and> P \<longmapsto>STCal Source Target P' \<longrightarrow> (\<exists>Q'. Q \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q') \<Longrightarrow> (\<forall>S S'. S \<longmapsto>Source S' \<longrightarrow> (\<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*)) \<and> strong_reduction_simulation (TRel\<^sup>+) Target
[PROOF STEP]
have "\<forall>S. SourceTerm S \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm (\<lbrakk>S\<rbrakk>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>S. SourceTerm S \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm (\<lbrakk>S\<rbrakk>)
[PROOF STEP]
by (simp add: indRelRTPO.encR)
[PROOF STATE]
proof (state)
this:
\<forall>S. SourceTerm S \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm (\<lbrakk>S\<rbrakk>)

goal (1 subgoal):
 1. \<forall>P Q P'. P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q \<and> P \<longmapsto>STCal Source Target P' \<longrightarrow> (\<exists>Q'. Q \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q') \<Longrightarrow> (\<forall>S S'. S \<longmapsto>Source S' \<longrightarrow> (\<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*)) \<and> strong_reduction_simulation (TRel\<^sup>+) Target
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>S. SourceTerm S \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm (\<lbrakk>S\<rbrakk>)

goal (1 subgoal):
 1. \<forall>P Q P'. P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q \<and> P \<longmapsto>STCal Source Target P' \<longrightarrow> (\<exists>Q'. Q \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q') \<Longrightarrow> (\<forall>S S'. S \<longmapsto>Source S' \<longrightarrow> (\<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*)) \<and> strong_reduction_simulation (TRel\<^sup>+) Target
[PROOF STEP]
have "\<forall>S T. SourceTerm S \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm T \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel\<^sup>*"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>S T. SourceTerm S \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm T \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel\<^sup>*
[PROOF STEP]
using indRelRTPO_to_TRel(2)[where TRel="TRel"] trans_closure_of_TRel_refl_cond
[PROOF STATE]
proof (prove)
using this:
?P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> ?Q \<Longrightarrow> \<forall>SP TQ. SP \<in>S ?P \<and> TQ \<in>T ?Q \<longrightarrow> (\<lbrakk>SP\<rbrakk>, TQ) \<in> (TRel \<union> _Collect (T1, T2) (\<exists>S. T1 = \<lbrakk>S\<rbrakk> \<and> T2 = \<lbrakk>S\<rbrakk>))\<^sup>+
(?TP, ?TQ) \<in> (?TRel \<union> _Collect (T1, T2) (\<exists>S. T1 = \<lbrakk>S\<rbrakk> \<and> T2 = \<lbrakk>S\<rbrakk>))\<^sup>+ \<Longrightarrow> (?TP, ?TQ) \<in> ?TRel\<^sup>*

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

goal (1 subgoal):
 1. \<forall>P Q P'. P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q \<and> P \<longmapsto>STCal Source Target P' \<longrightarrow> (\<exists>Q'. Q \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q') \<Longrightarrow> (\<forall>S S'. S \<longmapsto>Source S' \<longrightarrow> (\<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*)) \<and> strong_reduction_simulation (TRel\<^sup>+) Target
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>S T. SourceTerm S \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm T \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel\<^sup>*

goal (1 subgoal):
 1. \<forall>P Q P'. P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q \<and> P \<longmapsto>STCal Source Target P' \<longrightarrow> (\<exists>Q'. Q \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q') \<Longrightarrow> (\<forall>S S'. S \<longmapsto>Source S' \<longrightarrow> (\<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*)) \<and> strong_reduction_simulation (TRel\<^sup>+) Target
[PROOF STEP]
assume sim: "strong_reduction_simulation (indRelRTPO TRel) (STCal Source Target)"
[PROOF STATE]
proof (state)
this:
\<forall>P Q P'. P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q \<and> P \<longmapsto>STCal Source Target P' \<longrightarrow> (\<exists>Q'. Q \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q')

goal (1 subgoal):
 1. \<forall>P Q P'. P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q \<and> P \<longmapsto>STCal Source Target P' \<longrightarrow> (\<exists>Q'. Q \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q') \<Longrightarrow> (\<forall>S S'. S \<longmapsto>Source S' \<longrightarrow> (\<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*)) \<and> strong_reduction_simulation (TRel\<^sup>+) Target
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<forall>S. SourceTerm S \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm (\<lbrakk>S\<rbrakk>)
\<forall>S T. SourceTerm S \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm T \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel\<^sup>*
\<forall>P Q P'. P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q \<and> P \<longmapsto>STCal Source Target P' \<longrightarrow> (\<exists>Q'. Q \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q')
[PROOF STEP]
have "strongly_operational_complete (TRel\<^sup>*)"
[PROOF STATE]
proof (prove)
using this:
\<forall>S. SourceTerm S \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm (\<lbrakk>S\<rbrakk>)
\<forall>S T. SourceTerm S \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm T \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel\<^sup>*
\<forall>P Q P'. P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q \<and> P \<longmapsto>STCal Source Target P' \<longrightarrow> (\<exists>Q'. Q \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q')

goal (1 subgoal):
 1. \<forall>S S'. S \<longmapsto>Source S' \<longrightarrow> (\<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*)
[PROOF STEP]
using strong_reduction_simulation_impl_SOCom[where Rel="indRelRTPO TRel" and TRel="TRel"]
[PROOF STATE]
proof (prove)
using this:
\<forall>S. SourceTerm S \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm (\<lbrakk>S\<rbrakk>)
\<forall>S T. SourceTerm S \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm T \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel\<^sup>*
\<forall>P Q P'. P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q \<and> P \<longmapsto>STCal Source Target P' \<longrightarrow> (\<exists>Q'. Q \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q')
(\<forall>S. SourceTerm S \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm (\<lbrakk>S\<rbrakk>)) \<and> (\<forall>S T. SourceTerm S \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm T \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel\<^sup>*) \<and> (\<forall>P Q P'. P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q \<and> P \<longmapsto>STCal Source Target P' \<longrightarrow> (\<exists>Q'. Q \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q')) \<Longrightarrow> \<forall>S S'. S \<longmapsto>Source S' \<longrightarrow> (\<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*)

goal (1 subgoal):
 1. \<forall>S S'. S \<longmapsto>Source S' \<longrightarrow> (\<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>S S'. S \<longmapsto>Source S' \<longrightarrow> (\<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*)

goal (1 subgoal):
 1. \<forall>P Q P'. P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q \<and> P \<longmapsto>STCal Source Target P' \<longrightarrow> (\<exists>Q'. Q \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q') \<Longrightarrow> (\<forall>S S'. S \<longmapsto>Source S' \<longrightarrow> (\<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*)) \<and> strong_reduction_simulation (TRel\<^sup>+) Target
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>S S'. S \<longmapsto>Source S' \<longrightarrow> (\<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*)

goal (1 subgoal):
 1. \<forall>P Q P'. P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q \<and> P \<longmapsto>STCal Source Target P' \<longrightarrow> (\<exists>Q'. Q \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q') \<Longrightarrow> (\<forall>S S'. S \<longmapsto>Source S' \<longrightarrow> (\<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*)) \<and> strong_reduction_simulation (TRel\<^sup>+) Target
[PROOF STEP]
from sim
[PROOF STATE]
proof (chain)
picking this:
\<forall>P Q P'. P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q \<and> P \<longmapsto>STCal Source Target P' \<longrightarrow> (\<exists>Q'. Q \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q')
[PROOF STEP]
have "strong_reduction_simulation (TRel\<^sup>+) Target"
[PROOF STATE]
proof (prove)
using this:
\<forall>P Q P'. P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q \<and> P \<longmapsto>STCal Source Target P' \<longrightarrow> (\<exists>Q'. Q \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q')

goal (1 subgoal):
 1. strong_reduction_simulation (TRel\<^sup>+) Target
[PROOF STEP]
using indRelRTPO_impl_TRel_is_strong_reduction_simulation[where TRel="TRel"]
[PROOF STATE]
proof (prove)
using this:
\<forall>P Q P'. P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q \<and> P \<longmapsto>STCal Source Target P' \<longrightarrow> (\<exists>Q'. Q \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q')
\<forall>P Q P'. P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q \<and> P \<longmapsto>STCal Source Target P' \<longrightarrow> (\<exists>Q'. Q \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q') \<Longrightarrow> strong_reduction_simulation (TRel\<^sup>+) Target

goal (1 subgoal):
 1. strong_reduction_simulation (TRel\<^sup>+) Target
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
strong_reduction_simulation (TRel\<^sup>+) Target

goal (1 subgoal):
 1. \<forall>P Q P'. P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q \<and> P \<longmapsto>STCal Source Target P' \<longrightarrow> (\<exists>Q'. Q \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q') \<Longrightarrow> (\<forall>S S'. S \<longmapsto>Source S' \<longrightarrow> (\<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*)) \<and> strong_reduction_simulation (TRel\<^sup>+) Target
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<forall>S S'. S \<longmapsto>Source S' \<longrightarrow> (\<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*)
strong_reduction_simulation (TRel\<^sup>+) Target
[PROOF STEP]
show "strongly_operational_complete (TRel\<^sup>*)
                   \<and> strong_reduction_simulation (TRel\<^sup>+) Target"
[PROOF STATE]
proof (prove)
using this:
\<forall>S S'. S \<longmapsto>Source S' \<longrightarrow> (\<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*)
strong_reduction_simulation (TRel\<^sup>+) Target

goal (1 subgoal):
 1. (\<forall>S S'. S \<longmapsto>Source S' \<longrightarrow> (\<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*)) \<and> strong_reduction_simulation (TRel\<^sup>+) Target
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<forall>S S'. S \<longmapsto>Source S' \<longrightarrow> (\<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*)) \<and> strong_reduction_simulation (TRel\<^sup>+) Target

goal:
No subgoals!
[PROOF STEP]
qed