[STATEMENT]
lemma (in encoding) SOC_wrt_TRel_iff_strong_reduction_bisimulation:
  shows "(\<exists>TRel. strongly_operational_corresponding (TRel\<^sup>*)
         \<and> strong_reduction_bisimulation (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_bisimulation 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> (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*))) \<and> strong_reduction_simulation (TRel\<^sup>+) Target \<and> (\<forall>P Q Q'. (P, Q) \<in> TRel\<^sup>+ \<and> Q \<longmapsto>Target Q' \<longrightarrow> (\<exists>P'. P \<longmapsto>Target P' \<and> (P', Q') \<in> TRel\<^sup>+))) = (\<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) \<and> (\<forall>P Q Q'. (P, Q) \<in> Rel \<and> Q \<longmapsto>STCal Source Target Q' \<longrightarrow> (\<exists>P'. P \<longmapsto>STCal Source Target P' \<and> (P', Q') \<in> Rel)))
[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> (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*))) \<and> strong_reduction_simulation (TRel\<^sup>+) Target \<and> (\<forall>P Q Q'. (P, Q) \<in> TRel\<^sup>+ \<and> Q \<longmapsto>Target Q' \<longrightarrow> (\<exists>P'. P \<longmapsto>Target P' \<and> (P', Q') \<in> TRel\<^sup>+)) \<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) \<and> (\<forall>P Q Q'. (P, Q) \<in> Rel \<and> Q \<longmapsto>STCal Source Target Q' \<longrightarrow> (\<exists>P'. P \<longmapsto>STCal Source Target P' \<and> (P', Q') \<in> Rel))
 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) \<and> (\<forall>P Q Q'. (P, Q) \<in> Rel \<and> Q \<longmapsto>STCal Source Target Q' \<longrightarrow> (\<exists>P'. P \<longmapsto>STCal Source Target P' \<and> (P', Q') \<in> Rel)) \<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> (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*))) \<and> strong_reduction_simulation (TRel\<^sup>+) Target \<and> (\<forall>P Q Q'. (P, Q) \<in> TRel\<^sup>+ \<and> Q \<longmapsto>Target Q' \<longrightarrow> (\<exists>P'. P \<longmapsto>Target P' \<and> (P', Q') \<in> TRel\<^sup>+))
[PROOF STEP]
assume "\<exists>TRel. strongly_operational_corresponding (TRel\<^sup>*)
          \<and> strong_reduction_bisimulation (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> (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*))) \<and> strong_reduction_simulation (TRel\<^sup>+) Target \<and> (\<forall>P Q Q'. (P, Q) \<in> TRel\<^sup>+ \<and> Q \<longmapsto>Target Q' \<longrightarrow> (\<exists>P'. P \<longmapsto>Target P' \<and> (P', Q') \<in> 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> (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*))) \<and> strong_reduction_simulation (TRel\<^sup>+) Target \<and> (\<forall>P Q Q'. (P, Q) \<in> TRel\<^sup>+ \<and> Q \<longmapsto>Target Q' \<longrightarrow> (\<exists>P'. P \<longmapsto>Target P' \<and> (P', Q') \<in> TRel\<^sup>+)) \<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) \<and> (\<forall>P Q Q'. (P, Q) \<in> Rel \<and> Q \<longmapsto>STCal Source Target Q' \<longrightarrow> (\<exists>P'. P \<longmapsto>STCal Source Target P' \<and> (P', Q') \<in> Rel))
 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) \<and> (\<forall>P Q Q'. (P, Q) \<in> Rel \<and> Q \<longmapsto>STCal Source Target Q' \<longrightarrow> (\<exists>P'. P \<longmapsto>STCal Source Target P' \<and> (P', Q') \<in> Rel)) \<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> (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*))) \<and> strong_reduction_simulation (TRel\<^sup>+) Target \<and> (\<forall>P Q Q'. (P, Q) \<in> TRel\<^sup>+ \<and> Q \<longmapsto>Target Q' \<longrightarrow> (\<exists>P'. P \<longmapsto>Target P' \<and> (P', Q') \<in> TRel\<^sup>+))
