[STATEMENT]
lemma (in encoding) OSou_iff_inverse_of_indRelRTPO_is_weak_reduction_simulation:
  fixes TRel :: "('procT \<times> 'procT) set"
  shows "(operational_sound (TRel\<^sup>*)
         \<and> weak_reduction_simulation ((TRel\<^sup>+)\<inverse>) Target)
         = weak_reduction_simulation ((indRelRTPO TRel)\<inverse>) (STCal Source Target)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (operational_sound (TRel\<^sup>*) \<and> weak_reduction_simulation ((TRel\<^sup>+)\<inverse>) Target) = weak_reduction_simulation ((indRelRTPO TRel)\<inverse>) (STCal Source Target)
[PROOF STEP]
proof (rule iffI, erule conjE)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. operational_sound (TRel\<^sup>*) \<and> weak_reduction_simulation ((TRel\<^sup>+)\<inverse>) Target \<Longrightarrow> weak_reduction_simulation ((indRelRTPO TRel)\<inverse>) (STCal Source Target)
 2. weak_reduction_simulation ((indRelRTPO TRel)\<inverse>) (STCal Source Target) \<Longrightarrow> operational_sound (TRel\<^sup>*) \<and> weak_reduction_simulation ((TRel\<^sup>+)\<inverse>) Target
[PROOF STEP]
assume os:  "operational_sound (TRel\<^sup>*)"
     and sim: "weak_reduction_simulation ((TRel\<^sup>+)\<inverse>) Target"
[PROOF STATE]
proof (state)
this:
operational_sound (TRel\<^sup>*)
weak_reduction_simulation ((TRel\<^sup>+)\<inverse>) Target

goal (2 subgoals):
 1. operational_sound (TRel\<^sup>*) \<and> weak_reduction_simulation ((TRel\<^sup>+)\<inverse>) Target \<Longrightarrow> weak_reduction_simulation ((indRelRTPO TRel)\<inverse>) (STCal Source Target)
 2. weak_reduction_simulation ((indRelRTPO TRel)\<inverse>) (STCal Source Target) \<Longrightarrow> operational_sound (TRel\<^sup>*) \<and> weak_reduction_simulation ((TRel\<^sup>+)\<inverse>) Target
[PROOF STEP]
show "weak_reduction_simulation ((indRelRTPO TRel)\<inverse>) (STCal Source Target)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. weak_reduction_simulation ((indRelRTPO TRel)\<inverse>) (STCal Source Target)
[PROOF STEP]
proof clarify
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>P Q P'. P \<longmapsto>STCal Source Target* P' \<and> Q \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> P \<Longrightarrow> \<exists>Q'. Q \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>
[PROOF STEP]
fix P Q P'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>P Q P'. P \<longmapsto>STCal Source Target* P' \<and> Q \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> P \<Longrightarrow> \<exists>Q'. Q \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>
[PROOF STEP]
assume "Q \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> P" and "P \<longmapsto>(STCal Source Target)* P'"
[PROOF STATE]
proof (state)
this:
Q \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> P
P \<longmapsto>STCal Source Target* P'

goal (1 subgoal):
 1. \<And>P Q P'. P \<longmapsto>STCal Source Target* P' \<and> Q \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> P \<Longrightarrow> \<exists>Q'. Q \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>
[PROOF STEP]
thus "\<exists>Q'. Q \<longmapsto>(STCal Source Target)* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>"
[PROOF STATE]
proof (prove)
using this:
Q \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> P
P \<longmapsto>STCal Source Target* P'

goal (1 subgoal):
 1. \<exists>Q'. Q \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>
