[STATEMENT]
lemma (in encoding) SOSou_iff_strong_reduction_simulation:
  fixes TRel :: "('procT \<times> 'procT) set"
  shows "(strongly_operational_sound (TRel\<^sup>*) \<and> strong_reduction_simulation ((TRel\<^sup>+)\<inverse>) Target)
         = (\<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel)
            \<and> (\<forall>T1 T2. (T1, T2) \<in> TRel \<longrightarrow> (TargetTerm T1, TargetTerm T2) \<in> Rel)
            \<and> (\<forall>T1 T2. (TargetTerm T1, TargetTerm T2) \<in> Rel \<longrightarrow> (T1, T2) \<in> TRel\<^sup>+)
            \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel\<^sup>*)
            \<and> strong_reduction_simulation (Rel\<inverse>) (STCal Source Target))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*)) \<and> strong_reduction_simulation ((TRel\<^sup>+)\<inverse>) Target) = (\<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel) \<and> (\<forall>T1 T2. (T1, T2) \<in> TRel \<longrightarrow> (TargetTerm T1, TargetTerm T2) \<in> Rel) \<and> (\<forall>T1 T2. (TargetTerm T1, TargetTerm T2) \<in> Rel \<longrightarrow> (T1, T2) \<in> TRel\<^sup>+) \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel\<^sup>*) \<and> strong_reduction_simulation (Rel\<inverse>) (STCal Source Target))
[PROOF STEP]
proof (rule iffI, erule conjE)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*)) \<and> strong_reduction_simulation ((TRel\<^sup>+)\<inverse>) Target \<Longrightarrow> \<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel) \<and> (\<forall>T1 T2. (T1, T2) \<in> TRel \<longrightarrow> (TargetTerm T1, TargetTerm T2) \<in> Rel) \<and> (\<forall>T1 T2. (TargetTerm T1, TargetTerm T2) \<in> Rel \<longrightarrow> (T1, T2) \<in> TRel\<^sup>+) \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel\<^sup>*) \<and> strong_reduction_simulation (Rel\<inverse>) (STCal Source Target)
 2. \<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel) \<and> (\<forall>T1 T2. (T1, T2) \<in> TRel \<longrightarrow> (TargetTerm T1, TargetTerm T2) \<in> Rel) \<and> (\<forall>T1 T2. (TargetTerm T1, TargetTerm T2) \<in> Rel \<longrightarrow> (T1, T2) \<in> TRel\<^sup>+) \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel\<^sup>*) \<and> strong_reduction_simulation (Rel\<inverse>) (STCal Source Target) \<Longrightarrow> (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*)) \<and> strong_reduction_simulation ((TRel\<^sup>+)\<inverse>) Target
[PROOF STEP]
have "\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> indRelRTPO TRel"
[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. (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*)) \<and> strong_reduction_simulation ((TRel\<^sup>+)\<inverse>) Target \<Longrightarrow> \<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel) \<and> (\<forall>T1 T2. (T1, T2) \<in> TRel \<longrightarrow> (TargetTerm T1, TargetTerm T2) \<in> Rel) \<and> (\<forall>T1 T2. (TargetTerm T1, TargetTerm T2) \<in> Rel \<longrightarrow> (T1, T2) \<in> TRel\<^sup>+) \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel\<^sup>*) \<and> strong_reduction_simulation (Rel\<inverse>) (STCal Source Target)
 2. \<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel) \<and> (\<forall>T1 T2. (T1, T2) \<in> TRel \<longrightarrow> (TargetTerm T1, TargetTerm T2) \<in> Rel) \<and> (\<forall>T1 T2. (TargetTerm T1, TargetTerm T2) \<in> Rel \<longrightarrow> (T1, T2) \<in> TRel\<^sup>+) \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel\<^sup>*) \<and> strong_reduction_simulation (Rel\<inverse>) (STCal Source Target) \<Longrightarrow> (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*)) \<and> strong_reduction_simulation ((TRel\<^sup>+)\<inverse>) 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. (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*)) \<and> strong_reduction_simulation ((TRel\<^sup>+)\<inverse>) Target \<Longrightarrow> \<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel) \<and> (\<forall>T1 T2. (T1, T2) \<in> TRel \<longrightarrow> (TargetTerm T1, TargetTerm T2) \<in> Rel) \<and> (\<forall>T1 T2. (TargetTerm T1, TargetTerm T2) \<in> Rel \<longrightarrow> (T1, T2) \<in> TRel\<^sup>+) \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel\<^sup>*) \<and> strong_reduction_simulation (Rel\<inverse>) (STCal Source Target)
 2. \<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel) \<and> (\<forall>T1 T2. (T1, T2) \<in> TRel \<longrightarrow> (TargetTerm T1, TargetTerm T2) \<in> Rel) \<and> (\<forall>T1 T2. (TargetTerm T1, TargetTerm T2) \<in> Rel \<longrightarrow> (T1, T2) \<in> TRel\<^sup>+) \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel\<^sup>*) \<and> strong_reduction_simulation (Rel\<inverse>) (STCal Source Target) \<Longrightarrow> (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*)) \<and> strong_reduction_simulation ((TRel\<^sup>+)\<inverse>) Target
[PROOF STEP]
have "\<forall>T1 T2. (T1, T2) \<in> TRel \<longrightarrow> TargetTerm T1 \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm T2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>T1 T2. (T1, T2) \<in> TRel \<longrightarrow> TargetTerm T1 \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm T2
[PROOF STEP]
by (simp add: indRelRTPO.target)
[PROOF STATE]
proof (state)
this:
\<forall>T1 T2. (T1, T2) \<in> TRel \<longrightarrow> TargetTerm T1 \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm T2

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

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

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

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