[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> (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*))) \<and> strong_reduction_simulation (TRel\<^sup>+) Target \<and> (\<forall>P Q Q'. (P, Q) \<in> TRel\<^sup>+ \<and> Q \<longmapsto>Target Q' \<longrightarrow> (\<exists>P'. P \<longmapsto>Target P' \<and> (P', Q') \<in> TRel\<^sup>+))
[PROOF STEP]
obtain TRel where "strongly_operational_corresponding (TRel\<^sup>*)"
                          and "strong_reduction_bisimulation (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> (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*))) \<and> strong_reduction_simulation (TRel\<^sup>+) Target \<and> (\<forall>P Q Q'. (P, Q) \<in> TRel\<^sup>+ \<and> Q \<longmapsto>Target Q' \<longrightarrow> (\<exists>P'. P \<longmapsto>Target P' \<and> (P', Q') \<in> TRel\<^sup>+))

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> (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*))) \<and> strong_reduction_simulation (TRel\<^sup>+) Target \<and> (\<forall>P Q Q'. (P, Q) \<in> TRel\<^sup>+ \<and> Q \<longmapsto>Target Q' \<longrightarrow> (\<exists>P'. P \<longmapsto>Target P' \<and> (P', Q') \<in> TRel\<^sup>+)) \<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>*)) \<and> (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*))
strong_reduction_simulation (TRel\<^sup>+) Target \<and> (\<forall>P Q Q'. (P, Q) \<in> TRel\<^sup>+ \<and> Q \<longmapsto>Target Q' \<longrightarrow> (\<exists>P'. P \<longmapsto>Target P' \<and> (P', Q') \<in> 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> (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*))) \<and> strong_reduction_simulation (TRel\<^sup>+) Target \<and> (\<forall>P Q Q'. (P, Q) \<in> TRel\<^sup>+ \<and> Q \<longmapsto>Target Q' \<longrightarrow> (\<exists>P'. P \<longmapsto>Target P' \<and> (P', Q') \<in> TRel\<^sup>+)) \<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) \<and> (\<forall>P Q Q'. (P, Q) \<in> Rel \<and> Q \<longmapsto>STCal Source Target Q' \<longrightarrow> (\<exists>P'. P \<longmapsto>STCal Source Target P' \<and> (P', Q') \<in> Rel))
 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) \<and> (\<forall>P Q Q'. (P, Q) \<in> Rel \<and> Q \<longmapsto>STCal Source Target Q' \<longrightarrow> (\<exists>P'. P \<longmapsto>STCal Source Target P' \<and> (P', Q') \<in> Rel)) \<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> (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*))) \<and> strong_reduction_simulation (TRel\<^sup>+) Target \<and> (\<forall>P Q Q'. (P, Q) \<in> TRel\<^sup>+ \<and> Q \<longmapsto>Target Q' \<longrightarrow> (\<exists>P'. P \<longmapsto>Target P' \<and> (P', Q') \<in> TRel\<^sup>+))
