[STATEMENT]
lemma (in encoding) SOC_wrt_equivalence_iff_strong_reduction_bisimulation:
  fixes TRel :: "('procT \<times> 'procT) set"
  assumes eqT: "equivalence TRel"
  shows "(strongly_operational_corresponding TRel \<and> strong_reduction_bisimulation TRel Target)
         \<longleftrightarrow> (\<exists>Rel.
         (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel \<and> (TargetTerm (\<lbrakk>S\<rbrakk>), SourceTerm S) \<in> Rel)
         \<and> TRel = {(T1, T2). (TargetTerm T1, TargetTerm T2) \<in> Rel}
         \<and> trans Rel \<and> strong_reduction_bisimulation Rel (STCal Source Target))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (((\<forall>S S'. S \<longmapsto>Source S' \<longrightarrow> (\<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel)) \<and> (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel))) \<and> strong_reduction_simulation TRel Target \<and> (\<forall>P Q Q'. (P, Q) \<in> TRel \<and> Q \<longmapsto>Target Q' \<longrightarrow> (\<exists>P'. P \<longmapsto>Target P' \<and> (P', Q') \<in> TRel))) = (\<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel \<and> (TargetTerm (\<lbrakk>S\<rbrakk>), SourceTerm S) \<in> Rel) \<and> TRel = _Collect (T1, T2) ((TargetTerm T1, TargetTerm T2) \<in> Rel) \<and> trans Rel \<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, 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)) \<and> (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel))) \<and> strong_reduction_simulation TRel Target \<and> (\<forall>P Q Q'. (P, Q) \<in> TRel \<and> Q \<longmapsto>Target Q' \<longrightarrow> (\<exists>P'. P \<longmapsto>Target P' \<and> (P', Q') \<in> TRel)) \<Longrightarrow> \<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel \<and> (TargetTerm (\<lbrakk>S\<rbrakk>), SourceTerm S) \<in> Rel) \<and> TRel = _Collect (T1, T2) ((TargetTerm T1, TargetTerm T2) \<in> Rel) \<and> trans Rel \<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> (TargetTerm (\<lbrakk>S\<rbrakk>), SourceTerm S) \<in> Rel) \<and> TRel = _Collect (T1, T2) ((TargetTerm T1, TargetTerm T2) \<in> Rel) \<and> trans Rel \<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> ((\<forall>S S'. S \<longmapsto>Source S' \<longrightarrow> (\<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel)) \<and> (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel))) \<and> strong_reduction_simulation TRel Target \<and> (\<forall>P Q Q'. (P, Q) \<in> TRel \<and> Q \<longmapsto>Target Q' \<longrightarrow> (\<exists>P'. P \<longmapsto>Target P' \<and> (P', Q') \<in> TRel))
[PROOF STEP]
assume oc:     "strongly_operational_corresponding TRel"
     and bisimT: "strong_reduction_bisimulation TRel 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)) \<and> (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel))
strong_reduction_simulation TRel Target \<and> (\<forall>P Q Q'. (P, Q) \<in> TRel \<and> Q \<longmapsto>Target Q' \<longrightarrow> (\<exists>P'. P \<longmapsto>Target P' \<and> (P', Q') \<in> TRel))

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)) \<and> (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel))) \<and> strong_reduction_simulation TRel Target \<and> (\<forall>P Q Q'. (P, Q) \<in> TRel \<and> Q \<longmapsto>Target Q' \<longrightarrow> (\<exists>P'. P \<longmapsto>Target P' \<and> (P', Q') \<in> TRel)) \<Longrightarrow> \<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel \<and> (TargetTerm (\<lbrakk>S\<rbrakk>), SourceTerm S) \<in> Rel) \<and> TRel = _Collect (T1, T2) ((TargetTerm T1, TargetTerm T2) \<in> Rel) \<and> trans Rel \<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> (TargetTerm (\<lbrakk>S\<rbrakk>), SourceTerm S) \<in> Rel) \<and> TRel = _Collect (T1, T2) ((TargetTerm T1, TargetTerm T2) \<in> Rel) \<and> trans Rel \<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> ((\<forall>S S'. S \<longmapsto>Source S' \<longrightarrow> (\<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel)) \<and> (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel))) \<and> strong_reduction_simulation TRel Target \<and> (\<forall>P Q Q'. (P, Q) \<in> TRel \<and> Q \<longmapsto>Target Q' \<longrightarrow> (\<exists>P'. P \<longmapsto>Target P' \<and> (P', Q') \<in> TRel))
[PROOF STEP]
from eqT
[PROOF STATE]
proof (chain)
picking this:
equivalence TRel
[PROOF STEP]
have rt: "TRel\<^sup>* = TRel"
[PROOF STATE]
proof (prove)
using this:
equivalence TRel

goal (1 subgoal):
 1. TRel\<^sup>* = TRel
[PROOF STEP]
using reflcl_trancl[of TRel] trancl_id[of TRel]
[PROOF STATE]
proof (prove)
using this:
equivalence TRel
(TRel\<^sup>+)\<^sup>= = TRel\<^sup>*
trans TRel \<Longrightarrow> TRel\<^sup>+ = TRel

goal (1 subgoal):
 1. TRel\<^sup>* = TRel
[PROOF STEP]
unfolding equiv_def refl_on_def
[PROOF STATE]
proof (prove)
using this:
(TRel \<subseteq> UNIV \<times> UNIV \<and> (\<forall>x\<in>UNIV. (x, x) \<in> TRel)) \<and> sym TRel \<and> trans TRel
(TRel\<^sup>+)\<^sup>= = TRel\<^sup>*
trans TRel \<Longrightarrow> TRel\<^sup>+ = TRel

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

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)) \<and> (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel))) \<and> strong_reduction_simulation TRel Target \<and> (\<forall>P Q Q'. (P, Q) \<in> TRel \<and> Q \<longmapsto>Target Q' \<longrightarrow> (\<exists>P'. P \<longmapsto>Target P' \<and> (P', Q') \<in> TRel)) \<Longrightarrow> \<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel \<and> (TargetTerm (\<lbrakk>S\<rbrakk>), SourceTerm S) \<in> Rel) \<and> TRel = _Collect (T1, T2) ((TargetTerm T1, TargetTerm T2) \<in> Rel) \<and> trans Rel \<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> (TargetTerm (\<lbrakk>S\<rbrakk>), SourceTerm S) \<in> Rel) \<and> TRel = _Collect (T1, T2) ((TargetTerm T1, TargetTerm T2) \<in> Rel) \<and> trans Rel \<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> ((\<forall>S S'. S \<longmapsto>Source S' \<longrightarrow> (\<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel)) \<and> (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel))) \<and> strong_reduction_simulation TRel Target \<and> (\<forall>P Q Q'. (P, Q) \<in> TRel \<and> Q \<longmapsto>Target Q' \<longrightarrow> (\<exists>P'. P \<longmapsto>Target P' \<and> (P', Q') \<in> TRel))
[PROOF STEP]
have "\<forall>S. SourceTerm S \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> TargetTerm (\<lbrakk>S\<rbrakk>) \<and> TargetTerm (\<lbrakk>S\<rbrakk>) \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> SourceTerm S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>S. SourceTerm S \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> TargetTerm (\<lbrakk>S\<rbrakk>) \<and> TargetTerm (\<lbrakk>S\<rbrakk>) \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> SourceTerm S
[PROOF STEP]
by (simp add: indRelTEQ.encR indRelTEQ.encL)
[PROOF STATE]
proof (state)
this:
\<forall>S. SourceTerm S \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> TargetTerm (\<lbrakk>S\<rbrakk>) \<and> TargetTerm (\<lbrakk>S\<rbrakk>) \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> SourceTerm S

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)) \<and> (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel))) \<and> strong_reduction_simulation TRel Target \<and> (\<forall>P Q Q'. (P, Q) \<in> TRel \<and> Q \<longmapsto>Target Q' \<longrightarrow> (\<exists>P'. P \<longmapsto>Target P' \<and> (P', Q') \<in> TRel)) \<Longrightarrow> \<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel \<and> (TargetTerm (\<lbrakk>S\<rbrakk>), SourceTerm S) \<in> Rel) \<and> TRel = _Collect (T1, T2) ((TargetTerm T1, TargetTerm T2) \<in> Rel) \<and> trans Rel \<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> (TargetTerm (\<lbrakk>S\<rbrakk>), SourceTerm S) \<in> Rel) \<and> TRel = _Collect (T1, T2) ((TargetTerm T1, TargetTerm T2) \<in> Rel) \<and> trans Rel \<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> ((\<forall>S S'. S \<longmapsto>Source S' \<longrightarrow> (\<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel)) \<and> (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel))) \<and> strong_reduction_simulation TRel Target \<and> (\<forall>P Q Q'. (P, Q) \<in> TRel \<and> Q \<longmapsto>Target Q' \<longrightarrow> (\<exists>P'. P \<longmapsto>Target P' \<and> (P', Q') \<in> TRel))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>S. SourceTerm S \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> TargetTerm (\<lbrakk>S\<rbrakk>) \<and> TargetTerm (\<lbrakk>S\<rbrakk>) \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> SourceTerm S

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)) \<and> (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel))) \<and> strong_reduction_simulation TRel Target \<and> (\<forall>P Q Q'. (P, Q) \<in> TRel \<and> Q \<longmapsto>Target Q' \<longrightarrow> (\<exists>P'. P \<longmapsto>Target P' \<and> (P', Q') \<in> TRel)) \<Longrightarrow> \<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel \<and> (TargetTerm (\<lbrakk>S\<rbrakk>), SourceTerm S) \<in> Rel) \<and> TRel = _Collect (T1, T2) ((TargetTerm T1, TargetTerm T2) \<in> Rel) \<and> trans Rel \<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> (TargetTerm (\<lbrakk>S\<rbrakk>), SourceTerm S) \<in> Rel) \<and> TRel = _Collect (T1, T2) ((TargetTerm T1, TargetTerm T2) \<in> Rel) \<and> trans Rel \<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> ((\<forall>S S'. S \<longmapsto>Source S' \<longrightarrow> (\<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel)) \<and> (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel))) \<and> strong_reduction_simulation TRel Target \<and> (\<forall>P Q Q'. (P, Q) \<in> TRel \<and> Q \<longmapsto>Target Q' \<longrightarrow> (\<exists>P'. P \<longmapsto>Target P' \<and> (P', Q') \<in> TRel))
[PROOF STEP]
from rt
[PROOF STATE]
proof (chain)
picking this:
TRel\<^sup>* = TRel
[PROOF STEP]
have "TRel = {(T1, T2). TargetTerm T1 \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> TargetTerm T2}"
[PROOF STATE]
proof (prove)
using this:
TRel\<^sup>* = TRel