goal (2 subgoals):
 1. (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*)) \<and> strong_reduction_simulation ((TRel\<^sup>+)\<inverse>) Target \<Longrightarrow> \<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel) \<and> (\<forall>T1 T2. (T1, T2) \<in> TRel \<longrightarrow> (TargetTerm T1, TargetTerm T2) \<in> Rel) \<and> (\<forall>T1 T2. (TargetTerm T1, TargetTerm T2) \<in> Rel \<longrightarrow> (T1, T2) \<in> TRel\<^sup>+) \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel\<^sup>*) \<and> strong_reduction_simulation (Rel\<inverse>) (STCal Source Target)
 2. \<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel) \<and> (\<forall>T1 T2. (T1, T2) \<in> TRel \<longrightarrow> (TargetTerm T1, TargetTerm T2) \<in> Rel) \<and> (\<forall>T1 T2. (TargetTerm T1, TargetTerm T2) \<in> Rel \<longrightarrow> (T1, T2) \<in> TRel\<^sup>+) \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel\<^sup>*) \<and> strong_reduction_simulation (Rel\<inverse>) (STCal Source Target) \<Longrightarrow> (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*)) \<and> strong_reduction_simulation ((TRel\<^sup>+)\<inverse>) 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. (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*)) \<and> strong_reduction_simulation ((TRel\<^sup>+)\<inverse>) Target \<Longrightarrow> \<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel) \<and> (\<forall>T1 T2. (T1, T2) \<in> TRel \<longrightarrow> (TargetTerm T1, TargetTerm T2) \<in> Rel) \<and> (\<forall>T1 T2. (TargetTerm T1, TargetTerm T2) \<in> Rel \<longrightarrow> (T1, T2) \<in> TRel\<^sup>+) \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel\<^sup>*) \<and> strong_reduction_simulation (Rel\<inverse>) (STCal Source Target)
 2. \<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel) \<and> (\<forall>T1 T2. (T1, T2) \<in> TRel \<longrightarrow> (TargetTerm T1, TargetTerm T2) \<in> Rel) \<and> (\<forall>T1 T2. (TargetTerm T1, TargetTerm T2) \<in> Rel \<longrightarrow> (T1, T2) \<in> TRel\<^sup>+) \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel\<^sup>*) \<and> strong_reduction_simulation (Rel\<inverse>) (STCal Source Target) \<Longrightarrow> (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*)) \<and> strong_reduction_simulation ((TRel\<^sup>+)\<inverse>) 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 (2 subgoals):
 1. (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*)) \<and> strong_reduction_simulation ((TRel\<^sup>+)\<inverse>) Target \<Longrightarrow> \<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel) \<and> (\<forall>T1 T2. (T1, T2) \<in> TRel \<longrightarrow> (TargetTerm T1, TargetTerm T2) \<in> Rel) \<and> (\<forall>T1 T2. (TargetTerm T1, TargetTerm T2) \<in> Rel \<longrightarrow> (T1, T2) \<in> TRel\<^sup>+) \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel\<^sup>*) \<and> strong_reduction_simulation (Rel\<inverse>) (STCal Source Target)
 2. \<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel) \<and> (\<forall>T1 T2. (T1, T2) \<in> TRel \<longrightarrow> (TargetTerm T1, TargetTerm T2) \<in> Rel) \<and> (\<forall>T1 T2. (TargetTerm T1, TargetTerm T2) \<in> Rel \<longrightarrow> (T1, T2) \<in> TRel\<^sup>+) \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel\<^sup>*) \<and> strong_reduction_simulation (Rel\<inverse>) (STCal Source Target) \<Longrightarrow> (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*)) \<and> strong_reduction_simulation ((TRel\<^sup>+)\<inverse>) Target
[PROOF STEP]
assume "strongly_operational_sound (TRel\<^sup>*)"
              and "strong_reduction_simulation ((TRel\<^sup>+)\<inverse>) Target"
[PROOF STATE]
proof (state)
this:
\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*)
strong_reduction_simulation ((TRel\<^sup>+)\<inverse>) Target

goal (2 subgoals):
 1. (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*)) \<and> strong_reduction_simulation ((TRel\<^sup>+)\<inverse>) Target \<Longrightarrow> \<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel) \<and> (\<forall>T1 T2. (T1, T2) \<in> TRel \<longrightarrow> (TargetTerm T1, TargetTerm T2) \<in> Rel) \<and> (\<forall>T1 T2. (TargetTerm T1, TargetTerm T2) \<in> Rel \<longrightarrow> (T1, T2) \<in> TRel\<^sup>+) \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel\<^sup>*) \<and> strong_reduction_simulation (Rel\<inverse>) (STCal Source Target)
 2. \<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel) \<and> (\<forall>T1 T2. (T1, T2) \<in> TRel \<longrightarrow> (TargetTerm T1, TargetTerm T2) \<in> Rel) \<and> (\<forall>T1 T2. (TargetTerm T1, TargetTerm T2) \<in> Rel \<longrightarrow> (T1, T2) \<in> TRel\<^sup>+) \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel\<^sup>*) \<and> strong_reduction_simulation (Rel\<inverse>) (STCal Source Target) \<Longrightarrow> (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*)) \<and> strong_reduction_simulation ((TRel\<^sup>+)\<inverse>) Target
[PROOF STEP]
hence "strong_reduction_simulation ((indRelRTPO TRel)\<inverse>) (STCal Source Target)"
[PROOF STATE]
proof (prove)
using this:
\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*)
strong_reduction_simulation ((TRel\<^sup>+)\<inverse>) Target

goal (1 subgoal):
 1. strong_reduction_simulation ((indRelRTPO TRel)\<inverse>) (STCal Source Target)
[PROOF STEP]
using SOSou_iff_inverse_of_indRelRTPO_is_strong_reduction_simulation[where TRel="TRel"]
[PROOF STATE]
proof (prove)
using this:
\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*)
strong_reduction_simulation ((TRel\<^sup>+)\<inverse>) Target
((\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*)) \<and> strong_reduction_simulation ((TRel\<^sup>+)\<inverse>) Target) = strong_reduction_simulation ((indRelRTPO TRel)\<inverse>) (STCal Source Target)

goal (1 subgoal):
 1. strong_reduction_simulation ((indRelRTPO TRel)\<inverse>) (STCal Source Target)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
strong_reduction_simulation ((indRelRTPO TRel)\<inverse>) (STCal Source Target)

goal (2 subgoals):
 1. (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*)) \<and> strong_reduction_simulation ((TRel\<^sup>+)\<inverse>) Target \<Longrightarrow> \<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel) \<and> (\<forall>T1 T2. (T1, T2) \<in> TRel \<longrightarrow> (TargetTerm T1, TargetTerm T2) \<in> Rel) \<and> (\<forall>T1 T2. (TargetTerm T1, TargetTerm T2) \<in> Rel \<longrightarrow> (T1, T2) \<in> TRel\<^sup>+) \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel\<^sup>*) \<and> strong_reduction_simulation (Rel\<inverse>) (STCal Source Target)
 2. \<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel) \<and> (\<forall>T1 T2. (T1, T2) \<in> TRel \<longrightarrow> (TargetTerm T1, TargetTerm T2) \<in> Rel) \<and> (\<forall>T1 T2. (TargetTerm T1, TargetTerm T2) \<in> Rel \<longrightarrow> (T1, T2) \<in> TRel\<^sup>+) \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel\<^sup>*) \<and> strong_reduction_simulation (Rel\<inverse>) (STCal Source Target) \<Longrightarrow> (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*)) \<and> strong_reduction_simulation ((TRel\<^sup>+)\<inverse>) 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>T1 T2. (T1, T2) \<in> TRel \<longrightarrow> TargetTerm T1 \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm T2
\<forall>T1 T2. TargetTerm T1 \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm T2 \<longrightarrow> (T1, T2) \<in> TRel\<^sup>+
\<forall>S T. SourceTerm S \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm T \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel\<^sup>*
strong_reduction_simulation ((indRelRTPO TRel)\<inverse>) (STCal Source Target)
[PROOF STEP]
show "\<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel)
                   \<and> (\<forall>T1 T2. (T1, T2) \<in> TRel \<longrightarrow> (TargetTerm T1, TargetTerm T2) \<in> Rel)
                   \<and> (\<forall>T1 T2. (TargetTerm T1, TargetTerm T2) \<in> Rel \<longrightarrow> (T1, T2) \<in> TRel\<^sup>+)
                   \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel\<^sup>*)
                   \<and> strong_reduction_simulation (Rel\<inverse>) (STCal Source Target)"
