[STATEMENT]
lemma (in encoding) OC_wrt_preorder_iff_weak_reduction_bisimulation:
  fixes TRel :: "('procT \<times> 'procT) set"
  shows "(operational_corresponding TRel \<and> preorder TRel
         \<and> weak_reduction_bisimulation TRel Target)
         = (\<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel)
            \<and> TRel = {(T1, T2). (TargetTerm T1, TargetTerm T2) \<in> Rel}
            \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel)
            \<and> preorder Rel
            \<and> weak_reduction_bisimulation Rel (STCal Source Target))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (operational_corresponding TRel \<and> preorder TRel \<and> weak_reduction_bisimulation TRel Target) = (\<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel) \<and> TRel = _Collect (T1, T2) ((TargetTerm T1, TargetTerm T2) \<in> Rel) \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel) \<and> preorder Rel \<and> weak_reduction_bisimulation Rel (STCal Source Target))
[PROOF STEP]
proof (rule iffI, erule conjE, erule conjE, erule conjE)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. operational_complete TRel \<and> operational_sound TRel \<and> preorder TRel \<and> weak_reduction_bisimulation TRel Target \<Longrightarrow> \<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel) \<and> TRel = _Collect (T1, T2) ((TargetTerm T1, TargetTerm T2) \<in> Rel) \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel) \<and> preorder Rel \<and> weak_reduction_bisimulation Rel (STCal Source Target)
 2. \<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel) \<and> TRel = _Collect (T1, T2) ((TargetTerm T1, TargetTerm T2) \<in> Rel) \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel) \<and> preorder Rel \<and> weak_reduction_bisimulation Rel (STCal Source Target) \<Longrightarrow> operational_corresponding TRel \<and> preorder TRel \<and> weak_reduction_bisimulation TRel Target
[PROOF STEP]
assume A1: "operational_complete TRel" and A2: "operational_sound TRel"
     and A3:"preorder TRel" and A4: "weak_reduction_bisimulation TRel Target"
[PROOF STATE]
proof (state)
this:
operational_complete TRel
operational_sound TRel
preorder TRel
weak_reduction_bisimulation TRel Target

goal (2 subgoals):
 1. operational_complete TRel \<and> operational_sound TRel \<and> preorder TRel \<and> weak_reduction_bisimulation TRel Target \<Longrightarrow> \<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel) \<and> TRel = _Collect (T1, T2) ((TargetTerm T1, TargetTerm T2) \<in> Rel) \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel) \<and> preorder Rel \<and> weak_reduction_bisimulation Rel (STCal Source Target)
 2. \<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel) \<and> TRel = _Collect (T1, T2) ((TargetTerm T1, TargetTerm T2) \<in> Rel) \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel) \<and> preorder Rel \<and> weak_reduction_bisimulation Rel (STCal Source Target) \<Longrightarrow> operational_corresponding TRel \<and> preorder TRel \<and> weak_reduction_bisimulation TRel Target
[PROOF STEP]
from A3
[PROOF STATE]
proof (chain)
picking this:
preorder TRel
[PROOF STEP]
have A5: "TRel\<^sup>+ = TRel"
[PROOF STATE]
proof (prove)
using this:
preorder TRel

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

goal (1 subgoal):
 1. TRel\<^sup>+ = TRel
[PROOF STEP]
unfolding preorder_on_def
[PROOF STATE]
proof (prove)
using this:
refl TRel \<and> trans TRel
trans TRel \<Longrightarrow> TRel\<^sup>+ = TRel

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

goal (2 subgoals):
 1. operational_complete TRel \<and> operational_sound TRel \<and> preorder TRel \<and> weak_reduction_bisimulation TRel Target \<Longrightarrow> \<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel) \<and> TRel = _Collect (T1, T2) ((TargetTerm T1, TargetTerm T2) \<in> Rel) \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel) \<and> preorder Rel \<and> weak_reduction_bisimulation Rel (STCal Source Target)
 2. \<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel) \<and> TRel = _Collect (T1, T2) ((TargetTerm T1, TargetTerm T2) \<in> Rel) \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel) \<and> preorder Rel \<and> weak_reduction_bisimulation Rel (STCal Source Target) \<Longrightarrow> operational_corresponding TRel \<and> preorder TRel \<and> weak_reduction_bisimulation TRel Target
[PROOF STEP]
with A3
[PROOF STATE]
proof (chain)
picking this:
preorder TRel
TRel\<^sup>+ = TRel
[PROOF STEP]
have "TRel\<^sup>* = TRel"
[PROOF STATE]
proof (prove)
using this:
preorder TRel
TRel\<^sup>+ = TRel

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

goal (1 subgoal):
 1. TRel\<^sup>* = TRel
[PROOF STEP]
unfolding preorder_on_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> trans TRel
TRel\<^sup>+ = TRel
(TRel\<^sup>+)\<^sup>= = TRel\<^sup>*

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

goal (2 subgoals):
 1. operational_complete TRel \<and> operational_sound TRel \<and> preorder TRel \<and> weak_reduction_bisimulation TRel Target \<Longrightarrow> \<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel) \<and> TRel = _Collect (T1, T2) ((TargetTerm T1, TargetTerm T2) \<in> Rel) \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel) \<and> preorder Rel \<and> weak_reduction_bisimulation Rel (STCal Source Target)
 2. \<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel) \<and> TRel = _Collect (T1, T2) ((TargetTerm T1, TargetTerm T2) \<in> Rel) \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel) \<and> preorder Rel \<and> weak_reduction_bisimulation Rel (STCal Source Target) \<Longrightarrow> operational_corresponding TRel \<and> preorder TRel \<and> weak_reduction_bisimulation TRel Target
[PROOF STEP]
with A1 A2
[PROOF STATE]
proof (chain)
picking this:
operational_complete TRel
operational_sound TRel
TRel\<^sup>* = TRel
[PROOF STEP]
have "operational_corresponding (TRel\<^sup>*)"
[PROOF STATE]
proof (prove)
using this:
operational_complete TRel
operational_sound TRel
TRel\<^sup>* = TRel

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

