[STATEMENT]
lemma (in encoding) OC_wrt_equivalence_iff_weak_reduction_bisimulation:
  fixes TRel :: "('procT \<times> 'procT) set"
  assumes eqT: "equivalence TRel"
  shows "(operational_corresponding TRel \<and> weak_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> weak_reduction_bisimulation Rel (STCal Source Target))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (operational_corresponding TRel \<and> weak_reduction_bisimulation TRel Target) = (\<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> weak_reduction_bisimulation Rel (STCal Source Target))
[PROOF STEP]
proof (rule iffI, erule conjE)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. operational_corresponding TRel \<and> weak_reduction_bisimulation TRel Target \<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> weak_reduction_bisimulation Rel (STCal Source Target)
 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> weak_reduction_bisimulation Rel (STCal Source Target) \<Longrightarrow> operational_corresponding TRel \<and> weak_reduction_bisimulation TRel Target
[PROOF STEP]
assume oc: "operational_corresponding TRel" and bisimT: "weak_reduction_bisimulation TRel Target"
[PROOF STATE]
proof (state)
this:
operational_corresponding TRel
weak_reduction_bisimulation TRel Target

goal (2 subgoals):
 1. operational_corresponding TRel \<and> weak_reduction_bisimulation TRel Target \<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> weak_reduction_bisimulation Rel (STCal Source Target)
 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> weak_reduction_bisimulation Rel (STCal Source Target) \<Longrightarrow> operational_corresponding TRel \<and> weak_reduction_bisimulation TRel Target