[PROOF STATE]
proof (prove)
using this:
\<forall>S. SourceTerm S \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm (\<lbrakk>S\<rbrakk>)
\<forall>T1 T2. (T1, T2) \<in> TRel \<longrightarrow> TargetTerm T1 \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm T2
\<forall>T1 T2. TargetTerm T1 \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm T2 \<longrightarrow> (T1, T2) \<in> TRel\<^sup>+
\<forall>S T. SourceTerm S \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm T \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel\<^sup>*
strong_reduction_simulation ((indRelRTPO TRel)\<inverse>) (STCal Source Target)

goal (1 subgoal):
 1. \<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel) \<and> (\<forall>T1 T2. (T1, T2) \<in> TRel \<longrightarrow> (TargetTerm T1, TargetTerm T2) \<in> Rel) \<and> (\<forall>T1 T2. (TargetTerm T1, TargetTerm T2) \<in> Rel \<longrightarrow> (T1, T2) \<in> TRel\<^sup>+) \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel\<^sup>*) \<and> strong_reduction_simulation (Rel\<inverse>) (STCal Source Target)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel) \<and> (\<forall>T1 T2. (T1, T2) \<in> TRel \<longrightarrow> (TargetTerm T1, TargetTerm T2) \<in> Rel) \<and> (\<forall>T1 T2. (TargetTerm T1, TargetTerm T2) \<in> Rel \<longrightarrow> (T1, T2) \<in> TRel\<^sup>+) \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel\<^sup>*) \<and> strong_reduction_simulation (Rel\<inverse>) (STCal Source Target)

goal (1 subgoal):
 1. \<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel) \<and> (\<forall>T1 T2. (T1, T2) \<in> TRel \<longrightarrow> (TargetTerm T1, TargetTerm T2) \<in> Rel) \<and> (\<forall>T1 T2. (TargetTerm T1, TargetTerm T2) \<in> Rel \<longrightarrow> (T1, T2) \<in> TRel\<^sup>+) \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel\<^sup>*) \<and> strong_reduction_simulation (Rel\<inverse>) (STCal Source Target) \<Longrightarrow> (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*)) \<and> strong_reduction_simulation ((TRel\<^sup>+)\<inverse>) Target
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel) \<and> (\<forall>T1 T2. (T1, T2) \<in> TRel \<longrightarrow> (TargetTerm T1, TargetTerm T2) \<in> Rel) \<and> (\<forall>T1 T2. (TargetTerm T1, TargetTerm T2) \<in> Rel \<longrightarrow> (T1, T2) \<in> TRel\<^sup>+) \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel\<^sup>*) \<and> strong_reduction_simulation (Rel\<inverse>) (STCal Source Target) \<Longrightarrow> (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*)) \<and> strong_reduction_simulation ((TRel\<^sup>+)\<inverse>) Target
[PROOF STEP]
assume "\<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel)
          \<and> (\<forall>T1 T2. (T1, T2) \<in> TRel \<longrightarrow> (TargetTerm T1, TargetTerm T2) \<in> Rel)
          \<and> (\<forall>T1 T2. (TargetTerm T1, TargetTerm T2) \<in> Rel \<longrightarrow> (T1, T2) \<in> TRel\<^sup>+)
          \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel\<^sup>*)
          \<and> strong_reduction_simulation (Rel\<inverse>) (STCal Source Target)"
[PROOF STATE]
proof (state)
this:
\<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel) \<and> (\<forall>T1 T2. (T1, T2) \<in> TRel \<longrightarrow> (TargetTerm T1, TargetTerm T2) \<in> Rel) \<and> (\<forall>T1 T2. (TargetTerm T1, TargetTerm T2) \<in> Rel \<longrightarrow> (T1, T2) \<in> TRel\<^sup>+) \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel\<^sup>*) \<and> strong_reduction_simulation (Rel\<inverse>) (STCal Source Target)

goal (1 subgoal):
 1. \<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel) \<and> (\<forall>T1 T2. (T1, T2) \<in> TRel \<longrightarrow> (TargetTerm T1, TargetTerm T2) \<in> Rel) \<and> (\<forall>T1 T2. (TargetTerm T1, TargetTerm T2) \<in> Rel \<longrightarrow> (T1, T2) \<in> TRel\<^sup>+) \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel\<^sup>*) \<and> strong_reduction_simulation (Rel\<inverse>) (STCal Source Target) \<Longrightarrow> (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*)) \<and> strong_reduction_simulation ((TRel\<^sup>+)\<inverse>) Target
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
\<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel) \<and> (\<forall>T1 T2. (T1, T2) \<in> TRel \<longrightarrow> (TargetTerm T1, TargetTerm T2) \<in> Rel) \<and> (\<forall>T1 T2. (TargetTerm T1, TargetTerm T2) \<in> Rel \<longrightarrow> (T1, T2) \<in> TRel\<^sup>+) \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel\<^sup>*) \<and> strong_reduction_simulation (Rel\<inverse>) (STCal Source Target)
[PROOF STEP]
obtain Rel where A1: "\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel"
    and A2: "\<forall>T1 T2. (T1, T2) \<in> TRel \<longrightarrow> (TargetTerm T1, TargetTerm T2) \<in> Rel"
    and A3: "\<forall>T1 T2. (TargetTerm T1, TargetTerm T2) \<in> Rel \<longrightarrow> (T1, T2) \<in> TRel\<^sup>+"
    and A4: "\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel\<^sup>*"
    and A5: "strong_reduction_simulation (Rel\<inverse>) (STCal Source Target)"
[PROOF STATE]
proof (prove)
using this:
\<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel) \<and> (\<forall>T1 T2. (T1, T2) \<in> TRel \<longrightarrow> (TargetTerm T1, TargetTerm T2) \<in> Rel) \<and> (\<forall>T1 T2. (TargetTerm T1, TargetTerm T2) \<in> Rel \<longrightarrow> (T1, T2) \<in> TRel\<^sup>+) \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel\<^sup>*) \<and> strong_reduction_simulation (Rel\<inverse>) (STCal Source Target)

goal (1 subgoal):
 1. (\<And>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel) \<and> (\<forall>T1 T2. (T1, T2) \<in> TRel \<longrightarrow> (TargetTerm T1, TargetTerm T2) \<in> Rel) \<and> (\<forall>T1 T2. (TargetTerm T1, TargetTerm T2) \<in> Rel \<longrightarrow> (T1, T2) \<in> TRel\<^sup>+) \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel\<^sup>*) \<and> strong_reduction_simulation (Rel\<inverse>) (STCal Source Target) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel
\<forall>T1 T2. (T1, T2) \<in> TRel \<longrightarrow> (TargetTerm T1, TargetTerm T2) \<in> Rel
\<forall>T1 T2. (TargetTerm T1, TargetTerm T2) \<in> Rel \<longrightarrow> (T1, T2) \<in> TRel\<^sup>+
\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel\<^sup>*
strong_reduction_simulation (Rel\<inverse>) (STCal Source Target)