goal (2 subgoals):
 1. operational_complete TRel \<and> operational_sound TRel \<and> preorder TRel \<and> weak_reduction_bisimulation TRel Target \<Longrightarrow> \<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel) \<and> TRel = _Collect (T1, T2) ((TargetTerm T1, TargetTerm T2) \<in> Rel) \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel) \<and> preorder Rel \<and> weak_reduction_bisimulation Rel (STCal Source Target)
 2. \<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel) \<and> TRel = _Collect (T1, T2) ((TargetTerm T1, TargetTerm T2) \<in> Rel) \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel) \<and> preorder Rel \<and> weak_reduction_bisimulation Rel (STCal Source Target) \<Longrightarrow> operational_corresponding TRel \<and> preorder TRel \<and> weak_reduction_bisimulation TRel Target
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
operational_corresponding (TRel\<^sup>*)

goal (2 subgoals):
 1. operational_complete TRel \<and> operational_sound TRel \<and> preorder TRel \<and> weak_reduction_bisimulation TRel Target \<Longrightarrow> \<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel) \<and> TRel = _Collect (T1, T2) ((TargetTerm T1, TargetTerm T2) \<in> Rel) \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel) \<and> preorder Rel \<and> weak_reduction_bisimulation Rel (STCal Source Target)
 2. \<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel) \<and> TRel = _Collect (T1, T2) ((TargetTerm T1, TargetTerm T2) \<in> Rel) \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel) \<and> preorder Rel \<and> weak_reduction_bisimulation Rel (STCal Source Target) \<Longrightarrow> operational_corresponding TRel \<and> preorder TRel \<and> weak_reduction_bisimulation TRel Target
[PROOF STEP]
from A4 A5
[PROOF STATE]
proof (chain)
picking this:
weak_reduction_bisimulation TRel Target
TRel\<^sup>+ = TRel
[PROOF STEP]
have "weak_reduction_bisimulation (TRel\<^sup>+) Target"
[PROOF STATE]
proof (prove)
using this:
weak_reduction_bisimulation TRel Target
TRel\<^sup>+ = TRel

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

goal (2 subgoals):
 1. operational_complete TRel \<and> operational_sound TRel \<and> preorder TRel \<and> weak_reduction_bisimulation TRel Target \<Longrightarrow> \<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel) \<and> TRel = _Collect (T1, T2) ((TargetTerm T1, TargetTerm T2) \<in> Rel) \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel) \<and> preorder Rel \<and> weak_reduction_bisimulation Rel (STCal Source Target)
 2. \<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel) \<and> TRel = _Collect (T1, T2) ((TargetTerm T1, TargetTerm T2) \<in> Rel) \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel) \<and> preorder Rel \<and> weak_reduction_bisimulation Rel (STCal Source Target) \<Longrightarrow> operational_corresponding TRel \<and> preorder TRel \<and> weak_reduction_bisimulation TRel Target
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
operational_corresponding (TRel\<^sup>*)
weak_reduction_bisimulation (TRel\<^sup>+) Target
[PROOF STEP]
have "weak_reduction_bisimulation (indRelRTPO TRel) (STCal Source Target)"
[PROOF STATE]
proof (prove)
using this:
operational_corresponding (TRel\<^sup>*)
weak_reduction_bisimulation (TRel\<^sup>+) Target

goal (1 subgoal):
 1. weak_reduction_bisimulation (indRelRTPO TRel) (STCal Source Target)
[PROOF STEP]
using OC_iff_indRelRTPO_is_weak_reduction_bisimulation[where TRel="TRel"]
[PROOF STATE]
proof (prove)
using this:
operational_corresponding (TRel\<^sup>*)
weak_reduction_bisimulation (TRel\<^sup>+) Target
(operational_corresponding (TRel\<^sup>*) \<and> weak_reduction_bisimulation (TRel\<^sup>+) Target) = weak_reduction_bisimulation (indRelRTPO TRel) (STCal Source Target)

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

goal (2 subgoals):
 1. operational_complete TRel \<and> operational_sound TRel \<and> preorder TRel \<and> weak_reduction_bisimulation TRel Target \<Longrightarrow> \<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel) \<and> TRel = _Collect (T1, T2) ((TargetTerm T1, TargetTerm T2) \<in> Rel) \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel) \<and> preorder Rel \<and> weak_reduction_bisimulation Rel (STCal Source Target)
 2. \<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel) \<and> TRel = _Collect (T1, T2) ((TargetTerm T1, TargetTerm T2) \<in> Rel) \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel) \<and> preorder Rel \<and> weak_reduction_bisimulation Rel (STCal Source Target) \<Longrightarrow> operational_corresponding TRel \<and> preorder TRel \<and> weak_reduction_bisimulation TRel Target
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
weak_reduction_bisimulation (indRelRTPO TRel) (STCal Source Target)

goal (2 subgoals):
 1. operational_complete TRel \<and> operational_sound TRel \<and> preorder TRel \<and> weak_reduction_bisimulation TRel Target \<Longrightarrow> \<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel) \<and> TRel = _Collect (T1, T2) ((TargetTerm T1, TargetTerm T2) \<in> Rel) \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel) \<and> preorder Rel \<and> weak_reduction_bisimulation Rel (STCal Source Target)
 2. \<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel) \<and> TRel = _Collect (T1, T2) ((TargetTerm T1, TargetTerm T2) \<in> Rel) \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel) \<and> preorder Rel \<and> weak_reduction_bisimulation Rel (STCal Source Target) \<Longrightarrow> operational_corresponding TRel \<and> preorder TRel \<and> weak_reduction_bisimulation TRel Target
[PROOF STEP]
have "\<forall>S. SourceTerm S \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm (\<lbrakk>S\<rbrakk>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>S. SourceTerm S \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm (\<lbrakk>S\<rbrakk>)
[PROOF STEP]
by (simp add: indRelRTPO.encR)
[PROOF STATE]
proof (state)
this:
\<forall>S. SourceTerm S \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm (\<lbrakk>S\<rbrakk>)