goal (1 subgoal):
 1. TRel = _Collect (T1, T2) (TargetTerm T1 \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> TargetTerm T2)
[PROOF STEP]
using indRelTEQ_to_TRel(4)[where TRel="TRel"]
            trans_closure_of_TRel_refl_cond[where TRel="TRel"]
[PROOF STATE]
proof (prove)
using this:
TRel\<^sup>* = TRel
?P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> ?Q \<Longrightarrow> \<forall>TP TQ. TP \<in>T ?P \<and> TQ \<in>T ?Q \<longrightarrow> (TP, TQ) \<in> (TRel \<union> _Collect (T1, T2) (\<exists>S. T1 = \<lbrakk>S\<rbrakk> \<and> T2 = \<lbrakk>S\<rbrakk>))\<^sup>+
(?TP, ?TQ) \<in> (TRel \<union> _Collect (T1, T2) (\<exists>S. T1 = \<lbrakk>S\<rbrakk> \<and> T2 = \<lbrakk>S\<rbrakk>))\<^sup>+ \<Longrightarrow> (?TP, ?TQ) \<in> TRel\<^sup>*

goal (1 subgoal):
 1. TRel = _Collect (T1, T2) (TargetTerm T1 \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> TargetTerm T2)
[PROOF STEP]
by (auto simp add: indRelTEQ.target)
[PROOF STATE]
proof (state)
this:
TRel = _Collect (T1, T2) (TargetTerm T1 \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> TargetTerm T2)

goal (2 subgoals):
 1. ((\<forall>S S'. S \<longmapsto>Source S' \<longrightarrow> (\<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel)) \<and> (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel))) \<and> strong_reduction_simulation TRel Target \<and> (\<forall>P Q Q'. (P, Q) \<in> TRel \<and> Q \<longmapsto>Target Q' \<longrightarrow> (\<exists>P'. P \<longmapsto>Target P' \<and> (P', Q') \<in> TRel)) \<Longrightarrow> \<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel \<and> (TargetTerm (\<lbrakk>S\<rbrakk>), SourceTerm S) \<in> Rel) \<and> TRel = _Collect (T1, T2) ((TargetTerm T1, TargetTerm T2) \<in> Rel) \<and> trans Rel \<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> (TargetTerm (\<lbrakk>S\<rbrakk>), SourceTerm S) \<in> Rel) \<and> TRel = _Collect (T1, T2) ((TargetTerm T1, TargetTerm T2) \<in> Rel) \<and> trans Rel \<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> ((\<forall>S S'. S \<longmapsto>Source S' \<longrightarrow> (\<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel)) \<and> (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel))) \<and> strong_reduction_simulation TRel Target \<and> (\<forall>P Q Q'. (P, Q) \<in> TRel \<and> Q \<longmapsto>Target Q' \<longrightarrow> (\<exists>P'. P \<longmapsto>Target P' \<and> (P', Q') \<in> TRel))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
TRel = _Collect (T1, T2) (TargetTerm T1 \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> TargetTerm T2)

goal (2 subgoals):
 1. ((\<forall>S S'. S \<longmapsto>Source S' \<longrightarrow> (\<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel)) \<and> (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel))) \<and> strong_reduction_simulation TRel Target \<and> (\<forall>P Q Q'. (P, Q) \<in> TRel \<and> Q \<longmapsto>Target Q' \<longrightarrow> (\<exists>P'. P \<longmapsto>Target P' \<and> (P', Q') \<in> TRel)) \<Longrightarrow> \<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel \<and> (TargetTerm (\<lbrakk>S\<rbrakk>), SourceTerm S) \<in> Rel) \<and> TRel = _Collect (T1, T2) ((TargetTerm T1, TargetTerm T2) \<in> Rel) \<and> trans Rel \<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> (TargetTerm (\<lbrakk>S\<rbrakk>), SourceTerm S) \<in> Rel) \<and> TRel = _Collect (T1, T2) ((TargetTerm T1, TargetTerm T2) \<in> Rel) \<and> trans Rel \<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> ((\<forall>S S'. S \<longmapsto>Source S' \<longrightarrow> (\<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel)) \<and> (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel))) \<and> strong_reduction_simulation TRel Target \<and> (\<forall>P Q Q'. (P, Q) \<in> TRel \<and> Q \<longmapsto>Target Q' \<longrightarrow> (\<exists>P'. P \<longmapsto>Target P' \<and> (P', Q') \<in> TRel))
[PROOF STEP]
have "trans (indRelTEQ TRel)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trans (indRelTEQ TRel)
[PROOF STEP]
using indRelTEQ.trans[where TRel="TRel"]
[PROOF STATE]
proof (prove)
using this:
?P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> ?Q \<and> ?Q \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> ?R \<Longrightarrow> ?P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> ?R

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

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

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)) \<and> (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel))) \<and> strong_reduction_simulation TRel Target \<and> (\<forall>P Q Q'. (P, Q) \<in> TRel \<and> Q \<longmapsto>Target Q' \<longrightarrow> (\<exists>P'. P \<longmapsto>Target P' \<and> (P', Q') \<in> TRel)) \<Longrightarrow> \<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel \<and> (TargetTerm (\<lbrakk>S\<rbrakk>), SourceTerm S) \<in> Rel) \<and> TRel = _Collect (T1, T2) ((TargetTerm T1, TargetTerm T2) \<in> Rel) \<and> trans Rel \<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> (TargetTerm (\<lbrakk>S\<rbrakk>), SourceTerm S) \<in> Rel) \<and> TRel = _Collect (T1, T2) ((TargetTerm T1, TargetTerm T2) \<in> Rel) \<and> trans Rel \<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> ((\<forall>S S'. S \<longmapsto>Source S' \<longrightarrow> (\<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel)) \<and> (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel))) \<and> strong_reduction_simulation TRel Target \<and> (\<forall>P Q Q'. (P, Q) \<in> TRel \<and> Q \<longmapsto>Target Q' \<longrightarrow> (\<exists>P'. P \<longmapsto>Target P' \<and> (P', Q') \<in> TRel))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
trans (indRelTEQ TRel)

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)) \<and> (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel))) \<and> strong_reduction_simulation TRel Target \<and> (\<forall>P Q Q'. (P, Q) \<in> TRel \<and> Q \<longmapsto>Target Q' \<longrightarrow> (\<exists>P'. P \<longmapsto>Target P' \<and> (P', Q') \<in> TRel)) \<Longrightarrow> \<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel \<and> (TargetTerm (\<lbrakk>S\<rbrakk>), SourceTerm S) \<in> Rel) \<and> TRel = _Collect (T1, T2) ((TargetTerm T1, TargetTerm T2) \<in> Rel) \<and> trans Rel \<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> (TargetTerm (\<lbrakk>S\<rbrakk>), SourceTerm S) \<in> Rel) \<and> TRel = _Collect (T1, T2) ((TargetTerm T1, TargetTerm T2) \<in> Rel) \<and> trans Rel \<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> ((\<forall>S S'. S \<longmapsto>Source S' \<longrightarrow> (\<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel)) \<and> (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel))) \<and> strong_reduction_simulation TRel Target \<and> (\<forall>P Q Q'. (P, Q) \<in> TRel \<and> Q \<longmapsto>Target Q' \<longrightarrow> (\<exists>P'. P \<longmapsto>Target P' \<and> (P', Q') \<in> TRel))
[PROOF STEP]
from eqT oc bisimT
[PROOF STATE]
proof (chain)
picking this:
equivalence TRel
(\<forall>S S'. S \<longmapsto>Source S' \<longrightarrow> (\<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel)) \<and> (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel))
strong_reduction_simulation TRel Target \<and> (\<forall>P Q Q'. (P, Q) \<in> TRel \<and> Q \<longmapsto>Target Q' \<longrightarrow> (\<exists>P'. P \<longmapsto>Target P' \<and> (P', Q') \<in> TRel))
[PROOF STEP]
have "strong_reduction_bisimulation (indRelTEQ TRel) (STCal Source Target)"
[PROOF STATE]
proof (prove)
using this:
equivalence TRel
(\<forall>S S'. S \<longmapsto>Source S' \<longrightarrow> (\<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel)) \<and> (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel))
strong_reduction_simulation TRel Target \<and> (\<forall>P Q Q'. (P, Q) \<in> TRel \<and> Q \<longmapsto>Target Q' \<longrightarrow> (\<exists>P'. P \<longmapsto>Target P' \<and> (P', Q') \<in> TRel))

goal (1 subgoal):
 1. (\<forall>P Q P'. P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q \<and> P \<longmapsto>STCal Source Target P' \<longrightarrow> (\<exists>Q'. Q \<longmapsto>STCal Source Target Q' \<and> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q')) \<and> (\<forall>P Q Q'. P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q \<and> Q \<longmapsto>STCal Source Target Q' \<longrightarrow> (\<exists>P'. P \<longmapsto>STCal Source Target P' \<and> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'))
[PROOF STEP]
using SOC_wrt_equivalence_iff_indRelTEQ_strong_reduction_bisimulation[where TRel="TRel"]
[PROOF STATE]
proof (prove)
using this:
equivalence TRel
(\<forall>S S'. S \<longmapsto>Source S' \<longrightarrow> (\<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel)) \<and> (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel))
strong_reduction_simulation TRel Target \<and> (\<forall>P Q Q'. (P, Q) \<in> TRel \<and> Q \<longmapsto>Target Q' \<longrightarrow> (\<exists>P'. P \<longmapsto>Target P' \<and> (P', Q') \<in> TRel))
equivalence TRel \<Longrightarrow> (((\<forall>S S'. S \<longmapsto>Source S' \<longrightarrow> (\<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel)) \<and> (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel))) \<and> strong_reduction_simulation TRel Target \<and> (\<forall>P Q Q'. (P, Q) \<in> TRel \<and> Q \<longmapsto>Target Q' \<longrightarrow> (\<exists>P'. P \<longmapsto>Target P' \<and> (P', Q') \<in> TRel))) = ((\<forall>P Q P'. P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q \<and> P \<longmapsto>STCal Source Target P' \<longrightarrow> (\<exists>Q'. Q \<longmapsto>STCal Source Target Q' \<and> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q')) \<and> (\<forall>P Q Q'. P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q \<and> Q \<longmapsto>STCal Source Target Q' \<longrightarrow> (\<exists>P'. P \<longmapsto>STCal Source Target P' \<and> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q')))