goal (1 subgoal):
 1. \<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel) \<and> (\<forall>T1 T2. (T1, T2) \<in> TRel \<longrightarrow> (TargetTerm T1, TargetTerm T2) \<in> Rel) \<and> (\<forall>T1 T2. (TargetTerm T1, TargetTerm T2) \<in> Rel \<longrightarrow> (T1, T2) \<in> TRel\<^sup>+) \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel\<^sup>*) \<and> strong_reduction_simulation (Rel\<inverse>) (STCal Source Target) \<Longrightarrow> (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*)) \<and> strong_reduction_simulation ((TRel\<^sup>+)\<inverse>) Target
[PROOF STEP]
from A1 A4 A5
[PROOF STATE]
proof (chain)
picking this:
\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel
\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel\<^sup>*
strong_reduction_simulation (Rel\<inverse>) (STCal Source Target)
[PROOF STEP]
have "strongly_operational_sound (TRel\<^sup>*)"
[PROOF STATE]
proof (prove)
using this:
\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel
\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel\<^sup>*
strong_reduction_simulation (Rel\<inverse>) (STCal Source Target)

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

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

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

goal (1 subgoal):
 1. \<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel) \<and> (\<forall>T1 T2. (T1, T2) \<in> TRel \<longrightarrow> (TargetTerm T1, TargetTerm T2) \<in> Rel) \<and> (\<forall>T1 T2. (TargetTerm T1, TargetTerm T2) \<in> Rel \<longrightarrow> (T1, T2) \<in> TRel\<^sup>+) \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel\<^sup>*) \<and> strong_reduction_simulation (Rel\<inverse>) (STCal Source Target) \<Longrightarrow> (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*)) \<and> strong_reduction_simulation ((TRel\<^sup>+)\<inverse>) Target
[PROOF STEP]
from A2 A3 A5
[PROOF STATE]
proof (chain)
picking this:
\<forall>T1 T2. (T1, T2) \<in> TRel \<longrightarrow> (TargetTerm T1, TargetTerm T2) \<in> Rel
\<forall>T1 T2. (TargetTerm T1, TargetTerm T2) \<in> Rel \<longrightarrow> (T1, T2) \<in> TRel\<^sup>+
strong_reduction_simulation (Rel\<inverse>) (STCal Source Target)
[PROOF STEP]
have "strong_reduction_simulation ((TRel\<^sup>+)\<inverse>) Target"
[PROOF STATE]
proof (prove)
using this:
\<forall>T1 T2. (T1, T2) \<in> TRel \<longrightarrow> (TargetTerm T1, TargetTerm T2) \<in> Rel
\<forall>T1 T2. (TargetTerm T1, TargetTerm T2) \<in> Rel \<longrightarrow> (T1, T2) \<in> TRel\<^sup>+
strong_reduction_simulation (Rel\<inverse>) (STCal Source Target)

goal (1 subgoal):
 1. strong_reduction_simulation ((TRel\<^sup>+)\<inverse>) Target
[PROOF STEP]
using rel_with_target_impl_transC_TRel_is_strong_reduction_simulation_rev[where Rel="Rel" and
             TRel="TRel"]
[PROOF STATE]
proof (prove)
using this:
\<forall>T1 T2. (T1, T2) \<in> TRel \<longrightarrow> (TargetTerm T1, TargetTerm T2) \<in> Rel
\<forall>T1 T2. (TargetTerm T1, TargetTerm T2) \<in> Rel \<longrightarrow> (T1, T2) \<in> TRel\<^sup>+
strong_reduction_simulation (Rel\<inverse>) (STCal Source Target)
strong_reduction_simulation (Rel\<inverse>) (STCal Source Target) \<and> (\<forall>T1 T2. (T1, T2) \<in> TRel \<longrightarrow> (TargetTerm T1, TargetTerm T2) \<in> Rel) \<and> (\<forall>T1 T2. (TargetTerm T1, TargetTerm T2) \<in> Rel \<longrightarrow> (T1, T2) \<in> TRel\<^sup>+) \<Longrightarrow> strong_reduction_simulation ((TRel\<^sup>+)\<inverse>) Target

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

goal (1 subgoal):
 1. \<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel) \<and> (\<forall>T1 T2. (T1, T2) \<in> TRel \<longrightarrow> (TargetTerm T1, TargetTerm T2) \<in> Rel) \<and> (\<forall>T1 T2. (TargetTerm T1, TargetTerm T2) \<in> Rel \<longrightarrow> (T1, T2) \<in> TRel\<^sup>+) \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel\<^sup>*) \<and> strong_reduction_simulation (Rel\<inverse>) (STCal Source Target) \<Longrightarrow> (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*)) \<and> strong_reduction_simulation ((TRel\<^sup>+)\<inverse>) Target
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*)
strong_reduction_simulation ((TRel\<^sup>+)\<inverse>) Target
[PROOF STEP]
show "strongly_operational_sound (TRel\<^sup>*) \<and> strong_reduction_simulation ((TRel\<^sup>+)\<inverse>) Target"
[PROOF STATE]
proof (prove)
using this:
\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*)
strong_reduction_simulation ((TRel\<^sup>+)\<inverse>) Target

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in encoding) SOSou_modulo_TRel_iff_strong_reduction_simulation:
  shows "(\<exists>TRel. strongly_operational_sound (TRel\<^sup>*)
         \<and> strong_reduction_simulation ((TRel\<^sup>+)\<inverse>) Target)
         = (\<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel)
           \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (TargetTerm (\<lbrakk>S\<rbrakk>), TargetTerm T) \<in> Rel\<^sup>=)
           \<and> strong_reduction_simulation (Rel\<inverse>) (STCal Source Target))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>TRel. (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*)) \<and> strong_reduction_simulation ((TRel\<^sup>+)\<inverse>) Target) = (\<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel) \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (TargetTerm (\<lbrakk>S\<rbrakk>), TargetTerm T) \<in> Rel\<^sup>=) \<and> strong_reduction_simulation (Rel\<inverse>) (STCal Source Target))
[PROOF STEP]
proof (rule iffI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<exists>TRel. (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*)) \<and> strong_reduction_simulation ((TRel\<^sup>+)\<inverse>) Target \<Longrightarrow> \<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel) \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (TargetTerm (\<lbrakk>S\<rbrakk>), TargetTerm T) \<in> Rel\<^sup>=) \<and> strong_reduction_simulation (Rel\<inverse>) (STCal Source Target)
 2. \<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel) \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (TargetTerm (\<lbrakk>S\<rbrakk>), TargetTerm T) \<in> Rel\<^sup>=) \<and> strong_reduction_simulation (Rel\<inverse>) (STCal Source Target) \<Longrightarrow> \<exists>TRel. (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*)) \<and> strong_reduction_simulation ((TRel\<^sup>+)\<inverse>) Target
[PROOF STEP]
assume "\<exists>TRel. strongly_operational_sound (TRel\<^sup>*)
          \<and> strong_reduction_simulation ((TRel\<^sup>+)\<inverse>) Target"