[PROOF STEP]
hence "strong_reduction_bisimulation (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>*)) \<and> (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*))
strong_reduction_simulation (TRel\<^sup>+) Target \<and> (\<forall>P Q Q'. (P, Q) \<in> TRel\<^sup>+ \<and> Q \<longmapsto>Target Q' \<longrightarrow> (\<exists>P'. P \<longmapsto>Target P' \<and> (P', Q') \<in> TRel\<^sup>+))

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

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

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

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

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) \<and> (\<forall>P Q Q'. (P, Q) \<in> Rel \<and> Q \<longmapsto>STCal Source Target Q' \<longrightarrow> (\<exists>P'. P \<longmapsto>STCal Source Target P' \<and> (P', Q') \<in> Rel)) \<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> (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*))) \<and> strong_reduction_simulation (TRel\<^sup>+) Target \<and> (\<forall>P Q Q'. (P, Q) \<in> TRel\<^sup>+ \<and> Q \<longmapsto>Target Q' \<longrightarrow> (\<exists>P'. P \<longmapsto>Target P' \<and> (P', Q') \<in> TRel\<^sup>+))
[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) \<and> (\<forall>P Q Q'. (P, Q) \<in> Rel \<and> Q \<longmapsto>STCal Source Target Q' \<longrightarrow> (\<exists>P'. P \<longmapsto>STCal Source Target P' \<and> (P', Q') \<in> Rel)) \<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> (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*))) \<and> strong_reduction_simulation (TRel\<^sup>+) Target \<and> (\<forall>P Q Q'. (P, Q) \<in> TRel\<^sup>+ \<and> Q \<longmapsto>Target Q' \<longrightarrow> (\<exists>P'. P \<longmapsto>Target P' \<and> (P', Q') \<in> TRel\<^sup>+))
[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_bisimulation 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) \<and> (\<forall>P Q Q'. (P, Q) \<in> Rel \<and> Q \<longmapsto>STCal Source Target Q' \<longrightarrow> (\<exists>P'. P \<longmapsto>STCal Source Target P' \<and> (P', Q') \<in> Rel))

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) \<and> (\<forall>P Q Q'. (P, Q) \<in> Rel \<and> Q \<longmapsto>STCal Source Target Q' \<longrightarrow> (\<exists>P'. P \<longmapsto>STCal Source Target P' \<and> (P', Q') \<in> Rel)) \<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> (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*))) \<and> strong_reduction_simulation (TRel\<^sup>+) Target \<and> (\<forall>P Q Q'. (P, Q) \<in> TRel\<^sup>+ \<and> Q \<longmapsto>Target Q' \<longrightarrow> (\<exists>P'. P \<longmapsto>Target P' \<and> (P', Q') \<in> TRel\<^sup>+))
[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) \<and> (\<forall>P Q Q'. (P, Q) \<in> Rel \<and> Q \<longmapsto>STCal Source Target Q' \<longrightarrow> (\<exists>P'. P \<longmapsto>STCal Source Target P' \<and> (P', Q') \<in> Rel))
[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_bisimulation 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) \<and> (\<forall>P Q Q'. (P, Q) \<in> Rel \<and> Q \<longmapsto>STCal Source Target Q' \<longrightarrow> (\<exists>P'. P \<longmapsto>STCal Source Target P' \<and> (P', Q') \<in> Rel))

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) \<and> (\<forall>P Q Q'. (P, Q) \<in> Rel \<and> Q \<longmapsto>STCal Source Target Q' \<longrightarrow> (\<exists>P'. P \<longmapsto>STCal Source Target P' \<and> (P', Q') \<in> Rel)) \<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) \<and> (\<forall>P Q Q'. (P, Q) \<in> Rel \<and> Q \<longmapsto>STCal Source Target Q' \<longrightarrow> (\<exists>P'. P \<longmapsto>STCal Source Target P' \<and> (P', Q') \<in> Rel))

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

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) \<and> (\<forall>P Q Q'. (P, Q) \<in> Rel \<and> Q \<longmapsto>STCal Source Target Q' \<longrightarrow> (\<exists>P'. P \<longmapsto>STCal Source Target P' \<and> (P', Q') \<in> Rel))
[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) \<and> (\<forall>P Q Q'. (P, Q) \<in> Rel \<and> Q \<longmapsto>STCal Source Target Q' \<longrightarrow> (\<exists>P'. P \<longmapsto>STCal Source Target P' \<and> (P', Q') \<in> Rel))

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) \<and> (\<forall>P Q Q'. (P, Q) \<in> Rel \<and> Q \<longmapsto>STCal Source Target Q' \<longrightarrow> (\<exists>P'. P \<longmapsto>STCal Source Target P' \<and> (P', Q') \<in> Rel)) \<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> (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*))) \<and> strong_reduction_simulation (TRel\<^sup>+) Target \<and> (\<forall>P Q Q'. (P, Q) \<in> TRel\<^sup>+ \<and> Q \<longmapsto>Target Q' \<longrightarrow> (\<exists>P'. P \<longmapsto>Target P' \<and> (P', Q') \<in> TRel\<^sup>+))
[PROOF STEP]
hence "strongly_operational_corresponding (TRel\<^sup>*)
         \<and> strong_reduction_bisimulation (TRel\<^sup>+) 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) \<and> (\<forall>P Q Q'. (P, Q) \<in> Rel \<and> Q \<longmapsto>STCal Source Target Q' \<longrightarrow> (\<exists>P'. P \<longmapsto>STCal Source Target P' \<and> (P', Q') \<in> Rel))

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> (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*))) \<and> strong_reduction_simulation (TRel\<^sup>+) Target \<and> (\<forall>P Q Q'. (P, Q) \<in> TRel\<^sup>+ \<and> Q \<longmapsto>Target Q' \<longrightarrow> (\<exists>P'. P \<longmapsto>Target P' \<and> (P', Q') \<in> TRel\<^sup>+))
[PROOF STEP]
using SOC_iff_strong_reduction_bisimulation[where TRel="TRel"]
[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) \<and> (\<forall>P Q Q'. (P, Q) \<in> Rel \<and> Q \<longmapsto>STCal Source Target Q' \<longrightarrow> (\<exists>P'. P \<longmapsto>STCal Source Target P' \<and> (P', Q') \<in> Rel))
(((\<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> (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*))) \<and> strong_reduction_simulation (TRel\<^sup>+) Target \<and> (\<forall>P Q Q'. (P, Q) \<in> TRel\<^sup>+ \<and> Q \<longmapsto>Target Q' \<longrightarrow> (\<exists>P'. P \<longmapsto>Target P' \<and> (P', Q') \<in> TRel\<^sup>+))) = (\<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) \<and> (\<forall>P Q Q'. (P, Q) \<in> Rel \<and> Q \<longmapsto>STCal Source Target Q' \<longrightarrow> (\<exists>P'. P \<longmapsto>STCal Source Target P' \<and> (P', Q') \<in> Rel)))

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> (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*))) \<and> strong_reduction_simulation (TRel\<^sup>+) Target \<and> (\<forall>P Q Q'. (P, Q) \<in> TRel\<^sup>+ \<and> Q \<longmapsto>Target Q' \<longrightarrow> (\<exists>P'. P \<longmapsto>Target P' \<and> (P', Q') \<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>*)) \<and> (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*))) \<and> strong_reduction_simulation (TRel\<^sup>+) Target \<and> (\<forall>P Q Q'. (P, Q) \<in> TRel\<^sup>+ \<and> Q \<longmapsto>Target Q' \<longrightarrow> (\<exists>P'. P \<longmapsto>Target P' \<and> (P', Q') \<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) \<and> (\<forall>P Q Q'. (P, Q) \<in> Rel \<and> Q \<longmapsto>STCal Source Target Q' \<longrightarrow> (\<exists>P'. P \<longmapsto>STCal Source Target P' \<and> (P', Q') \<in> Rel)) \<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> (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*))) \<and> strong_reduction_simulation (TRel\<^sup>+) Target \<and> (\<forall>P Q Q'. (P, Q) \<in> TRel\<^sup>+ \<and> Q \<longmapsto>Target Q' \<longrightarrow> (\<exists>P'. P \<longmapsto>Target P' \<and> (P', Q') \<in> TRel\<^sup>+))
[PROOF STEP]
thus "\<exists>TRel. strongly_operational_corresponding (TRel\<^sup>*)
        \<and> strong_reduction_bisimulation (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> (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*))) \<and> strong_reduction_simulation (TRel\<^sup>+) Target \<and> (\<forall>P Q Q'. (P, Q) \<in> TRel\<^sup>+ \<and> Q \<longmapsto>Target Q' \<longrightarrow> (\<exists>P'. P \<longmapsto>Target P' \<and> (P', Q') \<in> TRel\<^sup>+))

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> (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*))) \<and> strong_reduction_simulation (TRel\<^sup>+) Target \<and> (\<forall>P Q Q'. (P, Q) \<in> TRel\<^sup>+ \<and> Q \<longmapsto>Target Q' \<longrightarrow> (\<exists>P'. P \<longmapsto>Target P' \<and> (P', Q') \<in> TRel\<^sup>+))
[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> (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*))) \<and> strong_reduction_simulation (TRel\<^sup>+) Target \<and> (\<forall>P Q Q'. (P, Q) \<in> TRel\<^sup>+ \<and> Q \<longmapsto>Target Q' \<longrightarrow> (\<exists>P'. P \<longmapsto>Target P' \<and> (P', Q') \<in> TRel\<^sup>+))

goal:
No subgoals!
[PROOF STEP]
qed