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

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

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

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

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

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

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

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

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

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

goal (2 subgoals):
 1. (\<forall>S S'. S \<longmapsto>Source S' \<longrightarrow> (\<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*)) \<and> strong_reduction_simulation (TRel\<^sup>+) Target \<Longrightarrow> \<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 (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 (STCal Source Target) \<Longrightarrow> (\<forall>S S'. S \<longmapsto>Source S' \<longrightarrow> (\<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*)) \<and> strong_reduction_simulation (TRel\<^sup>+) Target
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<forall>S. SourceTerm S \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm (\<lbrakk>S\<rbrakk>)
\<forall>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>*
\<forall>P Q P'. P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q \<and> P \<longmapsto>STCal Source Target P' \<longrightarrow> (\<exists>Q'. Q \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q')
[PROOF STEP]
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 (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>*
\<forall>P Q P'. P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q \<and> P \<longmapsto>STCal Source Target P' \<longrightarrow> (\<exists>Q'. Q \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q')

goal (1 subgoal):
 1. \<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 (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 (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 (STCal Source Target) \<Longrightarrow> (\<forall>S S'. S \<longmapsto>Source S' \<longrightarrow> (\<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*)) \<and> strong_reduction_simulation (TRel\<^sup>+) Target
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<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 (STCal Source Target) \<Longrightarrow> (\<forall>S S'. S \<longmapsto>Source S' \<longrightarrow> (\<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*)) \<and> strong_reduction_simulation (TRel\<^sup>+) Target
[PROOF STEP]
assume "\<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 (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 (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 (STCal Source Target) \<Longrightarrow> (\<forall>S S'. S \<longmapsto>Source S' \<longrightarrow> (\<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*)) \<and> strong_reduction_simulation (TRel\<^sup>+) Target
[PROOF STEP]
from 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 (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 (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 (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 (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 (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 (STCal Source Target) \<Longrightarrow> (\<forall>S S'. S \<longmapsto>Source S' \<longrightarrow> (\<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*)) \<and> strong_reduction_simulation (TRel\<^sup>+) Target
[PROOF STEP]
from 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 (STCal Source Target)
[PROOF STEP]
have "strongly_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>*
strong_reduction_simulation Rel (STCal Source Target)

goal (1 subgoal):
 1. \<forall>S S'. S \<longmapsto>Source S' \<longrightarrow> (\<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*)
[PROOF STEP]
using strong_reduction_simulation_impl_SOCom[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 (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 (STCal Source Target) \<Longrightarrow> \<forall>S S'. S \<longmapsto>Source S' \<longrightarrow> (\<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*)

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

goal (1 subgoal):
 1. \<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 (STCal Source Target) \<Longrightarrow> (\<forall>S S'. S \<longmapsto>Source S' \<longrightarrow> (\<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*)) \<and> strong_reduction_simulation (TRel\<^sup>+) Target
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>S S'. S \<longmapsto>Source S' \<longrightarrow> (\<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*)

goal (1 subgoal):
 1. \<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 (STCal Source Target) \<Longrightarrow> (\<forall>S S'. S \<longmapsto>Source S' \<longrightarrow> (\<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*)) \<and> strong_reduction_simulation (TRel\<^sup>+) Target
[PROOF STEP]
from 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 (STCal Source Target)
[PROOF STEP]
have "strong_reduction_simulation (TRel\<^sup>+) 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 (STCal Source Target)

goal (1 subgoal):
 1. strong_reduction_simulation (TRel\<^sup>+) Target
[PROOF STEP]
using rel_with_target_impl_transC_TRel_is_strong_reduction_simulation[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 (STCal Source Target)
strong_reduction_simulation Rel (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>+) Target

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in encoding) target_relation_from_source_target_relation:
  fixes Rel :: "(('procS, 'procT) Proc \<times> ('procS, 'procT) Proc) set"
  assumes stre: "\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel
                 \<longrightarrow> (TargetTerm (\<lbrakk>S\<rbrakk>), TargetTerm T) \<in> Rel\<^sup>="
  shows "\<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>*)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<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>*)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<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>*)
[PROOF STEP]
define TRel where "TRel = {(T1, T2). (TargetTerm T1, TargetTerm T2) \<in> Rel}"
[PROOF STATE]
proof (state)
this:
TRel = _Collect (T1, T2) ((TargetTerm T1, TargetTerm T2) \<in> Rel)

goal (1 subgoal):
 1. \<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>*)
[PROOF STEP]
from TRel_def
[PROOF STATE]
proof (chain)
picking this:
TRel = _Collect (T1, T2) ((TargetTerm T1, TargetTerm T2) \<in> Rel)
[PROOF STEP]
have "\<forall>T1 T2. (T1, T2) \<in> TRel \<longrightarrow> (TargetTerm T1, TargetTerm T2) \<in> Rel"
[PROOF STATE]
proof (prove)
using this:
TRel = _Collect (T1, T2) ((TargetTerm T1, TargetTerm T2) \<in> Rel)

goal (1 subgoal):
 1. \<forall>T1 T2. (T1, T2) \<in> TRel \<longrightarrow> (TargetTerm T1, TargetTerm T2) \<in> Rel
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>T1 T2. (T1, T2) \<in> TRel \<longrightarrow> (TargetTerm T1, TargetTerm T2) \<in> Rel

goal (1 subgoal):
 1. \<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>*)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>T1 T2. (T1, T2) \<in> TRel \<longrightarrow> (TargetTerm T1, TargetTerm T2) \<in> Rel

goal (1 subgoal):
 1. \<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>*)
[PROOF STEP]
from TRel_def
[PROOF STATE]
proof (chain)
picking this:
TRel = _Collect (T1, T2) ((TargetTerm T1, TargetTerm T2) \<in> Rel)
[PROOF STEP]
have "\<forall>T1 T2. (TargetTerm T1, TargetTerm T2) \<in> Rel \<longrightarrow> (T1, T2) \<in> TRel\<^sup>+"
[PROOF STATE]
proof (prove)
using this:
TRel = _Collect (T1, T2) ((TargetTerm T1, TargetTerm T2) \<in> Rel)

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

goal (1 subgoal):
 1. \<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>*)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>T1 T2. (TargetTerm T1, TargetTerm T2) \<in> Rel \<longrightarrow> (T1, T2) \<in> TRel\<^sup>+

goal (1 subgoal):
 1. \<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>*)
[PROOF STEP]
from stre TRel_def
[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>=
TRel = _Collect (T1, T2) ((TargetTerm T1, TargetTerm T2) \<in> Rel)
[PROOF STEP]
have "\<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>=
TRel = _Collect (T1, T2) ((TargetTerm T1, TargetTerm T2) \<in> Rel)

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

goal (1 subgoal):
 1. \<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>*)
[PROOF STEP]
ultimately
[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>+
\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel\<^sup>*
[PROOF STEP]
show ?thesis
[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>+
\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel\<^sup>*

goal (1 subgoal):
 1. \<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>*)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<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:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in encoding) SOCom_modulo_TRel_iff_strong_reduction_simulation:
  shows "(\<exists>TRel. strongly_operational_complete (TRel\<^sup>*)
         \<and> strong_reduction_simulation (TRel\<^sup>+) 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 (STCal Source Target))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>TRel. (\<forall>S S'. S \<longmapsto>Source S' \<longrightarrow> (\<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*)) \<and> strong_reduction_simulation (TRel\<^sup>+) Target) = (\<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 (STCal Source Target))
[PROOF STEP]
proof (rule iffI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<exists>TRel. (\<forall>S S'. S \<longmapsto>Source S' \<longrightarrow> (\<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*)) \<and> strong_reduction_simulation (TRel\<^sup>+) Target \<Longrightarrow> \<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 (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 (STCal Source Target) \<Longrightarrow> \<exists>TRel. (\<forall>S S'. S \<longmapsto>Source S' \<longrightarrow> (\<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*)) \<and> strong_reduction_simulation (TRel\<^sup>+) Target
[PROOF STEP]
assume "\<exists>TRel. strongly_operational_complete (TRel\<^sup>*)
          \<and> strong_reduction_simulation (TRel\<^sup>+) Target"
[PROOF STATE]
proof (state)
this:
\<exists>TRel. (\<forall>S S'. S \<longmapsto>Source S' \<longrightarrow> (\<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*)) \<and> strong_reduction_simulation (TRel\<^sup>+) Target

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

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

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

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

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

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

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

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

goal (2 subgoals):
 1. \<exists>TRel. (\<forall>S S'. S \<longmapsto>Source S' \<longrightarrow> (\<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*)) \<and> strong_reduction_simulation (TRel\<^sup>+) Target \<Longrightarrow> \<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 (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 (STCal Source Target) \<Longrightarrow> \<exists>TRel. (\<forall>S S'. S \<longmapsto>Source S' \<longrightarrow> (\<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*)) \<and> strong_reduction_simulation (TRel\<^sup>+) Target
[PROOF STEP]
have "\<forall>S T. SourceTerm S \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm T
                 \<longrightarrow> (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 S'. S \<longmapsto>Source S' \<longrightarrow> (\<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*)) \<and> strong_reduction_simulation (TRel\<^sup>+) Target \<Longrightarrow> \<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 (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 (STCal Source Target) \<Longrightarrow> \<exists>TRel. (\<forall>S S'. S \<longmapsto>Source S' \<longrightarrow> (\<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*)) \<and> strong_reduction_simulation (TRel\<^sup>+) Target
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<forall>P Q P'. P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q \<and> P \<longmapsto>STCal Source Target P' \<longrightarrow> (\<exists>Q'. Q \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q')
\<forall>S. SourceTerm S \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm (\<lbrakk>S\<rbrakk>)
\<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 (STCal Source Target)"
[PROOF STATE]
proof (prove)
using this:
\<forall>P Q P'. P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q \<and> P \<longmapsto>STCal Source Target P' \<longrightarrow> (\<exists>Q'. Q \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q')
\<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 (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 (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 (STCal Source Target) \<Longrightarrow> \<exists>TRel. (\<forall>S S'. S \<longmapsto>Source S' \<longrightarrow> (\<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*)) \<and> strong_reduction_simulation (TRel\<^sup>+) Target
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<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 (STCal Source Target) \<Longrightarrow> \<exists>TRel. (\<forall>S S'. S \<longmapsto>Source S' \<longrightarrow> (\<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*)) \<and> strong_reduction_simulation (TRel\<^sup>+) Target
[PROOF STEP]
assume "\<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 (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 (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 (STCal Source Target) \<Longrightarrow> \<exists>TRel. (\<forall>S S'. S \<longmapsto>Source S' \<longrightarrow> (\<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*)) \<and> strong_reduction_simulation (TRel\<^sup>+) Target
[PROOF STEP]
from 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 (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 (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 (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 (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 (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 (STCal Source Target) \<Longrightarrow> \<exists>TRel. (\<forall>S S'. S \<longmapsto>Source S' \<longrightarrow> (\<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*)) \<and> strong_reduction_simulation (TRel\<^sup>+) Target
[PROOF STEP]
from 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 (STCal Source Target) \<Longrightarrow> \<exists>TRel. (\<forall>S S'. S \<longmapsto>Source S' \<longrightarrow> (\<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*)) \<and> strong_reduction_simulation (TRel\<^sup>+) Target
[PROOF STEP]
with A1 A3
[PROOF STATE]
proof (chain)
picking this:
\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel
strong_reduction_simulation Rel (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_complete (TRel\<^sup>*)
                   \<and> strong_reduction_simulation (TRel\<^sup>+) Target"
[PROOF STATE]
proof (prove)
using this:
\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel
strong_reduction_simulation Rel (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 S'. S \<longmapsto>Source S' \<longrightarrow> (\<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*)) \<and> strong_reduction_simulation (TRel\<^sup>+) Target
[PROOF STEP]
using SOCom_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 (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 S'. S \<longmapsto>Source S' \<longrightarrow> (\<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*)) \<and> strong_reduction_simulation (TRel\<^sup>+) Target) = (\<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 (STCal Source Target))

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

goal (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 (STCal Source Target) \<Longrightarrow> \<exists>TRel. (\<forall>S S'. S \<longmapsto>Source S' \<longrightarrow> (\<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*)) \<and> strong_reduction_simulation (TRel\<^sup>+) Target
[PROOF STEP]
thus "\<exists>TRel. strongly_operational_complete (TRel\<^sup>*)
        \<and> strong_reduction_simulation (TRel\<^sup>+) Target"
[PROOF STATE]
proof (prove)
using this:
(\<forall>S S'. S \<longmapsto>Source S' \<longrightarrow> (\<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*)) \<and> strong_reduction_simulation (TRel\<^sup>+) Target

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in encoding) weak_reduction_contrasimulation_impl_WOSou:
  fixes Rel  :: "(('procS, 'procT) Proc \<times> ('procS, 'procT) Proc) set"
    and TRel :: "('procT \<times> 'procT) set"
  assumes A1: "\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel"
      and A2: "\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel\<^sup>*"
      and A3: "weak_reduction_contrasimulation (Rel\<inverse>) (STCal Source Target)"
  shows "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 A1
[PROOF STATE]
proof (chain)
picking this:
\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel
[PROOF STEP]
have "(TargetTerm (\<lbrakk>S\<rbrakk>), SourceTerm S) \<in> Rel\<inverse>"
[PROOF STATE]
proof (prove)
using this:
\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel

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

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:
(TargetTerm (\<lbrakk>S\<rbrakk>), SourceTerm S) \<in> Rel\<inverse>

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:
(TargetTerm (\<lbrakk>S\<rbrakk>), SourceTerm S) \<in> Rel\<inverse>
TargetTerm (\<lbrakk>S\<rbrakk>) \<longmapsto>STCal Source Target* TargetTerm T
[PROOF STEP]
obtain Q' where A5: "SourceTerm S \<longmapsto>(STCal Source Target)* Q'"
                         and A6: "(Q', TargetTerm T) \<in> Rel\<inverse>"
[PROOF STATE]
proof (prove)
using this:
(TargetTerm (\<lbrakk>S\<rbrakk>), SourceTerm S) \<in> Rel\<inverse>
TargetTerm (\<lbrakk>S\<rbrakk>) \<longmapsto>STCal Source Target* TargetTerm T

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

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

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 A5
[PROOF STATE]
proof (chain)
picking this:
SourceTerm S \<longmapsto>STCal Source Target* Q'
[PROOF STEP]
obtain S' where A7: "S' \<in>S Q'" and A8: "S \<longmapsto>Source* S'"
[PROOF STATE]
proof (prove)
using this:
SourceTerm S \<longmapsto>STCal Source Target* Q'

goal (1 subgoal):
 1. (\<And>S'. S' \<in>S Q' \<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 Q'
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]
have "Q' \<longmapsto>(STCal Source Target)* Q'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Q' \<longmapsto>STCal Source Target* Q'
[PROOF STEP]
by (simp add: steps_refl)
[PROOF STATE]
proof (state)
this:
Q' \<longmapsto>STCal Source Target* Q'

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 A6 A3
[PROOF STATE]
proof (chain)
picking this:
(Q', TargetTerm T) \<in> Rel\<inverse>
weak_reduction_contrasimulation (Rel\<inverse>) (STCal Source Target)
Q' \<longmapsto>STCal Source Target* Q'
[PROOF STEP]
obtain P'' where A9:  "TargetTerm T \<longmapsto>(STCal Source Target)* P''"
                          and A10: "(P'', Q') \<in> Rel\<inverse>"
[PROOF STATE]
proof (prove)
using this:
(Q', TargetTerm T) \<in> Rel\<inverse>
weak_reduction_contrasimulation (Rel\<inverse>) (STCal Source Target)
Q' \<longmapsto>STCal Source Target* Q'

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

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 A9
[PROOF STATE]
proof (chain)
picking this:
TargetTerm T \<longmapsto>STCal Source Target* P''
[PROOF STEP]
obtain T' where A11: "T' \<in>T P''" and A12: "T \<longmapsto>Target* T'"
[PROOF STATE]
proof (prove)
using this:
TargetTerm T \<longmapsto>STCal Source Target* P''

goal (1 subgoal):
 1. (\<And>T'. T' \<in>T P'' \<and> T \<longmapsto>Target* T' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp add: STCal_steps(2))
[PROOF STATE]
proof (state)
this:
T' \<in>T P''
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 A10
[PROOF STATE]
proof (chain)
picking this:
(P'', Q') \<in> Rel\<inverse>
[PROOF STEP]
have "(Q', P'') \<in> Rel"
[PROOF STATE]
proof (prove)
using this:
(P'', Q') \<in> Rel\<inverse>

goal (1 subgoal):
 1. (Q', P'') \<in> Rel
[PROOF STEP]
by induct
[PROOF STATE]
proof (state)
this:
(Q', P'') \<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]
with A2 A7 A11
[PROOF STATE]
proof (chain)
picking this:
\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel\<^sup>*
S' \<in>S Q'
T' \<in>T P''
(Q', P'') \<in> Rel
[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>*
S' \<in>S Q'
T' \<in>T P''
(Q', P'') \<in> Rel

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 A8 A12
[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


[STATEMENT]
lemma (in encoding) weak_reduction_simulation_impl_OSou:
  fixes Rel  :: "(('procS, 'procT) Proc \<times> ('procS, 'procT) Proc) set"
    and TRel :: "('procT \<times> 'procT) set"
  assumes A1: "\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel"
      and A2: "\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel\<^sup>*"
      and A3: "weak_reduction_simulation (Rel\<inverse>) (STCal Source Target)"
  shows "operational_sound (TRel\<^sup>*)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 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'. S \<longmapsto>Source* S' \<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'. S \<longmapsto>Source* S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*
[PROOF STEP]
from A1
[PROOF STATE]
proof (chain)
picking this:
\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel
[PROOF STEP]
have "(TargetTerm (\<lbrakk>S\<rbrakk>), SourceTerm S) \<in> Rel\<inverse>"
[PROOF STATE]
proof (prove)
using this:
\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel

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

goal (1 subgoal):
 1. \<And>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]
moreover
[PROOF STATE]
proof (state)
this:
(TargetTerm (\<lbrakk>S\<rbrakk>), SourceTerm S) \<in> Rel\<inverse>

goal (1 subgoal):
 1. \<And>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]
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'. S \<longmapsto>Source* S' \<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'. S \<longmapsto>Source* S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(TargetTerm (\<lbrakk>S\<rbrakk>), SourceTerm S) \<in> Rel\<inverse>
TargetTerm (\<lbrakk>S\<rbrakk>) \<longmapsto>STCal Source Target* TargetTerm T
[PROOF STEP]
obtain Q' where A5: "SourceTerm S \<longmapsto>(STCal Source Target)* Q'"
                         and A6: "(TargetTerm T, Q') \<in> Rel\<inverse>"
[PROOF STATE]
proof (prove)
using this:
(TargetTerm (\<lbrakk>S\<rbrakk>), SourceTerm S) \<in> Rel\<inverse>
TargetTerm (\<lbrakk>S\<rbrakk>) \<longmapsto>STCal Source Target* TargetTerm T

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

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

goal (1 subgoal):
 1. \<And>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]
from A5
[PROOF STATE]
proof (chain)
picking this:
SourceTerm S \<longmapsto>STCal Source Target* Q'
[PROOF STEP]
obtain S' where A7: "S' \<in>S Q'" and A8: "S \<longmapsto>Source* S'"
[PROOF STATE]
proof (prove)
using this:
SourceTerm S \<longmapsto>STCal Source Target* Q'

goal (1 subgoal):
 1. (\<And>S'. S' \<in>S Q' \<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 Q'
S \<longmapsto>Source* S'

goal (1 subgoal):
 1. \<And>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]
from A6
[PROOF STATE]
proof (chain)
picking this:
(TargetTerm T, Q') \<in> Rel\<inverse>
[PROOF STEP]
have "(Q', TargetTerm T) \<in> Rel"
[PROOF STATE]
proof (prove)
using this:
(TargetTerm T, Q') \<in> Rel\<inverse>

goal (1 subgoal):
 1. (Q', TargetTerm T) \<in> Rel
[PROOF STEP]
by induct
[PROOF STATE]
proof (state)
this:
(Q', TargetTerm T) \<in> Rel

goal (1 subgoal):
 1. \<And>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]
with A2 A7
[PROOF STATE]
proof (chain)
picking this:
\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel\<^sup>*
S' \<in>S Q'
(Q', TargetTerm T) \<in> Rel
[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>*
S' \<in>S Q'
(Q', TargetTerm T) \<in> Rel

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'. S \<longmapsto>Source* S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*
[PROOF STEP]
with A8
[PROOF STATE]
proof (chain)
picking this:
S \<longmapsto>Source* S'
(\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*
[PROOF STEP]
show "\<exists>S'. S \<longmapsto>Source* S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*"
[PROOF STATE]
proof (prove)
using this:
S \<longmapsto>Source* S'
(\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*

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

goal:
No subgoals!
[PROOF STEP]
qed