[PROOF STATE]
proof (state)
this:
\<exists>TRel. (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*)) \<and> strong_reduction_simulation ((TRel\<^sup>+)\<inverse>) Target

goal (2 subgoals):
 1. \<exists>TRel. (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*)) \<and> strong_reduction_simulation ((TRel\<^sup>+)\<inverse>) Target \<Longrightarrow> \<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel) \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (TargetTerm (\<lbrakk>S\<rbrakk>), TargetTerm T) \<in> Rel\<^sup>=) \<and> strong_reduction_simulation (Rel\<inverse>) (STCal Source Target)
 2. \<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel) \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (TargetTerm (\<lbrakk>S\<rbrakk>), TargetTerm T) \<in> Rel\<^sup>=) \<and> strong_reduction_simulation (Rel\<inverse>) (STCal Source Target) \<Longrightarrow> \<exists>TRel. (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*)) \<and> strong_reduction_simulation ((TRel\<^sup>+)\<inverse>) Target
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
\<exists>TRel. (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*)) \<and> strong_reduction_simulation ((TRel\<^sup>+)\<inverse>) Target
[PROOF STEP]
obtain TRel where "strongly_operational_sound (TRel\<^sup>*)"
                          and "strong_reduction_simulation ((TRel\<^sup>+)\<inverse>) Target"
[PROOF STATE]
proof (prove)
using this:
\<exists>TRel. (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*)) \<and> strong_reduction_simulation ((TRel\<^sup>+)\<inverse>) Target

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

goal (2 subgoals):
 1. \<exists>TRel. (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*)) \<and> strong_reduction_simulation ((TRel\<^sup>+)\<inverse>) Target \<Longrightarrow> \<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel) \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (TargetTerm (\<lbrakk>S\<rbrakk>), TargetTerm T) \<in> Rel\<^sup>=) \<and> strong_reduction_simulation (Rel\<inverse>) (STCal Source Target)
 2. \<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel) \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (TargetTerm (\<lbrakk>S\<rbrakk>), TargetTerm T) \<in> Rel\<^sup>=) \<and> strong_reduction_simulation (Rel\<inverse>) (STCal Source Target) \<Longrightarrow> \<exists>TRel. (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*)) \<and> strong_reduction_simulation ((TRel\<^sup>+)\<inverse>) Target
[PROOF STEP]
hence "strong_reduction_simulation ((indRelRTPO TRel)\<inverse>) (STCal Source Target)"
[PROOF STATE]
proof (prove)
using this:
\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*)
strong_reduction_simulation ((TRel\<^sup>+)\<inverse>) Target

goal (1 subgoal):
 1. strong_reduction_simulation ((indRelRTPO TRel)\<inverse>) (STCal Source Target)
[PROOF STEP]
using SOSou_iff_inverse_of_indRelRTPO_is_strong_reduction_simulation[where TRel="TRel"]
[PROOF STATE]
proof (prove)
using this:
\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*)
strong_reduction_simulation ((TRel\<^sup>+)\<inverse>) Target
((\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*)) \<and> strong_reduction_simulation ((TRel\<^sup>+)\<inverse>) Target) = strong_reduction_simulation ((indRelRTPO TRel)\<inverse>) (STCal Source Target)

goal (1 subgoal):
 1. strong_reduction_simulation ((indRelRTPO TRel)\<inverse>) (STCal Source Target)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
strong_reduction_simulation ((indRelRTPO TRel)\<inverse>) (STCal Source Target)

goal (2 subgoals):
 1. \<exists>TRel. (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*)) \<and> strong_reduction_simulation ((TRel\<^sup>+)\<inverse>) Target \<Longrightarrow> \<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel) \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (TargetTerm (\<lbrakk>S\<rbrakk>), TargetTerm T) \<in> Rel\<^sup>=) \<and> strong_reduction_simulation (Rel\<inverse>) (STCal Source Target)
 2. \<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel) \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (TargetTerm (\<lbrakk>S\<rbrakk>), TargetTerm T) \<in> Rel\<^sup>=) \<and> strong_reduction_simulation (Rel\<inverse>) (STCal Source Target) \<Longrightarrow> \<exists>TRel. (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*)) \<and> strong_reduction_simulation ((TRel\<^sup>+)\<inverse>) Target
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
strong_reduction_simulation ((indRelRTPO TRel)\<inverse>) (STCal Source Target)

goal (2 subgoals):
 1. \<exists>TRel. (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*)) \<and> strong_reduction_simulation ((TRel\<^sup>+)\<inverse>) Target \<Longrightarrow> \<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel) \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (TargetTerm (\<lbrakk>S\<rbrakk>), TargetTerm T) \<in> Rel\<^sup>=) \<and> strong_reduction_simulation (Rel\<inverse>) (STCal Source Target)
 2. \<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel) \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (TargetTerm (\<lbrakk>S\<rbrakk>), TargetTerm T) \<in> Rel\<^sup>=) \<and> strong_reduction_simulation (Rel\<inverse>) (STCal Source Target) \<Longrightarrow> \<exists>TRel. (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*)) \<and> strong_reduction_simulation ((TRel\<^sup>+)\<inverse>) Target
[PROOF STEP]
have "\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> indRelRTPO TRel"
[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. \<exists>TRel. (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*)) \<and> strong_reduction_simulation ((TRel\<^sup>+)\<inverse>) Target \<Longrightarrow> \<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel) \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (TargetTerm (\<lbrakk>S\<rbrakk>), TargetTerm T) \<in> Rel\<^sup>=) \<and> strong_reduction_simulation (Rel\<inverse>) (STCal Source Target)
 2. \<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel) \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (TargetTerm (\<lbrakk>S\<rbrakk>), TargetTerm T) \<in> Rel\<^sup>=) \<and> strong_reduction_simulation (Rel\<inverse>) (STCal Source Target) \<Longrightarrow> \<exists>TRel. (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*)) \<and> strong_reduction_simulation ((TRel\<^sup>+)\<inverse>) 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. \<exists>TRel. (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*)) \<and> strong_reduction_simulation ((TRel\<^sup>+)\<inverse>) Target \<Longrightarrow> \<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel) \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (TargetTerm (\<lbrakk>S\<rbrakk>), TargetTerm T) \<in> Rel\<^sup>=) \<and> strong_reduction_simulation (Rel\<inverse>) (STCal Source Target)
 2. \<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel) \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (TargetTerm (\<lbrakk>S\<rbrakk>), TargetTerm T) \<in> Rel\<^sup>=) \<and> strong_reduction_simulation (Rel\<inverse>) (STCal Source Target) \<Longrightarrow> \<exists>TRel. (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*)) \<and> strong_reduction_simulation ((TRel\<^sup>+)\<inverse>) Target