goal (2 subgoals):
 1. operational_complete TRel \<and> operational_sound TRel \<and> preorder TRel \<and> weak_reduction_bisimulation TRel Target \<Longrightarrow> \<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel) \<and> TRel = _Collect (T1, T2) ((TargetTerm T1, TargetTerm T2) \<in> Rel) \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel) \<and> preorder Rel \<and> weak_reduction_bisimulation Rel (STCal Source Target)
 2. \<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel) \<and> TRel = _Collect (T1, T2) ((TargetTerm T1, TargetTerm T2) \<in> Rel) \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel) \<and> preorder Rel \<and> weak_reduction_bisimulation Rel (STCal Source Target) \<Longrightarrow> operational_corresponding TRel \<and> preorder TRel \<and> weak_reduction_bisimulation TRel Target
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>S. SourceTerm S \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm (\<lbrakk>S\<rbrakk>)

goal (2 subgoals):
 1. operational_complete TRel \<and> operational_sound TRel \<and> preorder TRel \<and> weak_reduction_bisimulation TRel Target \<Longrightarrow> \<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel) \<and> TRel = _Collect (T1, T2) ((TargetTerm T1, TargetTerm T2) \<in> Rel) \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel) \<and> preorder Rel \<and> weak_reduction_bisimulation Rel (STCal Source Target)
 2. \<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel) \<and> TRel = _Collect (T1, T2) ((TargetTerm T1, TargetTerm T2) \<in> Rel) \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel) \<and> preorder Rel \<and> weak_reduction_bisimulation Rel (STCal Source Target) \<Longrightarrow> operational_corresponding TRel \<and> preorder TRel \<and> weak_reduction_bisimulation TRel Target
[PROOF STEP]
have "TRel = {(T1, T2). TargetTerm T1 \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm T2}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. TRel = _Collect (T1, T2) (TargetTerm T1 \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm T2)
[PROOF STEP]
proof auto
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>a b. (a, b) \<in> TRel \<Longrightarrow> TargetTerm a \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm b
 2. \<And>a b. TargetTerm a \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm b \<Longrightarrow> (a, b) \<in> TRel
[PROOF STEP]
fix TP TQ
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>a b. (a, b) \<in> TRel \<Longrightarrow> TargetTerm a \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm b
 2. \<And>a b. TargetTerm a \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm b \<Longrightarrow> (a, b) \<in> TRel
[PROOF STEP]
assume "(TP, TQ) \<in> TRel"
[PROOF STATE]
proof (state)
this:
(TP, TQ) \<in> TRel

goal (2 subgoals):
 1. \<And>a b. (a, b) \<in> TRel \<Longrightarrow> TargetTerm a \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm b
 2. \<And>a b. TargetTerm a \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm b \<Longrightarrow> (a, b) \<in> TRel
[PROOF STEP]
thus "TargetTerm TP \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm TQ"
[PROOF STATE]
proof (prove)
using this:
(TP, TQ) \<in> TRel

goal (1 subgoal):
 1. TargetTerm TP \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm TQ
[PROOF STEP]
by (rule indRelRTPO.target)
[PROOF STATE]
proof (state)
this:
TargetTerm TP \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm TQ

goal (1 subgoal):
 1. \<And>a b. TargetTerm a \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm b \<Longrightarrow> (a, b) \<in> TRel
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b. TargetTerm a \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm b \<Longrightarrow> (a, b) \<in> TRel
[PROOF STEP]
fix TP TQ
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b. TargetTerm a \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm b \<Longrightarrow> (a, b) \<in> TRel
[PROOF STEP]
assume "TargetTerm TP \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm TQ"
[PROOF STATE]
proof (state)
this:
TargetTerm TP \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm TQ

goal (1 subgoal):
 1. \<And>a b. TargetTerm a \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm b \<Longrightarrow> (a, b) \<in> TRel
[PROOF STEP]
with A3
[PROOF STATE]
proof (chain)
picking this:
preorder TRel
TargetTerm TP \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm TQ
[PROOF STEP]
show "(TP, TQ) \<in> TRel"
[PROOF STATE]
proof (prove)
using this:
preorder TRel
TargetTerm TP \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm TQ

goal (1 subgoal):
 1. (TP, TQ) \<in> TRel
[PROOF STEP]
using indRelRTPO_to_TRel(4)[where TRel="TRel"] trancl_id[of TRel]
[PROOF STATE]
proof (prove)
using this:
preorder TRel
TargetTerm TP \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm TQ
?P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> ?Q \<Longrightarrow> \<forall>TP TQ. TP \<in>T ?P \<and> TQ \<in>T ?Q \<longrightarrow> (TP, TQ) \<in> TRel\<^sup>+
trans TRel \<Longrightarrow> TRel\<^sup>+ = TRel

goal (1 subgoal):
 1. (TP, TQ) \<in> TRel
[PROOF STEP]
unfolding preorder_on_def
[PROOF STATE]
proof (prove)
using this:
refl TRel \<and> trans TRel
TargetTerm TP \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm TQ
?P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> ?Q \<Longrightarrow> \<forall>TP TQ. TP \<in>T ?P \<and> TQ \<in>T ?Q \<longrightarrow> (TP, TQ) \<in> TRel\<^sup>+
trans TRel \<Longrightarrow> TRel\<^sup>+ = TRel

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
TRel = _Collect (T1, T2) (TargetTerm T1 \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm T2)

goal (2 subgoals):
 1. operational_complete TRel \<and> operational_sound TRel \<and> preorder TRel \<and> weak_reduction_bisimulation TRel Target \<Longrightarrow> \<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel) \<and> TRel = _Collect (T1, T2) ((TargetTerm T1, TargetTerm T2) \<in> Rel) \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel) \<and> preorder Rel \<and> weak_reduction_bisimulation Rel (STCal Source Target)
 2. \<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel) \<and> TRel = _Collect (T1, T2) ((TargetTerm T1, TargetTerm T2) \<in> Rel) \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel) \<and> preorder Rel \<and> weak_reduction_bisimulation Rel (STCal Source Target) \<Longrightarrow> operational_corresponding TRel \<and> preorder TRel \<and> weak_reduction_bisimulation TRel Target
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
TRel = _Collect (T1, T2) (TargetTerm T1 \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm T2)