[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. operational_corresponding TRel \<and> weak_reduction_bisimulation TRel Target \<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> weak_reduction_bisimulation Rel (STCal Source Target)
 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> weak_reduction_bisimulation Rel (STCal Source Target) \<Longrightarrow> operational_corresponding TRel \<and> weak_reduction_bisimulation TRel Target
[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. operational_corresponding TRel \<and> weak_reduction_bisimulation TRel Target \<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> weak_reduction_bisimulation Rel (STCal Source Target)
 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> weak_reduction_bisimulation Rel (STCal Source Target) \<Longrightarrow> operational_corresponding TRel \<and> weak_reduction_bisimulation TRel Target
[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. operational_corresponding TRel \<and> weak_reduction_bisimulation TRel Target \<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> weak_reduction_bisimulation Rel (STCal Source Target)
 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> weak_reduction_bisimulation Rel (STCal Source Target) \<Longrightarrow> operational_corresponding TRel \<and> weak_reduction_bisimulation TRel Target
[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. operational_corresponding TRel \<and> weak_reduction_bisimulation TRel Target \<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> weak_reduction_bisimulation Rel (STCal Source Target)
 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> weak_reduction_bisimulation Rel (STCal Source Target) \<Longrightarrow> operational_corresponding TRel \<and> weak_reduction_bisimulation TRel Target
[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. operational_corresponding TRel \<and> weak_reduction_bisimulation TRel Target \<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> weak_reduction_bisimulation Rel (STCal Source Target)
 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> weak_reduction_bisimulation Rel (STCal Source Target) \<Longrightarrow> operational_corresponding TRel \<and> weak_reduction_bisimulation TRel Target
[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. operational_corresponding TRel \<and> weak_reduction_bisimulation TRel Target \<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> weak_reduction_bisimulation Rel (STCal Source Target)
 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> weak_reduction_bisimulation Rel (STCal Source Target) \<Longrightarrow> operational_corresponding TRel \<and> weak_reduction_bisimulation TRel Target
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
trans (indRelTEQ TRel)

goal (2 subgoals):
 1. operational_corresponding TRel \<and> weak_reduction_bisimulation TRel Target \<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> weak_reduction_bisimulation Rel (STCal Source Target)
 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> weak_reduction_bisimulation Rel (STCal Source Target) \<Longrightarrow> operational_corresponding TRel \<and> weak_reduction_bisimulation TRel Target
[PROOF STEP]
from eqT oc bisimT
[PROOF STATE]
proof (chain)
picking this:
equivalence TRel
operational_corresponding TRel
weak_reduction_bisimulation TRel Target
[PROOF STEP]
have "weak_reduction_bisimulation (indRelTEQ TRel) (STCal Source Target)"
[PROOF STATE]
proof (prove)
using this:
equivalence TRel
operational_corresponding TRel
weak_reduction_bisimulation TRel Target

goal (1 subgoal):
 1. weak_reduction_bisimulation (indRelTEQ TRel) (STCal Source Target)
[PROOF STEP]
using OC_wrt_equivalence_iff_indRelTEQ_weak_reduction_bisimulation[where TRel="TRel"]
[PROOF STATE]
proof (prove)
using this:
equivalence TRel
operational_corresponding TRel
weak_reduction_bisimulation TRel Target
equivalence TRel \<Longrightarrow> (operational_corresponding TRel \<and> weak_reduction_bisimulation TRel Target) = weak_reduction_bisimulation (indRelTEQ TRel) (STCal Source Target)

goal (1 subgoal):
 1. weak_reduction_bisimulation (indRelTEQ TRel) (STCal Source Target)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
weak_reduction_bisimulation (indRelTEQ TRel) (STCal Source Target)

goal (2 subgoals):
 1. operational_corresponding TRel \<and> weak_reduction_bisimulation TRel Target \<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> weak_reduction_bisimulation Rel (STCal Source Target)
 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> weak_reduction_bisimulation Rel (STCal Source Target) \<Longrightarrow> operational_corresponding TRel \<and> weak_reduction_bisimulation TRel Target
[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)
weak_reduction_bisimulation (indRelTEQ TRel) (STCal Source Target)
[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> weak_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)
weak_reduction_bisimulation (indRelTEQ TRel) (STCal Source Target)

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> weak_reduction_bisimulation Rel (STCal Source Target)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel \<and> (TargetTerm (\<lbrakk>S\<rbrakk>), SourceTerm S) \<in> Rel) \<and> TRel = _Collect (T1, T2) ((TargetTerm T1, TargetTerm T2) \<in> Rel) \<and> trans Rel \<and> weak_reduction_bisimulation Rel (STCal Source Target)

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> weak_reduction_bisimulation Rel (STCal Source Target) \<Longrightarrow> operational_corresponding TRel \<and> weak_reduction_bisimulation TRel Target
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel \<and> (TargetTerm (\<lbrakk>S\<rbrakk>), SourceTerm S) \<in> Rel) \<and> TRel = _Collect (T1, T2) ((TargetTerm T1, TargetTerm T2) \<in> Rel) \<and> trans Rel \<and> weak_reduction_bisimulation Rel (STCal Source Target) \<Longrightarrow> operational_corresponding TRel \<and> weak_reduction_bisimulation TRel Target
[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> weak_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> weak_reduction_bisimulation Rel (STCal Source Target)

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> weak_reduction_bisimulation Rel (STCal Source Target) \<Longrightarrow> operational_corresponding TRel \<and> weak_reduction_bisimulation TRel Target
[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> weak_reduction_bisimulation Rel (STCal Source Target)
[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: "weak_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> weak_reduction_bisimulation Rel (STCal Source Target)

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> weak_reduction_bisimulation Rel (STCal Source Target) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel \<and> (TargetTerm (\<lbrakk>S\<rbrakk>), SourceTerm S) \<in> Rel
TRel = _Collect (T1, T2) ((TargetTerm T1, TargetTerm T2) \<in> Rel)
trans Rel
weak_reduction_bisimulation Rel (STCal Source Target)

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> weak_reduction_bisimulation Rel (STCal Source Target) \<Longrightarrow> operational_corresponding TRel \<and> weak_reduction_bisimulation TRel Target
[PROOF STEP]
have "operational_corresponding TRel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. operational_corresponding 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_steps(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'
weak_reduction_bisimulation Rel (STCal Source Target)

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_steps(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_steps(2))
[PROOF STATE]
proof (state)
this:
TargetTerm (\<lbrakk>S\<rbrakk>) \<longmapsto>STCal Source Target* TargetTerm T

goal (1 subgoal):
 1. \<And>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target* T \<Longrightarrow> \<exists>S'. S \<longmapsto>Source* S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel
[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
weak_reduction_bisimulation Rel (STCal Source Target)

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_steps(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:
operational_corresponding 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> weak_reduction_bisimulation Rel (STCal Source Target) \<Longrightarrow> operational_corresponding TRel \<and> weak_reduction_bisimulation TRel Target
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
operational_corresponding 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> weak_reduction_bisimulation Rel (STCal Source Target) \<Longrightarrow> operational_corresponding TRel \<and> weak_reduction_bisimulation TRel Target
[PROOF STEP]
have "weak_reduction_bisimulation TRel Target"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. weak_reduction_bisimulation TRel Target
[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_steps(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'
weak_reduction_bisimulation Rel (STCal Source Target)

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_steps(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_steps(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'
weak_reduction_bisimulation Rel (STCal Source Target)

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_steps(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:
weak_reduction_bisimulation TRel Target

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> weak_reduction_bisimulation Rel (STCal Source Target) \<Longrightarrow> operational_corresponding TRel \<and> weak_reduction_bisimulation TRel Target
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
operational_corresponding TRel
weak_reduction_bisimulation TRel Target
[PROOF STEP]
show "operational_corresponding TRel \<and> weak_reduction_bisimulation TRel Target"
[PROOF STATE]
proof (prove)
using this:
operational_corresponding TRel
weak_reduction_bisimulation TRel Target

goal (1 subgoal):
 1. operational_corresponding TRel \<and> weak_reduction_bisimulation TRel Target
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
operational_corresponding TRel \<and> weak_reduction_bisimulation TRel Target

goal:
No subgoals!
[PROOF STEP]
qed