[PROOF STEP]
have "\<forall>S T. (SourceTerm S, TargetTerm T) \<in> indRelRTPO TRel
                 \<longrightarrow> (TargetTerm (\<lbrakk>S\<rbrakk>), TargetTerm T) \<in> (indRelRTPO TRel)\<^sup>="
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>S T. SourceTerm S \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm T \<longrightarrow> (TargetTerm (\<lbrakk>S\<rbrakk>), TargetTerm T) \<in> (indRelRTPO TRel)\<^sup>=
[PROOF STEP]
using indRelRTPO_relates_source_target[where TRel="TRel"]
[PROOF STATE]
proof (prove)
using this:
SourceTerm ?S \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm ?T \<Longrightarrow> (TargetTerm (\<lbrakk>?S\<rbrakk>), TargetTerm ?T) \<in> (indRelRTPO TRel)\<^sup>=

goal (1 subgoal):
 1. \<forall>S T. SourceTerm S \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm T \<longrightarrow> (TargetTerm (\<lbrakk>S\<rbrakk>), TargetTerm T) \<in> (indRelRTPO 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> (TargetTerm (\<lbrakk>S\<rbrakk>), TargetTerm T) \<in> (indRelRTPO TRel)\<^sup>=

goal (2 subgoals):
 1. \<exists>TRel. (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*)) \<and> strong_reduction_simulation ((TRel\<^sup>+)\<inverse>) Target \<Longrightarrow> \<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel) \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (TargetTerm (\<lbrakk>S\<rbrakk>), TargetTerm T) \<in> Rel\<^sup>=) \<and> strong_reduction_simulation (Rel\<inverse>) (STCal Source Target)
 2. \<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel) \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (TargetTerm (\<lbrakk>S\<rbrakk>), TargetTerm T) \<in> Rel\<^sup>=) \<and> strong_reduction_simulation (Rel\<inverse>) (STCal Source Target) \<Longrightarrow> \<exists>TRel. (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*)) \<and> strong_reduction_simulation ((TRel\<^sup>+)\<inverse>) Target
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
strong_reduction_simulation ((indRelRTPO TRel)\<inverse>) (STCal Source Target)
\<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> (TargetTerm (\<lbrakk>S\<rbrakk>), TargetTerm T) \<in> (indRelRTPO TRel)\<^sup>=
[PROOF STEP]
show "\<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel)
                   \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel
                      \<longrightarrow> (TargetTerm (\<lbrakk>S\<rbrakk>), TargetTerm T) \<in> Rel\<^sup>=)
                   \<and> strong_reduction_simulation (Rel\<inverse>) (STCal Source Target)"
[PROOF STATE]
proof (prove)
using this:
strong_reduction_simulation ((indRelRTPO TRel)\<inverse>) (STCal Source Target)
\<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> (TargetTerm (\<lbrakk>S\<rbrakk>), TargetTerm T) \<in> (indRelRTPO TRel)\<^sup>=

goal (1 subgoal):
 1. \<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel) \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (TargetTerm (\<lbrakk>S\<rbrakk>), TargetTerm T) \<in> Rel\<^sup>=) \<and> strong_reduction_simulation (Rel\<inverse>) (STCal Source Target)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel) \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (TargetTerm (\<lbrakk>S\<rbrakk>), TargetTerm T) \<in> Rel\<^sup>=) \<and> strong_reduction_simulation (Rel\<inverse>) (STCal Source Target)

goal (1 subgoal):
 1. \<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel) \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (TargetTerm (\<lbrakk>S\<rbrakk>), TargetTerm T) \<in> Rel\<^sup>=) \<and> strong_reduction_simulation (Rel\<inverse>) (STCal Source Target) \<Longrightarrow> \<exists>TRel. (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*)) \<and> strong_reduction_simulation ((TRel\<^sup>+)\<inverse>) Target
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel) \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (TargetTerm (\<lbrakk>S\<rbrakk>), TargetTerm T) \<in> Rel\<^sup>=) \<and> strong_reduction_simulation (Rel\<inverse>) (STCal Source Target) \<Longrightarrow> \<exists>TRel. (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*)) \<and> strong_reduction_simulation ((TRel\<^sup>+)\<inverse>) Target
[PROOF STEP]
assume "\<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel)
          \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel
             \<longrightarrow> (TargetTerm (\<lbrakk>S\<rbrakk>), TargetTerm T) \<in> Rel\<^sup>=)
          \<and> strong_reduction_simulation (Rel\<inverse>) (STCal Source Target)"
[PROOF STATE]
proof (state)
this:
\<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel) \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (TargetTerm (\<lbrakk>S\<rbrakk>), TargetTerm T) \<in> Rel\<^sup>=) \<and> strong_reduction_simulation (Rel\<inverse>) (STCal Source Target)

goal (1 subgoal):
 1. \<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel) \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (TargetTerm (\<lbrakk>S\<rbrakk>), TargetTerm T) \<in> Rel\<^sup>=) \<and> strong_reduction_simulation (Rel\<inverse>) (STCal Source Target) \<Longrightarrow> \<exists>TRel. (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*)) \<and> strong_reduction_simulation ((TRel\<^sup>+)\<inverse>) Target
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
\<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel) \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (TargetTerm (\<lbrakk>S\<rbrakk>), TargetTerm T) \<in> Rel\<^sup>=) \<and> strong_reduction_simulation (Rel\<inverse>) (STCal Source Target)
[PROOF STEP]
obtain Rel where A1: "\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel"
   and A2: "(\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel
            \<longrightarrow> (TargetTerm (\<lbrakk>S\<rbrakk>), TargetTerm T) \<in> Rel\<^sup>=)"
   and A3: "strong_reduction_simulation (Rel\<inverse>) (STCal Source Target)"
[PROOF STATE]
proof (prove)
using this:
\<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel) \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (TargetTerm (\<lbrakk>S\<rbrakk>), TargetTerm T) \<in> Rel\<^sup>=) \<and> strong_reduction_simulation (Rel\<inverse>) (STCal Source Target)

goal (1 subgoal):
 1. (\<And>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel) \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (TargetTerm (\<lbrakk>S\<rbrakk>), TargetTerm T) \<in> Rel\<^sup>=) \<and> strong_reduction_simulation (Rel\<inverse>) (STCal Source Target) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel
\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (TargetTerm (\<lbrakk>S\<rbrakk>), TargetTerm T) \<in> Rel\<^sup>=
strong_reduction_simulation (Rel\<inverse>) (STCal Source Target)

goal (1 subgoal):
 1. \<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel) \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (TargetTerm (\<lbrakk>S\<rbrakk>), TargetTerm T) \<in> Rel\<^sup>=) \<and> strong_reduction_simulation (Rel\<inverse>) (STCal Source Target) \<Longrightarrow> \<exists>TRel. (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*)) \<and> strong_reduction_simulation ((TRel\<^sup>+)\<inverse>) Target
[PROOF STEP]
from A2
[PROOF STATE]
proof (chain)
picking this:
\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (TargetTerm (\<lbrakk>S\<rbrakk>), TargetTerm T) \<in> Rel\<^sup>=
[PROOF STEP]
obtain TRel where "\<forall>T1 T2. (T1, T2) \<in> TRel \<longrightarrow> (TargetTerm T1, TargetTerm T2) \<in> Rel"
   and "\<forall>T1 T2. (TargetTerm T1, TargetTerm T2) \<in> Rel \<longrightarrow> (T1, T2) \<in> TRel\<^sup>+"
   and "\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel\<^sup>*"