goal (2 subgoals):
 1. operational_complete TRel \<and> operational_sound TRel \<and> preorder TRel \<and> weak_reduction_bisimulation TRel Target \<Longrightarrow> \<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel) \<and> TRel = _Collect (T1, T2) ((TargetTerm T1, TargetTerm T2) \<in> Rel) \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel) \<and> preorder Rel \<and> weak_reduction_bisimulation Rel (STCal Source Target)
 2. \<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel) \<and> TRel = _Collect (T1, T2) ((TargetTerm T1, TargetTerm T2) \<in> Rel) \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel) \<and> preorder Rel \<and> weak_reduction_bisimulation Rel (STCal Source Target) \<Longrightarrow> operational_corresponding TRel \<and> preorder TRel \<and> weak_reduction_bisimulation TRel Target
[PROOF STEP]
from A3
[PROOF STATE]
proof (chain)
picking this:
preorder TRel
[PROOF STEP]
have "\<forall>S T. SourceTerm S \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm T \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel\<^sup>+"
[PROOF STATE]
proof (prove)
using this:
preorder TRel

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

goal (1 subgoal):
 1. \<forall>S T. SourceTerm S \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm T \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel\<^sup>+
[PROOF STEP]
unfolding preorder_on_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> trans TRel
?P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> ?Q \<Longrightarrow> \<forall>SP TQ. SP \<in>S ?P \<and> TQ \<in>T ?Q \<longrightarrow> (\<lbrakk>SP\<rbrakk>, TQ) \<in> (TRel \<union> _Collect (T1, T2) (\<exists>S. T1 = \<lbrakk>S\<rbrakk> \<and> T2 = \<lbrakk>S\<rbrakk>))\<^sup>+
(TRel\<^sup>+)\<^sup>= = TRel\<^sup>*
(?TP, ?TQ) \<in> (TRel \<union> _Collect (T1, T2) (\<exists>S. T1 = \<lbrakk>S\<rbrakk> \<and> T2 = \<lbrakk>S\<rbrakk>))\<^sup>+ \<Longrightarrow> (?TP, ?TQ) \<in> TRel\<^sup>*

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

goal (2 subgoals):
 1. operational_complete TRel \<and> operational_sound TRel \<and> preorder TRel \<and> weak_reduction_bisimulation TRel Target \<Longrightarrow> \<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel) \<and> TRel = _Collect (T1, T2) ((TargetTerm T1, TargetTerm T2) \<in> Rel) \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel) \<and> preorder Rel \<and> weak_reduction_bisimulation Rel (STCal Source Target)
 2. \<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel) \<and> TRel = _Collect (T1, T2) ((TargetTerm T1, TargetTerm T2) \<in> Rel) \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel) \<and> preorder Rel \<and> weak_reduction_bisimulation Rel (STCal Source Target) \<Longrightarrow> operational_corresponding TRel \<and> preorder TRel \<and> weak_reduction_bisimulation TRel Target
[PROOF STEP]
with A3
[PROOF STATE]
proof (chain)
picking this:
preorder TRel
\<forall>S T. SourceTerm S \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm T \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel\<^sup>+
[PROOF STEP]
have "\<forall>S T. SourceTerm S \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm T \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel"
[PROOF STATE]
proof (prove)
using this:
preorder TRel
\<forall>S T. SourceTerm S \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm T \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel\<^sup>+

goal (1 subgoal):
 1. \<forall>S T. SourceTerm S \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm T \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel
[PROOF STEP]
using trancl_id[of TRel]
[PROOF STATE]
proof (prove)
using this:
preorder TRel
\<forall>S T. SourceTerm S \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm T \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel\<^sup>+
trans TRel \<Longrightarrow> TRel\<^sup>+ = TRel

goal (1 subgoal):
 1. \<forall>S T. SourceTerm S \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm T \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel
[PROOF STEP]
unfolding preorder_on_def
[PROOF STATE]
proof (prove)
using this:
refl TRel \<and> trans TRel
\<forall>S T. SourceTerm S \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm T \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel\<^sup>+
trans TRel \<Longrightarrow> TRel\<^sup>+ = TRel

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

goal (2 subgoals):
 1. operational_complete TRel \<and> operational_sound TRel \<and> preorder TRel \<and> weak_reduction_bisimulation TRel Target \<Longrightarrow> \<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel) \<and> TRel = _Collect (T1, T2) ((TargetTerm T1, TargetTerm T2) \<in> Rel) \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel) \<and> preorder Rel \<and> weak_reduction_bisimulation Rel (STCal Source Target)
 2. \<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel) \<and> TRel = _Collect (T1, T2) ((TargetTerm T1, TargetTerm T2) \<in> Rel) \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel) \<and> preorder Rel \<and> weak_reduction_bisimulation Rel (STCal Source Target) \<Longrightarrow> operational_corresponding TRel \<and> preorder TRel \<and> weak_reduction_bisimulation TRel Target
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>S T. SourceTerm S \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm T \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel

goal (2 subgoals):
 1. operational_complete TRel \<and> operational_sound TRel \<and> preorder TRel \<and> weak_reduction_bisimulation TRel Target \<Longrightarrow> \<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel) \<and> TRel = _Collect (T1, T2) ((TargetTerm T1, TargetTerm T2) \<in> Rel) \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel) \<and> preorder Rel \<and> weak_reduction_bisimulation Rel (STCal Source Target)
 2. \<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel) \<and> TRel = _Collect (T1, T2) ((TargetTerm T1, TargetTerm T2) \<in> Rel) \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel) \<and> preorder Rel \<and> weak_reduction_bisimulation Rel (STCal Source Target) \<Longrightarrow> operational_corresponding TRel \<and> preorder TRel \<and> weak_reduction_bisimulation TRel Target
