[STATEMENT]
lemma (in encoding) SOC_iff_indRelRTPO_is_strong_reduction_bisimulation:
  fixes TRel :: "('procT \<times> 'procT) set"
  shows "(strongly_operational_corresponding (TRel\<^sup>*)
         \<and> strong_reduction_bisimulation (TRel\<^sup>+) Target)
         = strong_reduction_bisimulation (indRelRTPO TRel) (STCal Source Target)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (((\<forall>S S'. S \<longmapsto>Source S' \<longrightarrow> (\<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*)) \<and> (\<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')))
[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> (\<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> (\<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'))
 2. (\<forall>P Q P'. P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q \<and> P \<longmapsto>STCal Source Target P' \<longrightarrow> (\<exists>Q'. Q \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q')) \<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')) \<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> (\<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 ocorr: "strongly_operational_corresponding (TRel\<^sup>*)"
     and bisim: "strong_reduction_bisimulation (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>*)) \<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. ((\<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> (\<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'))
 2. (\<forall>P Q P'. P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q \<and> P \<longmapsto>STCal Source Target P' \<longrightarrow> (\<exists>Q'. Q \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q')) \<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')) \<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> (\<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_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>*)) \<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')
[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>*)) \<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> 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> (\<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> (\<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'))
 2. (\<forall>P Q P'. P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q \<and> P \<longmapsto>STCal Source Target P' \<longrightarrow> (\<exists>Q'. Q \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q')) \<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')) \<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> (\<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')

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> (\<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> (\<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'))
 2. (\<forall>P Q P'. P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q \<and> P \<longmapsto>STCal Source Target P' \<longrightarrow> (\<exists>Q'. Q \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q')) \<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')) \<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> (\<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 bisim
[PROOF STATE]
proof (chain)
picking this:
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 "strong_reduction_simulation ((TRel\<^sup>+)\<inverse>) Target"
[PROOF STATE]
proof (prove)
using this:
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. strong_reduction_simulation ((TRel\<^sup>+)\<inverse>) Target
[PROOF STEP]
using strong_reduction_bisimulations_impl_inverse_is_simulation[where Rel="TRel\<^sup>+"]
[PROOF STATE]
proof (prove)
using this:
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>+))
strong_reduction_simulation (TRel\<^sup>+) ?Cal \<and> (\<forall>P Q Q'. (P, Q) \<in> TRel\<^sup>+ \<and> Q \<longmapsto>?Cal Q' \<longrightarrow> (\<exists>P'. P \<longmapsto>?Cal P' \<and> (P', Q') \<in> TRel\<^sup>+)) \<Longrightarrow> strong_reduction_simulation ((TRel\<^sup>+)\<inverse>) ?Cal

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

goal (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> (\<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> (\<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'))
 2. (\<forall>P Q P'. P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q \<and> P \<longmapsto>STCal Source Target P' \<longrightarrow> (\<exists>Q'. Q \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q')) \<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')) \<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> (\<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 ocorr
[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>*)) \<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>+)\<inverse>) Target
[PROOF STEP]
have "strong_reduction_simulation ((indRelRTPO TRel)\<inverse>) (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>+)\<inverse>) Target

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

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

goal (2 subgoals):
 1. ((\<forall>S 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> (\<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'))
 2. (\<forall>P Q P'. P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q \<and> P \<longmapsto>STCal Source Target P' \<longrightarrow> (\<exists>Q'. Q \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q')) \<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')) \<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> (\<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')
strong_reduction_simulation ((indRelRTPO TRel)\<inverse>) (STCal Source Target)
[PROOF STEP]
show "strong_reduction_bisimulation (indRelRTPO TRel) (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')
strong_reduction_simulation ((indRelRTPO TRel)\<inverse>) (STCal Source 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')) \<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 strong_reduction_simulations_impl_bisimulation[where Rel="indRelRTPO TRel"]
[PROOF STATE]
proof (prove)
using this:
\<forall>P Q P'. P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q \<and> P \<longmapsto>STCal Source Target P' \<longrightarrow> (\<exists>Q'. Q \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q')
strong_reduction_simulation ((indRelRTPO TRel)\<inverse>) (STCal Source Target)
(\<forall>P Q P'. P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q \<and> P \<longmapsto>?Cal P' \<longrightarrow> (\<exists>Q'. Q \<longmapsto>?Cal Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q')) \<and> strong_reduction_simulation ((indRelRTPO TRel)\<inverse>) ?Cal \<Longrightarrow> (\<forall>P Q P'. P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q \<and> P \<longmapsto>?Cal P' \<longrightarrow> (\<exists>Q'. Q \<longmapsto>?Cal 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>?Cal Q' \<longrightarrow> (\<exists>P'. P \<longmapsto>?Cal 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 (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')) \<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> (\<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. (\<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')) \<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> (\<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 bisim: "strong_reduction_bisimulation (indRelRTPO TRel) (STCal Source Target)"
[PROOF STATE]
proof (state)
this:
(\<forall>P Q P'. P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q \<and> P \<longmapsto>STCal Source Target P' \<longrightarrow> (\<exists>Q'. Q \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q')) \<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')) \<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> (\<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_complete (TRel\<^sup>*) \<and> strong_reduction_simulation (TRel\<^sup>+) Target"
[PROOF STATE]
proof (prove)
using this:
(\<forall>P Q P'. P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q \<and> P \<longmapsto>STCal Source Target P' \<longrightarrow> (\<exists>Q'. Q \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q')) \<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>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_indRelRTPO_is_strong_reduction_simulation[where TRel="TRel"]
[PROOF STATE]
proof (prove)
using this:
(\<forall>P Q P'. P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q \<and> P \<longmapsto>STCal Source Target P' \<longrightarrow> (\<exists>Q'. Q \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q')) \<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 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>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 (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')) \<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> (\<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 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. (\<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')) \<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> (\<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 bisim
[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'))
[PROOF STEP]
have "strong_reduction_simulation ((indRelRTPO TRel)\<inverse>) (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'))

goal (1 subgoal):
 1. strong_reduction_simulation ((indRelRTPO TRel)\<inverse>) (STCal Source Target)
[PROOF STEP]
using strong_reduction_bisimulations_impl_inverse_is_simulation[where Rel="indRelRTPO TRel"]
[PROOF STATE]
proof (prove)
using this:
(\<forall>P Q P'. P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q \<and> P \<longmapsto>STCal Source Target P' \<longrightarrow> (\<exists>Q'. Q \<longmapsto>STCal Source Target Q' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q')) \<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>P Q P'. P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q \<and> P \<longmapsto>?Cal P' \<longrightarrow> (\<exists>Q'. Q \<longmapsto>?Cal 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>?Cal Q' \<longrightarrow> (\<exists>P'. P \<longmapsto>?Cal P' \<and> P' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q')) \<Longrightarrow> strong_reduction_simulation ((indRelRTPO TRel)\<inverse>) ?Cal

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

goal (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')) \<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> (\<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_sound (TRel\<^sup>*) \<and> strong_reduction_simulation ((TRel\<^sup>+)\<inverse>) Target"
[PROOF STATE]
proof (prove)
using this:
strong_reduction_simulation ((indRelRTPO TRel)\<inverse>) (STCal Source Target)

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

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

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

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 strong_reduction_simulations_impl_bisimulation[where Rel="TRel\<^sup>+"]
[PROOF STATE]
proof (prove)
using this:
(\<forall>S S'. S \<longmapsto>Source S' \<longrightarrow> (\<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*)) \<and> strong_reduction_simulation (TRel\<^sup>+) Target
(\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*)) \<and> strong_reduction_simulation ((TRel\<^sup>+)\<inverse>) Target
strong_reduction_simulation (TRel\<^sup>+) ?Cal \<and> strong_reduction_simulation ((TRel\<^sup>+)\<inverse>) ?Cal \<Longrightarrow> strong_reduction_simulation (TRel\<^sup>+) ?Cal \<and> (\<forall>P Q Q'. (P, Q) \<in> TRel\<^sup>+ \<and> Q \<longmapsto>?Cal Q' \<longrightarrow> (\<exists>P'. P \<longmapsto>?Cal P' \<and> (P', Q') \<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> (\<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:
No subgoals!
[PROOF STEP]
qed