[PROOF STATE]
proof (prove)
using this:
\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (TargetTerm (\<lbrakk>S\<rbrakk>), TargetTerm T) \<in> Rel\<^sup>=

goal (1 subgoal):
 1. (\<And>TRel. (\<forall>T1 T2. (T1, T2) \<in> TRel \<longrightarrow> (TargetTerm T1, TargetTerm T2) \<in> Rel) \<and> (\<forall>T1 T2. (TargetTerm T1, TargetTerm T2) \<in> Rel \<longrightarrow> (T1, T2) \<in> TRel\<^sup>+) \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel\<^sup>*) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using target_relation_from_source_target_relation[where Rel="Rel"]
[PROOF STATE]
proof (prove)
using this:
\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (TargetTerm (\<lbrakk>S\<rbrakk>), TargetTerm T) \<in> Rel\<^sup>=
\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (TargetTerm (\<lbrakk>S\<rbrakk>), TargetTerm T) \<in> Rel\<^sup>= \<Longrightarrow> \<exists>TRel. (\<forall>T1 T2. (T1, T2) \<in> TRel \<longrightarrow> (TargetTerm T1, TargetTerm T2) \<in> Rel) \<and> (\<forall>T1 T2. (TargetTerm T1, TargetTerm T2) \<in> Rel \<longrightarrow> (T1, T2) \<in> TRel\<^sup>+) \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel\<^sup>*)

goal (1 subgoal):
 1. (\<And>TRel. (\<forall>T1 T2. (T1, T2) \<in> TRel \<longrightarrow> (TargetTerm T1, TargetTerm T2) \<in> Rel) \<and> (\<forall>T1 T2. (TargetTerm T1, TargetTerm T2) \<in> Rel \<longrightarrow> (T1, T2) \<in> TRel\<^sup>+) \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel\<^sup>*) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>T1 T2. (T1, T2) \<in> TRel \<longrightarrow> (TargetTerm T1, TargetTerm T2) \<in> Rel
\<forall>T1 T2. (TargetTerm T1, TargetTerm T2) \<in> Rel \<longrightarrow> (T1, T2) \<in> TRel\<^sup>+
\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel\<^sup>*

goal (1 subgoal):
 1. \<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel) \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (TargetTerm (\<lbrakk>S\<rbrakk>), TargetTerm T) \<in> Rel\<^sup>=) \<and> strong_reduction_simulation (Rel\<inverse>) (STCal Source Target) \<Longrightarrow> \<exists>TRel. (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*)) \<and> strong_reduction_simulation ((TRel\<^sup>+)\<inverse>) Target
[PROOF STEP]
with A1 A3
[PROOF STATE]
proof (chain)
picking this:
\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel
strong_reduction_simulation (Rel\<inverse>) (STCal Source Target)
\<forall>T1 T2. (T1, T2) \<in> TRel \<longrightarrow> (TargetTerm T1, TargetTerm T2) \<in> Rel
\<forall>T1 T2. (TargetTerm T1, TargetTerm T2) \<in> Rel \<longrightarrow> (T1, T2) \<in> TRel\<^sup>+
\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel\<^sup>*
[PROOF STEP]
have "strongly_operational_sound (TRel\<^sup>*) \<and> strong_reduction_simulation ((TRel\<^sup>+)\<inverse>) Target"
[PROOF STATE]
proof (prove)
using this:
\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel
strong_reduction_simulation (Rel\<inverse>) (STCal Source Target)
\<forall>T1 T2. (T1, T2) \<in> TRel \<longrightarrow> (TargetTerm T1, TargetTerm T2) \<in> Rel
\<forall>T1 T2. (TargetTerm T1, TargetTerm T2) \<in> Rel \<longrightarrow> (T1, T2) \<in> TRel\<^sup>+
\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel\<^sup>*

goal (1 subgoal):
 1. (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*)) \<and> strong_reduction_simulation ((TRel\<^sup>+)\<inverse>) Target
[PROOF STEP]
using SOSou_iff_strong_reduction_simulation[where TRel="TRel"]
[PROOF STATE]
proof (prove)
using this:
\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel
strong_reduction_simulation (Rel\<inverse>) (STCal Source Target)
\<forall>T1 T2. (T1, T2) \<in> TRel \<longrightarrow> (TargetTerm T1, TargetTerm T2) \<in> Rel
\<forall>T1 T2. (TargetTerm T1, TargetTerm T2) \<in> Rel \<longrightarrow> (T1, T2) \<in> TRel\<^sup>+
\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel\<^sup>*
((\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*)) \<and> strong_reduction_simulation ((TRel\<^sup>+)\<inverse>) Target) = (\<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel) \<and> (\<forall>T1 T2. (T1, T2) \<in> TRel \<longrightarrow> (TargetTerm T1, TargetTerm T2) \<in> Rel) \<and> (\<forall>T1 T2. (TargetTerm T1, TargetTerm T2) \<in> Rel \<longrightarrow> (T1, T2) \<in> TRel\<^sup>+) \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel\<^sup>*) \<and> strong_reduction_simulation (Rel\<inverse>) (STCal Source Target))

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

goal (1 subgoal):
 1. \<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel) \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (TargetTerm (\<lbrakk>S\<rbrakk>), TargetTerm T) \<in> Rel\<^sup>=) \<and> strong_reduction_simulation (Rel\<inverse>) (STCal Source Target) \<Longrightarrow> \<exists>TRel. (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*)) \<and> strong_reduction_simulation ((TRel\<^sup>+)\<inverse>) Target
[PROOF STEP]
thus "\<exists>TRel. strongly_operational_sound (TRel\<^sup>*) \<and> strong_reduction_simulation ((TRel\<^sup>+)\<inverse>) Target"
[PROOF STATE]
proof (prove)
using this:
(\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*)) \<and> strong_reduction_simulation ((TRel\<^sup>+)\<inverse>) Target

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in encoding) weak_reduction_correspondence_simulation_impl_WOC:
  fixes Rel  :: "(('procS, 'procT) Proc \<times> ('procS, 'procT) Proc) set"
    and TRel :: "('procT \<times> 'procT) set"
  assumes enc:  "\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel"
      and tRel: "(\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel\<^sup>*)"
      and cs:   "weak_reduction_correspondence_simulation Rel (STCal Source Target)"
  shows "weakly_operational_corresponding (TRel\<^sup>*)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. weakly_operational_corresponding (TRel\<^sup>*)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. operational_complete (TRel\<^sup>*)
 2. weakly_operational_sound (TRel\<^sup>*)
[PROOF STEP]
from enc tRel cs
[PROOF STATE]
proof (chain)
picking this:
\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel
\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel\<^sup>*
weak_reduction_correspondence_simulation Rel (STCal Source Target)
[PROOF STEP]
show "operational_complete (TRel\<^sup>*)"
[PROOF STATE]
proof (prove)
using this:
\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel
\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel\<^sup>*
weak_reduction_correspondence_simulation Rel (STCal Source Target)