[PROOF STEP]
from A3
[PROOF STATE]
proof (chain)
picking this:
preorder TRel
[PROOF STEP]
have "refl (indRelRTPO TRel)"
[PROOF STATE]
proof (prove)
using this:
preorder TRel

goal (1 subgoal):
 1. refl (indRelRTPO TRel)
[PROOF STEP]
unfolding preorder_on_def
[PROOF STATE]
proof (prove)
using this:
refl TRel \<and> trans TRel

goal (1 subgoal):
 1. refl (indRelRTPO TRel)
[PROOF STEP]
by (simp add: indRelRTPO_refl)
[PROOF STATE]
proof (state)
this:
refl (indRelRTPO TRel)

goal (2 subgoals):
 1. operational_complete TRel \<and> operational_sound TRel \<and> preorder TRel \<and> weak_reduction_bisimulation TRel Target \<Longrightarrow> \<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel) \<and> TRel = _Collect (T1, T2) ((TargetTerm T1, TargetTerm T2) \<in> Rel) \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel) \<and> preorder Rel \<and> weak_reduction_bisimulation Rel (STCal Source Target)
 2. \<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel) \<and> TRel = _Collect (T1, T2) ((TargetTerm T1, TargetTerm T2) \<in> Rel) \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel) \<and> preorder Rel \<and> weak_reduction_bisimulation Rel (STCal Source Target) \<Longrightarrow> operational_corresponding TRel \<and> preorder TRel \<and> weak_reduction_bisimulation TRel Target
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
refl (indRelRTPO TRel)

goal (2 subgoals):
 1. operational_complete TRel \<and> operational_sound TRel \<and> preorder TRel \<and> weak_reduction_bisimulation TRel Target \<Longrightarrow> \<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel) \<and> TRel = _Collect (T1, T2) ((TargetTerm T1, TargetTerm T2) \<in> Rel) \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel) \<and> preorder Rel \<and> weak_reduction_bisimulation Rel (STCal Source Target)
 2. \<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel) \<and> TRel = _Collect (T1, T2) ((TargetTerm T1, TargetTerm T2) \<in> Rel) \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel) \<and> preorder Rel \<and> weak_reduction_bisimulation Rel (STCal Source Target) \<Longrightarrow> operational_corresponding TRel \<and> preorder TRel \<and> weak_reduction_bisimulation TRel Target
[PROOF STEP]
have "trans (indRelRTPO TRel)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trans (indRelRTPO TRel)
[PROOF STEP]
using indRelRTPO.trans
[PROOF STATE]
proof (prove)
using this:
?P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<?TRel> ?Q \<and> ?Q \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<?TRel> ?R \<Longrightarrow> ?P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<?TRel> ?R

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

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

goal (2 subgoals):
 1. operational_complete TRel \<and> operational_sound TRel \<and> preorder TRel \<and> weak_reduction_bisimulation TRel Target \<Longrightarrow> \<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel) \<and> TRel = _Collect (T1, T2) ((TargetTerm T1, TargetTerm T2) \<in> Rel) \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel) \<and> preorder Rel \<and> weak_reduction_bisimulation Rel (STCal Source Target)
 2. \<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel) \<and> TRel = _Collect (T1, T2) ((TargetTerm T1, TargetTerm T2) \<in> Rel) \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel) \<and> preorder Rel \<and> weak_reduction_bisimulation Rel (STCal Source Target) \<Longrightarrow> operational_corresponding TRel \<and> preorder TRel \<and> weak_reduction_bisimulation TRel Target
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
weak_reduction_bisimulation (indRelRTPO TRel) (STCal Source Target)
\<forall>S. SourceTerm S \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm (\<lbrakk>S\<rbrakk>)
TRel = _Collect (T1, T2) (TargetTerm T1 \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm T2)
\<forall>S T. SourceTerm S \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm T \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel
refl (indRelRTPO TRel)
trans (indRelRTPO TRel)
[PROOF STEP]
show "\<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel)
                   \<and> TRel = {(T1, T2). (TargetTerm T1, TargetTerm T2) \<in> Rel}
                   \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel)
                   \<and> preorder Rel
                   \<and> weak_reduction_bisimulation Rel (STCal Source Target)"
[PROOF STATE]
proof (prove)
using this:
weak_reduction_bisimulation (indRelRTPO TRel) (STCal Source Target)
\<forall>S. SourceTerm S \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm (\<lbrakk>S\<rbrakk>)
TRel = _Collect (T1, T2) (TargetTerm T1 \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm T2)
\<forall>S T. SourceTerm S \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm T \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel
refl (indRelRTPO TRel)
trans (indRelRTPO TRel)

goal (1 subgoal):
 1. \<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel) \<and> TRel = _Collect (T1, T2) ((TargetTerm T1, TargetTerm T2) \<in> Rel) \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel) \<and> preorder Rel \<and> weak_reduction_bisimulation Rel (STCal Source Target)
[PROOF STEP]
unfolding preorder_on_def
[PROOF STATE]
proof (prove)
using this:
weak_reduction_bisimulation (indRelRTPO TRel) (STCal Source Target)
\<forall>S. SourceTerm S \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm (\<lbrakk>S\<rbrakk>)
TRel = _Collect (T1, T2) (TargetTerm T1 \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm T2)
\<forall>S T. SourceTerm S \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm T \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel
refl (indRelRTPO TRel)
trans (indRelRTPO TRel)

