[STATEMENT]
lemma (in encoding) OCom_iff_weak_reduction_simulation:
  fixes TRel :: "('procT \<times> 'procT) set"
  shows "(operational_complete (TRel\<^sup>*)
         \<and> weak_reduction_simulation (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_simulation Rel (STCal Source Target))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (operational_complete (TRel\<^sup>*) \<and> weak_reduction_simulation (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_simulation Rel (STCal Source Target))
[PROOF STEP]
proof (rule iffI, erule conjE)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. operational_complete (TRel\<^sup>*) \<and> weak_reduction_simulation (TRel\<^sup>+) Target \<Longrightarrow> \<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_simulation Rel (STCal Source Target)
 2. \<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_simulation Rel (STCal Source Target) \<Longrightarrow> operational_complete (TRel\<^sup>*) \<and> weak_reduction_simulation (TRel\<^sup>+) Target
[PROOF STEP]
have "\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> indRelRTPO TRel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>S. SourceTerm S \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm (\<lbrakk>S\<rbrakk>)
[PROOF STEP]
by (simp add: indRelRTPO.encR)
[PROOF STATE]
proof (state)
this:
\<forall>S. SourceTerm S \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm (\<lbrakk>S\<rbrakk>)

goal (2 subgoals):
 1. operational_complete (TRel\<^sup>*) \<and> weak_reduction_simulation (TRel\<^sup>+) Target \<Longrightarrow> \<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_simulation Rel (STCal Source Target)
 2. \<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_simulation Rel (STCal Source Target) \<Longrightarrow> operational_complete (TRel\<^sup>*) \<and> weak_reduction_simulation (TRel\<^sup>+) 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\<^sup>*) \<and> weak_reduction_simulation (TRel\<^sup>+) Target \<Longrightarrow> \<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_simulation Rel (STCal Source Target)
 2. \<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_simulation Rel (STCal Source Target) \<Longrightarrow> operational_complete (TRel\<^sup>*) \<and> weak_reduction_simulation (TRel\<^sup>+) Target
[PROOF STEP]
have "\<forall>T1 T2. (T1, T2) \<in> TRel \<longrightarrow> TargetTerm T1 \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm T2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>T1 T2. (T1, T2) \<in> TRel \<longrightarrow> TargetTerm T1 \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm T2
[PROOF STEP]
by (simp add: indRelRTPO.target)
[PROOF STATE]
proof (state)
this:
\<forall>T1 T2. (T1, T2) \<in> TRel \<longrightarrow> TargetTerm T1 \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm T2

goal (2 subgoals):
 1. operational_complete (TRel\<^sup>*) \<and> weak_reduction_simulation (TRel\<^sup>+) Target \<Longrightarrow> \<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_simulation Rel (STCal Source Target)
 2. \<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_simulation Rel (STCal Source Target) \<Longrightarrow> operational_complete (TRel\<^sup>*) \<and> weak_reduction_simulation (TRel\<^sup>+) Target
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>T1 T2. (T1, T2) \<in> TRel \<longrightarrow> TargetTerm T1 \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm T2

goal (2 subgoals):
 1. operational_complete (TRel\<^sup>*) \<and> weak_reduction_simulation (TRel\<^sup>+) Target \<Longrightarrow> \<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_simulation Rel (STCal Source Target)
 2. \<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_simulation Rel (STCal Source Target) \<Longrightarrow> operational_complete (TRel\<^sup>*) \<and> weak_reduction_simulation (TRel\<^sup>+) Target
[PROOF STEP]
have "\<forall>T1 T2. TargetTerm T1 \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm T2 \<longrightarrow> (T1, T2) \<in> TRel\<^sup>+"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>T1 T2. TargetTerm T1 \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm T2 \<longrightarrow> (T1, T2) \<in> TRel\<^sup>+
[PROOF STEP]
using indRelRTPO_to_TRel(4)[where TRel="TRel"]
[PROOF STATE]
proof (prove)
using this:
?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>+

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