goal (1 subgoal):
 1. operational_complete (TRel\<^sup>*)
[PROOF STEP]
using weak_reduction_simulation_impl_OCom[where TRel="TRel"]
[PROOF STATE]
proof (prove)
using this:
\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel
\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel\<^sup>*
weak_reduction_correspondence_simulation Rel (STCal Source Target)
(\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> ?Rel) \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> ?Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel\<^sup>*) \<and> weak_reduction_simulation ?Rel (STCal Source Target) \<Longrightarrow> operational_complete (TRel\<^sup>*)

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

goal (1 subgoal):
 1. weakly_operational_sound (TRel\<^sup>*)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. weakly_operational_sound (TRel\<^sup>*)
[PROOF STEP]
show "weakly_operational_sound (TRel\<^sup>*)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. weakly_operational_sound (TRel\<^sup>*)
[PROOF STEP]
proof clarify
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target* T \<Longrightarrow> \<exists>S' T'. S \<longmapsto>Source* S' \<and> T \<longmapsto>Target* T' \<and> (\<lbrakk>S'\<rbrakk>, T') \<in> TRel\<^sup>*
[PROOF STEP]
fix S T
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target* T \<Longrightarrow> \<exists>S' T'. S \<longmapsto>Source* S' \<and> T \<longmapsto>Target* T' \<and> (\<lbrakk>S'\<rbrakk>, T') \<in> TRel\<^sup>*
[PROOF STEP]
from enc
[PROOF STATE]
proof (chain)
picking this:
\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel
[PROOF STEP]
have "(SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel"
[PROOF STATE]
proof (prove)
using this:
\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel

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

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

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

goal (1 subgoal):
 1. \<And>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target* T \<Longrightarrow> \<exists>S' T'. S \<longmapsto>Source* S' \<and> T \<longmapsto>Target* T' \<and> (\<lbrakk>S'\<rbrakk>, T') \<in> TRel\<^sup>*
[PROOF STEP]
hence "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_steps(2))
[PROOF STATE]
proof (state)
this:
TargetTerm (\<lbrakk>S\<rbrakk>) \<longmapsto>STCal Source Target* TargetTerm T

goal (1 subgoal):
 1. \<And>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target* T \<Longrightarrow> \<exists>S' T'. S \<longmapsto>Source* S' \<and> T \<longmapsto>Target* T' \<and> (\<lbrakk>S'\<rbrakk>, T') \<in> TRel\<^sup>*
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel
TargetTerm (\<lbrakk>S\<rbrakk>) \<longmapsto>STCal Source Target* TargetTerm T
[PROOF STEP]
obtain P' Q' where A1: "SourceTerm S \<longmapsto>(STCal Source Target)* P'"
     and A2: "TargetTerm T \<longmapsto>(STCal Source Target)* Q'" and A3: "(P', Q') \<in> Rel"
[PROOF STATE]
proof (prove)
using this:
(SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel
TargetTerm (\<lbrakk>S\<rbrakk>) \<longmapsto>STCal Source Target* TargetTerm T

goal (1 subgoal):
 1. (\<And>P' Q'. SourceTerm S \<longmapsto>STCal Source Target* P' \<and> TargetTerm T \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> Rel \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using cs
[PROOF STATE]
proof (prove)
using this:
(SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel
TargetTerm (\<lbrakk>S\<rbrakk>) \<longmapsto>STCal Source Target* TargetTerm T
weak_reduction_correspondence_simulation Rel (STCal Source Target)

goal (1 subgoal):
 1. (\<And>P' Q'. SourceTerm S \<longmapsto>STCal Source Target* P' \<and> TargetTerm T \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> Rel \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
SourceTerm S \<longmapsto>STCal Source Target* P'
TargetTerm T \<longmapsto>STCal Source Target* Q'
(P', Q') \<in> Rel

goal (1 subgoal):
 1. \<And>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target* T \<Longrightarrow> \<exists>S' T'. S \<longmapsto>Source* S' \<and> T \<longmapsto>Target* T' \<and> (\<lbrakk>S'\<rbrakk>, T') \<in> TRel\<^sup>*
[PROOF STEP]
from A1
[PROOF STATE]
proof (chain)
picking this:
SourceTerm S \<longmapsto>STCal Source Target* P'
[PROOF STEP]
obtain S' where A4: "S' \<in>S P'" and A5: "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_steps(1))
[PROOF STATE]
proof (state)
this:
S' \<in>S P'
S \<longmapsto>Source* S'

goal (1 subgoal):
 1. \<And>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target* T \<Longrightarrow> \<exists>S' T'. S \<longmapsto>Source* S' \<and> T \<longmapsto>Target* T' \<and> (\<lbrakk>S'\<rbrakk>, T') \<in> TRel\<^sup>*
[PROOF STEP]
from A2
[PROOF STATE]
proof (chain)
picking this:
TargetTerm T \<longmapsto>STCal Source Target* Q'
[PROOF STEP]
obtain T' where A6: "T' \<in>T Q'" and A7: "T \<longmapsto>Target* T'"
[PROOF STATE]
proof (prove)
using this:
TargetTerm T \<longmapsto>STCal Source Target* Q'

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

goal (1 subgoal):
 1. \<And>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target* T \<Longrightarrow> \<exists>S' T'. S \<longmapsto>Source* S' \<and> T \<longmapsto>Target* T' \<and> (\<lbrakk>S'\<rbrakk>, T') \<in> TRel\<^sup>*
[PROOF STEP]
from tRel A3 A4 A6
[PROOF STATE]
proof (chain)
picking this:
\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel\<^sup>*
(P', Q') \<in> Rel
S' \<in>S P'
T' \<in>T Q'
[PROOF STEP]
have "(\<lbrakk>S'\<rbrakk>, T') \<in> TRel\<^sup>*"
[PROOF STATE]
proof (prove)
using this:
\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel\<^sup>*
(P', Q') \<in> Rel
S' \<in>S P'
T' \<in>T Q'

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

goal (1 subgoal):
 1. \<And>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target* T \<Longrightarrow> \<exists>S' T'. S \<longmapsto>Source* S' \<and> T \<longmapsto>Target* T' \<and> (\<lbrakk>S'\<rbrakk>, T') \<in> TRel\<^sup>*
[PROOF STEP]
with A5 A7
[PROOF STATE]
proof (chain)
picking this:
S \<longmapsto>Source* S'
T \<longmapsto>Target* T'
(\<lbrakk>S'\<rbrakk>, T') \<in> TRel\<^sup>*
[PROOF STEP]
show "\<exists>S' T'. S \<longmapsto>Source* S' \<and> T \<longmapsto>Target* T' \<and> (\<lbrakk>S'\<rbrakk>, T') \<in> TRel\<^sup>*"
[PROOF STATE]
proof (prove)
using this:
S \<longmapsto>Source* S'
T \<longmapsto>Target* T'
(\<lbrakk>S'\<rbrakk>, T') \<in> TRel\<^sup>*

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
weakly_operational_sound (TRel\<^sup>*)

goal:
No subgoals!
[PROOF STEP]
qed