goal (1 subgoal):
 1. \<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel) \<and> TRel = _Collect (T1, T2) ((TargetTerm T1, TargetTerm T2) \<in> Rel) \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel) \<and> (refl 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> TRel = _Collect (T1, T2) ((TargetTerm T1, TargetTerm T2) \<in> Rel) \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel) \<and> preorder 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> TRel = _Collect (T1, T2) ((TargetTerm T1, TargetTerm T2) \<in> Rel) \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel) \<and> preorder Rel \<and> weak_reduction_bisimulation Rel (STCal Source Target) \<Longrightarrow> operational_corresponding TRel \<and> preorder 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> TRel = _Collect (T1, T2) ((TargetTerm T1, TargetTerm T2) \<in> Rel) \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel) \<and> preorder Rel \<and> weak_reduction_bisimulation Rel (STCal Source Target) \<Longrightarrow> operational_corresponding TRel \<and> preorder TRel \<and> weak_reduction_bisimulation TRel Target
[PROOF STEP]
assume "\<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel)
          \<and> TRel = {(T1, T2). (TargetTerm T1, TargetTerm T2) \<in> Rel}
          \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel)
          \<and> preorder 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> TRel = _Collect (T1, T2) ((TargetTerm T1, TargetTerm T2) \<in> Rel) \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel) \<and> preorder 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> TRel = _Collect (T1, T2) ((TargetTerm T1, TargetTerm T2) \<in> Rel) \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel) \<and> preorder Rel \<and> weak_reduction_bisimulation Rel (STCal Source Target) \<Longrightarrow> operational_corresponding TRel \<and> preorder 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> TRel = _Collect (T1, T2) ((TargetTerm T1, TargetTerm T2) \<in> Rel) \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel) \<and> preorder Rel \<and> weak_reduction_bisimulation Rel (STCal Source Target)
[PROOF STEP]
obtain Rel where B1: "\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel"
   and B2: "TRel = {(T1, T2). (TargetTerm T1, TargetTerm T2) \<in> Rel}"
   and B3: "\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel" and B4: "preorder Rel"
   and B5: "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> TRel = _Collect (T1, T2) ((TargetTerm T1, TargetTerm T2) \<in> Rel) \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel) \<and> preorder 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> TRel = _Collect (T1, T2) ((TargetTerm T1, TargetTerm T2) \<in> Rel) \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel) \<and> preorder 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
TRel = _Collect (T1, T2) ((TargetTerm T1, TargetTerm T2) \<in> Rel)
\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel
preorder 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> TRel = _Collect (T1, T2) ((TargetTerm T1, TargetTerm T2) \<in> Rel) \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel) \<and> preorder Rel \<and> weak_reduction_bisimulation Rel (STCal Source Target) \<Longrightarrow> operational_corresponding TRel \<and> preorder TRel \<and> weak_reduction_bisimulation TRel Target
[PROOF STEP]
from B2 B4
[PROOF STATE]
proof (chain)
picking this:
TRel = _Collect (T1, T2) ((TargetTerm T1, TargetTerm T2) \<in> Rel)
preorder Rel
[PROOF STEP]
have B6: "refl TRel"
[PROOF STATE]
proof (prove)
using this:
TRel = _Collect (T1, T2) ((TargetTerm T1, TargetTerm T2) \<in> Rel)
preorder Rel

goal (1 subgoal):
 1. refl TRel
[PROOF STEP]
unfolding preorder_on_def refl_on_def
[PROOF STATE]
proof (prove)
using this:
TRel = _Collect (T1, T2) ((TargetTerm T1, TargetTerm T2) \<in> Rel)
(Rel \<subseteq> UNIV \<times> UNIV \<and> (\<forall>x\<in>UNIV. (x, x) \<in> Rel)) \<and> trans Rel

goal (1 subgoal):
 1. TRel \<subseteq> UNIV \<times> UNIV \<and> (\<forall>x\<in>UNIV. (x, x) \<in> TRel)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
refl TRel

goal (1 subgoal):
 1. \<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel) \<and> TRel = _Collect (T1, T2) ((TargetTerm T1, TargetTerm T2) \<in> Rel) \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel) \<and> preorder Rel \<and> weak_reduction_bisimulation Rel (STCal Source Target) \<Longrightarrow> operational_corresponding TRel \<and> preorder TRel \<and> weak_reduction_bisimulation TRel Target
[PROOF STEP]
from B2 B4
[PROOF STATE]
proof (chain)
picking this:
TRel = _Collect (T1, T2) ((TargetTerm T1, TargetTerm T2) \<in> Rel)
preorder Rel
[PROOF STEP]
have B7: "trans TRel"
[PROOF STATE]
proof (prove)
using this:
TRel = _Collect (T1, T2) ((TargetTerm T1, TargetTerm T2) \<in> Rel)
preorder Rel

goal (1 subgoal):
 1. trans TRel
[PROOF STEP]
unfolding trans_def preorder_on_def
[PROOF STATE]
proof (prove)
using this:
TRel = _Collect (T1, T2) ((TargetTerm T1, TargetTerm T2) \<in> Rel)
refl Rel \<and> (\<forall>x y z. (x, y) \<in> Rel \<longrightarrow> (y, z) \<in> Rel \<longrightarrow> (x, z) \<in> Rel)

goal (1 subgoal):
 1. \<forall>x y z. (x, y) \<in> TRel \<longrightarrow> (y, z) \<in> TRel \<longrightarrow> (x, z) \<in> TRel
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
trans TRel

goal (1 subgoal):
 1. \<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel) \<and> TRel = _Collect (T1, T2) ((TargetTerm T1, TargetTerm T2) \<in> Rel) \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel) \<and> preorder Rel \<and> weak_reduction_bisimulation Rel (STCal Source Target) \<Longrightarrow> operational_corresponding TRel \<and> preorder TRel \<and> weak_reduction_bisimulation TRel Target
[PROOF STEP]
hence B8: "TRel\<^sup>+ = TRel"
[PROOF STATE]
proof (prove)
using this:
trans TRel

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

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

goal (1 subgoal):
 1. \<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel) \<and> TRel = _Collect (T1, T2) ((TargetTerm T1, TargetTerm T2) \<in> Rel) \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel) \<and> preorder Rel \<and> weak_reduction_bisimulation Rel (STCal Source Target) \<Longrightarrow> operational_corresponding TRel \<and> preorder TRel \<and> weak_reduction_bisimulation TRel Target