goal (1 subgoal):
 1. (\<forall>P Q P'. P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q \<and> P \<longmapsto>STCal Source Target P' \<longrightarrow> (\<exists>Q'. Q \<longmapsto>STCal Source Target Q' \<and> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q')) \<and> (\<forall>P Q Q'. P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q \<and> Q \<longmapsto>STCal Source Target Q' \<longrightarrow> (\<exists>P'. P \<longmapsto>STCal Source Target P' \<and> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(\<forall>P Q P'. P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q \<and> P \<longmapsto>STCal Source Target P' \<longrightarrow> (\<exists>Q'. Q \<longmapsto>STCal Source Target Q' \<and> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q')) \<and> (\<forall>P Q Q'. P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q \<and> Q \<longmapsto>STCal Source Target Q' \<longrightarrow> (\<exists>P'. P \<longmapsto>STCal Source Target P' \<and> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<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)) \<and> (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel))) \<and> strong_reduction_simulation TRel Target \<and> (\<forall>P Q Q'. (P, Q) \<in> TRel \<and> Q \<longmapsto>Target Q' \<longrightarrow> (\<exists>P'. P \<longmapsto>Target P' \<and> (P', Q') \<in> TRel)) \<Longrightarrow> \<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel \<and> (TargetTerm (\<lbrakk>S\<rbrakk>), SourceTerm S) \<in> Rel) \<and> TRel = _Collect (T1, T2) ((TargetTerm T1, TargetTerm T2) \<in> Rel) \<and> trans Rel \<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> (TargetTerm (\<lbrakk>S\<rbrakk>), SourceTerm S) \<in> Rel) \<and> TRel = _Collect (T1, T2) ((TargetTerm T1, TargetTerm T2) \<in> Rel) \<and> trans Rel \<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> ((\<forall>S S'. S \<longmapsto>Source S' \<longrightarrow> (\<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel)) \<and> (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel))) \<and> strong_reduction_simulation TRel Target \<and> (\<forall>P Q Q'. (P, Q) \<in> TRel \<and> Q \<longmapsto>Target Q' \<longrightarrow> (\<exists>P'. P \<longmapsto>Target P' \<and> (P', Q') \<in> TRel))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<forall>S. SourceTerm S \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> TargetTerm (\<lbrakk>S\<rbrakk>) \<and> TargetTerm (\<lbrakk>S\<rbrakk>) \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> SourceTerm S
TRel = _Collect (T1, T2) (TargetTerm T1 \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> TargetTerm T2)
trans (indRelTEQ TRel)
(\<forall>P Q P'. P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q \<and> P \<longmapsto>STCal Source Target P' \<longrightarrow> (\<exists>Q'. Q \<longmapsto>STCal Source Target Q' \<and> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q')) \<and> (\<forall>P Q Q'. P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q \<and> Q \<longmapsto>STCal Source Target Q' \<longrightarrow> (\<exists>P'. P \<longmapsto>STCal Source Target P' \<and> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'))
[PROOF STEP]
show "\<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel \<and> (TargetTerm (\<lbrakk>S\<rbrakk>), SourceTerm S) \<in> Rel)
        \<and> TRel = {(T1, T2). (TargetTerm T1, TargetTerm T2) \<in> Rel} \<and> trans Rel
        \<and> strong_reduction_bisimulation Rel (STCal Source Target)"
[PROOF STATE]
proof (prove)
using this:
\<forall>S. SourceTerm S \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> TargetTerm (\<lbrakk>S\<rbrakk>) \<and> TargetTerm (\<lbrakk>S\<rbrakk>) \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> SourceTerm S
TRel = _Collect (T1, T2) (TargetTerm T1 \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> TargetTerm T2)
trans (indRelTEQ TRel)
(\<forall>P Q P'. P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q \<and> P \<longmapsto>STCal Source Target P' \<longrightarrow> (\<exists>Q'. Q \<longmapsto>STCal Source Target Q' \<and> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q')) \<and> (\<forall>P Q Q'. P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q \<and> Q \<longmapsto>STCal Source Target Q' \<longrightarrow> (\<exists>P'. P \<longmapsto>STCal Source Target P' \<and> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'))

goal (1 subgoal):
 1. \<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel \<and> (TargetTerm (\<lbrakk>S\<rbrakk>), SourceTerm S) \<in> Rel) \<and> TRel = _Collect (T1, T2) ((TargetTerm T1, TargetTerm T2) \<in> Rel) \<and> trans Rel \<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> (TargetTerm (\<lbrakk>S\<rbrakk>), SourceTerm S) \<in> Rel) \<and> TRel = _Collect (T1, T2) ((TargetTerm T1, TargetTerm T2) \<in> Rel) \<and> trans Rel \<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> (TargetTerm (\<lbrakk>S\<rbrakk>), SourceTerm S) \<in> Rel) \<and> TRel = _Collect (T1, T2) ((TargetTerm T1, TargetTerm T2) \<in> Rel) \<and> trans Rel \<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> ((\<forall>S S'. S \<longmapsto>Source S' \<longrightarrow> (\<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel)) \<and> (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel))) \<and> strong_reduction_simulation TRel Target \<and> (\<forall>P Q Q'. (P, Q) \<in> TRel \<and> Q \<longmapsto>Target Q' \<longrightarrow> (\<exists>P'. P \<longmapsto>Target P' \<and> (P', Q') \<in> TRel))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel \<and> (TargetTerm (\<lbrakk>S\<rbrakk>), SourceTerm S) \<in> Rel) \<and> TRel = _Collect (T1, T2) ((TargetTerm T1, TargetTerm T2) \<in> Rel) \<and> trans Rel \<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> ((\<forall>S S'. S \<longmapsto>Source S' \<longrightarrow> (\<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel)) \<and> (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel))) \<and> strong_reduction_simulation TRel Target \<and> (\<forall>P Q Q'. (P, Q) \<in> TRel \<and> Q \<longmapsto>Target Q' \<longrightarrow> (\<exists>P'. P \<longmapsto>Target P' \<and> (P', Q') \<in> TRel))
[PROOF STEP]
assume "\<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel
                 \<and> (TargetTerm (\<lbrakk>S\<rbrakk>), SourceTerm S) \<in> Rel)
          \<and> TRel = {(T1, T2). (TargetTerm T1, TargetTerm T2) \<in> Rel} \<and> trans Rel
          \<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> (TargetTerm (\<lbrakk>S\<rbrakk>), SourceTerm S) \<in> Rel) \<and> TRel = _Collect (T1, T2) ((TargetTerm T1, TargetTerm T2) \<in> Rel) \<and> trans Rel \<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> (TargetTerm (\<lbrakk>S\<rbrakk>), SourceTerm S) \<in> Rel) \<and> TRel = _Collect (T1, T2) ((TargetTerm T1, TargetTerm T2) \<in> Rel) \<and> trans Rel \<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> ((\<forall>S S'. S \<longmapsto>Source S' \<longrightarrow> (\<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel)) \<and> (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel))) \<and> strong_reduction_simulation TRel Target \<and> (\<forall>P Q Q'. (P, Q) \<in> TRel \<and> Q \<longmapsto>Target Q' \<longrightarrow> (\<exists>P'. P \<longmapsto>Target P' \<and> (P', Q') \<in> TRel))
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
\<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel \<and> (TargetTerm (\<lbrakk>S\<rbrakk>), SourceTerm S) \<in> Rel) \<and> TRel = _Collect (T1, T2) ((TargetTerm T1, TargetTerm T2) \<in> Rel) \<and> trans Rel \<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> (TargetTerm (\<lbrakk>S\<rbrakk>), SourceTerm S) \<in> Rel"
   and A2: "TRel = {(T1, T2). (TargetTerm T1, TargetTerm T2) \<in> Rel}" and A3: "trans Rel"
   and A4: "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> (TargetTerm (\<lbrakk>S\<rbrakk>), SourceTerm S) \<in> Rel) \<and> TRel = _Collect (T1, T2) ((TargetTerm T1, TargetTerm T2) \<in> Rel) \<and> trans Rel \<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> (TargetTerm (\<lbrakk>S\<rbrakk>), SourceTerm S) \<in> Rel) \<and> TRel = _Collect (T1, T2) ((TargetTerm T1, TargetTerm T2) \<in> Rel) \<and> trans Rel \<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 \<and> (TargetTerm (\<lbrakk>S\<rbrakk>), SourceTerm S) \<in> Rel
TRel = _Collect (T1, T2) ((TargetTerm T1, TargetTerm T2) \<in> Rel)
trans 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))

goal (1 subgoal):
 1. \<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel \<and> (TargetTerm (\<lbrakk>S\<rbrakk>), SourceTerm S) \<in> Rel) \<and> TRel = _Collect (T1, T2) ((TargetTerm T1, TargetTerm T2) \<in> Rel) \<and> trans Rel \<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> ((\<forall>S S'. S \<longmapsto>Source S' \<longrightarrow> (\<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel)) \<and> (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel))) \<and> strong_reduction_simulation TRel Target \<and> (\<forall>P Q Q'. (P, Q) \<in> TRel \<and> Q \<longmapsto>Target Q' \<longrightarrow> (\<exists>P'. P \<longmapsto>Target P' \<and> (P', Q') \<in> TRel))
[PROOF STEP]
have "strongly_operational_corresponding TRel"
[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)) \<and> (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel))
[PROOF STEP]
proof auto
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>S S'. S \<longmapsto>Source S' \<Longrightarrow> \<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel
 2. \<And>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<Longrightarrow> \<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel
[PROOF STEP]
fix S S'
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>S S'. S \<longmapsto>Source S' \<Longrightarrow> \<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel
 2. \<And>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<Longrightarrow> \<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel
[PROOF STEP]
from A1
[PROOF STATE]
proof (chain)
picking this:
\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel \<and> (TargetTerm (\<lbrakk>S\<rbrakk>), SourceTerm S) \<in> Rel
[PROOF STEP]
have "(SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel"
[PROOF STATE]
proof (prove)
using this:
\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel \<and> (TargetTerm (\<lbrakk>S\<rbrakk>), SourceTerm S) \<in> Rel

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

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

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

goal (2 subgoals):
 1. \<And>S S'. S \<longmapsto>Source S' \<Longrightarrow> \<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel
 2. \<And>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<Longrightarrow> \<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel
[PROOF STEP]
hence "SourceTerm S \<longmapsto>(STCal Source Target) (SourceTerm S')"
[PROOF STATE]
proof (prove)
using this:
S \<longmapsto>Source S'

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

goal (2 subgoals):
 1. \<And>S S'. S \<longmapsto>Source S' \<Longrightarrow> \<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel
 2. \<And>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<Longrightarrow> \<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel
SourceTerm S \<longmapsto>STCal Source Target SourceTerm S'
[PROOF STEP]
obtain Q' where B1: "TargetTerm (\<lbrakk>S\<rbrakk>) \<longmapsto>(STCal Source Target) Q'"
                           and B2: "(SourceTerm S', Q') \<in> Rel"