goal (2 subgoals):
 1. operational_complete (TRel\<^sup>*) \<and> weak_reduction_simulation (TRel\<^sup>+) Target \<Longrightarrow> \<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_simulation Rel (STCal Source Target)
 2. \<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_simulation Rel (STCal Source Target) \<Longrightarrow> operational_complete (TRel\<^sup>*) \<and> weak_reduction_simulation (TRel\<^sup>+) Target
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>T1 T2. TargetTerm T1 \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm T2 \<longrightarrow> (T1, T2) \<in> TRel\<^sup>+

goal (2 subgoals):
 1. operational_complete (TRel\<^sup>*) \<and> weak_reduction_simulation (TRel\<^sup>+) Target \<Longrightarrow> \<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_simulation Rel (STCal Source Target)
 2. \<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_simulation Rel (STCal Source Target) \<Longrightarrow> operational_complete (TRel\<^sup>*) \<and> weak_reduction_simulation (TRel\<^sup>+) Target
[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)
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"] trans_closure_of_TRel_refl_cond
[PROOF STATE]
proof (prove)
using this:
?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>+
(?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 simp
[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\<^sup>*) \<and> weak_reduction_simulation (TRel\<^sup>+) Target \<Longrightarrow> \<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_simulation Rel (STCal Source Target)
 2. \<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_simulation Rel (STCal Source Target) \<Longrightarrow> operational_complete (TRel\<^sup>*) \<and> weak_reduction_simulation (TRel\<^sup>+) 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\<^sup>*

goal (2 subgoals):
 1. operational_complete (TRel\<^sup>*) \<and> weak_reduction_simulation (TRel\<^sup>+) Target \<Longrightarrow> \<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_simulation Rel (STCal Source Target)
 2. \<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_simulation Rel (STCal Source Target) \<Longrightarrow> operational_complete (TRel\<^sup>*) \<and> weak_reduction_simulation (TRel\<^sup>+) Target
[PROOF STEP]
assume "operational_complete (TRel\<^sup>*)"
              and "weak_reduction_simulation (TRel\<^sup>+) Target"
[PROOF STATE]
proof (state)
this:
operational_complete (TRel\<^sup>*)
weak_reduction_simulation (TRel\<^sup>+) Target

goal (2 subgoals):
 1. operational_complete (TRel\<^sup>*) \<and> weak_reduction_simulation (TRel\<^sup>+) Target \<Longrightarrow> \<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_simulation Rel (STCal Source Target)
 2. \<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_simulation Rel (STCal Source Target) \<Longrightarrow> operational_complete (TRel\<^sup>*) \<and> weak_reduction_simulation (TRel\<^sup>+) Target
[PROOF STEP]
hence "weak_reduction_simulation (indRelRTPO TRel) (STCal Source Target)"
[PROOF STATE]
proof (prove)
using this:
operational_complete (TRel\<^sup>*)
weak_reduction_simulation (TRel\<^sup>+) Target

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

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

goal (2 subgoals):
 1. operational_complete (TRel\<^sup>*) \<and> weak_reduction_simulation (TRel\<^sup>+) Target \<Longrightarrow> \<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_simulation Rel (STCal Source Target)
 2. \<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_simulation Rel (STCal Source Target) \<Longrightarrow> operational_complete (TRel\<^sup>*) \<and> weak_reduction_simulation (TRel\<^sup>+) Target
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<forall>S. SourceTerm S \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm (\<lbrakk>S\<rbrakk>)
\<forall>T1 T2. (T1, T2) \<in> TRel \<longrightarrow> TargetTerm T1 \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm T2
\<forall>T1 T2. TargetTerm T1 \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm T2 \<longrightarrow> (T1, T2) \<in> TRel\<^sup>+
\<forall>S T. SourceTerm S \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm T \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel\<^sup>*
weak_reduction_simulation (indRelRTPO TRel) (STCal Source Target)
[PROOF STEP]
show "\<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_simulation Rel (STCal Source Target)"
[PROOF STATE]
proof (prove)
using this:
\<forall>S. SourceTerm S \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm (\<lbrakk>S\<rbrakk>)
\<forall>T1 T2. (T1, T2) \<in> TRel \<longrightarrow> TargetTerm T1 \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm T2
\<forall>T1 T2. TargetTerm T1 \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm T2 \<longrightarrow> (T1, T2) \<in> TRel\<^sup>+
\<forall>S T. SourceTerm S \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm T \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel\<^sup>*
weak_reduction_simulation (indRelRTPO TRel) (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_simulation 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_simulation 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_simulation Rel (STCal Source Target) \<Longrightarrow> operational_complete (TRel\<^sup>*) \<and> weak_reduction_simulation (TRel\<^sup>+) 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> (\<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_simulation Rel (STCal Source Target) \<Longrightarrow> operational_complete (TRel\<^sup>*) \<and> weak_reduction_simulation (TRel\<^sup>+) Target
[PROOF STEP]
assume "\<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_simulation Rel (STCal Source Target)"
[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_simulation 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_simulation Rel (STCal Source Target) \<Longrightarrow> operational_complete (TRel\<^sup>*) \<and> weak_reduction_simulation (TRel\<^sup>+) Target
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking 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_simulation Rel (STCal Source Target)
[PROOF STEP]
obtain Rel where A1: "\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel"
    and A2: "\<forall>T1 T2. (T1, T2) \<in> TRel \<longrightarrow> (TargetTerm T1, TargetTerm T2) \<in> Rel"
    and A3: "\<forall>T1 T2. (TargetTerm T1, TargetTerm T2) \<in> Rel \<longrightarrow> (T1, T2) \<in> TRel\<^sup>+"
    and A4: "\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel\<^sup>*"
    and A5: "weak_reduction_simulation Rel (STCal Source 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_simulation Rel (STCal Source Target)

goal (1 subgoal):
 1. (\<And>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_simulation 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
\<forall>T1 T2. (T1, T2) \<in> TRel \<longrightarrow> (TargetTerm T1, TargetTerm T2) \<in> Rel
\<forall>T1 T2. (TargetTerm T1, TargetTerm T2) \<in> Rel \<longrightarrow> (T1, T2) \<in> TRel\<^sup>+
\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel\<^sup>*
weak_reduction_simulation 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_simulation Rel (STCal Source Target) \<Longrightarrow> operational_complete (TRel\<^sup>*) \<and> weak_reduction_simulation (TRel\<^sup>+) Target
[PROOF STEP]
from A1 A4 A5
[PROOF STATE]
proof (chain)
picking this:
\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel
\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel\<^sup>*
weak_reduction_simulation Rel (STCal Source Target)
[PROOF STEP]
have "operational_complete (TRel\<^sup>*)"
[PROOF STATE]
proof (prove)
using this:
\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel
\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel\<^sup>*
weak_reduction_simulation Rel (STCal Source Target)

goal (1 subgoal):
 1. operational_complete (TRel\<^sup>*)
[PROOF STEP]
using weak_reduction_simulation_impl_OCom[where Rel="Rel" and TRel="TRel"]
[PROOF STATE]
proof (prove)
using this:
\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel
\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel\<^sup>*
weak_reduction_simulation Rel (STCal Source Target)
(\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel) \<and> (\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel\<^sup>*) \<and> weak_reduction_simulation Rel (STCal Source Target) \<Longrightarrow> operational_complete (TRel\<^sup>*)

goal (1 subgoal):
 1. operational_complete (TRel\<^sup>*)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
operational_complete (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_simulation Rel (STCal Source Target) \<Longrightarrow> operational_complete (TRel\<^sup>*) \<and> weak_reduction_simulation (TRel\<^sup>+) Target
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
operational_complete (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_simulation Rel (STCal Source Target) \<Longrightarrow> operational_complete (TRel\<^sup>*) \<and> weak_reduction_simulation (TRel\<^sup>+) Target
[PROOF STEP]
from A2 A3 A5
[PROOF STATE]
proof (chain)
picking 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>+
weak_reduction_simulation Rel (STCal Source Target)
[PROOF STEP]
have "weak_reduction_simulation (TRel\<^sup>+) Target"
[PROOF STATE]
proof (prove)
using 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>+
weak_reduction_simulation Rel (STCal Source Target)

goal (1 subgoal):
 1. weak_reduction_simulation (TRel\<^sup>+) Target
[PROOF STEP]
using rel_with_target_impl_transC_TRel_is_weak_reduction_simulation[where Rel="Rel" and
             TRel="TRel"]
[PROOF STATE]
proof (prove)
using 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>+
weak_reduction_simulation Rel (STCal Source Target)
weak_reduction_simulation Rel (STCal Source Target) \<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>+) \<Longrightarrow> weak_reduction_simulation (TRel\<^sup>+) Target

goal (1 subgoal):
 1. weak_reduction_simulation (TRel\<^sup>+) Target
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
weak_reduction_simulation (TRel\<^sup>+) 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_simulation Rel (STCal Source Target) \<Longrightarrow> operational_complete (TRel\<^sup>*) \<and> weak_reduction_simulation (TRel\<^sup>+) Target
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
operational_complete (TRel\<^sup>*)
weak_reduction_simulation (TRel\<^sup>+) Target
[PROOF STEP]
show "operational_complete (TRel\<^sup>*)
                   \<and> weak_reduction_simulation (TRel\<^sup>+) Target"
[PROOF STATE]
proof (prove)
using this:
operational_complete (TRel\<^sup>*)
weak_reduction_simulation (TRel\<^sup>+) Target

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in encoding) strong_reduction_simulation_impl_SOCom:
  fixes Rel  :: "(('procS, 'procT) Proc \<times> ('procS, 'procT) Proc) set"
    and TRel :: "('procT \<times> 'procT) set"
  assumes A1: "\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel"
      and A2: "\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel\<^sup>*"
      and A3: "strong_reduction_simulation Rel (STCal Source Target)"
  shows "strongly_operational_complete (TRel\<^sup>*)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>S S'. S \<longmapsto>Source S' \<longrightarrow> (\<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*)
[PROOF STEP]
proof clarify
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>S S'. S \<longmapsto>Source S' \<Longrightarrow> \<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*
[PROOF STEP]
fix S S'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>S S'. S \<longmapsto>Source S' \<Longrightarrow> \<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*
[PROOF STEP]
from A1
[PROOF STATE]
proof (chain)
picking this:
\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<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

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 S'. S \<longmapsto>Source S' \<Longrightarrow> \<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel

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

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

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

goal (1 subgoal):
 1. \<And>S S'. S \<longmapsto>Source S' \<Longrightarrow> \<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*
[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 A5: "TargetTerm (\<lbrakk>S\<rbrakk>) \<longmapsto>(STCal Source Target) Q'"
                         and A6: "(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 A3
[PROOF STATE]
proof (prove)
using this:
(SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel
SourceTerm S \<longmapsto>STCal Source Target SourceTerm S'
strong_reduction_simulation Rel (STCal Source Target)

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 (1 subgoal):
 1. \<And>S S'. S \<longmapsto>Source S' \<Longrightarrow> \<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*
[PROOF STEP]
from A5
[PROOF STATE]
proof (chain)
picking this:
TargetTerm (\<lbrakk>S\<rbrakk>) \<longmapsto>STCal Source Target Q'
[PROOF STEP]
obtain T where A7: "T \<in>T Q'" and A8: "\<lbrakk>S\<rbrakk> \<longmapsto>Target T"
[PROOF STATE]
proof (prove)
using this:
TargetTerm (\<lbrakk>S\<rbrakk>) \<longmapsto>STCal Source Target Q'

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

goal (1 subgoal):
 1. \<And>S S'. S \<longmapsto>Source S' \<Longrightarrow> \<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*
[PROOF STEP]
from A2 A6 A7
[PROOF STATE]
proof (chain)
picking this:
\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel\<^sup>*
(SourceTerm S', Q') \<in> Rel
T \<in>T Q'
[PROOF STEP]
have "(\<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\<^sup>*
(SourceTerm S', Q') \<in> Rel
T \<in>T Q'

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed