[STATEMENT]
lemma (in encoding) WOC_iff_indRelRTPO_is_reduction_correspondence_simulation:
  fixes TRel :: "('procT \<times> 'procT) set"
  shows "(weakly_operational_corresponding (TRel\<^sup>*)
         \<and> weak_reduction_correspondence_simulation (TRel\<^sup>+) Target)
         = weak_reduction_correspondence_simulation (indRelRTPO TRel) (STCal Source Target)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (weakly_operational_corresponding (TRel\<^sup>*) \<and> weak_reduction_correspondence_simulation (TRel\<^sup>+) Target) = weak_reduction_correspondence_simulation (indRelRTPO TRel) (STCal Source Target)
[PROOF STEP]
proof (rule iffI, erule conjE)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. weakly_operational_corresponding (TRel\<^sup>*) \<and> weak_reduction_correspondence_simulation (TRel\<^sup>+) Target \<Longrightarrow> weak_reduction_correspondence_simulation (indRelRTPO TRel) (STCal Source Target)
 2. weak_reduction_correspondence_simulation (indRelRTPO TRel) (STCal Source Target) \<Longrightarrow> weakly_operational_corresponding (TRel\<^sup>*) \<and> weak_reduction_correspondence_simulation (TRel\<^sup>+) Target
[PROOF STEP]
assume woc: "weakly_operational_corresponding (TRel\<^sup>*)"
     and csi: "weak_reduction_correspondence_simulation (TRel\<^sup>+) Target"
[PROOF STATE]
proof (state)
this:
weakly_operational_corresponding (TRel\<^sup>*)
weak_reduction_correspondence_simulation (TRel\<^sup>+) Target

goal (2 subgoals):
 1. weakly_operational_corresponding (TRel\<^sup>*) \<and> weak_reduction_correspondence_simulation (TRel\<^sup>+) Target \<Longrightarrow> weak_reduction_correspondence_simulation (indRelRTPO TRel) (STCal Source Target)
 2. weak_reduction_correspondence_simulation (indRelRTPO TRel) (STCal Source Target) \<Longrightarrow> weakly_operational_corresponding (TRel\<^sup>*) \<and> weak_reduction_correspondence_simulation (TRel\<^sup>+) Target