[PROOF STEP]
with B6
[PROOF STATE]
proof (chain)
picking this:
refl TRel
TRel\<^sup>+ = TRel
[PROOF STEP]
have B9: "TRel\<^sup>* = TRel"
[PROOF STATE]
proof (prove)
using this:
refl TRel
TRel\<^sup>+ = TRel

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

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

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

goal (1 subgoal):
 1. \<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel) \<and> TRel = _Collect (T1, T2) ((TargetTerm T1, TargetTerm T2) \<in> Rel) \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel) \<and> preorder Rel \<and> weak_reduction_bisimulation Rel (STCal Source Target) \<Longrightarrow> operational_corresponding TRel \<and> preorder TRel \<and> weak_reduction_bisimulation TRel Target
[PROOF STEP]
with B3
[PROOF STATE]
proof (chain)
picking this:
\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel
TRel\<^sup>* = TRel
[PROOF STEP]
have "\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel\<^sup>*"
[PROOF STATE]
proof (prove)
using this:
\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel
TRel\<^sup>* = TRel

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

goal (1 subgoal):
 1. \<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel) \<and> TRel = _Collect (T1, T2) ((TargetTerm T1, TargetTerm T2) \<in> Rel) \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel) \<and> preorder Rel \<and> weak_reduction_bisimulation Rel (STCal Source Target) \<Longrightarrow> operational_corresponding TRel \<and> preorder TRel \<and> weak_reduction_bisimulation TRel Target
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel\<^sup>*

goal (1 subgoal):
 1. \<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel) \<and> TRel = _Collect (T1, T2) ((TargetTerm T1, TargetTerm T2) \<in> Rel) \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel) \<and> preorder Rel \<and> weak_reduction_bisimulation Rel (STCal Source Target) \<Longrightarrow> operational_corresponding TRel \<and> preorder TRel \<and> weak_reduction_bisimulation TRel Target
[PROOF STEP]
from B2 B8
[PROOF STATE]
proof (chain)
picking this:
TRel = _Collect (T1, T2) ((TargetTerm T1, TargetTerm T2) \<in> Rel)
TRel\<^sup>+ = TRel
[PROOF STEP]
have "\<forall>T1 T2. (T1, T2) \<in> TRel \<longrightarrow> (TargetTerm T1, TargetTerm T2) \<in> Rel"
   and "\<forall>T1 T2. (TargetTerm T1, TargetTerm T2) \<in> Rel \<longrightarrow> (T1, T2) \<in> TRel\<^sup>+"
[PROOF STATE]
proof (prove)
using this:
TRel = _Collect (T1, T2) ((TargetTerm T1, TargetTerm T2) \<in> Rel)
TRel\<^sup>+ = TRel

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

goal (1 subgoal):
 1. \<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel) \<and> TRel = _Collect (T1, T2) ((TargetTerm T1, TargetTerm T2) \<in> Rel) \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel) \<and> preorder Rel \<and> weak_reduction_bisimulation Rel (STCal Source Target) \<Longrightarrow> operational_corresponding TRel \<and> preorder TRel \<and> weak_reduction_bisimulation TRel Target
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel\<^sup>*
\<forall>T1 T2. (T1, T2) \<in> TRel \<longrightarrow> (TargetTerm T1, TargetTerm T2) \<in> Rel
\<forall>T1 T2. (TargetTerm T1, TargetTerm T2) \<in> Rel \<longrightarrow> (T1, T2) \<in> TRel\<^sup>+
[PROOF STEP]
have "\<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel)
   \<and> (\<forall>T1 T2. (T1, T2) \<in> TRel \<longrightarrow> (TargetTerm T1, TargetTerm T2) \<in> Rel)
   \<and> (\<forall>T1 T2. (TargetTerm T1, TargetTerm T2) \<in> Rel \<longrightarrow> (T1, T2) \<in> TRel\<^sup>+)
   \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel\<^sup>*)
   \<and> weak_reduction_bisimulation Rel (STCal Source Target)"
[PROOF STATE]
proof (prove)
using this:
\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel\<^sup>*
\<forall>T1 T2. (T1, T2) \<in> TRel \<longrightarrow> (TargetTerm T1, TargetTerm T2) \<in> Rel
\<forall>T1 T2. (TargetTerm T1, TargetTerm T2) \<in> Rel \<longrightarrow> (T1, T2) \<in> TRel\<^sup>+

goal (1 subgoal):
 1. \<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel) \<and> (\<forall>T1 T2. (T1, T2) \<in> TRel \<longrightarrow> (TargetTerm T1, TargetTerm T2) \<in> Rel) \<and> (\<forall>T1 T2. (TargetTerm T1, TargetTerm T2) \<in> Rel \<longrightarrow> (T1, T2) \<in> TRel\<^sup>+) \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel\<^sup>*) \<and> weak_reduction_bisimulation Rel (STCal Source Target)
[PROOF STEP]
using B1 B5
[PROOF STATE]
proof (prove)
using this:
\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel\<^sup>*
\<forall>T1 T2. (T1, T2) \<in> TRel \<longrightarrow> (TargetTerm T1, TargetTerm T2) \<in> Rel
\<forall>T1 T2. (TargetTerm T1, TargetTerm T2) \<in> Rel \<longrightarrow> (T1, T2) \<in> TRel\<^sup>+
\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> 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> (\<forall>T1 T2. (T1, T2) \<in> TRel \<longrightarrow> (TargetTerm T1, TargetTerm T2) \<in> Rel) \<and> (\<forall>T1 T2. (TargetTerm T1, TargetTerm T2) \<in> Rel \<longrightarrow> (T1, T2) \<in> TRel\<^sup>+) \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel\<^sup>*) \<and> 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> (\<forall>T1 T2. (T1, T2) \<in> TRel \<longrightarrow> (TargetTerm T1, TargetTerm T2) \<in> Rel) \<and> (\<forall>T1 T2. (TargetTerm T1, TargetTerm T2) \<in> Rel \<longrightarrow> (T1, T2) \<in> TRel\<^sup>+) \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel\<^sup>*) \<and> weak_reduction_bisimulation Rel (STCal Source Target)

goal (1 subgoal):
 1. \<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel) \<and> TRel = _Collect (T1, T2) ((TargetTerm T1, TargetTerm T2) \<in> Rel) \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel) \<and> preorder Rel \<and> weak_reduction_bisimulation Rel (STCal Source Target) \<Longrightarrow> operational_corresponding TRel \<and> preorder TRel \<and> weak_reduction_bisimulation TRel Target
[PROOF STEP]
hence "operational_corresponding (TRel\<^sup>*)
         \<and> weak_reduction_bisimulation (TRel\<^sup>+) Target"
[PROOF STATE]
proof (prove)
using this:
\<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel) \<and> (\<forall>T1 T2. (T1, T2) \<in> TRel \<longrightarrow> (TargetTerm T1, TargetTerm T2) \<in> Rel) \<and> (\<forall>T1 T2. (TargetTerm T1, TargetTerm T2) \<in> Rel \<longrightarrow> (T1, T2) \<in> TRel\<^sup>+) \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel\<^sup>*) \<and> weak_reduction_bisimulation Rel (STCal Source Target)

goal (1 subgoal):
 1. operational_corresponding (TRel\<^sup>*) \<and> weak_reduction_bisimulation (TRel\<^sup>+) Target
[PROOF STEP]
using OC_iff_weak_reduction_bisimulation[where TRel="TRel"]
[PROOF STATE]
proof (prove)
using this:
\<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel) \<and> (\<forall>T1 T2. (T1, T2) \<in> TRel \<longrightarrow> (TargetTerm T1, TargetTerm T2) \<in> Rel) \<and> (\<forall>T1 T2. (TargetTerm T1, TargetTerm T2) \<in> Rel \<longrightarrow> (T1, T2) \<in> TRel\<^sup>+) \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel\<^sup>*) \<and> weak_reduction_bisimulation Rel (STCal Source Target)
(operational_corresponding (TRel\<^sup>*) \<and> weak_reduction_bisimulation (TRel\<^sup>+) Target) = (\<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel) \<and> (\<forall>T1 T2. (T1, T2) \<in> TRel \<longrightarrow> (TargetTerm T1, TargetTerm T2) \<in> Rel) \<and> (\<forall>T1 T2. (TargetTerm T1, TargetTerm T2) \<in> Rel \<longrightarrow> (T1, T2) \<in> TRel\<^sup>+) \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel\<^sup>*) \<and> weak_reduction_bisimulation Rel (STCal Source Target))

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

goal (1 subgoal):
 1. \<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel) \<and> TRel = _Collect (T1, T2) ((TargetTerm T1, TargetTerm T2) \<in> Rel) \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel) \<and> preorder Rel \<and> weak_reduction_bisimulation Rel (STCal Source Target) \<Longrightarrow> operational_corresponding TRel \<and> preorder TRel \<and> weak_reduction_bisimulation TRel Target
[PROOF STEP]
with B8 B9
[PROOF STATE]
proof (chain)
picking this:
TRel\<^sup>+ = TRel
TRel\<^sup>* = TRel
operational_corresponding (TRel\<^sup>*) \<and> weak_reduction_bisimulation (TRel\<^sup>+) Target
[PROOF STEP]
have "operational_corresponding TRel \<and> weak_reduction_bisimulation TRel Target"
[PROOF STATE]
proof (prove)
using this:
TRel\<^sup>+ = TRel
TRel\<^sup>* = TRel
operational_corresponding (TRel\<^sup>*) \<and> weak_reduction_bisimulation (TRel\<^sup>+) 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 (1 subgoal):
 1. \<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel) \<and> TRel = _Collect (T1, T2) ((TargetTerm T1, TargetTerm T2) \<in> Rel) \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel) \<and> preorder Rel \<and> weak_reduction_bisimulation Rel (STCal Source Target) \<Longrightarrow> operational_corresponding TRel \<and> preorder TRel \<and> weak_reduction_bisimulation TRel Target
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
operational_corresponding TRel \<and> weak_reduction_bisimulation TRel Target

goal (1 subgoal):
 1. \<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel) \<and> TRel = _Collect (T1, T2) ((TargetTerm T1, TargetTerm T2) \<in> Rel) \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel) \<and> preorder Rel \<and> weak_reduction_bisimulation Rel (STCal Source Target) \<Longrightarrow> operational_corresponding TRel \<and> preorder TRel \<and> weak_reduction_bisimulation TRel Target
[PROOF STEP]
from B6 B7
[PROOF STATE]
proof (chain)
picking this:
refl TRel
trans TRel
[PROOF STEP]
have "preorder TRel"
[PROOF STATE]
proof (prove)
using this:
refl TRel
trans TRel

goal (1 subgoal):
 1. preorder TRel
[PROOF STEP]
unfolding preorder_on_def
[PROOF STATE]
proof (prove)
using this:
refl TRel
trans TRel

goal (1 subgoal):
 1. refl TRel \<and> trans TRel
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
preorder TRel

goal (1 subgoal):
 1. \<exists>Rel. (\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel) \<and> TRel = _Collect (T1, T2) ((TargetTerm T1, TargetTerm T2) \<in> Rel) \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel) \<and> preorder Rel \<and> weak_reduction_bisimulation Rel (STCal Source Target) \<Longrightarrow> operational_corresponding TRel \<and> preorder TRel \<and> weak_reduction_bisimulation TRel Target
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
operational_corresponding TRel \<and> weak_reduction_bisimulation TRel Target
preorder TRel
[PROOF STEP]
show "operational_corresponding TRel \<and> preorder TRel
                   \<and> weak_reduction_bisimulation TRel Target"
[PROOF STATE]
proof (prove)
using this:
operational_corresponding TRel \<and> weak_reduction_bisimulation TRel Target
preorder TRel

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

goal:
No subgoals!
[PROOF STEP]
qed