[PROOF STEP]
proof (induct arbitrary: P')
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>S P'. TargetTerm (\<lbrakk>S\<rbrakk>) \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. SourceTerm S \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>
 2. \<And>S P'. SourceTerm S \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. SourceTerm S \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>
 3. \<And>T1 T2 P'. (T1, T2) \<in> TRel \<and> TargetTerm T2 \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. TargetTerm T1 \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>
 4. \<And>P Q R P'. \<lbrakk>P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q; \<And>P'. Q \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. P \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>; Q \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> R; \<And>P'. R \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. Q \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>; R \<longmapsto>STCal Source Target* P'\<rbrakk> \<Longrightarrow> \<exists>Q'. P \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>
[PROOF STEP]
case (encR S)
[PROOF STATE]
proof (state)
this:
TargetTerm (\<lbrakk>S\<rbrakk>) \<longmapsto>STCal Source Target* P'

goal (4 subgoals):
 1. \<And>S P'. TargetTerm (\<lbrakk>S\<rbrakk>) \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. SourceTerm S \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>
 2. \<And>S P'. SourceTerm S \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. SourceTerm S \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>
 3. \<And>T1 T2 P'. (T1, T2) \<in> TRel \<and> TargetTerm T2 \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. TargetTerm T1 \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>
 4. \<And>P Q R P'. \<lbrakk>P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q; \<And>P'. Q \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. P \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>; Q \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> R; \<And>P'. R \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. Q \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>; R \<longmapsto>STCal Source Target* P'\<rbrakk> \<Longrightarrow> \<exists>Q'. P \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>
[PROOF STEP]
assume "TargetTerm (\<lbrakk>S\<rbrakk>) \<longmapsto>(STCal Source Target)* P'"
[PROOF STATE]
proof (state)
this:
TargetTerm (\<lbrakk>S\<rbrakk>) \<longmapsto>STCal Source Target* P'

goal (4 subgoals):
 1. \<And>S P'. TargetTerm (\<lbrakk>S\<rbrakk>) \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. SourceTerm S \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>
 2. \<And>S P'. SourceTerm S \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. SourceTerm S \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>
 3. \<And>T1 T2 P'. (T1, T2) \<in> TRel \<and> TargetTerm T2 \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. TargetTerm T1 \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>
 4. \<And>P Q R P'. \<lbrakk>P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q; \<And>P'. Q \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. P \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>; Q \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> R; \<And>P'. R \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. Q \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>; R \<longmapsto>STCal Source Target* P'\<rbrakk> \<Longrightarrow> \<exists>Q'. P \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
TargetTerm (\<lbrakk>S\<rbrakk>) \<longmapsto>STCal Source Target* P'
[PROOF STEP]
obtain T where A1: "T \<in>T P'" and A2: "\<lbrakk>S\<rbrakk> \<longmapsto>Target* T"
[PROOF STATE]
proof (prove)
using this:
TargetTerm (\<lbrakk>S\<rbrakk>) \<longmapsto>STCal Source Target* P'

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

goal (4 subgoals):
 1. \<And>S P'. TargetTerm (\<lbrakk>S\<rbrakk>) \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. SourceTerm S \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>
 2. \<And>S P'. SourceTerm S \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. SourceTerm S \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>
 3. \<And>T1 T2 P'. (T1, T2) \<in> TRel \<and> TargetTerm T2 \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. TargetTerm T1 \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>
 4. \<And>P Q R P'. \<lbrakk>P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q; \<And>P'. Q \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. P \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>; Q \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> R; \<And>P'. R \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. Q \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>; R \<longmapsto>STCal Source Target* P'\<rbrakk> \<Longrightarrow> \<exists>Q'. P \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>
[PROOF STEP]
from os A2
[PROOF STATE]
proof (chain)
picking this:
operational_sound (TRel\<^sup>*)
\<lbrakk>S\<rbrakk> \<longmapsto>Target* T
[PROOF STEP]
obtain S' where A3: "S \<longmapsto>Source* S'" and A4: "(\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*"
[PROOF STATE]
proof (prove)
using this:
operational_sound (TRel\<^sup>*)
\<lbrakk>S\<rbrakk> \<longmapsto>Target* T

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

goal (4 subgoals):
 1. \<And>S P'. TargetTerm (\<lbrakk>S\<rbrakk>) \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. SourceTerm S \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>
 2. \<And>S P'. SourceTerm S \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. SourceTerm S \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>
 3. \<And>T1 T2 P'. (T1, T2) \<in> TRel \<and> TargetTerm T2 \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. TargetTerm T1 \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>
 4. \<And>P Q R P'. \<lbrakk>P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q; \<And>P'. Q \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. P \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>; Q \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> R; \<And>P'. R \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. Q \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>; R \<longmapsto>STCal Source Target* P'\<rbrakk> \<Longrightarrow> \<exists>Q'. P \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>
[PROOF STEP]
from A3
[PROOF STATE]
proof (chain)
picking this:
S \<longmapsto>Source* S'
[PROOF STEP]
have "SourceTerm S \<longmapsto>(STCal Source Target)* (SourceTerm S')"
[PROOF STATE]
proof (prove)
using this:
S \<longmapsto>Source* S'

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

goal (4 subgoals):
 1. \<And>S P'. TargetTerm (\<lbrakk>S\<rbrakk>) \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. SourceTerm S \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>
 2. \<And>S P'. SourceTerm S \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. SourceTerm S \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>
 3. \<And>T1 T2 P'. (T1, T2) \<in> TRel \<and> TargetTerm T2 \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. TargetTerm T1 \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>
 4. \<And>P Q R P'. \<lbrakk>P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q; \<And>P'. Q \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. P \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>; Q \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> R; \<And>P'. R \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. Q \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>; R \<longmapsto>STCal Source Target* P'\<rbrakk> \<Longrightarrow> \<exists>Q'. P \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
SourceTerm S \<longmapsto>STCal Source Target* SourceTerm S'

goal (4 subgoals):
 1. \<And>S P'. TargetTerm (\<lbrakk>S\<rbrakk>) \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. SourceTerm S \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>
 2. \<And>S P'. SourceTerm S \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. SourceTerm S \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>
 3. \<And>T1 T2 P'. (T1, T2) \<in> TRel \<and> TargetTerm T2 \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. TargetTerm T1 \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>
 4. \<And>P Q R P'. \<lbrakk>P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q; \<And>P'. Q \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. P \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>; Q \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> R; \<And>P'. R \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. Q \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>; R \<longmapsto>STCal Source Target* P'\<rbrakk> \<Longrightarrow> \<exists>Q'. P \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>
[PROOF STEP]
have "SourceTerm S' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> P'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. SourceTerm S' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> P'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. SourceTerm S' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> P'
[PROOF STEP]
from A4
[PROOF STATE]
proof (chain)
picking this:
(\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*
[PROOF STEP]
have "\<lbrakk>S'\<rbrakk> = T \<or> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>+"
[PROOF STATE]
proof (prove)
using this:
(\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*

goal (1 subgoal):
 1. \<lbrakk>S'\<rbrakk> = T \<or> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>+
[PROOF STEP]
using rtrancl_eq_or_trancl[of "\<lbrakk>S'\<rbrakk>" T TRel]
[PROOF STATE]
proof (prove)
using this:
(\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*
((\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*) = (\<lbrakk>S'\<rbrakk> = T \<or> \<lbrakk>S'\<rbrakk> \<noteq> T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>+)

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

goal (1 subgoal):
 1. SourceTerm S' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> P'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<lbrakk>S'\<rbrakk> = T \<or> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>+

goal (1 subgoal):
 1. SourceTerm S' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> P'
[PROOF STEP]
have A5: "SourceTerm S' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm (\<lbrakk>S'\<rbrakk>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. SourceTerm S' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm (\<lbrakk>S'\<rbrakk>)
[PROOF STEP]
by (simp add: indRelRTPO.encR)
[PROOF STATE]
proof (state)
this:
SourceTerm S' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm (\<lbrakk>S'\<rbrakk>)

goal (1 subgoal):
 1. SourceTerm S' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> P'
[PROOF STEP]
with A1
[PROOF STATE]
proof (chain)
picking this:
T \<in>T P'
SourceTerm S' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm (\<lbrakk>S'\<rbrakk>)
[PROOF STEP]
have "\<lbrakk>S'\<rbrakk> = T \<Longrightarrow> SourceTerm S' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> P'"
[PROOF STATE]
proof (prove)
using this:
T \<in>T P'
SourceTerm S' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm (\<lbrakk>S'\<rbrakk>)

goal (1 subgoal):
 1. \<lbrakk>S'\<rbrakk> = T \<Longrightarrow> SourceTerm S' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> P'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<lbrakk>S'\<rbrakk> = T \<Longrightarrow> SourceTerm S' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> P'

goal (1 subgoal):
 1. SourceTerm S' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> P'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<lbrakk>S'\<rbrakk> = T \<Longrightarrow> SourceTerm S' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> P'

goal (1 subgoal):
 1. SourceTerm S' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> P'
[PROOF STEP]
have "(\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>+ \<Longrightarrow> SourceTerm S' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> P'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>+ \<Longrightarrow> SourceTerm S' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> P'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>+ \<Longrightarrow> SourceTerm S' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> P'
[PROOF STEP]
assume "(\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>+"
[PROOF STATE]
proof (state)
this:
(\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>+

goal (1 subgoal):
 1. (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>+ \<Longrightarrow> SourceTerm S' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> P'
[PROOF STEP]
hence "TargetTerm (\<lbrakk>S'\<rbrakk>) \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm T"
[PROOF STATE]
proof (prove)
using this:
(\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>+

goal (1 subgoal):
 1. TargetTerm (\<lbrakk>S'\<rbrakk>) \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm T
[PROOF STEP]
by (rule transitive_closure_of_TRel_to_indRelRTPO)
[PROOF STATE]
proof (state)
this:
TargetTerm (\<lbrakk>S'\<rbrakk>) \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm T

goal (1 subgoal):
 1. (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>+ \<Longrightarrow> SourceTerm S' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> P'
[PROOF STEP]
with A5
[PROOF STATE]
proof (chain)
picking this:
SourceTerm S' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm (\<lbrakk>S'\<rbrakk>)
TargetTerm (\<lbrakk>S'\<rbrakk>) \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm T
[PROOF STEP]
have "SourceTerm S' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm T"
[PROOF STATE]
proof (prove)
using this:
SourceTerm S' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm (\<lbrakk>S'\<rbrakk>)
TargetTerm (\<lbrakk>S'\<rbrakk>) \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm T

goal (1 subgoal):
 1. SourceTerm S' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm T
[PROOF STEP]
by (rule indRelRTPO.trans)
[PROOF STATE]
proof (state)
this:
SourceTerm S' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm T

goal (1 subgoal):
 1. (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>+ \<Longrightarrow> SourceTerm S' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> P'
[PROOF STEP]
with A1
[PROOF STATE]
proof (chain)
picking this:
T \<in>T P'
SourceTerm S' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm T
[PROOF STEP]
show "SourceTerm S' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> P'"
[PROOF STATE]
proof (prove)
using this:
T \<in>T P'
SourceTerm S' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm T

goal (1 subgoal):
 1. SourceTerm S' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> P'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
SourceTerm S' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> P'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>+ \<Longrightarrow> SourceTerm S' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> P'

goal (1 subgoal):
 1. SourceTerm S' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> P'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>S'\<rbrakk> = T \<or> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>+
\<lbrakk>S'\<rbrakk> = T \<Longrightarrow> SourceTerm S' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> P'
(\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>+ \<Longrightarrow> SourceTerm S' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> P'
[PROOF STEP]
show "SourceTerm S' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> P'"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>S'\<rbrakk> = T \<or> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>+
\<lbrakk>S'\<rbrakk> = T \<Longrightarrow> SourceTerm S' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> P'
(\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>+ \<Longrightarrow> SourceTerm S' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> P'

goal (1 subgoal):
 1. SourceTerm S' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> P'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
SourceTerm S' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> P'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
SourceTerm S' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> P'

goal (4 subgoals):
 1. \<And>S P'. TargetTerm (\<lbrakk>S\<rbrakk>) \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. SourceTerm S \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>
 2. \<And>S P'. SourceTerm S \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. SourceTerm S \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>
 3. \<And>T1 T2 P'. (T1, T2) \<in> TRel \<and> TargetTerm T2 \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. TargetTerm T1 \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>
 4. \<And>P Q R P'. \<lbrakk>P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q; \<And>P'. Q \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. P \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>; Q \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> R; \<And>P'. R \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. Q \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>; R \<longmapsto>STCal Source Target* P'\<rbrakk> \<Longrightarrow> \<exists>Q'. P \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>
[PROOF STEP]
hence "(P', SourceTerm S') \<in> (indRelRTPO TRel)\<inverse>"
[PROOF STATE]
proof (prove)
using this:
SourceTerm S' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> P'

goal (1 subgoal):
 1. (P', SourceTerm S') \<in> (indRelRTPO TRel)\<inverse>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(P', SourceTerm S') \<in> (indRelRTPO TRel)\<inverse>

goal (4 subgoals):
 1. \<And>S P'. TargetTerm (\<lbrakk>S\<rbrakk>) \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. SourceTerm S \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>
 2. \<And>S P'. SourceTerm S \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. SourceTerm S \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>
 3. \<And>T1 T2 P'. (T1, T2) \<in> TRel \<and> TargetTerm T2 \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. TargetTerm T1 \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>
 4. \<And>P Q R P'. \<lbrakk>P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q; \<And>P'. Q \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. P \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>; Q \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> R; \<And>P'. R \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. Q \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>; R \<longmapsto>STCal Source Target* P'\<rbrakk> \<Longrightarrow> \<exists>Q'. P \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
SourceTerm S \<longmapsto>STCal Source Target* SourceTerm S'
(P', SourceTerm S') \<in> (indRelRTPO TRel)\<inverse>
[PROOF STEP]
show "\<exists>Q'. SourceTerm S \<longmapsto>(STCal Source Target)* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>"
[PROOF STATE]
proof (prove)
using this:
SourceTerm S \<longmapsto>STCal Source Target* SourceTerm S'
(P', SourceTerm S') \<in> (indRelRTPO TRel)\<inverse>

goal (1 subgoal):
 1. \<exists>Q'. SourceTerm S \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>Q'. SourceTerm S \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>

goal (3 subgoals):
 1. \<And>S P'. SourceTerm S \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. SourceTerm S \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>
 2. \<And>T1 T2 P'. (T1, T2) \<in> TRel \<and> TargetTerm T2 \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. TargetTerm T1 \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>
 3. \<And>P Q R P'. \<lbrakk>P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q; \<And>P'. Q \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. P \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>; Q \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> R; \<And>P'. R \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. Q \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>; R \<longmapsto>STCal Source Target* P'\<rbrakk> \<Longrightarrow> \<exists>Q'. P \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>S P'. SourceTerm S \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. SourceTerm S \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>
 2. \<And>T1 T2 P'. (T1, T2) \<in> TRel \<and> TargetTerm T2 \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. TargetTerm T1 \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>
 3. \<And>P Q R P'. \<lbrakk>P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q; \<And>P'. Q \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. P \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>; Q \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> R; \<And>P'. R \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. Q \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>; R \<longmapsto>STCal Source Target* P'\<rbrakk> \<Longrightarrow> \<exists>Q'. P \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>
[PROOF STEP]
case (source S)
[PROOF STATE]
proof (state)
this:
SourceTerm S \<longmapsto>STCal Source Target* P'

goal (3 subgoals):
 1. \<And>S P'. SourceTerm S \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. SourceTerm S \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>
 2. \<And>T1 T2 P'. (T1, T2) \<in> TRel \<and> TargetTerm T2 \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. TargetTerm T1 \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>
 3. \<And>P Q R P'. \<lbrakk>P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q; \<And>P'. Q \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. P \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>; Q \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> R; \<And>P'. R \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. Q \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>; R \<longmapsto>STCal Source Target* P'\<rbrakk> \<Longrightarrow> \<exists>Q'. P \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
SourceTerm S \<longmapsto>STCal Source Target* P'
[PROOF STEP]
obtain S' where B1: "S' \<in>S P'"
[PROOF STATE]
proof (prove)
using this:
SourceTerm S \<longmapsto>STCal Source Target* P'

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

goal (3 subgoals):
 1. \<And>S P'. SourceTerm S \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. SourceTerm S \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>
 2. \<And>T1 T2 P'. (T1, T2) \<in> TRel \<and> TargetTerm T2 \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. TargetTerm T1 \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>
 3. \<And>P Q R P'. \<lbrakk>P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q; \<And>P'. Q \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. P \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>; Q \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> R; \<And>P'. R \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. Q \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>; R \<longmapsto>STCal Source Target* P'\<rbrakk> \<Longrightarrow> \<exists>Q'. P \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>
[PROOF STEP]
hence "(P', P') \<in> (indRelRTPO TRel)\<inverse>"
[PROOF STATE]
proof (prove)
using this:
S' \<in>S P'

goal (1 subgoal):
 1. (P', P') \<in> (indRelRTPO TRel)\<inverse>
[PROOF STEP]
by (simp add: indRelRTPO.source)
[PROOF STATE]
proof (state)
this:
(P', P') \<in> (indRelRTPO TRel)\<inverse>

goal (3 subgoals):
 1. \<And>S P'. SourceTerm S \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. SourceTerm S \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>
 2. \<And>T1 T2 P'. (T1, T2) \<in> TRel \<and> TargetTerm T2 \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. TargetTerm T1 \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>
 3. \<And>P Q R P'. \<lbrakk>P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q; \<And>P'. Q \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. P \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>; Q \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> R; \<And>P'. R \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. Q \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>; R \<longmapsto>STCal Source Target* P'\<rbrakk> \<Longrightarrow> \<exists>Q'. P \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>
[PROOF STEP]
with source
[PROOF STATE]
proof (chain)
picking this:
SourceTerm S \<longmapsto>STCal Source Target* P'
(P', P') \<in> (indRelRTPO TRel)\<inverse>
[PROOF STEP]
show "\<exists>Q'. SourceTerm S \<longmapsto>(STCal Source Target)* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>"
[PROOF STATE]
proof (prove)
using this:
SourceTerm S \<longmapsto>STCal Source Target* P'
(P', P') \<in> (indRelRTPO TRel)\<inverse>

goal (1 subgoal):
 1. \<exists>Q'. SourceTerm S \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>Q'. SourceTerm S \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>

goal (2 subgoals):
 1. \<And>T1 T2 P'. (T1, T2) \<in> TRel \<and> TargetTerm T2 \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. TargetTerm T1 \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>
 2. \<And>P Q R P'. \<lbrakk>P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q; \<And>P'. Q \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. P \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>; Q \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> R; \<And>P'. R \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. Q \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>; R \<longmapsto>STCal Source Target* P'\<rbrakk> \<Longrightarrow> \<exists>Q'. P \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>T1 T2 P'. (T1, T2) \<in> TRel \<and> TargetTerm T2 \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. TargetTerm T1 \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>
 2. \<And>P Q R P'. \<lbrakk>P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q; \<And>P'. Q \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. P \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>; Q \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> R; \<And>P'. R \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. Q \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>; R \<longmapsto>STCal Source Target* P'\<rbrakk> \<Longrightarrow> \<exists>Q'. P \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>
[PROOF STEP]
case (target T1 T2)
[PROOF STATE]
proof (state)
this:
(T1, T2) \<in> TRel
TargetTerm T2 \<longmapsto>STCal Source Target* P'

goal (2 subgoals):
 1. \<And>T1 T2 P'. (T1, T2) \<in> TRel \<and> TargetTerm T2 \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. TargetTerm T1 \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>
 2. \<And>P Q R P'. \<lbrakk>P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q; \<And>P'. Q \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. P \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>; Q \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> R; \<And>P'. R \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. Q \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>; R \<longmapsto>STCal Source Target* P'\<rbrakk> \<Longrightarrow> \<exists>Q'. P \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>
[PROOF STEP]
assume "TargetTerm T2 \<longmapsto>(STCal Source Target)* P'"
[PROOF STATE]
proof (state)
this:
TargetTerm T2 \<longmapsto>STCal Source Target* P'

goal (2 subgoals):
 1. \<And>T1 T2 P'. (T1, T2) \<in> TRel \<and> TargetTerm T2 \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. TargetTerm T1 \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>
 2. \<And>P Q R P'. \<lbrakk>P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q; \<And>P'. Q \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. P \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>; Q \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> R; \<And>P'. R \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. Q \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>; R \<longmapsto>STCal Source Target* P'\<rbrakk> \<Longrightarrow> \<exists>Q'. P \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
TargetTerm T2 \<longmapsto>STCal Source Target* P'
[PROOF STEP]
obtain T2' where C1: "T2' \<in>T P'" and C2: "T2 \<longmapsto>Target* T2'"
[PROOF STATE]
proof (prove)
using this:
TargetTerm T2 \<longmapsto>STCal Source Target* P'

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

goal (2 subgoals):
 1. \<And>T1 T2 P'. (T1, T2) \<in> TRel \<and> TargetTerm T2 \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. TargetTerm T1 \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>
 2. \<And>P Q R P'. \<lbrakk>P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q; \<And>P'. Q \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. P \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>; Q \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> R; \<And>P'. R \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. Q \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>; R \<longmapsto>STCal Source Target* P'\<rbrakk> \<Longrightarrow> \<exists>Q'. P \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>
[PROOF STEP]
assume "(T1, T2) \<in> TRel"
[PROOF STATE]
proof (state)
this:
(T1, T2) \<in> TRel

goal (2 subgoals):
 1. \<And>T1 T2 P'. (T1, T2) \<in> TRel \<and> TargetTerm T2 \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. TargetTerm T1 \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>
 2. \<And>P Q R P'. \<lbrakk>P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q; \<And>P'. Q \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. P \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>; Q \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> R; \<And>P'. R \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. Q \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>; R \<longmapsto>STCal Source Target* P'\<rbrakk> \<Longrightarrow> \<exists>Q'. P \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>
[PROOF STEP]
hence "(T2, T1) \<in> (TRel\<^sup>+)\<inverse>"
[PROOF STATE]
proof (prove)
using this:
(T1, T2) \<in> TRel

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

goal (2 subgoals):
 1. \<And>T1 T2 P'. (T1, T2) \<in> TRel \<and> TargetTerm T2 \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. TargetTerm T1 \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>
 2. \<And>P Q R P'. \<lbrakk>P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q; \<And>P'. Q \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. P \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>; Q \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> R; \<And>P'. R \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. Q \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>; R \<longmapsto>STCal Source Target* P'\<rbrakk> \<Longrightarrow> \<exists>Q'. P \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>
[PROOF STEP]
with C2 sim
[PROOF STATE]
proof (chain)
picking this:
T2 \<longmapsto>Target* T2'
weak_reduction_simulation ((TRel\<^sup>+)\<inverse>) Target
(T2, T1) \<in> (TRel\<^sup>+)\<inverse>
[PROOF STEP]
obtain T1' where C3: "T1 \<longmapsto>Target* T1'" and C4: "(T2', T1') \<in> (TRel\<^sup>+)\<inverse>"
[PROOF STATE]
proof (prove)
using this:
T2 \<longmapsto>Target* T2'
weak_reduction_simulation ((TRel\<^sup>+)\<inverse>) Target
(T2, T1) \<in> (TRel\<^sup>+)\<inverse>

goal (1 subgoal):
 1. (\<And>T1'. T1 \<longmapsto>Target* T1' \<and> (T2', T1') \<in> (TRel\<^sup>+)\<inverse> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
T1 \<longmapsto>Target* T1'
(T2', T1') \<in> (TRel\<^sup>+)\<inverse>

goal (2 subgoals):
 1. \<And>T1 T2 P'. (T1, T2) \<in> TRel \<and> TargetTerm T2 \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. TargetTerm T1 \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>
 2. \<And>P Q R P'. \<lbrakk>P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q; \<And>P'. Q \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. P \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>; Q \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> R; \<And>P'. R \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. Q \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>; R \<longmapsto>STCal Source Target* P'\<rbrakk> \<Longrightarrow> \<exists>Q'. P \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>
[PROOF STEP]
from C3
[PROOF STATE]
proof (chain)
picking this:
T1 \<longmapsto>Target* T1'
[PROOF STEP]
have "TargetTerm T1 \<longmapsto>(STCal Source Target)* (TargetTerm T1')"
[PROOF STATE]
proof (prove)
using this:
T1 \<longmapsto>Target* T1'

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

goal (2 subgoals):
 1. \<And>T1 T2 P'. (T1, T2) \<in> TRel \<and> TargetTerm T2 \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. TargetTerm T1 \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>
 2. \<And>P Q R P'. \<lbrakk>P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q; \<And>P'. Q \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. P \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>; Q \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> R; \<And>P'. R \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. Q \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>; R \<longmapsto>STCal Source Target* P'\<rbrakk> \<Longrightarrow> \<exists>Q'. P \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
TargetTerm T1 \<longmapsto>STCal Source Target* TargetTerm T1'

goal (2 subgoals):
 1. \<And>T1 T2 P'. (T1, T2) \<in> TRel \<and> TargetTerm T2 \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. TargetTerm T1 \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>
 2. \<And>P Q R P'. \<lbrakk>P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q; \<And>P'. Q \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. P \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>; Q \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> R; \<And>P'. R \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. Q \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>; R \<longmapsto>STCal Source Target* P'\<rbrakk> \<Longrightarrow> \<exists>Q'. P \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>
[PROOF STEP]
from C4
[PROOF STATE]
proof (chain)
picking this:
(T2', T1') \<in> (TRel\<^sup>+)\<inverse>
[PROOF STEP]
have "(T1', T2') \<in> TRel\<^sup>+"
[PROOF STATE]
proof (prove)
using this:
(T2', T1') \<in> (TRel\<^sup>+)\<inverse>

goal (1 subgoal):
 1. (T1', T2') \<in> TRel\<^sup>+
[PROOF STEP]
by induct
[PROOF STATE]
proof (state)
this:
(T1', T2') \<in> TRel\<^sup>+

goal (2 subgoals):
 1. \<And>T1 T2 P'. (T1, T2) \<in> TRel \<and> TargetTerm T2 \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. TargetTerm T1 \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>
 2. \<And>P Q R P'. \<lbrakk>P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q; \<And>P'. Q \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. P \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>; Q \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> R; \<And>P'. R \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. Q \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>; R \<longmapsto>STCal Source Target* P'\<rbrakk> \<Longrightarrow> \<exists>Q'. P \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>
[PROOF STEP]
hence "TargetTerm T1' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm T2'"
[PROOF STATE]
proof (prove)
using this:
(T1', T2') \<in> TRel\<^sup>+

goal (1 subgoal):
 1. TargetTerm T1' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm T2'
[PROOF STEP]
by (rule transitive_closure_of_TRel_to_indRelRTPO)
[PROOF STATE]
proof (state)
this:
TargetTerm T1' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm T2'

goal (2 subgoals):
 1. \<And>T1 T2 P'. (T1, T2) \<in> TRel \<and> TargetTerm T2 \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. TargetTerm T1 \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>
 2. \<And>P Q R P'. \<lbrakk>P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q; \<And>P'. Q \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. P \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>; Q \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> R; \<And>P'. R \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. Q \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>; R \<longmapsto>STCal Source Target* P'\<rbrakk> \<Longrightarrow> \<exists>Q'. P \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>
[PROOF STEP]
with C1
[PROOF STATE]
proof (chain)
picking this:
T2' \<in>T P'
TargetTerm T1' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm T2'
[PROOF STEP]
have "(P', TargetTerm T1') \<in> (indRelRTPO TRel)\<inverse>"
[PROOF STATE]
proof (prove)
using this:
T2' \<in>T P'
TargetTerm T1' \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm T2'

goal (1 subgoal):
 1. (P', TargetTerm T1') \<in> (indRelRTPO TRel)\<inverse>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(P', TargetTerm T1') \<in> (indRelRTPO TRel)\<inverse>

goal (2 subgoals):
 1. \<And>T1 T2 P'. (T1, T2) \<in> TRel \<and> TargetTerm T2 \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. TargetTerm T1 \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>
 2. \<And>P Q R P'. \<lbrakk>P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q; \<And>P'. Q \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. P \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>; Q \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> R; \<And>P'. R \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. Q \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>; R \<longmapsto>STCal Source Target* P'\<rbrakk> \<Longrightarrow> \<exists>Q'. P \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
TargetTerm T1 \<longmapsto>STCal Source Target* TargetTerm T1'
(P', TargetTerm T1') \<in> (indRelRTPO TRel)\<inverse>
[PROOF STEP]
show "\<exists>Q'. TargetTerm T1 \<longmapsto>(STCal Source Target)* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>"
[PROOF STATE]
proof (prove)
using this:
TargetTerm T1 \<longmapsto>STCal Source Target* TargetTerm T1'
(P', TargetTerm T1') \<in> (indRelRTPO TRel)\<inverse>

goal (1 subgoal):
 1. \<exists>Q'. TargetTerm T1 \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>Q'. TargetTerm T1 \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>

goal (1 subgoal):
 1. \<And>P Q R P'. \<lbrakk>P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q; \<And>P'. Q \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. P \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>; Q \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> R; \<And>P'. R \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. Q \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>; R \<longmapsto>STCal Source Target* P'\<rbrakk> \<Longrightarrow> \<exists>Q'. P \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>P Q R P'. \<lbrakk>P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q; \<And>P'. Q \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. P \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>; Q \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> R; \<And>P'. R \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. Q \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>; R \<longmapsto>STCal Source Target* P'\<rbrakk> \<Longrightarrow> \<exists>Q'. P \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>
[PROOF STEP]
case (trans P Q R R')
[PROOF STATE]
proof (state)
this:
P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q
Q \<longmapsto>STCal Source Target* ?P'3 \<Longrightarrow> \<exists>Q'. P \<longmapsto>STCal Source Target* Q' \<and> (?P'3, Q') \<in> (indRelRTPO TRel)\<inverse>
Q \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> R
R \<longmapsto>STCal Source Target* ?P'3 \<Longrightarrow> \<exists>Q'. Q \<longmapsto>STCal Source Target* Q' \<and> (?P'3, Q') \<in> (indRelRTPO TRel)\<inverse>
R \<longmapsto>STCal Source Target* R'

goal (1 subgoal):
 1. \<And>P Q R P'. \<lbrakk>P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q; \<And>P'. Q \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. P \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>; Q \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> R; \<And>P'. R \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. Q \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>; R \<longmapsto>STCal Source Target* P'\<rbrakk> \<Longrightarrow> \<exists>Q'. P \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>
[PROOF STEP]
assume "R \<longmapsto>(STCal Source Target)* R'"
         and "\<And>R'. R \<longmapsto>(STCal Source Target)* R'
              \<Longrightarrow> \<exists>Q'. Q \<longmapsto>(STCal Source Target)* Q' \<and> (R', Q') \<in> (indRelRTPO TRel)\<inverse>"
[PROOF STATE]
proof (state)
this:
R \<longmapsto>STCal Source Target* R'
R \<longmapsto>STCal Source Target* ?R'3 \<Longrightarrow> \<exists>Q'. Q \<longmapsto>STCal Source Target* Q' \<and> (?R'3, Q') \<in> (indRelRTPO TRel)\<inverse>

goal (1 subgoal):
 1. \<And>P Q R P'. \<lbrakk>P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q; \<And>P'. Q \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. P \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>; Q \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> R; \<And>P'. R \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. Q \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>; R \<longmapsto>STCal Source Target* P'\<rbrakk> \<Longrightarrow> \<exists>Q'. P \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
R \<longmapsto>STCal Source Target* R'
R \<longmapsto>STCal Source Target* ?R'3 \<Longrightarrow> \<exists>Q'. Q \<longmapsto>STCal Source Target* Q' \<and> (?R'3, Q') \<in> (indRelRTPO TRel)\<inverse>
[PROOF STEP]
obtain Q' where D1: "Q \<longmapsto>(STCal Source Target)* Q'"
                            and D2: "(R', Q') \<in> (indRelRTPO TRel)\<inverse>"
[PROOF STATE]
proof (prove)
using this:
R \<longmapsto>STCal Source Target* R'
R \<longmapsto>STCal Source Target* ?R'3 \<Longrightarrow> \<exists>Q'. Q \<longmapsto>STCal Source Target* Q' \<and> (?R'3, Q') \<in> (indRelRTPO TRel)\<inverse>

goal (1 subgoal):
 1. (\<And>Q'. Q \<longmapsto>STCal Source Target* Q' \<and> (R', Q') \<in> (indRelRTPO TRel)\<inverse> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Q \<longmapsto>STCal Source Target* Q'
(R', Q') \<in> (indRelRTPO TRel)\<inverse>

goal (1 subgoal):
 1. \<And>P Q R P'. \<lbrakk>P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q; \<And>P'. Q \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. P \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>; Q \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> R; \<And>P'. R \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. Q \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>; R \<longmapsto>STCal Source Target* P'\<rbrakk> \<Longrightarrow> \<exists>Q'. P \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>
[PROOF STEP]
assume "\<And>Q'. Q \<longmapsto>(STCal Source Target)* Q'
              \<Longrightarrow> \<exists>P'. P \<longmapsto>(STCal Source Target)* P' \<and> (Q', P') \<in> (indRelRTPO TRel)\<inverse>"
[PROOF STATE]
proof (state)
this:
Q \<longmapsto>STCal Source Target* ?Q'3 \<Longrightarrow> \<exists>P'. P \<longmapsto>STCal Source Target* P' \<and> (?Q'3, P') \<in> (indRelRTPO TRel)\<inverse>

goal (1 subgoal):
 1. \<And>P Q R P'. \<lbrakk>P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q; \<And>P'. Q \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. P \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>; Q \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> R; \<And>P'. R \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. Q \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>; R \<longmapsto>STCal Source Target* P'\<rbrakk> \<Longrightarrow> \<exists>Q'. P \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>
[PROOF STEP]
with D1
[PROOF STATE]
proof (chain)
picking this:
Q \<longmapsto>STCal Source Target* Q'
Q \<longmapsto>STCal Source Target* ?Q'3 \<Longrightarrow> \<exists>P'. P \<longmapsto>STCal Source Target* P' \<and> (?Q'3, P') \<in> (indRelRTPO TRel)\<inverse>
[PROOF STEP]
obtain P' where D3: "P \<longmapsto>(STCal Source Target)* P'"
                          and D4: "(Q', P') \<in> (indRelRTPO TRel)\<inverse>"
[PROOF STATE]
proof (prove)
using this:
Q \<longmapsto>STCal Source Target* Q'
Q \<longmapsto>STCal Source Target* ?Q'3 \<Longrightarrow> \<exists>P'. P \<longmapsto>STCal Source Target* P' \<and> (?Q'3, P') \<in> (indRelRTPO TRel)\<inverse>

goal (1 subgoal):
 1. (\<And>P'. P \<longmapsto>STCal Source Target* P' \<and> (Q', P') \<in> (indRelRTPO TRel)\<inverse> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
P \<longmapsto>STCal Source Target* P'
(Q', P') \<in> (indRelRTPO TRel)\<inverse>

goal (1 subgoal):
 1. \<And>P Q R P'. \<lbrakk>P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q; \<And>P'. Q \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. P \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>; Q \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> R; \<And>P'. R \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. Q \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>; R \<longmapsto>STCal Source Target* P'\<rbrakk> \<Longrightarrow> \<exists>Q'. P \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>
[PROOF STEP]
from D4 D2
[PROOF STATE]
proof (chain)
picking this:
(Q', P') \<in> (indRelRTPO TRel)\<inverse>
(R', Q') \<in> (indRelRTPO TRel)\<inverse>
[PROOF STEP]
have "(R', P') \<in> (indRelRTPO TRel)\<inverse>"
[PROOF STATE]
proof (prove)
using this:
(Q', P') \<in> (indRelRTPO TRel)\<inverse>
(R', Q') \<in> (indRelRTPO TRel)\<inverse>

goal (1 subgoal):
 1. (R', P') \<in> (indRelRTPO TRel)\<inverse>
[PROOF STEP]
by (simp add: indRelRTPO.trans[where P="P'" and Q="Q'" and R="R'"])
[PROOF STATE]
proof (state)
this:
(R', P') \<in> (indRelRTPO TRel)\<inverse>

goal (1 subgoal):
 1. \<And>P Q R P'. \<lbrakk>P \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> Q; \<And>P'. Q \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. P \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>; Q \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> R; \<And>P'. R \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. Q \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>; R \<longmapsto>STCal Source Target* P'\<rbrakk> \<Longrightarrow> \<exists>Q'. P \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>
[PROOF STEP]
with D3
[PROOF STATE]
proof (chain)
picking this:
P \<longmapsto>STCal Source Target* P'
(R', P') \<in> (indRelRTPO TRel)\<inverse>
[PROOF STEP]
show "\<exists>P'. P \<longmapsto>(STCal Source Target)* P' \<and> (R', P') \<in> (indRelRTPO TRel)\<inverse>"
[PROOF STATE]
proof (prove)
using this:
P \<longmapsto>STCal Source Target* P'
(R', P') \<in> (indRelRTPO TRel)\<inverse>

goal (1 subgoal):
 1. \<exists>P'. P \<longmapsto>STCal Source Target* P' \<and> (R', P') \<in> (indRelRTPO TRel)\<inverse>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>P'. P \<longmapsto>STCal Source Target* P' \<and> (R', P') \<in> (indRelRTPO TRel)\<inverse>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>Q'. Q \<longmapsto>STCal Source Target* Q' \<and> (P', Q') \<in> (indRelRTPO TRel)\<inverse>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
weak_reduction_simulation ((indRelRTPO TRel)\<inverse>) (STCal Source Target)

goal (1 subgoal):
 1. weak_reduction_simulation ((indRelRTPO TRel)\<inverse>) (STCal Source Target) \<Longrightarrow> operational_sound (TRel\<^sup>*) \<and> weak_reduction_simulation ((TRel\<^sup>+)\<inverse>) Target
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. weak_reduction_simulation ((indRelRTPO TRel)\<inverse>) (STCal Source Target) \<Longrightarrow> operational_sound (TRel\<^sup>*) \<and> weak_reduction_simulation ((TRel\<^sup>+)\<inverse>) 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 (1 subgoal):
 1. weak_reduction_simulation ((indRelRTPO TRel)\<inverse>) (STCal Source Target) \<Longrightarrow> operational_sound (TRel\<^sup>*) \<and> weak_reduction_simulation ((TRel\<^sup>+)\<inverse>) Target
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>S. SourceTerm S \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm (\<lbrakk>S\<rbrakk>)

goal (1 subgoal):
 1. weak_reduction_simulation ((indRelRTPO TRel)\<inverse>) (STCal Source Target) \<Longrightarrow> operational_sound (TRel\<^sup>*) \<and> weak_reduction_simulation ((TRel\<^sup>+)\<inverse>) 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 (1 subgoal):
 1. weak_reduction_simulation ((indRelRTPO TRel)\<inverse>) (STCal Source Target) \<Longrightarrow> operational_sound (TRel\<^sup>*) \<and> weak_reduction_simulation ((TRel\<^sup>+)\<inverse>) 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 (1 subgoal):
 1. weak_reduction_simulation ((indRelRTPO TRel)\<inverse>) (STCal Source Target) \<Longrightarrow> operational_sound (TRel\<^sup>*) \<and> weak_reduction_simulation ((TRel\<^sup>+)\<inverse>) Target
[PROOF STEP]
assume sim: "weak_reduction_simulation ((indRelRTPO TRel)\<inverse>) (STCal Source Target)"
[PROOF STATE]
proof (state)
this:
weak_reduction_simulation ((indRelRTPO TRel)\<inverse>) (STCal Source Target)

goal (1 subgoal):
 1. weak_reduction_simulation ((indRelRTPO TRel)\<inverse>) (STCal Source Target) \<Longrightarrow> operational_sound (TRel\<^sup>*) \<and> weak_reduction_simulation ((TRel\<^sup>+)\<inverse>) 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>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)\<inverse>) (STCal Source Target)
[PROOF STEP]
have "operational_sound (TRel\<^sup>*)"
[PROOF STATE]
proof (prove)
using this:
\<forall>S. SourceTerm S \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm (\<lbrakk>S\<rbrakk>)
\<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)\<inverse>) (STCal Source Target)

goal (1 subgoal):
 1. operational_sound (TRel\<^sup>*)
[PROOF STEP]
using weak_reduction_simulation_impl_OSou[where Rel="indRelRTPO TRel" and TRel="TRel"]
[PROOF STATE]
proof (prove)
using this:
\<forall>S. SourceTerm S \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm (\<lbrakk>S\<rbrakk>)
\<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)\<inverse>) (STCal Source Target)
(\<forall>S. SourceTerm S \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm (\<lbrakk>S\<rbrakk>)) \<and> (\<forall>S T. SourceTerm S \<lesssim>\<lbrakk>\<cdot>\<rbrakk>RT<TRel> TargetTerm T \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel\<^sup>*) \<and> weak_reduction_simulation ((indRelRTPO TRel)\<inverse>) (STCal Source Target) \<Longrightarrow> operational_sound (TRel\<^sup>*)

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

goal (1 subgoal):
 1. weak_reduction_simulation ((indRelRTPO TRel)\<inverse>) (STCal Source Target) \<Longrightarrow> operational_sound (TRel\<^sup>*) \<and> weak_reduction_simulation ((TRel\<^sup>+)\<inverse>) Target
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
operational_sound (TRel\<^sup>*)

goal (1 subgoal):
 1. weak_reduction_simulation ((indRelRTPO TRel)\<inverse>) (STCal Source Target) \<Longrightarrow> operational_sound (TRel\<^sup>*) \<and> weak_reduction_simulation ((TRel\<^sup>+)\<inverse>) Target
[PROOF STEP]
from sim
[PROOF STATE]
proof (chain)
picking this:
weak_reduction_simulation ((indRelRTPO TRel)\<inverse>) (STCal Source Target)
[PROOF STEP]
have "weak_reduction_simulation ((TRel\<^sup>+)\<inverse>) Target"
[PROOF STATE]
proof (prove)
using this:
weak_reduction_simulation ((indRelRTPO TRel)\<inverse>) (STCal Source Target)

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

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

goal (1 subgoal):
 1. weak_reduction_simulation ((indRelRTPO TRel)\<inverse>) (STCal Source Target) \<Longrightarrow> operational_sound (TRel\<^sup>*) \<and> weak_reduction_simulation ((TRel\<^sup>+)\<inverse>) Target
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
operational_sound (TRel\<^sup>*)
weak_reduction_simulation ((TRel\<^sup>+)\<inverse>) Target
[PROOF STEP]
show "operational_sound (TRel\<^sup>*) \<and> weak_reduction_simulation ((TRel\<^sup>+)\<inverse>) Target"
[PROOF STATE]
proof (prove)
using this:
operational_sound (TRel\<^sup>*)
weak_reduction_simulation ((TRel\<^sup>+)\<inverse>) Target

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

goal:
No subgoals!
[PROOF STEP]
qed