[PROOF STEP]
show "weak_reduction_correspondence_simulation (indRelRTPO TRel) (STCal Source Target)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. weak_reduction_correspondence_simulation (indRelRTPO TRel) (STCal Source Target)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. weak_reduction_simulation (indRelRTPO TRel) (STCal Source Target)
 2. \<forall>P Q Q'. P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q \<and> Q \<longmapsto>STCal Source Target* Q' \<longrightarrow> (\<exists>P'' Q''. P \<longmapsto>STCal Source Target* P'' \<and> Q' \<longmapsto>STCal Source Target* Q'' \<and> P'' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'')
[PROOF STEP]
from woc csi
[PROOF STATE]
proof (chain)
picking this:
weakly_operational_corresponding (TRel\<^sup>*)
weak_reduction_correspondence_simulation (TRel\<^sup>+) Target
[PROOF STEP]
show sim: "weak_reduction_simulation (indRelRTPO TRel) (STCal Source Target)"
[PROOF STATE]
proof (prove)
using this:
weakly_operational_corresponding (TRel\<^sup>*)
weak_reduction_correspondence_simulation (TRel\<^sup>+) Target

goal (1 subgoal):
 1. weak_reduction_simulation (indRelRTPO TRel) (STCal Source Target)
[PROOF STEP]
using OCom_iff_indRelRTPO_is_weak_reduction_simulation[where TRel="TRel"]
[PROOF STATE]
proof (prove)
using this:
weakly_operational_corresponding (TRel\<^sup>*)
weak_reduction_correspondence_simulation (TRel\<^sup>+) Target
(operational_complete (TRel\<^sup>*) \<and> weak_reduction_simulation (TRel\<^sup>+) Target) = weak_reduction_simulation (indRelRTPO TRel) (STCal Source Target)

goal (1 subgoal):
 1. weak_reduction_simulation (indRelRTPO TRel) (STCal Source Target)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
weak_reduction_simulation (indRelRTPO TRel) (STCal Source Target)

goal (1 subgoal):
 1. \<forall>P Q Q'. P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q \<and> Q \<longmapsto>STCal Source Target* Q' \<longrightarrow> (\<exists>P'' Q''. P \<longmapsto>STCal Source Target* P'' \<and> Q' \<longmapsto>STCal Source Target* Q'' \<and> P'' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'')
[PROOF STEP]
show "\<forall>P Q Q'. P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q \<and> Q \<longmapsto>(STCal Source Target)* Q'
          \<longrightarrow> (\<exists>P'' Q''. P \<longmapsto>(STCal Source Target)* P'' \<and> Q' \<longmapsto>(STCal Source Target)* Q''
          \<and> P'' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>P Q Q'. P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q \<and> Q \<longmapsto>STCal Source Target* Q' \<longrightarrow> (\<exists>P'' Q''. P \<longmapsto>STCal Source Target* P'' \<and> 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 Q'. P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q \<and> Q \<longmapsto>STCal Source Target* Q' \<Longrightarrow> \<exists>P'' Q''. P \<longmapsto>STCal Source Target* P'' \<and> Q' \<longmapsto>STCal Source Target* Q'' \<and> P'' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q''
[PROOF STEP]
fix P Q Q'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>P Q Q'. P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q \<and> Q \<longmapsto>STCal Source Target* Q' \<Longrightarrow> \<exists>P'' Q''. P \<longmapsto>STCal Source Target* P'' \<and> 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 "Q \<longmapsto>(STCal Source Target)* Q'"
[PROOF STATE]
proof (state)
this:
P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q
Q \<longmapsto>STCal Source Target* Q'

goal (1 subgoal):
 1. \<And>P Q Q'. P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q \<and> Q \<longmapsto>STCal Source Target* Q' \<Longrightarrow> \<exists>P'' Q''. P \<longmapsto>STCal Source Target* P'' \<and> Q' \<longmapsto>STCal Source Target* Q'' \<and> P'' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q''
[PROOF STEP]
thus "\<exists>P'' Q''. P \<longmapsto>(STCal Source Target)* P'' \<and> 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
Q \<longmapsto>STCal Source Target* Q'

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

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

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

goal (1 subgoal):
 1. (\<And>T. T \<in>T Q' \<and> \<lbrakk>S\<rbrakk> \<longmapsto>Target* T \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp add: STCal_steps(2))
[PROOF STATE]
proof (state)
this:
T \<in>T Q'
\<lbrakk>S\<rbrakk> \<longmapsto>Target* T

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

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

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

goal (1 subgoal):
 1. SourceTerm S \<longmapsto>STCal Source Target* SourceTerm S'
[PROOF STEP]
by (simp add: STCal_steps(1))
[PROOF STATE]
proof (state)
this:
SourceTerm S \<longmapsto>STCal Source Target* SourceTerm S'

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

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

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

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

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

goal (1 subgoal):
 1. SourceTerm S' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm T'
[PROOF STEP]
from A5
[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. SourceTerm S' \<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. SourceTerm S' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm T'
[PROOF STEP]
from A6
[PROOF STATE]
proof (chain)
picking this:
SourceTerm S' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm (\<lbrakk>S'\<rbrakk>)
[PROOF STEP]
have "\<lbrakk>S'\<rbrakk> = T' \<Longrightarrow> SourceTerm S' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm T'"
[PROOF STATE]
proof (prove)
using this:
SourceTerm S' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm (\<lbrakk>S'\<rbrakk>)

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

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

goal (1 subgoal):
 1. SourceTerm S' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm T'
[PROOF STEP]
have "(\<lbrakk>S'\<rbrakk>, T') \<in> TRel\<^sup>+ \<Longrightarrow> SourceTerm S' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm T'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>S'\<rbrakk>, T') \<in> TRel\<^sup>+ \<Longrightarrow> SourceTerm S' \<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> SourceTerm S' \<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> SourceTerm S' \<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]
by (simp add: transitive_closure_of_TRel_to_indRelRTPO[where TRel="TRel"])
[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> SourceTerm S' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm T'
[PROOF STEP]
with A6
[PROOF STATE]
proof (chain)
picking this:
SourceTerm S' \<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 "SourceTerm S' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm T'"
[PROOF STATE]
proof (prove)
using this:
SourceTerm S' \<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. SourceTerm S' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm T'
[PROOF STEP]
by (rule indRelRTPO.trans)
[PROOF STATE]
proof (state)
this:
SourceTerm S' \<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> SourceTerm S' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm T'

goal (1 subgoal):
 1. SourceTerm S' \<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> SourceTerm S' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm T'
(\<lbrakk>S'\<rbrakk>, T') \<in> TRel\<^sup>+ \<Longrightarrow> SourceTerm S' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm T'
[PROOF STEP]
show "SourceTerm S' \<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> SourceTerm S' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm T'
(\<lbrakk>S'\<rbrakk>, T') \<in> TRel\<^sup>+ \<Longrightarrow> SourceTerm S' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm T'

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

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

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

goal (1 subgoal):
 1. \<exists>P'' Q''. SourceTerm S \<longmapsto>STCal Source Target* P'' \<and> Q' \<longmapsto>STCal Source Target* Q'' \<and> P'' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q''
[PROOF STEP]
using A1
[PROOF STATE]
proof (prove)
using this:
SourceTerm S \<longmapsto>STCal Source Target* SourceTerm S'
TargetTerm T \<longmapsto>STCal Source Target* TargetTerm T'
SourceTerm S' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm T'
T \<in>T Q'

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

goal (3 subgoals):
 1. \<And>S Q'. SourceTerm S \<longmapsto>STCal Source Target* Q' \<Longrightarrow> \<exists>P'' Q''. SourceTerm S \<longmapsto>STCal Source Target* P'' \<and> Q' \<longmapsto>STCal Source Target* Q'' \<and> P'' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q''
 2. \<And>T1 T2 Q'. (T1, T2) \<in> TRel \<and> TargetTerm T2 \<longmapsto>STCal Source Target* Q' \<Longrightarrow> \<exists>P'' Q''. TargetTerm T1 \<longmapsto>STCal Source Target* P'' \<and> Q' \<longmapsto>STCal Source Target* Q'' \<and> P'' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q''
 3. \<And>P Q R Q'. \<lbrakk>P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q; \<And>Q'. Q \<longmapsto>STCal Source Target* Q' \<Longrightarrow> \<exists>P'' Q''. P \<longmapsto>STCal Source Target* P'' \<and> Q' \<longmapsto>STCal Source Target* Q'' \<and> P'' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q''; Q \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> R; \<And>Q'. R \<longmapsto>STCal Source Target* Q' \<Longrightarrow> \<exists>P'' Q''. Q \<longmapsto>STCal Source Target* P'' \<and> Q' \<longmapsto>STCal Source Target* Q'' \<and> P'' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q''; R \<longmapsto>STCal Source Target* Q'\<rbrakk> \<Longrightarrow> \<exists>P'' Q''. P \<longmapsto>STCal Source Target* P'' \<and> Q' \<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 Q'. SourceTerm S \<longmapsto>STCal Source Target* Q' \<Longrightarrow> \<exists>P'' Q''. SourceTerm S \<longmapsto>STCal Source Target* P'' \<and> Q' \<longmapsto>STCal Source Target* Q'' \<and> P'' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q''
 2. \<And>T1 T2 Q'. (T1, T2) \<in> TRel \<and> TargetTerm T2 \<longmapsto>STCal Source Target* Q' \<Longrightarrow> \<exists>P'' Q''. TargetTerm T1 \<longmapsto>STCal Source Target* P'' \<and> Q' \<longmapsto>STCal Source Target* Q'' \<and> P'' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q''
 3. \<And>P Q R Q'. \<lbrakk>P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q; \<And>Q'. Q \<longmapsto>STCal Source Target* Q' \<Longrightarrow> \<exists>P'' Q''. P \<longmapsto>STCal Source Target* P'' \<and> Q' \<longmapsto>STCal Source Target* Q'' \<and> P'' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q''; Q \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> R; \<And>Q'. R \<longmapsto>STCal Source Target* Q' \<Longrightarrow> \<exists>P'' Q''. Q \<longmapsto>STCal Source Target* P'' \<and> Q' \<longmapsto>STCal Source Target* Q'' \<and> P'' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q''; R \<longmapsto>STCal Source Target* Q'\<rbrakk> \<Longrightarrow> \<exists>P'' Q''. P \<longmapsto>STCal Source Target* P'' \<and> Q' \<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* Q'

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

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

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

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

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

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

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

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

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

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

goal (2 subgoals):
 1. \<And>T1 T2 Q'. (T1, T2) \<in> TRel \<and> TargetTerm T2 \<longmapsto>STCal Source Target* Q' \<Longrightarrow> \<exists>P'' Q''. TargetTerm T1 \<longmapsto>STCal Source Target* P'' \<and> Q' \<longmapsto>STCal Source Target* Q'' \<and> P'' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q''
 2. \<And>P Q R Q'. \<lbrakk>P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q; \<And>Q'. Q \<longmapsto>STCal Source Target* Q' \<Longrightarrow> \<exists>P'' Q''. P \<longmapsto>STCal Source Target* P'' \<and> Q' \<longmapsto>STCal Source Target* Q'' \<and> P'' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q''; Q \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> R; \<And>Q'. R \<longmapsto>STCal Source Target* Q' \<Longrightarrow> \<exists>P'' Q''. Q \<longmapsto>STCal Source Target* P'' \<and> Q' \<longmapsto>STCal Source Target* Q'' \<and> P'' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q''; R \<longmapsto>STCal Source Target* Q'\<rbrakk> \<Longrightarrow> \<exists>P'' Q''. P \<longmapsto>STCal Source Target* P'' \<and> Q' \<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 Q'. (T1, T2) \<in> TRel \<and> TargetTerm T2 \<longmapsto>STCal Source Target* Q' \<Longrightarrow> \<exists>P'' Q''. TargetTerm T1 \<longmapsto>STCal Source Target* P'' \<and> Q' \<longmapsto>STCal Source Target* Q'' \<and> P'' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q''
 2. \<And>P Q R Q'. \<lbrakk>P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q; \<And>Q'. Q \<longmapsto>STCal Source Target* Q' \<Longrightarrow> \<exists>P'' Q''. P \<longmapsto>STCal Source Target* P'' \<and> Q' \<longmapsto>STCal Source Target* Q'' \<and> P'' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q''; Q \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> R; \<And>Q'. R \<longmapsto>STCal Source Target* Q' \<Longrightarrow> \<exists>P'' Q''. Q \<longmapsto>STCal Source Target* P'' \<and> Q' \<longmapsto>STCal Source Target* Q'' \<and> P'' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q''; R \<longmapsto>STCal Source Target* Q'\<rbrakk> \<Longrightarrow> \<exists>P'' Q''. P \<longmapsto>STCal Source Target* P'' \<and> Q' \<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 T2 \<longmapsto>STCal Source Target* Q'

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

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

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

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

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

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

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

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

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

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

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

goal (2 subgoals):
 1. \<And>T1 T2 Q'. (T1, T2) \<in> TRel \<and> TargetTerm T2 \<longmapsto>STCal Source Target* Q' \<Longrightarrow> \<exists>P'' Q''. TargetTerm T1 \<longmapsto>STCal Source Target* P'' \<and> Q' \<longmapsto>STCal Source Target* Q'' \<and> P'' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q''
 2. \<And>P Q R Q'. \<lbrakk>P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q; \<And>Q'. Q \<longmapsto>STCal Source Target* Q' \<Longrightarrow> \<exists>P'' Q''. P \<longmapsto>STCal Source Target* P'' \<and> Q' \<longmapsto>STCal Source Target* Q'' \<and> P'' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q''; Q \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> R; \<And>Q'. R \<longmapsto>STCal Source Target* Q' \<Longrightarrow> \<exists>P'' Q''. Q \<longmapsto>STCal Source Target* P'' \<and> Q' \<longmapsto>STCal Source Target* Q'' \<and> P'' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q''; R \<longmapsto>STCal Source Target* Q'\<rbrakk> \<Longrightarrow> \<exists>P'' Q''. P \<longmapsto>STCal Source Target* P'' \<and> Q' \<longmapsto>STCal Source Target* Q'' \<and> P'' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q''
[PROOF STEP]
from C5
[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]
by (simp add: transitive_closure_of_TRel_to_indRelRTPO)
[PROOF STATE]
proof (state)
this:
TargetTerm T1' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm T2''

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

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

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

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

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

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

goal (1 subgoal):
 1. trans (indRelRTPO TRel)
[PROOF STEP]
unfolding trans_def
[PROOF STATE]
proof (prove)
using this:
?P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<?TRel> ?Q \<and> ?Q \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<?TRel> ?R \<Longrightarrow> ?P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<?TRel> ?R

goal (1 subgoal):
 1. \<forall>x y z. x \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> y \<longrightarrow> y \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> z \<longrightarrow> x \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> z
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
trans (indRelRTPO TRel)

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

goal (1 subgoal):
 1. \<exists>P'' Q''. P \<longmapsto>STCal Source Target* P'' \<and> R' \<longmapsto>STCal Source Target* Q'' \<and> P'' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q''
[PROOF STEP]
using sim reduction_correspondence_simulation_condition_trans[where P="P" and
                   Rel="indRelRTPO TRel" and Cal="STCal Source Target" and Q="Q" and R="R"]
[PROOF STATE]
proof (prove)
using this:
R \<longmapsto>STCal Source Target* R'
R \<longmapsto>STCal Source Target* ?R'3 \<Longrightarrow> \<exists>Q'' R''. Q \<longmapsto>STCal Source Target* Q'' \<and> ?R'3 \<longmapsto>STCal Source Target* R'' \<and> Q'' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> R''
Q \<longmapsto>STCal Source Target* ?Q'3 \<Longrightarrow> \<exists>P'' Q''. P \<longmapsto>STCal Source Target* P'' \<and> ?Q'3 \<longmapsto>STCal Source Target* Q'' \<and> P'' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q''
trans (indRelRTPO TRel)
weak_reduction_simulation (indRelRTPO TRel) (STCal Source Target)
(\<forall>Q'. Q \<longmapsto>STCal Source Target* Q' \<longrightarrow> (\<exists>P'' Q''. P \<longmapsto>STCal Source Target* P'' \<and> Q' \<longmapsto>STCal Source Target* Q'' \<and> P'' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q'')) \<and> (\<forall>R'. R \<longmapsto>STCal Source Target* R' \<longrightarrow> (\<exists>Q'' R''. Q \<longmapsto>STCal Source Target* Q'' \<and> R' \<longmapsto>STCal Source Target* R'' \<and> Q'' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> R'')) \<and> weak_reduction_simulation (indRelRTPO TRel) (STCal Source Target) \<and> trans (indRelRTPO TRel) \<Longrightarrow> \<forall>R'. R \<longmapsto>STCal Source Target* R' \<longrightarrow> (\<exists>P'' R''. P \<longmapsto>STCal Source Target* P'' \<and> R' \<longmapsto>STCal Source Target* R'' \<and> P'' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> R'')

goal (1 subgoal):
 1. \<exists>P'' Q''. P \<longmapsto>STCal Source Target* P'' \<and> R' \<longmapsto>STCal Source Target* Q'' \<and> P'' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q''
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>P'' Q''. P \<longmapsto>STCal Source Target* P'' \<and> R' \<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:
\<exists>P'' Q''. P \<longmapsto>STCal Source Target* P'' \<and> 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 Q'. P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q \<and> Q \<longmapsto>STCal Source Target* Q' \<longrightarrow> (\<exists>P'' Q''. P \<longmapsto>STCal Source Target* P'' \<and> 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:
weak_reduction_correspondence_simulation (indRelRTPO TRel) (STCal Source Target)

goal (1 subgoal):
 1. weak_reduction_correspondence_simulation (indRelRTPO TRel) (STCal Source Target) \<Longrightarrow> weakly_operational_corresponding (TRel\<^sup>*) \<and> weak_reduction_correspondence_simulation (TRel\<^sup>+) Target
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. weak_reduction_correspondence_simulation (indRelRTPO TRel) (STCal Source Target) \<Longrightarrow> weakly_operational_corresponding (TRel\<^sup>*) \<and> weak_reduction_correspondence_simulation (TRel\<^sup>+) Target
[PROOF STEP]
assume csi: "weak_reduction_correspondence_simulation (indRelRTPO TRel) (STCal Source Target)"
[PROOF STATE]
proof (state)
this:
weak_reduction_correspondence_simulation (indRelRTPO TRel) (STCal Source Target)

goal (1 subgoal):
 1. weak_reduction_correspondence_simulation (indRelRTPO TRel) (STCal Source Target) \<Longrightarrow> weakly_operational_corresponding (TRel\<^sup>*) \<and> weak_reduction_correspondence_simulation (TRel\<^sup>+) Target
[PROOF STEP]
show "weakly_operational_corresponding (TRel\<^sup>*)
        \<and> weak_reduction_correspondence_simulation (TRel\<^sup>+) Target"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. weakly_operational_corresponding (TRel\<^sup>*) \<and> weak_reduction_correspondence_simulation (TRel\<^sup>+) Target
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. weakly_operational_corresponding (TRel\<^sup>*)
 2. weak_reduction_correspondence_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 (2 subgoals):
 1. weakly_operational_corresponding (TRel\<^sup>*)
 2. weak_reduction_correspondence_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 (2 subgoals):
 1. weakly_operational_corresponding (TRel\<^sup>*)
 2. weak_reduction_correspondence_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 (2 subgoals):
 1. weakly_operational_corresponding (TRel\<^sup>*)
 2. weak_reduction_correspondence_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>*
[PROOF STEP]
show "weakly_operational_corresponding (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>*

goal (1 subgoal):
 1. weakly_operational_corresponding (TRel\<^sup>*)
[PROOF STEP]
using weak_reduction_correspondence_simulation_impl_WOC[where Rel="indRelRTPO TRel" and
               TRel="TRel"] csi
[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>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> weak_reduction_correspondence_simulation (indRelRTPO TRel) (STCal Source Target) \<Longrightarrow> weakly_operational_corresponding (TRel\<^sup>*)
weak_reduction_correspondence_simulation (indRelRTPO TRel) (STCal Source Target)

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

goal (1 subgoal):
 1. weak_reduction_correspondence_simulation (TRel\<^sup>+) Target
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. weak_reduction_correspondence_simulation (TRel\<^sup>+) Target
[PROOF STEP]
from csi
[PROOF STATE]
proof (chain)
picking this:
weak_reduction_correspondence_simulation (indRelRTPO TRel) (STCal Source Target)
[PROOF STEP]
show "weak_reduction_correspondence_simulation (TRel\<^sup>+) Target"
[PROOF STATE]
proof (prove)
using this:
weak_reduction_correspondence_simulation (indRelRTPO TRel) (STCal Source Target)

goal (1 subgoal):
 1. weak_reduction_correspondence_simulation (TRel\<^sup>+) Target
[PROOF STEP]
using indRelRTPO_impl_TRel_is_weak_reduction_correspondence_simulation[where TRel="TRel"]
[PROOF STATE]
proof (prove)
using this:
weak_reduction_correspondence_simulation (indRelRTPO TRel) (STCal Source Target)
weak_reduction_correspondence_simulation (indRelRTPO TRel) (STCal Source Target) \<Longrightarrow> weak_reduction_correspondence_simulation (TRel\<^sup>+) Target

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
weakly_operational_corresponding (TRel\<^sup>*) \<and> weak_reduction_correspondence_simulation (TRel\<^sup>+) Target

goal:
No subgoals!
[PROOF STEP]
qed