[PROOF STATE]
proof (prove)
using this:
(SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel
SourceTerm S \<longmapsto>STCal Source Target SourceTerm S'

goal (1 subgoal):
 1. (\<And>Q'. TargetTerm (\<lbrakk>S\<rbrakk>) \<longmapsto>STCal Source Target Q' \<and> (SourceTerm S', Q') \<in> Rel \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using A4
[PROOF STATE]
proof (prove)
using this:
(SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel
SourceTerm S \<longmapsto>STCal Source Target SourceTerm S'
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>Q'. TargetTerm (\<lbrakk>S\<rbrakk>) \<longmapsto>STCal Source Target Q' \<and> (SourceTerm S', Q') \<in> Rel \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
TargetTerm (\<lbrakk>S\<rbrakk>) \<longmapsto>STCal Source Target Q'
(SourceTerm S', Q') \<in> Rel

goal (2 subgoals):
 1. \<And>S S'. S \<longmapsto>Source S' \<Longrightarrow> \<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel
 2. \<And>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<Longrightarrow> \<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel
[PROOF STEP]
from B1
[PROOF STATE]
proof (chain)
picking this:
TargetTerm (\<lbrakk>S\<rbrakk>) \<longmapsto>STCal Source Target Q'
[PROOF STEP]
obtain T where B3: "\<lbrakk>S\<rbrakk> \<longmapsto>Target T" and B4: "T \<in>T Q'"
[PROOF STATE]
proof (prove)
using this:
TargetTerm (\<lbrakk>S\<rbrakk>) \<longmapsto>STCal Source Target Q'

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

goal (2 subgoals):
 1. \<And>S S'. S \<longmapsto>Source S' \<Longrightarrow> \<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel
 2. \<And>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<Longrightarrow> \<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel
[PROOF STEP]
from A1
[PROOF STATE]
proof (chain)
picking this:
\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel \<and> (TargetTerm (\<lbrakk>S\<rbrakk>), SourceTerm S) \<in> Rel
[PROOF STEP]
have "(TargetTerm (\<lbrakk>S'\<rbrakk>), SourceTerm S') \<in> Rel"
[PROOF STATE]
proof (prove)
using this:
\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel \<and> (TargetTerm (\<lbrakk>S\<rbrakk>), SourceTerm S) \<in> Rel

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

goal (2 subgoals):
 1. \<And>S S'. S \<longmapsto>Source S' \<Longrightarrow> \<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel
 2. \<And>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<Longrightarrow> \<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel
[PROOF STEP]
with B2 A3
[PROOF STATE]
proof (chain)
picking this:
(SourceTerm S', Q') \<in> Rel
trans Rel
(TargetTerm (\<lbrakk>S'\<rbrakk>), SourceTerm S') \<in> Rel
[PROOF STEP]
have "(TargetTerm (\<lbrakk>S'\<rbrakk>), Q') \<in> Rel"
[PROOF STATE]
proof (prove)
using this:
(SourceTerm S', Q') \<in> Rel
trans Rel
(TargetTerm (\<lbrakk>S'\<rbrakk>), SourceTerm S') \<in> Rel

goal (1 subgoal):
 1. (TargetTerm (\<lbrakk>S'\<rbrakk>), Q') \<in> Rel
[PROOF STEP]
unfolding trans_def
[PROOF STATE]
proof (prove)
using this:
(SourceTerm S', Q') \<in> Rel
\<forall>x y z. (x, y) \<in> Rel \<longrightarrow> (y, z) \<in> Rel \<longrightarrow> (x, z) \<in> Rel
(TargetTerm (\<lbrakk>S'\<rbrakk>), SourceTerm S') \<in> Rel

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

goal (2 subgoals):
 1. \<And>S S'. S \<longmapsto>Source S' \<Longrightarrow> \<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel
 2. \<And>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<Longrightarrow> \<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel
[PROOF STEP]
with B4 A2
[PROOF STATE]
proof (chain)
picking this:
T \<in>T Q'
TRel = _Collect (T1, T2) ((TargetTerm T1, TargetTerm T2) \<in> Rel)
(TargetTerm (\<lbrakk>S'\<rbrakk>), Q') \<in> Rel
[PROOF STEP]
have "(\<lbrakk>S'\<rbrakk>, T) \<in> TRel"
[PROOF STATE]
proof (prove)
using this:
T \<in>T Q'
TRel = _Collect (T1, T2) ((TargetTerm T1, TargetTerm T2) \<in> Rel)
(TargetTerm (\<lbrakk>S'\<rbrakk>), Q') \<in> Rel

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

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

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

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

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

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

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

goal (1 subgoal):
 1. \<And>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<Longrightarrow> \<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel
[PROOF STEP]
hence "TargetTerm (\<lbrakk>S\<rbrakk>) \<longmapsto>(STCal Source Target) (TargetTerm T)"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>S\<rbrakk> \<longmapsto>Target T

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

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

goal (1 subgoal):
 1. (\<And>P'. SourceTerm S \<longmapsto>STCal Source Target P' \<and> (P', TargetTerm T) \<in> Rel \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using A4
[PROOF STATE]
proof (prove)
using this:
(SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel
TargetTerm (\<lbrakk>S\<rbrakk>) \<longmapsto>STCal Source Target TargetTerm T
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>P'. SourceTerm S \<longmapsto>STCal Source Target P' \<and> (P', TargetTerm T) \<in> Rel \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
SourceTerm S \<longmapsto>STCal Source Target P'
(P', TargetTerm T) \<in> Rel

goal (1 subgoal):
 1. \<And>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<Longrightarrow> \<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel
[PROOF STEP]
from C1
[PROOF STATE]
proof (chain)
picking this:
SourceTerm S \<longmapsto>STCal Source Target P'
[PROOF STEP]
obtain S' where C3: "S \<longmapsto>Source S'" and C4: "S' \<in>S P'"
[PROOF STATE]
proof (prove)
using this:
SourceTerm S \<longmapsto>STCal Source Target P'

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

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

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

goal (1 subgoal):
 1. \<And>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<Longrightarrow> \<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel
[PROOF STEP]
from A3 this C2
[PROOF STATE]
proof (chain)
picking this:
trans Rel
(TargetTerm (\<lbrakk>S'\<rbrakk>), P') \<in> Rel
(P', TargetTerm T) \<in> Rel
[PROOF STEP]
have "(TargetTerm (\<lbrakk>S'\<rbrakk>), TargetTerm T) \<in> Rel"
[PROOF STATE]
proof (prove)
using this:
trans Rel
(TargetTerm (\<lbrakk>S'\<rbrakk>), P') \<in> Rel
(P', TargetTerm T) \<in> Rel

goal (1 subgoal):
 1. (TargetTerm (\<lbrakk>S'\<rbrakk>), TargetTerm T) \<in> Rel
[PROOF STEP]
unfolding trans_def
[PROOF STATE]
proof (prove)
using this:
\<forall>x y z. (x, y) \<in> Rel \<longrightarrow> (y, z) \<in> Rel \<longrightarrow> (x, z) \<in> Rel
(TargetTerm (\<lbrakk>S'\<rbrakk>), P') \<in> Rel
(P', TargetTerm T) \<in> Rel

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

goal (1 subgoal):
 1. \<And>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<Longrightarrow> \<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel
[PROOF STEP]
with A2
[PROOF STATE]
proof (chain)
picking this:
TRel = _Collect (T1, T2) ((TargetTerm T1, TargetTerm T2) \<in> Rel)
(TargetTerm (\<lbrakk>S'\<rbrakk>), TargetTerm T) \<in> Rel
[PROOF STEP]
have "(\<lbrakk>S'\<rbrakk>, T) \<in> TRel"
[PROOF STATE]
proof (prove)
using this:
TRel = _Collect (T1, T2) ((TargetTerm T1, TargetTerm T2) \<in> Rel)
(TargetTerm (\<lbrakk>S'\<rbrakk>), TargetTerm T) \<in> Rel

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed
[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)) \<and> (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel))

goal (1 subgoal):
 1. \<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel \<and> (TargetTerm (\<lbrakk>S\<rbrakk>), SourceTerm S) \<in> Rel) \<and> TRel = _Collect (T1, T2) ((TargetTerm T1, TargetTerm T2) \<in> Rel) \<and> trans Rel \<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> ((\<forall>S S'. S \<longmapsto>Source S' \<longrightarrow> (\<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel)) \<and> (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel))) \<and> strong_reduction_simulation TRel Target \<and> (\<forall>P Q Q'. (P, Q) \<in> TRel \<and> Q \<longmapsto>Target Q' \<longrightarrow> (\<exists>P'. P \<longmapsto>Target P' \<and> (P', Q') \<in> TRel))
[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)) \<and> (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel))

goal (1 subgoal):
 1. \<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel \<and> (TargetTerm (\<lbrakk>S\<rbrakk>), SourceTerm S) \<in> Rel) \<and> TRel = _Collect (T1, T2) ((TargetTerm T1, TargetTerm T2) \<in> Rel) \<and> trans Rel \<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> ((\<forall>S S'. S \<longmapsto>Source S' \<longrightarrow> (\<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel)) \<and> (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel))) \<and> strong_reduction_simulation TRel Target \<and> (\<forall>P Q Q'. (P, Q) \<in> TRel \<and> Q \<longmapsto>Target Q' \<longrightarrow> (\<exists>P'. P \<longmapsto>Target P' \<and> (P', Q') \<in> TRel))
[PROOF STEP]
have "strong_reduction_bisimulation TRel Target"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. strong_reduction_simulation TRel Target \<and> (\<forall>P Q Q'. (P, Q) \<in> TRel \<and> Q \<longmapsto>Target Q' \<longrightarrow> (\<exists>P'. P \<longmapsto>Target P' \<and> (P', Q') \<in> TRel))
[PROOF STEP]
proof auto
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>P Q P'. (P, Q) \<in> TRel \<and> P \<longmapsto>Target P' \<Longrightarrow> \<exists>Q'. Q \<longmapsto>Target Q' \<and> (P', Q') \<in> TRel
 2. \<And>P Q Q'. (P, Q) \<in> TRel \<and> Q \<longmapsto>Target Q' \<Longrightarrow> \<exists>P'. P \<longmapsto>Target P' \<and> (P', Q') \<in> TRel
[PROOF STEP]
fix TP TQ TP'
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>P Q P'. (P, Q) \<in> TRel \<and> P \<longmapsto>Target P' \<Longrightarrow> \<exists>Q'. Q \<longmapsto>Target Q' \<and> (P', Q') \<in> TRel
 2. \<And>P Q Q'. (P, Q) \<in> TRel \<and> Q \<longmapsto>Target Q' \<Longrightarrow> \<exists>P'. P \<longmapsto>Target P' \<and> (P', Q') \<in> TRel
[PROOF STEP]
assume "(TP, TQ) \<in> TRel"
[PROOF STATE]
proof (state)
this:
(TP, TQ) \<in> TRel

goal (2 subgoals):
 1. \<And>P Q P'. (P, Q) \<in> TRel \<and> P \<longmapsto>Target P' \<Longrightarrow> \<exists>Q'. Q \<longmapsto>Target Q' \<and> (P', Q') \<in> TRel
 2. \<And>P Q Q'. (P, Q) \<in> TRel \<and> Q \<longmapsto>Target Q' \<Longrightarrow> \<exists>P'. P \<longmapsto>Target P' \<and> (P', Q') \<in> TRel
[PROOF STEP]
with A2
[PROOF STATE]
proof (chain)
picking this:
TRel = _Collect (T1, T2) ((TargetTerm T1, TargetTerm T2) \<in> Rel)
(TP, TQ) \<in> TRel
[PROOF STEP]
have "(TargetTerm TP, TargetTerm TQ) \<in> Rel"
[PROOF STATE]
proof (prove)
using this:
TRel = _Collect (T1, T2) ((TargetTerm T1, TargetTerm T2) \<in> Rel)
(TP, TQ) \<in> TRel

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

goal (2 subgoals):
 1. \<And>P Q P'. (P, Q) \<in> TRel \<and> P \<longmapsto>Target P' \<Longrightarrow> \<exists>Q'. Q \<longmapsto>Target Q' \<and> (P', Q') \<in> TRel
 2. \<And>P Q Q'. (P, Q) \<in> TRel \<and> Q \<longmapsto>Target Q' \<Longrightarrow> \<exists>P'. P \<longmapsto>Target P' \<and> (P', Q') \<in> TRel
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(TargetTerm TP, TargetTerm TQ) \<in> Rel

goal (2 subgoals):
 1. \<And>P Q P'. (P, Q) \<in> TRel \<and> P \<longmapsto>Target P' \<Longrightarrow> \<exists>Q'. Q \<longmapsto>Target Q' \<and> (P', Q') \<in> TRel
 2. \<And>P Q Q'. (P, Q) \<in> TRel \<and> Q \<longmapsto>Target Q' \<Longrightarrow> \<exists>P'. P \<longmapsto>Target P' \<and> (P', Q') \<in> TRel
[PROOF STEP]
assume "TP \<longmapsto>Target TP'"
[PROOF STATE]
proof (state)
this:
TP \<longmapsto>Target TP'

goal (2 subgoals):
 1. \<And>P Q P'. (P, Q) \<in> TRel \<and> P \<longmapsto>Target P' \<Longrightarrow> \<exists>Q'. Q \<longmapsto>Target Q' \<and> (P', Q') \<in> TRel
 2. \<And>P Q Q'. (P, Q) \<in> TRel \<and> Q \<longmapsto>Target Q' \<Longrightarrow> \<exists>P'. P \<longmapsto>Target P' \<and> (P', Q') \<in> TRel
[PROOF STEP]
hence "TargetTerm TP \<longmapsto>(STCal Source Target) (TargetTerm TP')"
[PROOF STATE]
proof (prove)
using this:
TP \<longmapsto>Target TP'

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

goal (2 subgoals):
 1. \<And>P Q P'. (P, Q) \<in> TRel \<and> P \<longmapsto>Target P' \<Longrightarrow> \<exists>Q'. Q \<longmapsto>Target Q' \<and> (P', Q') \<in> TRel
 2. \<And>P Q Q'. (P, Q) \<in> TRel \<and> Q \<longmapsto>Target Q' \<Longrightarrow> \<exists>P'. P \<longmapsto>Target P' \<and> (P', Q') \<in> TRel
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(TargetTerm TP, TargetTerm TQ) \<in> Rel
TargetTerm TP \<longmapsto>STCal Source Target TargetTerm TP'
[PROOF STEP]
obtain Q' where D1: "TargetTerm TQ \<longmapsto>(STCal Source Target) Q'"
                           and D2: "(TargetTerm TP', Q') \<in> Rel"
[PROOF STATE]
proof (prove)
using this:
(TargetTerm TP, TargetTerm TQ) \<in> Rel
TargetTerm TP \<longmapsto>STCal Source Target TargetTerm TP'

goal (1 subgoal):
 1. (\<And>Q'. TargetTerm TQ \<longmapsto>STCal Source Target Q' \<and> (TargetTerm TP', Q') \<in> Rel \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using A4
[PROOF STATE]
proof (prove)
using this:
(TargetTerm TP, TargetTerm TQ) \<in> Rel
TargetTerm TP \<longmapsto>STCal Source Target TargetTerm TP'
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>Q'. TargetTerm TQ \<longmapsto>STCal Source Target Q' \<and> (TargetTerm TP', Q') \<in> Rel \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
TargetTerm TQ \<longmapsto>STCal Source Target Q'
(TargetTerm TP', Q') \<in> Rel

goal (2 subgoals):
 1. \<And>P Q P'. (P, Q) \<in> TRel \<and> P \<longmapsto>Target P' \<Longrightarrow> \<exists>Q'. Q \<longmapsto>Target Q' \<and> (P', Q') \<in> TRel
 2. \<And>P Q Q'. (P, Q) \<in> TRel \<and> Q \<longmapsto>Target Q' \<Longrightarrow> \<exists>P'. P \<longmapsto>Target P' \<and> (P', Q') \<in> TRel
[PROOF STEP]
from D1
[PROOF STATE]
proof (chain)
picking this:
TargetTerm TQ \<longmapsto>STCal Source Target Q'
[PROOF STEP]
obtain TQ' where D3: "TQ \<longmapsto>Target TQ'" and D4: "TQ' \<in>T Q'"
[PROOF STATE]
proof (prove)
using this:
TargetTerm TQ \<longmapsto>STCal Source Target Q'

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

goal (2 subgoals):
 1. \<And>P Q P'. (P, Q) \<in> TRel \<and> P \<longmapsto>Target P' \<Longrightarrow> \<exists>Q'. Q \<longmapsto>Target Q' \<and> (P', Q') \<in> TRel
 2. \<And>P Q Q'. (P, Q) \<in> TRel \<and> Q \<longmapsto>Target Q' \<Longrightarrow> \<exists>P'. P \<longmapsto>Target P' \<and> (P', Q') \<in> TRel
[PROOF STEP]
from A2 D2 D4
[PROOF STATE]
proof (chain)
picking this:
TRel = _Collect (T1, T2) ((TargetTerm T1, TargetTerm T2) \<in> Rel)
(TargetTerm TP', Q') \<in> Rel
TQ' \<in>T Q'
[PROOF STEP]
have "(TP', TQ') \<in> TRel"
[PROOF STATE]
proof (prove)
using this:
TRel = _Collect (T1, T2) ((TargetTerm T1, TargetTerm T2) \<in> Rel)
(TargetTerm TP', Q') \<in> Rel
TQ' \<in>T Q'

goal (1 subgoal):
 1. (TP', TQ') \<in> TRel
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(TP', TQ') \<in> TRel

goal (2 subgoals):
 1. \<And>P Q P'. (P, Q) \<in> TRel \<and> P \<longmapsto>Target P' \<Longrightarrow> \<exists>Q'. Q \<longmapsto>Target Q' \<and> (P', Q') \<in> TRel
 2. \<And>P Q Q'. (P, Q) \<in> TRel \<and> Q \<longmapsto>Target Q' \<Longrightarrow> \<exists>P'. P \<longmapsto>Target P' \<and> (P', Q') \<in> TRel
[PROOF STEP]
with D3
[PROOF STATE]
proof (chain)
picking this:
TQ \<longmapsto>Target TQ'
(TP', TQ') \<in> TRel
[PROOF STEP]
show "\<exists>TQ'. TQ \<longmapsto>Target TQ' \<and> (TP', TQ') \<in> TRel"
[PROOF STATE]
proof (prove)
using this:
TQ \<longmapsto>Target TQ'
(TP', TQ') \<in> TRel

goal (1 subgoal):
 1. \<exists>TQ'. TQ \<longmapsto>Target TQ' \<and> (TP', TQ') \<in> TRel
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>TQ'. TQ \<longmapsto>Target TQ' \<and> (TP', TQ') \<in> TRel

goal (1 subgoal):
 1. \<And>P Q Q'. (P, Q) \<in> TRel \<and> Q \<longmapsto>Target Q' \<Longrightarrow> \<exists>P'. P \<longmapsto>Target P' \<and> (P', Q') \<in> TRel
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>P Q Q'. (P, Q) \<in> TRel \<and> Q \<longmapsto>Target Q' \<Longrightarrow> \<exists>P'. P \<longmapsto>Target P' \<and> (P', Q') \<in> TRel
[PROOF STEP]
fix TP TQ TQ'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>P Q Q'. (P, Q) \<in> TRel \<and> Q \<longmapsto>Target Q' \<Longrightarrow> \<exists>P'. P \<longmapsto>Target P' \<and> (P', Q') \<in> TRel
[PROOF STEP]
assume "(TP, TQ) \<in> TRel"
[PROOF STATE]
proof (state)
this:
(TP, TQ) \<in> TRel

goal (1 subgoal):
 1. \<And>P Q Q'. (P, Q) \<in> TRel \<and> Q \<longmapsto>Target Q' \<Longrightarrow> \<exists>P'. P \<longmapsto>Target P' \<and> (P', Q') \<in> TRel
[PROOF STEP]
with A2
[PROOF STATE]
proof (chain)
picking this:
TRel = _Collect (T1, T2) ((TargetTerm T1, TargetTerm T2) \<in> Rel)
(TP, TQ) \<in> TRel
[PROOF STEP]
have "(TargetTerm TP, TargetTerm TQ) \<in> Rel"
[PROOF STATE]
proof (prove)
using this:
TRel = _Collect (T1, T2) ((TargetTerm T1, TargetTerm T2) \<in> Rel)
(TP, TQ) \<in> TRel

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

goal (1 subgoal):
 1. \<And>P Q Q'. (P, Q) \<in> TRel \<and> Q \<longmapsto>Target Q' \<Longrightarrow> \<exists>P'. P \<longmapsto>Target P' \<and> (P', Q') \<in> TRel
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(TargetTerm TP, TargetTerm TQ) \<in> Rel

goal (1 subgoal):
 1. \<And>P Q Q'. (P, Q) \<in> TRel \<and> Q \<longmapsto>Target Q' \<Longrightarrow> \<exists>P'. P \<longmapsto>Target P' \<and> (P', Q') \<in> TRel
[PROOF STEP]
assume "TQ \<longmapsto>Target TQ'"
[PROOF STATE]
proof (state)
this:
TQ \<longmapsto>Target TQ'

goal (1 subgoal):
 1. \<And>P Q Q'. (P, Q) \<in> TRel \<and> Q \<longmapsto>Target Q' \<Longrightarrow> \<exists>P'. P \<longmapsto>Target P' \<and> (P', Q') \<in> TRel
[PROOF STEP]
hence "TargetTerm TQ \<longmapsto>(STCal Source Target) (TargetTerm TQ')"
[PROOF STATE]
proof (prove)
using this:
TQ \<longmapsto>Target TQ'

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

goal (1 subgoal):
 1. \<And>P Q Q'. (P, Q) \<in> TRel \<and> Q \<longmapsto>Target Q' \<Longrightarrow> \<exists>P'. P \<longmapsto>Target P' \<and> (P', Q') \<in> TRel
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(TargetTerm TP, TargetTerm TQ) \<in> Rel
TargetTerm TQ \<longmapsto>STCal Source Target TargetTerm TQ'
[PROOF STEP]
obtain P' where E1: "TargetTerm TP \<longmapsto>(STCal Source Target) P'"
                           and E2: "(P', TargetTerm TQ') \<in> Rel"
[PROOF STATE]
proof (prove)
using this:
(TargetTerm TP, TargetTerm TQ) \<in> Rel
TargetTerm TQ \<longmapsto>STCal Source Target TargetTerm TQ'

goal (1 subgoal):
 1. (\<And>P'. TargetTerm TP \<longmapsto>STCal Source Target P' \<and> (P', TargetTerm TQ') \<in> Rel \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using A4
[PROOF STATE]
proof (prove)
using this:
(TargetTerm TP, TargetTerm TQ) \<in> Rel
TargetTerm TQ \<longmapsto>STCal Source Target TargetTerm TQ'
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>P'. TargetTerm TP \<longmapsto>STCal Source Target P' \<and> (P', TargetTerm TQ') \<in> Rel \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
TargetTerm TP \<longmapsto>STCal Source Target P'
(P', TargetTerm TQ') \<in> Rel

goal (1 subgoal):
 1. \<And>P Q Q'. (P, Q) \<in> TRel \<and> Q \<longmapsto>Target Q' \<Longrightarrow> \<exists>P'. P \<longmapsto>Target P' \<and> (P', Q') \<in> TRel
[PROOF STEP]
from E1
[PROOF STATE]
proof (chain)
picking this:
TargetTerm TP \<longmapsto>STCal Source Target P'
[PROOF STEP]
obtain TP' where E3: "TP \<longmapsto>Target TP'" and E4: "TP' \<in>T P'"
[PROOF STATE]
proof (prove)
using this:
TargetTerm TP \<longmapsto>STCal Source Target P'

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

goal (1 subgoal):
 1. \<And>P Q Q'. (P, Q) \<in> TRel \<and> Q \<longmapsto>Target Q' \<Longrightarrow> \<exists>P'. P \<longmapsto>Target P' \<and> (P', Q') \<in> TRel
[PROOF STEP]
from A2 E2 E4
[PROOF STATE]
proof (chain)
picking this:
TRel = _Collect (T1, T2) ((TargetTerm T1, TargetTerm T2) \<in> Rel)
(P', TargetTerm TQ') \<in> Rel
TP' \<in>T P'
[PROOF STEP]
have "(TP', TQ') \<in> TRel"
[PROOF STATE]
proof (prove)
using this:
TRel = _Collect (T1, T2) ((TargetTerm T1, TargetTerm T2) \<in> Rel)
(P', TargetTerm TQ') \<in> Rel
TP' \<in>T P'

goal (1 subgoal):
 1. (TP', TQ') \<in> TRel
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(TP', TQ') \<in> TRel

goal (1 subgoal):
 1. \<And>P Q Q'. (P, Q) \<in> TRel \<and> Q \<longmapsto>Target Q' \<Longrightarrow> \<exists>P'. P \<longmapsto>Target P' \<and> (P', Q') \<in> TRel
[PROOF STEP]
with E3
[PROOF STATE]
proof (chain)
picking this:
TP \<longmapsto>Target TP'
(TP', TQ') \<in> TRel
[PROOF STEP]
show "\<exists>TP'. TP \<longmapsto>Target TP' \<and> (TP', TQ') \<in> TRel"
[PROOF STATE]
proof (prove)
using this:
TP \<longmapsto>Target TP'
(TP', TQ') \<in> TRel

goal (1 subgoal):
 1. \<exists>TP'. TP \<longmapsto>Target TP' \<and> (TP', TQ') \<in> TRel
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>TP'. TP \<longmapsto>Target TP' \<and> (TP', TQ') \<in> TRel

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
strong_reduction_simulation TRel Target \<and> (\<forall>P Q Q'. (P, Q) \<in> TRel \<and> Q \<longmapsto>Target Q' \<longrightarrow> (\<exists>P'. P \<longmapsto>Target P' \<and> (P', Q') \<in> TRel))

goal (1 subgoal):
 1. \<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel \<and> (TargetTerm (\<lbrakk>S\<rbrakk>), SourceTerm S) \<in> Rel) \<and> TRel = _Collect (T1, T2) ((TargetTerm T1, TargetTerm T2) \<in> Rel) \<and> trans Rel \<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> ((\<forall>S S'. S \<longmapsto>Source S' \<longrightarrow> (\<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel)) \<and> (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel))) \<and> strong_reduction_simulation TRel Target \<and> (\<forall>P Q Q'. (P, Q) \<in> TRel \<and> Q \<longmapsto>Target Q' \<longrightarrow> (\<exists>P'. P \<longmapsto>Target P' \<and> (P', Q') \<in> TRel))
[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)) \<and> (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel))
strong_reduction_simulation TRel Target \<and> (\<forall>P Q Q'. (P, Q) \<in> TRel \<and> Q \<longmapsto>Target Q' \<longrightarrow> (\<exists>P'. P \<longmapsto>Target P' \<and> (P', Q') \<in> TRel))
[PROOF STEP]
show "strongly_operational_corresponding TRel \<and> strong_reduction_bisimulation TRel 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)) \<and> (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel))
strong_reduction_simulation TRel Target \<and> (\<forall>P Q Q'. (P, Q) \<in> TRel \<and> Q \<longmapsto>Target Q' \<longrightarrow> (\<exists>P'. P \<longmapsto>Target P' \<and> (P', Q') \<in> TRel))

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma [code]: "iam_\<alpha> a i \<equiv> array_get_oo None a i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. iam_\<alpha> a i \<equiv> array_get_oo None a i
[PROOF STEP]
unfolding array_get_oo_def iam_\<alpha>_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. if i < array_length a then array_get a i else None \<equiv> if i < array_length a then array_get a i else None
[PROOF STEP]
.


[STATEMENT]
lemma incr_correct: "\<not> idx < l \<Longrightarrow> idx < l + iam_increment l idx"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> idx < l \<Longrightarrow> idx < l + iam_increment l idx
[PROOF STEP]
unfolding iam_increment_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> idx < l \<Longrightarrow> idx < l + max (idx + 1 - l) (2 * l + 3)
[PROOF STEP]
by auto


[STATEMENT]
lemma [code]: "iam_update k v a \<equiv> array_set_oo
  (\<lambda>_. let l=array_length a in
         array_set (array_grow a (iam_increment l k) None) k (Some v))
  a k (Some v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. iam_update k v a \<equiv> array_set_oo (\<lambda>_. let l = array_length a in array_set (array_grow a (iam_increment l k) None) k (Some v)) a k (Some v)
[PROOF STEP]
unfolding iam_update_def array_set_oo_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. let l = array_length a; a = if k < l then a else array_grow a (iam_increment l k) None in array_set a k (Some v) \<equiv> if k < array_length a then array_set a k (Some v) else let l = array_length a in array_set (array_grow a (iam_increment l k) None) k (Some v)
[PROOF STEP]
apply (rule eq_reflection)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (let l = array_length a; a = if k < l then a else array_grow a (iam_increment l k) None in array_set a k (Some v)) = (if k < array_length a then array_set a k (Some v) else let l = array_length a in array_set (array_grow a (iam_increment l k) None) k (Some v))
[PROOF STEP]
by auto


[STATEMENT]
lemma [code]: "iam_delete k a \<equiv> array_set_oo (\<lambda>_. a) a k None"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. iam_delete k a \<equiv> array_set_oo (\<lambda>_. a) a k None
[PROOF STEP]
unfolding iam_delete_def array_set_oo_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. if k < array_length a then array_set a k None else a \<equiv> if k < array_length a then array_set a k None else a
[PROOF STEP]
by auto


[STATEMENT]
lemma iam_rel_def: "\<langle>R\<rangle> iam_rel = \<langle>\<langle>R\<rangle> option_rel\<rangle> array_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<langle>R\<rangle>iam_rel = \<langle>\<langle>R\<rangle>option_rel\<rangle>array_rel
[PROOF STEP]
by (simp add: iam_rel_def_internal relAPP_def)


[STATEMENT]
lemma iam_rel_sv[relator_props]:
  "single_valued Rv \<Longrightarrow> single_valued (\<langle>Rv\<rangle>iam_rel)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. single_valued Rv \<Longrightarrow> single_valued (\<langle>Rv\<rangle>iam_rel)
[PROOF STEP]
unfolding iam_rel_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. single_valued Rv \<Longrightarrow> single_valued (\<langle>\<langle>Rv\<rangle>option_rel\<rangle>array_rel)
[PROOF STEP]
by tagged_solver


[STATEMENT]
lemma param_iam_\<alpha>[param]:
  "(iam_\<alpha>, iam_\<alpha>) \<in> \<langle>R\<rangle> iam_rel \<rightarrow> nat_rel \<rightarrow> \<langle>R\<rangle> option_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (iam_\<alpha>, iam_\<alpha>) \<in> \<langle>R\<rangle>iam_rel \<rightarrow> nat_rel \<rightarrow> \<langle>R\<rangle>option_rel
[PROOF STEP]
unfolding iam_\<alpha>_def[abs_def] iam_rel_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>a i. if i < array_length a then array_get a i else None, \<lambda>a i. if i < array_length a then array_get a i else None) \<in> \<langle>\<langle>R\<rangle>option_rel\<rangle>array_rel \<rightarrow> nat_rel \<rightarrow> \<langle>R\<rangle>option_rel
[PROOF STEP]
by parametricity


[STATEMENT]
lemma param_iam_invar[param]:
  "(iam_invar, iam_invar) \<in> \<langle>R\<rangle> iam_rel \<rightarrow> bool_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (iam_invar, iam_invar) \<in> \<langle>R\<rangle>iam_rel \<rightarrow> bool_rel
[PROOF STEP]
unfolding iam_rel_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (iam_invar, iam_invar) \<in> \<langle>\<langle>R\<rangle>option_rel\<rangle>array_rel \<rightarrow> bool_rel
[PROOF STEP]
by parametricity


[STATEMENT]
lemma param_iam_empty[param]:
  "(iam_empty, iam_empty) \<in> unit_rel \<rightarrow> \<langle>R\<rangle>iam_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (iam_empty, iam_empty) \<in> unit_rel \<rightarrow> \<langle>R\<rangle>iam_rel
[PROOF STEP]
unfolding iam_empty_def[abs_def] iam_rel_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>_. array_of_list [], \<lambda>_. array_of_list []) \<in> unit_rel \<rightarrow> \<langle>\<langle>R\<rangle>option_rel\<rangle>array_rel
[PROOF STEP]
by parametricity


[STATEMENT]
lemma param_iam_lookup[param]:
  "(iam_lookup, iam_lookup) \<in> nat_rel \<rightarrow> \<langle>R\<rangle>iam_rel \<rightarrow> \<langle>R\<rangle>option_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (iam_lookup, iam_lookup) \<in> nat_rel \<rightarrow> \<langle>R\<rangle>iam_rel \<rightarrow> \<langle>R\<rangle>option_rel
[PROOF STEP]
unfolding iam_lookup_def[abs_def]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>k a. iam_\<alpha> a k, \<lambda>k a. iam_\<alpha> a k) \<in> nat_rel \<rightarrow> \<langle>R\<rangle>iam_rel \<rightarrow> \<langle>R\<rangle>option_rel
[PROOF STEP]
by parametricity


[STATEMENT]
lemma param_iam_increment[param]:
  "(iam_increment, iam_increment) \<in> nat_rel \<rightarrow> nat_rel \<rightarrow> nat_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (iam_increment, iam_increment) \<in> nat_rel \<rightarrow> nat_rel \<rightarrow> nat_rel
[PROOF STEP]
unfolding iam_increment_def[abs_def]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>l idx. max (idx + 1 - l) (2 * l + 3), \<lambda>l idx. max (idx + 1 - l) (2 * l + 3)) \<in> nat_rel \<rightarrow> nat_rel \<rightarrow> nat_rel
[PROOF STEP]
by simp


[STATEMENT]
lemma param_iam_update[param]:
  "(iam_update, iam_update) \<in> nat_rel \<rightarrow> R \<rightarrow> \<langle>R\<rangle>iam_rel \<rightarrow> \<langle>R\<rangle>iam_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (iam_update, iam_update) \<in> nat_rel \<rightarrow> R \<rightarrow> \<langle>R\<rangle>iam_rel \<rightarrow> \<langle>R\<rangle>iam_rel
[PROOF STEP]
unfolding iam_update_def[abs_def] iam_rel_def Let_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>k v a. array_set (if k < array_length a then a else array_grow a (iam_increment (array_length a) k) None) k (Some v), \<lambda>k v a. array_set (if k < array_length a then a else array_grow a (iam_increment (array_length a) k) None) k (Some v)) \<in> nat_rel \<rightarrow> R \<rightarrow> \<langle>\<langle>R\<rangle>option_rel\<rangle>array_rel \<rightarrow> \<langle>\<langle>R\<rangle>option_rel\<rangle>array_rel
[PROOF STEP]
apply parametricity
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma param_iam_delete[param]:
  "(iam_delete, iam_delete) \<in> nat_rel \<rightarrow> \<langle>R\<rangle>iam_rel \<rightarrow> \<langle>R\<rangle>iam_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (iam_delete, iam_delete) \<in> nat_rel \<rightarrow> \<langle>R\<rangle>iam_rel \<rightarrow> \<langle>R\<rangle>iam_rel
[PROOF STEP]
unfolding iam_delete_def[abs_def] iam_rel_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>k a. if k < array_length a then array_set a k None else a, \<lambda>k a. if k < array_length a then array_set a k None else a) \<in> nat_rel \<rightarrow> \<langle>\<langle>R\<rangle>option_rel\<rangle>array_rel \<rightarrow> \<langle>\<langle>R\<rangle>option_rel\<rangle>array_rel
[PROOF STEP]
by parametricity


[STATEMENT]
lemma param_iam_iteratei_aux[param]:
  assumes I: "i \<le> array_length a"
  assumes IR: "(i,i') \<in> nat_rel"
  assumes AR: "(a,a') \<in> \<langle>Ra\<rangle>iam_rel"
  assumes CR: "(c,c') \<in> Rb \<rightarrow> bool_rel"
  assumes FR: "(f,f') \<in> \<langle>nat_rel,Ra\<rangle>prod_rel \<rightarrow> Rb \<rightarrow> Rb"
  assumes \<sigma>R: "(\<sigma>,\<sigma>') \<in> Rb"
  shows "(iam_iteratei_aux i a c f \<sigma>, iam_iteratei_aux i' a' c' f' \<sigma>') \<in> Rb"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (iam_iteratei_aux i a c f \<sigma>, iam_iteratei_aux i' a' c' f' \<sigma>') \<in> Rb
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
i \<le> array_length a
(i, i') \<in> nat_rel
(a, a') \<in> \<langle>Ra\<rangle>iam_rel
(c, c') \<in> Rb \<rightarrow> bool_rel
(f, f') \<in> nat_rel \<times>\<^sub>r Ra \<rightarrow> Rb \<rightarrow> Rb
(\<sigma>, \<sigma>') \<in> Rb

goal (1 subgoal):
 1. (iam_iteratei_aux i a c f \<sigma>, iam_iteratei_aux i' a' c' f' \<sigma>') \<in> Rb
[PROOF STEP]
unfolding iam_rel_def
[PROOF STATE]
proof (prove)
using this:
i \<le> array_length a
(i, i') \<in> nat_rel
(a, a') \<in> \<langle>\<langle>Ra\<rangle>option_rel\<rangle>array_rel
(c, c') \<in> Rb \<rightarrow> bool_rel
(f, f') \<in> nat_rel \<times>\<^sub>r Ra \<rightarrow> Rb \<rightarrow> Rb
(\<sigma>, \<sigma>') \<in> Rb

goal (1 subgoal):
 1. (iam_iteratei_aux i a c f \<sigma>, iam_iteratei_aux i' a' c' f' \<sigma>') \<in> Rb
[PROOF STEP]
apply (induct i' arbitrary: i \<sigma> \<sigma>')
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>i \<sigma> \<sigma>'. \<lbrakk>i \<le> array_length a; (i, 0) \<in> nat_rel; (a, a') \<in> \<langle>\<langle>Ra\<rangle>option_rel\<rangle>array_rel; (c, c') \<in> Rb \<rightarrow> bool_rel; (f, f') \<in> nat_rel \<times>\<^sub>r Ra \<rightarrow> Rb \<rightarrow> Rb; (\<sigma>, \<sigma>') \<in> Rb\<rbrakk> \<Longrightarrow> (iam_iteratei_aux i a c f \<sigma>, iam_iteratei_aux 0 a' c' f' \<sigma>') \<in> Rb
 2. \<And>i' i \<sigma> \<sigma>'. \<lbrakk>\<And>i \<sigma> \<sigma>'. \<lbrakk>i \<le> array_length a; (i, i') \<in> nat_rel; (a, a') \<in> \<langle>\<langle>Ra\<rangle>option_rel\<rangle>array_rel; (c, c') \<in> Rb \<rightarrow> bool_rel; (f, f') \<in> nat_rel \<times>\<^sub>r Ra \<rightarrow> Rb \<rightarrow> Rb; (\<sigma>, \<sigma>') \<in> Rb\<rbrakk> \<Longrightarrow> (iam_iteratei_aux i a c f \<sigma>, iam_iteratei_aux i' a' c' f' \<sigma>') \<in> Rb; i \<le> array_length a; (i, Suc i') \<in> nat_rel; (a, a') \<in> \<langle>\<langle>Ra\<rangle>option_rel\<rangle>array_rel; (c, c') \<in> Rb \<rightarrow> bool_rel; (f, f') \<in> nat_rel \<times>\<^sub>r Ra \<rightarrow> Rb \<rightarrow> Rb; (\<sigma>, \<sigma>') \<in> Rb\<rbrakk> \<Longrightarrow> (iam_iteratei_aux i a c f \<sigma>, iam_iteratei_aux (Suc i') a' c' f' \<sigma>') \<in> Rb
[PROOF STEP]
apply (simp_all only: pair_in_Id_conv iam_iteratei_aux.simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i' i \<sigma> \<sigma>'. \<lbrakk>\<And>i \<sigma> \<sigma>'. \<lbrakk>i' \<le> array_length a; i = i'; True; True; True; (\<sigma>, \<sigma>') \<in> Rb\<rbrakk> \<Longrightarrow> (iam_iteratei_aux i' a c f \<sigma>, iam_iteratei_aux i' a' c' f' \<sigma>') \<in> Rb; Suc i' \<le> array_length a; i = Suc i'; (a, a') \<in> \<langle>\<langle>Ra\<rangle>option_rel\<rangle>array_rel; (c, c') \<in> Rb \<rightarrow> bool_rel; (f, f') \<in> nat_rel \<times>\<^sub>r Ra \<rightarrow> Rb \<rightarrow> Rb; (\<sigma>, \<sigma>') \<in> Rb\<rbrakk> \<Longrightarrow> (if c \<sigma> then iam_iteratei_aux i' a c f (case array_get a i' of None \<Rightarrow> \<sigma> | Some x \<Rightarrow> f (i', x) \<sigma>) else \<sigma>, if c' \<sigma>' then iam_iteratei_aux i' a' c' f' (case array_get a' i' of None \<Rightarrow> \<sigma>' | Some x \<Rightarrow> f' (i', x) \<sigma>') else \<sigma>') \<in> Rb
[PROOF STEP]
apply parametricity
[PROOF STATE]
proof (prove)
goal (8 subgoals):
 1. \<And>i' i \<sigma> \<sigma>'. \<lbrakk>Suc i' \<le> array_length a; i = Suc i'; (a, a') \<in> \<langle>\<langle>Ra\<rangle>option_rel\<rangle>array_rel; (c, c') \<in> Rb \<rightarrow> bool_rel; (f, f') \<in> nat_rel \<times>\<^sub>r Ra \<rightarrow> Rb \<rightarrow> Rb; (\<sigma>, \<sigma>') \<in> Rb; c \<sigma>; c' \<sigma>'\<rbrakk> \<Longrightarrow> i' \<le> array_length a
 2. \<And>i' i \<sigma> \<sigma>'. \<lbrakk>Suc i' \<le> array_length a; i = Suc i'; (a, a') \<in> \<langle>\<langle>Ra\<rangle>option_rel\<rangle>array_rel; (c, c') \<in> Rb \<rightarrow> bool_rel; (f, f') \<in> nat_rel \<times>\<^sub>r Ra \<rightarrow> Rb \<rightarrow> Rb; (\<sigma>, \<sigma>') \<in> Rb; c \<sigma>; c' \<sigma>'\<rbrakk> \<Longrightarrow> ?i15 i' i \<sigma> \<sigma>' = i'
 3. \<And>i' i \<sigma> \<sigma>'. \<lbrakk>Suc i' \<le> array_length a; i = Suc i'; (a, a') \<in> \<langle>\<langle>Ra\<rangle>option_rel\<rangle>array_rel; (c, c') \<in> Rb \<rightarrow> bool_rel; (f, f') \<in> nat_rel \<times>\<^sub>r Ra \<rightarrow> Rb \<rightarrow> Rb; (\<sigma>, \<sigma>') \<in> Rb; c \<sigma>; c' \<sigma>'\<rbrakk> \<Longrightarrow> True
 4. \<And>i' i \<sigma> \<sigma>'. \<lbrakk>Suc i' \<le> array_length a; i = Suc i'; (a, a') \<in> \<langle>\<langle>Ra\<rangle>option_rel\<rangle>array_rel; (c, c') \<in> Rb \<rightarrow> bool_rel; (f, f') \<in> nat_rel \<times>\<^sub>r Ra \<rightarrow> Rb \<rightarrow> Rb; (\<sigma>, \<sigma>') \<in> Rb; c \<sigma>; c' \<sigma>'\<rbrakk> \<Longrightarrow> True
 5. \<And>i' i \<sigma> \<sigma>'. \<lbrakk>Suc i' \<le> array_length a; i = Suc i'; (a, a') \<in> \<langle>\<langle>Ra\<rangle>option_rel\<rangle>array_rel; (c, c') \<in> Rb \<rightarrow> bool_rel; (f, f') \<in> nat_rel \<times>\<^sub>r Ra \<rightarrow> Rb \<rightarrow> Rb; (\<sigma>, \<sigma>') \<in> Rb; c \<sigma>; c' \<sigma>'\<rbrakk> \<Longrightarrow> True
 6. \<And>i' i \<sigma> \<sigma>' aa a'a. \<lbrakk>Suc i' \<le> array_length a; i = Suc i'; (a, a') \<in> \<langle>\<langle>Ra\<rangle>option_rel\<rangle>array_rel; (c, c') \<in> Rb \<rightarrow> bool_rel; (f, f') \<in> nat_rel \<times>\<^sub>r Ra \<rightarrow> Rb \<rightarrow> Rb; (\<sigma>, \<sigma>') \<in> Rb; c \<sigma>; c' \<sigma>'; (aa, a'a) \<in> Ra\<rbrakk> \<Longrightarrow> (i', i') \<in> nat_rel
 7. \<And>i' i \<sigma> \<sigma>'. \<lbrakk>Suc i' \<le> array_length a; i = Suc i'; (a, a') \<in> \<langle>\<langle>Ra\<rangle>option_rel\<rangle>array_rel; (c, c') \<in> Rb \<rightarrow> bool_rel; (f, f') \<in> nat_rel \<times>\<^sub>r Ra \<rightarrow> Rb \<rightarrow> Rb; (\<sigma>, \<sigma>') \<in> Rb; c \<sigma>; c' \<sigma>'\<rbrakk> \<Longrightarrow> i' < array_length a
 8. \<And>i' i \<sigma> \<sigma>'. \<lbrakk>Suc i' \<le> array_length a; i = Suc i'; (a, a') \<in> \<langle>\<langle>Ra\<rangle>option_rel\<rangle>array_rel; (c, c') \<in> Rb \<rightarrow> bool_rel; (f, f') \<in> nat_rel \<times>\<^sub>r Ra \<rightarrow> Rb \<rightarrow> Rb; (\<sigma>, \<sigma>') \<in> Rb; c \<sigma>; c' \<sigma>'\<rbrakk> \<Longrightarrow> (i', i') \<in> nat_rel
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma param_iam_iteratei[param]:
  "(iam_iteratei,iam_iteratei) \<in> \<langle>Ra\<rangle>iam_rel \<rightarrow> (Rb \<rightarrow> bool_rel) \<rightarrow>
      (\<langle>nat_rel,Ra\<rangle>prod_rel \<rightarrow> Rb \<rightarrow> Rb) \<rightarrow> Rb \<rightarrow> Rb"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (iam_iteratei, iam_iteratei) \<in> \<langle>Ra\<rangle>iam_rel \<rightarrow> (Rb \<rightarrow> bool_rel) \<rightarrow> (nat_rel \<times>\<^sub>r Ra \<rightarrow> Rb \<rightarrow> Rb) \<rightarrow> Rb \<rightarrow> Rb
[PROOF STEP]
unfolding iam_iteratei_def[abs_def]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>a. iam_iteratei_aux (array_length a) a, \<lambda>a. iam_iteratei_aux (array_length a) a) \<in> \<langle>Ra\<rangle>iam_rel \<rightarrow> (Rb \<rightarrow> bool_rel) \<rightarrow> (nat_rel \<times>\<^sub>r Ra \<rightarrow> Rb \<rightarrow> Rb) \<rightarrow> Rb \<rightarrow> Rb
[PROOF STEP]
by parametricity (simp_all add: iam_rel_def)


[STATEMENT]
lemma iam_empty_correct:
  "(iam_empty (), Map.empty) \<in>  iam_rel'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (iam_empty (), Map.empty) \<in> iam_rel'
[PROOF STEP]
by (simp add: iam_rel'_def br_def iam_\<alpha>_def[abs_def] iam_empty_def)


[STATEMENT]
lemma iam_update_correct:
  "(iam_update,op_map_update) \<in> nat_rel \<rightarrow> Id \<rightarrow> iam_rel'  \<rightarrow> iam_rel'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (iam_update, op_map_update) \<in> nat_rel \<rightarrow> Id \<rightarrow> iam_rel' \<rightarrow> iam_rel'
[PROOF STEP]
by (auto simp: iam_rel'_def br_def Let_def array_get_array_set_other
                  incr_correct iam_\<alpha>_def[abs_def] iam_update_def)


[STATEMENT]
lemma iam_lookup_correct:
  "(iam_lookup,op_map_lookup) \<in> Id \<rightarrow> iam_rel' \<rightarrow> \<langle>Id\<rangle>option_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (iam_lookup, op_map_lookup) \<in> nat_rel \<rightarrow> iam_rel' \<rightarrow> \<langle>Id\<rangle>option_rel
[PROOF STEP]
by (auto simp: iam_rel'_def br_def iam_lookup_def[abs_def])


[STATEMENT]
lemma array_get_set_iff: "i<array_length a \<Longrightarrow>
  array_get (array_set a i x) j = (if i=j then x else array_get a j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i < array_length a \<Longrightarrow> array_get (array_set a i x) j = (if i = j then x else array_get a j)
[PROOF STEP]
by (auto simp: array_get_array_set_other)