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

goal (2 subgoals):
 1. operational_corresponding TRel \<and> weak_reduction_bisimulation TRel Target \<Longrightarrow> weak_reduction_bisimulation (indRelTEQ TRel) (STCal Source Target)
 2. weak_reduction_bisimulation (indRelTEQ TRel) (STCal Source Target) \<Longrightarrow> operational_corresponding TRel \<and> weak_reduction_bisimulation TRel Target
[PROOF STEP]
show "weak_reduction_bisimulation (indRelTEQ TRel) (STCal Source Target)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. weak_reduction_bisimulation (indRelTEQ TRel) (STCal Source Target)
[PROOF STEP]
proof auto
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>P Q P'. P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q \<and> P \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. Q \<longmapsto>STCal Source Target* Q' \<and> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'
 2. \<And>P Q Q'. P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q \<and> Q \<longmapsto>STCal Source Target* Q' \<Longrightarrow> \<exists>P'. P \<longmapsto>STCal Source Target* P' \<and> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'
[PROOF STEP]
fix P Q P'
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>P Q P'. P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q \<and> P \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. Q \<longmapsto>STCal Source Target* Q' \<and> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'
 2. \<And>P Q Q'. P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q \<and> Q \<longmapsto>STCal Source Target* Q' \<Longrightarrow> \<exists>P'. P \<longmapsto>STCal Source Target* P' \<and> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'
[PROOF STEP]
assume "P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q" and "P \<longmapsto>(STCal Source Target)* P'"
[PROOF STATE]
proof (state)
this:
P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q
P \<longmapsto>STCal Source Target* P'

goal (2 subgoals):
 1. \<And>P Q P'. P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q \<and> P \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. Q \<longmapsto>STCal Source Target* Q' \<and> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'
 2. \<And>P Q Q'. P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q \<and> Q \<longmapsto>STCal Source Target* Q' \<Longrightarrow> \<exists>P'. P \<longmapsto>STCal Source Target* P' \<and> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'
[PROOF STEP]
thus "\<exists>Q'. Q \<longmapsto>(STCal Source Target)* Q' \<and> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'"
[PROOF STATE]
proof (prove)
using this:
P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q
P \<longmapsto>STCal Source Target* P'

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

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

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

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

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

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

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

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

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

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

goal (1 subgoal):
 1. P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> TargetTerm (\<lbrakk>S'\<rbrakk>)
[PROOF STEP]
by (simp add: indRelTEQ.encR)
[PROOF STATE]
proof (state)
this:
P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> TargetTerm (\<lbrakk>S'\<rbrakk>)

goal (1 subgoal):
 1. P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> TargetTerm T
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> TargetTerm (\<lbrakk>S'\<rbrakk>)

goal (1 subgoal):
 1. P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> TargetTerm T
[PROOF STEP]
from A4
[PROOF STATE]
proof (chain)
picking this:
(\<lbrakk>S'\<rbrakk>, T) \<in> TRel
[PROOF STEP]
have "TargetTerm (\<lbrakk>S'\<rbrakk>) \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> TargetTerm T"
[PROOF STATE]
proof (prove)
using this:
(\<lbrakk>S'\<rbrakk>, T) \<in> TRel

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

goal (1 subgoal):
 1. P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> TargetTerm T
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> TargetTerm (\<lbrakk>S'\<rbrakk>)
TargetTerm (\<lbrakk>S'\<rbrakk>) \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> TargetTerm T
[PROOF STEP]
show "P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> TargetTerm T"
[PROOF STATE]
proof (prove)
using this:
P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> TargetTerm (\<lbrakk>S'\<rbrakk>)
TargetTerm (\<lbrakk>S'\<rbrakk>) \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> TargetTerm T

goal (1 subgoal):
 1. P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> TargetTerm T
[PROOF STEP]
by (rule indRelTEQ.trans)
[PROOF STATE]
proof (state)
this:
P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> TargetTerm T

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> TargetTerm T

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

goal (1 subgoal):
 1. \<exists>Q'. TargetTerm (\<lbrakk>S\<rbrakk>) \<longmapsto>STCal Source Target* Q' \<and> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>Q'. TargetTerm (\<lbrakk>S\<rbrakk>) \<longmapsto>STCal Source Target* Q' \<and> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'

goal (3 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' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'
 2. \<And>T1 T2 P'. (T1, T2) \<in> TRel \<and> TargetTerm T1 \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. TargetTerm T2 \<longmapsto>STCal Source Target* Q' \<and> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'
 3. \<And>P Q R P'. \<lbrakk>P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q; \<And>P'. P \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. Q \<longmapsto>STCal Source Target* Q' \<and> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'; Q \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> R; \<And>P'. Q \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. R \<longmapsto>STCal Source Target* Q' \<and> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'; P \<longmapsto>STCal Source Target* P'\<rbrakk> \<Longrightarrow> \<exists>Q'. R \<longmapsto>STCal Source Target* Q' \<and> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 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' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'
 2. \<And>T1 T2 P'. (T1, T2) \<in> TRel \<and> TargetTerm T1 \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. TargetTerm T2 \<longmapsto>STCal Source Target* Q' \<and> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'
 3. \<And>P Q R P'. \<lbrakk>P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q; \<And>P'. P \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. Q \<longmapsto>STCal Source Target* Q' \<and> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'; Q \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> R; \<And>P'. Q \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. R \<longmapsto>STCal Source Target* Q' \<and> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'; P \<longmapsto>STCal Source Target* P'\<rbrakk> \<Longrightarrow> \<exists>Q'. R \<longmapsto>STCal Source Target* Q' \<and> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'
[PROOF STEP]
case (encL S)
[PROOF STATE]
proof (state)
this:
TargetTerm (\<lbrakk>S\<rbrakk>) \<longmapsto>STCal Source Target* P'

goal (3 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' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'
 2. \<And>T1 T2 P'. (T1, T2) \<in> TRel \<and> TargetTerm T1 \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. TargetTerm T2 \<longmapsto>STCal Source Target* Q' \<and> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'
 3. \<And>P Q R P'. \<lbrakk>P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q; \<And>P'. P \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. Q \<longmapsto>STCal Source Target* Q' \<and> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'; Q \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> R; \<And>P'. Q \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. R \<longmapsto>STCal Source Target* Q' \<and> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'; P \<longmapsto>STCal Source Target* P'\<rbrakk> \<Longrightarrow> \<exists>Q'. R \<longmapsto>STCal Source Target* Q' \<and> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'
[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 (3 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' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'
 2. \<And>T1 T2 P'. (T1, T2) \<in> TRel \<and> TargetTerm T1 \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. TargetTerm T2 \<longmapsto>STCal Source Target* Q' \<and> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'
 3. \<And>P Q R P'. \<lbrakk>P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q; \<And>P'. P \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. Q \<longmapsto>STCal Source Target* Q' \<and> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'; Q \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> R; \<And>P'. Q \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. R \<longmapsto>STCal Source Target* Q' \<and> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'; P \<longmapsto>STCal Source Target* P'\<rbrakk> \<Longrightarrow> \<exists>Q'. R \<longmapsto>STCal Source Target* Q' \<and> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
TargetTerm (\<lbrakk>S\<rbrakk>) \<longmapsto>STCal Source Target* P'
[PROOF STEP]
obtain T where B1: "\<lbrakk>S\<rbrakk> \<longmapsto>Target* T" and B2: "T \<in>T P'"
[PROOF STATE]
proof (prove)
using this:
TargetTerm (\<lbrakk>S\<rbrakk>) \<longmapsto>STCal Source Target* P'

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

goal (3 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' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'
 2. \<And>T1 T2 P'. (T1, T2) \<in> TRel \<and> TargetTerm T1 \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. TargetTerm T2 \<longmapsto>STCal Source Target* Q' \<and> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'
 3. \<And>P Q R P'. \<lbrakk>P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q; \<And>P'. P \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. Q \<longmapsto>STCal Source Target* Q' \<and> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'; Q \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> R; \<And>P'. Q \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. R \<longmapsto>STCal Source Target* Q' \<and> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'; P \<longmapsto>STCal Source Target* P'\<rbrakk> \<Longrightarrow> \<exists>Q'. R \<longmapsto>STCal Source Target* Q' \<and> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'
[PROOF STEP]
from B1 oc
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>S\<rbrakk> \<longmapsto>Target* T
operational_corresponding TRel
[PROOF STEP]
obtain S' where B3: "S \<longmapsto>Source* S'" and B4: "(\<lbrakk>S'\<rbrakk>, T) \<in> TRel"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>S\<rbrakk> \<longmapsto>Target* T
operational_corresponding TRel

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

goal (3 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' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'
 2. \<And>T1 T2 P'. (T1, T2) \<in> TRel \<and> TargetTerm T1 \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. TargetTerm T2 \<longmapsto>STCal Source Target* Q' \<and> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'
 3. \<And>P Q R P'. \<lbrakk>P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q; \<And>P'. P \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. Q \<longmapsto>STCal Source Target* Q' \<and> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'; Q \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> R; \<And>P'. Q \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. R \<longmapsto>STCal Source Target* Q' \<and> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'; P \<longmapsto>STCal Source Target* P'\<rbrakk> \<Longrightarrow> \<exists>Q'. R \<longmapsto>STCal Source Target* Q' \<and> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'
[PROOF STEP]
from B3
[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 (3 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' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'
 2. \<And>T1 T2 P'. (T1, T2) \<in> TRel \<and> TargetTerm T1 \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. TargetTerm T2 \<longmapsto>STCal Source Target* Q' \<and> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'
 3. \<And>P Q R P'. \<lbrakk>P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q; \<And>P'. P \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. Q \<longmapsto>STCal Source Target* Q' \<and> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'; Q \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> R; \<And>P'. Q \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. R \<longmapsto>STCal Source Target* Q' \<and> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'; P \<longmapsto>STCal Source Target* P'\<rbrakk> \<Longrightarrow> \<exists>Q'. R \<longmapsto>STCal Source Target* Q' \<and> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
SourceTerm S \<longmapsto>STCal Source Target* SourceTerm S'

goal (3 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' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'
 2. \<And>T1 T2 P'. (T1, T2) \<in> TRel \<and> TargetTerm T1 \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. TargetTerm T2 \<longmapsto>STCal Source Target* Q' \<and> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'
 3. \<And>P Q R P'. \<lbrakk>P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q; \<And>P'. P \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. Q \<longmapsto>STCal Source Target* Q' \<and> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'; Q \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> R; \<And>P'. Q \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. R \<longmapsto>STCal Source Target* Q' \<and> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'; P \<longmapsto>STCal Source Target* P'\<rbrakk> \<Longrightarrow> \<exists>Q'. R \<longmapsto>STCal Source Target* Q' \<and> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'
[PROOF STEP]
have "P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> SourceTerm S'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> SourceTerm S'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> SourceTerm S'
[PROOF STEP]
from B4 eqT
[PROOF STATE]
proof (chain)
picking this:
(\<lbrakk>S'\<rbrakk>, T) \<in> TRel
equivalence TRel
[PROOF STEP]
have "(T, \<lbrakk>S'\<rbrakk>) \<in> TRel"
[PROOF STATE]
proof (prove)
using this:
(\<lbrakk>S'\<rbrakk>, T) \<in> TRel
equivalence TRel

goal (1 subgoal):
 1. (T, \<lbrakk>S'\<rbrakk>) \<in> TRel
[PROOF STEP]
unfolding equiv_def sym_def
[PROOF STATE]
proof (prove)
using this:
(\<lbrakk>S'\<rbrakk>, T) \<in> TRel
refl TRel \<and> (\<forall>x y. (x, y) \<in> TRel \<longrightarrow> (y, x) \<in> TRel) \<and> trans TRel

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

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

goal (1 subgoal):
 1. P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> TargetTerm (\<lbrakk>S'\<rbrakk>)
[PROOF STEP]
by (simp add: indRelTEQ.target)
[PROOF STATE]
proof (state)
this:
P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> TargetTerm (\<lbrakk>S'\<rbrakk>)

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

goal (1 subgoal):
 1. P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> SourceTerm S'
[PROOF STEP]
have "TargetTerm (\<lbrakk>S'\<rbrakk>) \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> SourceTerm S'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. TargetTerm (\<lbrakk>S'\<rbrakk>) \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> SourceTerm S'
[PROOF STEP]
by (rule indRelTEQ.encL)
[PROOF STATE]
proof (state)
this:
TargetTerm (\<lbrakk>S'\<rbrakk>) \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> SourceTerm S'

goal (1 subgoal):
 1. P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> SourceTerm S'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> TargetTerm (\<lbrakk>S'\<rbrakk>)
TargetTerm (\<lbrakk>S'\<rbrakk>) \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> SourceTerm S'
[PROOF STEP]
show "P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> SourceTerm S'"
[PROOF STATE]
proof (prove)
using this:
P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> TargetTerm (\<lbrakk>S'\<rbrakk>)
TargetTerm (\<lbrakk>S'\<rbrakk>) \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> SourceTerm S'

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

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

goal (3 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' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'
 2. \<And>T1 T2 P'. (T1, T2) \<in> TRel \<and> TargetTerm T1 \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. TargetTerm T2 \<longmapsto>STCal Source Target* Q' \<and> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'
 3. \<And>P Q R P'. \<lbrakk>P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q; \<And>P'. P \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. Q \<longmapsto>STCal Source Target* Q' \<and> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'; Q \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> R; \<And>P'. Q \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. R \<longmapsto>STCal Source Target* Q' \<and> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'; P \<longmapsto>STCal Source Target* P'\<rbrakk> \<Longrightarrow> \<exists>Q'. R \<longmapsto>STCal Source Target* Q' \<and> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
SourceTerm S \<longmapsto>STCal Source Target* SourceTerm S'
P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> SourceTerm S'
[PROOF STEP]
show "\<exists>Q'. SourceTerm S \<longmapsto>(STCal Source Target)* Q' \<and> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'"
[PROOF STATE]
proof (prove)
using this:
SourceTerm S \<longmapsto>STCal Source Target* SourceTerm S'
P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> SourceTerm S'

goal (1 subgoal):
 1. \<exists>Q'. SourceTerm S \<longmapsto>STCal Source Target* Q' \<and> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>Q'. SourceTerm S \<longmapsto>STCal Source Target* Q' \<and> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'

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

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

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

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

goal (2 subgoals):
 1. \<And>T1 T2 P'. (T1, T2) \<in> TRel \<and> TargetTerm T1 \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. TargetTerm T2 \<longmapsto>STCal Source Target* Q' \<and> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'
 2. \<And>P Q R P'. \<lbrakk>P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q; \<And>P'. P \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. Q \<longmapsto>STCal Source Target* Q' \<and> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'; Q \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> R; \<And>P'. Q \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. R \<longmapsto>STCal Source Target* Q' \<and> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'; P \<longmapsto>STCal Source Target* P'\<rbrakk> \<Longrightarrow> \<exists>Q'. R \<longmapsto>STCal Source Target* Q' \<and> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'
[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 T1 \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. TargetTerm T2 \<longmapsto>STCal Source Target* Q' \<and> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'
 2. \<And>P Q R P'. \<lbrakk>P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q; \<And>P'. P \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. Q \<longmapsto>STCal Source Target* Q' \<and> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'; Q \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> R; \<And>P'. Q \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. R \<longmapsto>STCal Source Target* Q' \<and> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'; P \<longmapsto>STCal Source Target* P'\<rbrakk> \<Longrightarrow> \<exists>Q'. R \<longmapsto>STCal Source Target* Q' \<and> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'
[PROOF STEP]
with C1 bisimT
[PROOF STATE]
proof (chain)
picking this:
T1 \<longmapsto>Target* T1'
weak_reduction_bisimulation TRel Target
(T1, T2) \<in> TRel
[PROOF STEP]
obtain T2' where C3: "T2 \<longmapsto>Target* T2'" and C4: "(T1', T2') \<in> TRel"
[PROOF STATE]
proof (prove)
using this:
T1 \<longmapsto>Target* T1'
weak_reduction_bisimulation TRel Target
(T1, T2) \<in> TRel

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

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

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

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

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

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

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

goal (1 subgoal):
 1. \<exists>Q'. TargetTerm T2 \<longmapsto>STCal Source Target* Q' \<and> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>Q'. TargetTerm T2 \<longmapsto>STCal Source Target* Q' \<and> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'

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

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

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

goal (1 subgoal):
 1. (\<And>Q'. Q \<longmapsto>STCal Source Target* Q' \<and> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Q \<longmapsto>STCal Source Target* Q'
P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'

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

goal (1 subgoal):
 1. \<And>P Q R P'. \<lbrakk>P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q; \<And>P'. P \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. Q \<longmapsto>STCal Source Target* Q' \<and> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'; Q \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> R; \<And>P'. Q \<longmapsto>STCal Source Target* P' \<Longrightarrow> \<exists>Q'. R \<longmapsto>STCal Source Target* Q' \<and> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'; P \<longmapsto>STCal Source Target* P'\<rbrakk> \<Longrightarrow> \<exists>Q'. R \<longmapsto>STCal Source Target* Q' \<and> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'
[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>R'. R \<longmapsto>STCal Source Target* R' \<and> ?Q'3 \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> R'
[PROOF STEP]
obtain R' where D3: "R \<longmapsto>(STCal Source Target)* R'" and D4: "Q' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> R'"
[PROOF STATE]
proof (prove)
using this:
Q \<longmapsto>STCal Source Target* Q'
Q \<longmapsto>STCal Source Target* ?Q'3 \<Longrightarrow> \<exists>R'. R \<longmapsto>STCal Source Target* R' \<and> ?Q'3 \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> R'

goal (1 subgoal):
 1. (\<And>R'. R \<longmapsto>STCal Source Target* R' \<and> Q' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> R' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
R \<longmapsto>STCal Source Target* R'
Q' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> R'

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

goal (1 subgoal):
 1. P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> R'
[PROOF STEP]
by (rule indRelTEQ.trans)
[PROOF STATE]
proof (state)
this:
P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> R'

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

goal (1 subgoal):
 1. \<exists>R'. R \<longmapsto>STCal Source Target* R' \<and> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> R'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>R'. R \<longmapsto>STCal Source Target* R' \<and> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> R'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>Q'. Q \<longmapsto>STCal Source Target* Q' \<and> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'

goal (1 subgoal):
 1. \<And>P Q Q'. P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q \<and> Q \<longmapsto>STCal Source Target* Q' \<Longrightarrow> \<exists>P'. P \<longmapsto>STCal Source Target* P' \<and> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>P Q Q'. P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q \<and> Q \<longmapsto>STCal Source Target* Q' \<Longrightarrow> \<exists>P'. P \<longmapsto>STCal Source Target* P' \<and> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'
[PROOF STEP]
fix P Q Q'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>P Q Q'. P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q \<and> Q \<longmapsto>STCal Source Target* Q' \<Longrightarrow> \<exists>P'. P \<longmapsto>STCal Source Target* P' \<and> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'
[PROOF STEP]
assume "P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q" and "Q \<longmapsto>(STCal Source Target)* Q'"
[PROOF STATE]
proof (state)
this:
P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q
Q \<longmapsto>STCal Source Target* Q'

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

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

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

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

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

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

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

goal (4 subgoals):
 1. \<And>S Q'. TargetTerm (\<lbrakk>S\<rbrakk>) \<longmapsto>STCal Source Target* Q' \<Longrightarrow> \<exists>P'. SourceTerm S \<longmapsto>STCal Source Target* P' \<and> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'
 2. \<And>S Q'. SourceTerm S \<longmapsto>STCal Source Target* Q' \<Longrightarrow> \<exists>P'. TargetTerm (\<lbrakk>S\<rbrakk>) \<longmapsto>STCal Source Target* P' \<and> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'
 3. \<And>T1 T2 Q'. (T1, T2) \<in> TRel \<and> TargetTerm T2 \<longmapsto>STCal Source Target* Q' \<Longrightarrow> \<exists>P'. TargetTerm T1 \<longmapsto>STCal Source Target* P' \<and> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'
 4. \<And>P Q R Q'. \<lbrakk>P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q; \<And>Q'. Q \<longmapsto>STCal Source Target* Q' \<Longrightarrow> \<exists>P'. P \<longmapsto>STCal Source Target* P' \<and> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'; Q \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> R; \<And>Q'. R \<longmapsto>STCal Source Target* Q' \<Longrightarrow> \<exists>P'. Q \<longmapsto>STCal Source Target* P' \<and> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'; R \<longmapsto>STCal Source Target* Q'\<rbrakk> \<Longrightarrow> \<exists>P'. P \<longmapsto>STCal Source Target* P' \<and> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'
[PROOF STEP]
from E3
[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 Q'. TargetTerm (\<lbrakk>S\<rbrakk>) \<longmapsto>STCal Source Target* Q' \<Longrightarrow> \<exists>P'. SourceTerm S \<longmapsto>STCal Source Target* P' \<and> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'
 2. \<And>S Q'. SourceTerm S \<longmapsto>STCal Source Target* Q' \<Longrightarrow> \<exists>P'. TargetTerm (\<lbrakk>S\<rbrakk>) \<longmapsto>STCal Source Target* P' \<and> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'
 3. \<And>T1 T2 Q'. (T1, T2) \<in> TRel \<and> TargetTerm T2 \<longmapsto>STCal Source Target* Q' \<Longrightarrow> \<exists>P'. TargetTerm T1 \<longmapsto>STCal Source Target* P' \<and> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'
 4. \<And>P Q R Q'. \<lbrakk>P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q; \<And>Q'. Q \<longmapsto>STCal Source Target* Q' \<Longrightarrow> \<exists>P'. P \<longmapsto>STCal Source Target* P' \<and> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'; Q \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> R; \<And>Q'. R \<longmapsto>STCal Source Target* Q' \<Longrightarrow> \<exists>P'. Q \<longmapsto>STCal Source Target* P' \<and> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'; R \<longmapsto>STCal Source Target* Q'\<rbrakk> \<Longrightarrow> \<exists>P'. P \<longmapsto>STCal Source Target* P' \<and> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
SourceTerm S \<longmapsto>STCal Source Target* SourceTerm S'

goal (4 subgoals):
 1. \<And>S Q'. TargetTerm (\<lbrakk>S\<rbrakk>) \<longmapsto>STCal Source Target* Q' \<Longrightarrow> \<exists>P'. SourceTerm S \<longmapsto>STCal Source Target* P' \<and> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'
 2. \<And>S Q'. SourceTerm S \<longmapsto>STCal Source Target* Q' \<Longrightarrow> \<exists>P'. TargetTerm (\<lbrakk>S\<rbrakk>) \<longmapsto>STCal Source Target* P' \<and> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'
 3. \<And>T1 T2 Q'. (T1, T2) \<in> TRel \<and> TargetTerm T2 \<longmapsto>STCal Source Target* Q' \<Longrightarrow> \<exists>P'. TargetTerm T1 \<longmapsto>STCal Source Target* P' \<and> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'
 4. \<And>P Q R Q'. \<lbrakk>P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q; \<And>Q'. Q \<longmapsto>STCal Source Target* Q' \<Longrightarrow> \<exists>P'. P \<longmapsto>STCal Source Target* P' \<and> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'; Q \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> R; \<And>Q'. R \<longmapsto>STCal Source Target* Q' \<Longrightarrow> \<exists>P'. Q \<longmapsto>STCal Source Target* P' \<and> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'; R \<longmapsto>STCal Source Target* Q'\<rbrakk> \<Longrightarrow> \<exists>P'. P \<longmapsto>STCal Source Target* P' \<and> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'
[PROOF STEP]
have "SourceTerm S' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. SourceTerm S' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. SourceTerm S' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'
[PROOF STEP]
have "SourceTerm S' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> TargetTerm (\<lbrakk>S'\<rbrakk>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. SourceTerm S' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> TargetTerm (\<lbrakk>S'\<rbrakk>)
[PROOF STEP]
by (rule indRelTEQ.encR)
[PROOF STATE]
proof (state)
this:
SourceTerm S' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> TargetTerm (\<lbrakk>S'\<rbrakk>)

goal (1 subgoal):
 1. SourceTerm S' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
SourceTerm S' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> TargetTerm (\<lbrakk>S'\<rbrakk>)

goal (1 subgoal):
 1. SourceTerm S' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'
[PROOF STEP]
from E2 E4
[PROOF STATE]
proof (chain)
picking this:
T \<in>T Q'
(\<lbrakk>S'\<rbrakk>, T) \<in> TRel
[PROOF STEP]
have "TargetTerm (\<lbrakk>S'\<rbrakk>) \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'"
[PROOF STATE]
proof (prove)
using this:
T \<in>T Q'
(\<lbrakk>S'\<rbrakk>, T) \<in> TRel

goal (1 subgoal):
 1. TargetTerm (\<lbrakk>S'\<rbrakk>) \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'
[PROOF STEP]
by (simp add: indRelTEQ.target)
[PROOF STATE]
proof (state)
this:
TargetTerm (\<lbrakk>S'\<rbrakk>) \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'

goal (1 subgoal):
 1. SourceTerm S' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
SourceTerm S' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> TargetTerm (\<lbrakk>S'\<rbrakk>)
TargetTerm (\<lbrakk>S'\<rbrakk>) \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'
[PROOF STEP]
show "SourceTerm S' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'"
[PROOF STATE]
proof (prove)
using this:
SourceTerm S' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> TargetTerm (\<lbrakk>S'\<rbrakk>)
TargetTerm (\<lbrakk>S'\<rbrakk>) \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'

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

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

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

goal (1 subgoal):
 1. \<exists>P'. SourceTerm S \<longmapsto>STCal Source Target* P' \<and> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>P'. SourceTerm S \<longmapsto>STCal Source Target* P' \<and> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'

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

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

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

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

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

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

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

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

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

goal (3 subgoals):
 1. \<And>S Q'. SourceTerm S \<longmapsto>STCal Source Target* Q' \<Longrightarrow> \<exists>P'. TargetTerm (\<lbrakk>S\<rbrakk>) \<longmapsto>STCal Source Target* P' \<and> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'
 2. \<And>T1 T2 Q'. (T1, T2) \<in> TRel \<and> TargetTerm T2 \<longmapsto>STCal Source Target* Q' \<Longrightarrow> \<exists>P'. TargetTerm T1 \<longmapsto>STCal Source Target* P' \<and> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'
 3. \<And>P Q R Q'. \<lbrakk>P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q; \<And>Q'. Q \<longmapsto>STCal Source Target* Q' \<Longrightarrow> \<exists>P'. P \<longmapsto>STCal Source Target* P' \<and> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'; Q \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> R; \<And>Q'. R \<longmapsto>STCal Source Target* Q' \<Longrightarrow> \<exists>P'. Q \<longmapsto>STCal Source Target* P' \<and> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'; R \<longmapsto>STCal Source Target* Q'\<rbrakk> \<Longrightarrow> \<exists>P'. P \<longmapsto>STCal Source Target* P' \<and> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'
[PROOF STEP]
have "TargetTerm T \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. TargetTerm T \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. TargetTerm T \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'
[PROOF STEP]
from F4 eqT
[PROOF STATE]
proof (chain)
picking this:
(\<lbrakk>S'\<rbrakk>, T) \<in> TRel
equivalence TRel
[PROOF STEP]
have "(T, \<lbrakk>S'\<rbrakk>) \<in> TRel"
[PROOF STATE]
proof (prove)
using this:
(\<lbrakk>S'\<rbrakk>, T) \<in> TRel
equivalence TRel

goal (1 subgoal):
 1. (T, \<lbrakk>S'\<rbrakk>) \<in> TRel
[PROOF STEP]
unfolding equiv_def sym_def
[PROOF STATE]
proof (prove)
using this:
(\<lbrakk>S'\<rbrakk>, T) \<in> TRel
refl TRel \<and> (\<forall>x y. (x, y) \<in> TRel \<longrightarrow> (y, x) \<in> TRel) \<and> trans TRel

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

goal (1 subgoal):
 1. TargetTerm T \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'
[PROOF STEP]
hence "TargetTerm T \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> TargetTerm (\<lbrakk>S'\<rbrakk>)"
[PROOF STATE]
proof (prove)
using this:
(T, \<lbrakk>S'\<rbrakk>) \<in> TRel

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

goal (1 subgoal):
 1. TargetTerm T \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
TargetTerm T \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> TargetTerm (\<lbrakk>S'\<rbrakk>)

goal (1 subgoal):
 1. TargetTerm T \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'
[PROOF STEP]
from F2
[PROOF STATE]
proof (chain)
picking this:
S' \<in>S Q'
[PROOF STEP]
have "TargetTerm (\<lbrakk>S'\<rbrakk>) \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'"
[PROOF STATE]
proof (prove)
using this:
S' \<in>S Q'

goal (1 subgoal):
 1. TargetTerm (\<lbrakk>S'\<rbrakk>) \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'
[PROOF STEP]
by (simp add: indRelTEQ.encL)
[PROOF STATE]
proof (state)
this:
TargetTerm (\<lbrakk>S'\<rbrakk>) \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'

goal (1 subgoal):
 1. TargetTerm T \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
TargetTerm T \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> TargetTerm (\<lbrakk>S'\<rbrakk>)
TargetTerm (\<lbrakk>S'\<rbrakk>) \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'
[PROOF STEP]
show "TargetTerm T \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'"
[PROOF STATE]
proof (prove)
using this:
TargetTerm T \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> TargetTerm (\<lbrakk>S'\<rbrakk>)
TargetTerm (\<lbrakk>S'\<rbrakk>) \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'

goal (1 subgoal):
 1. TargetTerm T \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'
[PROOF STEP]
by (rule indRelTEQ.trans)
[PROOF STATE]
proof (state)
this:
TargetTerm T \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
TargetTerm T \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'

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

goal (1 subgoal):
 1. \<exists>P'. TargetTerm (\<lbrakk>S\<rbrakk>) \<longmapsto>STCal Source Target* P' \<and> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>P'. TargetTerm (\<lbrakk>S\<rbrakk>) \<longmapsto>STCal Source Target* P' \<and> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'

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

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

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

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

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

goal (2 subgoals):
 1. \<And>T1 T2 Q'. (T1, T2) \<in> TRel \<and> TargetTerm T2 \<longmapsto>STCal Source Target* Q' \<Longrightarrow> \<exists>P'. TargetTerm T1 \<longmapsto>STCal Source Target* P' \<and> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'
 2. \<And>P Q R Q'. \<lbrakk>P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q; \<And>Q'. Q \<longmapsto>STCal Source Target* Q' \<Longrightarrow> \<exists>P'. P \<longmapsto>STCal Source Target* P' \<and> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'; Q \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> R; \<And>Q'. R \<longmapsto>STCal Source Target* Q' \<Longrightarrow> \<exists>P'. Q \<longmapsto>STCal Source Target* P' \<and> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'; R \<longmapsto>STCal Source Target* Q'\<rbrakk> \<Longrightarrow> \<exists>P'. P \<longmapsto>STCal Source Target* P' \<and> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'
[PROOF STEP]
with G1 bisimT
[PROOF STATE]
proof (chain)
picking this:
T2 \<longmapsto>Target* T2'
weak_reduction_bisimulation TRel Target
(T1, T2) \<in> TRel
[PROOF STEP]
obtain T1' where G3: "T1 \<longmapsto>Target* T1'" and G4: "(T1', T2') \<in> TRel"
[PROOF STATE]
proof (prove)
using this:
T2 \<longmapsto>Target* T2'
weak_reduction_bisimulation TRel Target
(T1, T2) \<in> TRel

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

goal (2 subgoals):
 1. \<And>T1 T2 Q'. (T1, T2) \<in> TRel \<and> TargetTerm T2 \<longmapsto>STCal Source Target* Q' \<Longrightarrow> \<exists>P'. TargetTerm T1 \<longmapsto>STCal Source Target* P' \<and> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'
 2. \<And>P Q R Q'. \<lbrakk>P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q; \<And>Q'. Q \<longmapsto>STCal Source Target* Q' \<Longrightarrow> \<exists>P'. P \<longmapsto>STCal Source Target* P' \<and> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'; Q \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> R; \<And>Q'. R \<longmapsto>STCal Source Target* Q' \<Longrightarrow> \<exists>P'. Q \<longmapsto>STCal Source Target* P' \<and> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'; R \<longmapsto>STCal Source Target* Q'\<rbrakk> \<Longrightarrow> \<exists>P'. P \<longmapsto>STCal Source Target* P' \<and> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'
[PROOF STEP]
from G3
[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 Q'. (T1, T2) \<in> TRel \<and> TargetTerm T2 \<longmapsto>STCal Source Target* Q' \<Longrightarrow> \<exists>P'. TargetTerm T1 \<longmapsto>STCal Source Target* P' \<and> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'
 2. \<And>P Q R Q'. \<lbrakk>P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q; \<And>Q'. Q \<longmapsto>STCal Source Target* Q' \<Longrightarrow> \<exists>P'. P \<longmapsto>STCal Source Target* P' \<and> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'; Q \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> R; \<And>Q'. R \<longmapsto>STCal Source Target* Q' \<Longrightarrow> \<exists>P'. Q \<longmapsto>STCal Source Target* P' \<and> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'; R \<longmapsto>STCal Source Target* Q'\<rbrakk> \<Longrightarrow> \<exists>P'. P \<longmapsto>STCal Source Target* P' \<and> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
TargetTerm T1 \<longmapsto>STCal Source Target* TargetTerm T1'

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

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

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

goal (1 subgoal):
 1. \<exists>P'. TargetTerm T1 \<longmapsto>STCal Source Target* P' \<and> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>P'. TargetTerm T1 \<longmapsto>STCal Source Target* P' \<and> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'

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

goal (1 subgoal):
 1. \<And>P Q R Q'. \<lbrakk>P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q; \<And>Q'. Q \<longmapsto>STCal Source Target* Q' \<Longrightarrow> \<exists>P'. P \<longmapsto>STCal Source Target* P' \<and> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'; Q \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> R; \<And>Q'. R \<longmapsto>STCal Source Target* Q' \<Longrightarrow> \<exists>P'. Q \<longmapsto>STCal Source Target* P' \<and> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'; R \<longmapsto>STCal Source Target* Q'\<rbrakk> \<Longrightarrow> \<exists>P'. P \<longmapsto>STCal Source Target* P' \<and> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'
[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> Q' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> R'"
[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> Q' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> ?R'3

goal (1 subgoal):
 1. \<And>P Q R Q'. \<lbrakk>P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q; \<And>Q'. Q \<longmapsto>STCal Source Target* Q' \<Longrightarrow> \<exists>P'. P \<longmapsto>STCal Source Target* P' \<and> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'; Q \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> R; \<And>Q'. R \<longmapsto>STCal Source Target* Q' \<Longrightarrow> \<exists>P'. Q \<longmapsto>STCal Source Target* P' \<and> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'; R \<longmapsto>STCal Source Target* Q'\<rbrakk> \<Longrightarrow> \<exists>P'. P \<longmapsto>STCal Source Target* P' \<and> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'
[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> Q' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> ?R'3
[PROOF STEP]
obtain Q' where H1: "Q \<longmapsto>(STCal Source Target)* Q'" and H2: "Q' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> R'"
[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> Q' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> ?R'3

goal (1 subgoal):
 1. (\<And>Q'. Q \<longmapsto>STCal Source Target* Q' \<and> Q' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> R' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Q \<longmapsto>STCal Source Target* Q'
Q' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> R'

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

goal (1 subgoal):
 1. \<And>P Q R Q'. \<lbrakk>P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q; \<And>Q'. Q \<longmapsto>STCal Source Target* Q' \<Longrightarrow> \<exists>P'. P \<longmapsto>STCal Source Target* P' \<and> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'; Q \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> R; \<And>Q'. R \<longmapsto>STCal Source Target* Q' \<Longrightarrow> \<exists>P'. Q \<longmapsto>STCal Source Target* P' \<and> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'; R \<longmapsto>STCal Source Target* Q'\<rbrakk> \<Longrightarrow> \<exists>P'. P \<longmapsto>STCal Source Target* P' \<and> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'
[PROOF STEP]
with H1
[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> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> ?Q'3
[PROOF STEP]
obtain P' where H3: "P \<longmapsto>(STCal Source Target)* P'" and H4: "P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'"
[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> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> ?Q'3

goal (1 subgoal):
 1. (\<And>P'. P \<longmapsto>STCal Source Target* P' \<and> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
P \<longmapsto>STCal Source Target* P'
P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'

goal (1 subgoal):
 1. \<And>P Q R Q'. \<lbrakk>P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q; \<And>Q'. Q \<longmapsto>STCal Source Target* Q' \<Longrightarrow> \<exists>P'. P \<longmapsto>STCal Source Target* P' \<and> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'; Q \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> R; \<And>Q'. R \<longmapsto>STCal Source Target* Q' \<Longrightarrow> \<exists>P'. Q \<longmapsto>STCal Source Target* P' \<and> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'; R \<longmapsto>STCal Source Target* Q'\<rbrakk> \<Longrightarrow> \<exists>P'. P \<longmapsto>STCal Source Target* P' \<and> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'
[PROOF STEP]
from H4 H2
[PROOF STATE]
proof (chain)
picking this:
P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'
Q' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> R'
[PROOF STEP]
have "P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> R'"
[PROOF STATE]
proof (prove)
using this:
P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'
Q' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> R'

goal (1 subgoal):
 1. P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> R'
[PROOF STEP]
by (rule indRelTEQ.trans)
[PROOF STATE]
proof (state)
this:
P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> R'

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

goal (1 subgoal):
 1. \<exists>P'. P \<longmapsto>STCal Source Target* P' \<and> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> R'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>P'. P \<longmapsto>STCal Source Target* P' \<and> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> R'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>P'. P \<longmapsto>STCal Source Target* P' \<and> P' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
weak_reduction_bisimulation (indRelTEQ TRel) (STCal Source Target)

goal (1 subgoal):
 1. weak_reduction_bisimulation (indRelTEQ TRel) (STCal Source Target) \<Longrightarrow> operational_corresponding TRel \<and> weak_reduction_bisimulation TRel Target
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. weak_reduction_bisimulation (indRelTEQ TRel) (STCal Source Target) \<Longrightarrow> operational_corresponding TRel \<and> weak_reduction_bisimulation TRel Target
[PROOF STEP]
assume bisim: "weak_reduction_bisimulation (indRelTEQ TRel) (STCal Source Target)"
[PROOF STATE]
proof (state)
this:
weak_reduction_bisimulation (indRelTEQ TRel) (STCal Source Target)

goal (1 subgoal):
 1. weak_reduction_bisimulation (indRelTEQ TRel) (STCal Source Target) \<Longrightarrow> operational_corresponding TRel \<and> weak_reduction_bisimulation TRel Target
[PROOF STEP]
have "operational_corresponding TRel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. operational_corresponding TRel
[PROOF STEP]
proof auto
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>S S'. S \<longmapsto>Source* S' \<Longrightarrow> \<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target* T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel
 2. \<And>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target* T \<Longrightarrow> \<exists>S'. S \<longmapsto>Source* S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel
[PROOF STEP]
fix S S'
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>S S'. S \<longmapsto>Source* S' \<Longrightarrow> \<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target* T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel
 2. \<And>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target* T \<Longrightarrow> \<exists>S'. S \<longmapsto>Source* S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel
[PROOF STEP]
have "SourceTerm S \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> TargetTerm (\<lbrakk>S\<rbrakk>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. SourceTerm S \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> TargetTerm (\<lbrakk>S\<rbrakk>)
[PROOF STEP]
by (rule indRelTEQ.encR)
[PROOF STATE]
proof (state)
this:
SourceTerm S \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> TargetTerm (\<lbrakk>S\<rbrakk>)

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

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

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

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

goal (2 subgoals):
 1. \<And>S S'. S \<longmapsto>Source* S' \<Longrightarrow> \<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target* T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel
 2. \<And>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target* T \<Longrightarrow> \<exists>S'. S \<longmapsto>Source* S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
SourceTerm S \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> TargetTerm (\<lbrakk>S\<rbrakk>)
SourceTerm S \<longmapsto>STCal Source Target* SourceTerm S'
[PROOF STEP]
obtain Q' where I1: "TargetTerm (\<lbrakk>S\<rbrakk>) \<longmapsto>(STCal Source Target)* Q'"
                           and I2: "SourceTerm S' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'"
[PROOF STATE]
proof (prove)
using this:
SourceTerm S \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> TargetTerm (\<lbrakk>S\<rbrakk>)
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' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using bisim
[PROOF STATE]
proof (prove)
using this:
SourceTerm S \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> TargetTerm (\<lbrakk>S\<rbrakk>)
SourceTerm S \<longmapsto>STCal Source Target* SourceTerm S'
weak_reduction_bisimulation (indRelTEQ TRel) (STCal Source Target)

goal (1 subgoal):
 1. (\<And>Q'. TargetTerm (\<lbrakk>S\<rbrakk>) \<longmapsto>STCal Source Target* Q' \<and> SourceTerm S' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
TargetTerm (\<lbrakk>S\<rbrakk>) \<longmapsto>STCal Source Target* Q'
SourceTerm S' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'

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

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

goal (2 subgoals):
 1. \<And>S S'. S \<longmapsto>Source* S' \<Longrightarrow> \<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target* T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel
 2. \<And>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target* T \<Longrightarrow> \<exists>S'. S \<longmapsto>Source* S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel
[PROOF STEP]
from eqT
[PROOF STATE]
proof (chain)
picking this:
equivalence TRel
[PROOF STEP]
have "TRel\<^sup>* = TRel"
[PROOF STATE]
proof (prove)
using this:
equivalence TRel

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

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

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

goal (2 subgoals):
 1. \<And>S S'. S \<longmapsto>Source* S' \<Longrightarrow> \<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target* T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel
 2. \<And>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target* T \<Longrightarrow> \<exists>S'. S \<longmapsto>Source* S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel
[PROOF STEP]
with I2 I4
[PROOF STATE]
proof (chain)
picking this:
SourceTerm S' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'
T \<in>T Q'
TRel\<^sup>* = TRel
[PROOF STEP]
have "(\<lbrakk>S'\<rbrakk>, T) \<in> TRel"
[PROOF STATE]
proof (prove)
using this:
SourceTerm S' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'
T \<in>T Q'
TRel\<^sup>* = TRel

goal (1 subgoal):
 1. (\<lbrakk>S'\<rbrakk>, T) \<in> TRel
[PROOF STEP]
using indRelTEQ_to_TRel(2)[where TRel="TRel"]
              trans_closure_of_TRel_refl_cond[where TRel="TRel"]
[PROOF STATE]
proof (prove)
using this:
SourceTerm S' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q'
T \<in>T Q'
TRel\<^sup>* = TRel
?P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<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. (\<lbrakk>S'\<rbrakk>, T) \<in> TRel
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<lbrakk>S'\<rbrakk>, T) \<in> TRel

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

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

goal (1 subgoal):
 1. \<And>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target* T \<Longrightarrow> \<exists>S'. S \<longmapsto>Source* S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target* T \<Longrightarrow> \<exists>S'. S \<longmapsto>Source* S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel
[PROOF STEP]
fix S T
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target* T \<Longrightarrow> \<exists>S'. S \<longmapsto>Source* S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel
[PROOF STEP]
have "SourceTerm S \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> TargetTerm (\<lbrakk>S\<rbrakk>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. SourceTerm S \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> TargetTerm (\<lbrakk>S\<rbrakk>)
[PROOF STEP]
by (rule indRelTEQ.encR)
[PROOF STATE]
proof (state)
this:
SourceTerm S \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> TargetTerm (\<lbrakk>S\<rbrakk>)

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

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

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

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

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

goal (1 subgoal):
 1. (\<And>Q'. SourceTerm S \<longmapsto>STCal Source Target* Q' \<and> Q' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> TargetTerm T \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using bisim
[PROOF STATE]
proof (prove)
using this:
SourceTerm S \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> TargetTerm (\<lbrakk>S\<rbrakk>)
TargetTerm (\<lbrakk>S\<rbrakk>) \<longmapsto>STCal Source Target* TargetTerm T
weak_reduction_bisimulation (indRelTEQ TRel) (STCal Source Target)

goal (1 subgoal):
 1. (\<And>Q'. SourceTerm S \<longmapsto>STCal Source Target* Q' \<and> Q' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> TargetTerm T \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
SourceTerm S \<longmapsto>STCal Source Target* Q'
Q' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> TargetTerm T

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

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

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

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

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

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

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

goal (1 subgoal):
 1. (\<lbrakk>S'\<rbrakk>, T) \<in> TRel
[PROOF STEP]
using indRelTEQ_to_TRel(2)[where TRel="TRel"]
              trans_closure_of_TRel_refl_cond[where TRel="TRel"]
[PROOF STATE]
proof (prove)
using this:
Q' \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> TargetTerm T
S' \<in>S Q'
TRel\<^sup>* = TRel
?P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<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. (\<lbrakk>S'\<rbrakk>, T) \<in> TRel
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(\<lbrakk>S'\<rbrakk>, T) \<in> TRel

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

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
operational_corresponding TRel

goal (1 subgoal):
 1. weak_reduction_bisimulation (indRelTEQ TRel) (STCal Source Target) \<Longrightarrow> operational_corresponding TRel \<and> weak_reduction_bisimulation TRel Target
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
operational_corresponding TRel

goal (1 subgoal):
 1. weak_reduction_bisimulation (indRelTEQ TRel) (STCal Source Target) \<Longrightarrow> operational_corresponding TRel \<and> weak_reduction_bisimulation TRel Target
[PROOF STEP]
have "weak_reduction_bisimulation TRel Target"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. weak_reduction_bisimulation TRel Target
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. weak_reduction_bisimulation TRel Target
[PROOF STEP]
from eqT
[PROOF STATE]
proof (chain)
picking this:
equivalence TRel
[PROOF STEP]
have "TRel\<^sup>* = TRel"
[PROOF STATE]
proof (prove)
using this:
equivalence TRel

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

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

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

goal (1 subgoal):
 1. weak_reduction_bisimulation TRel Target
[PROOF STEP]
with bisim
[PROOF STATE]
proof (chain)
picking this:
weak_reduction_bisimulation (indRelTEQ TRel) (STCal Source Target)
TRel\<^sup>* = TRel
[PROOF STEP]
show "weak_reduction_bisimulation TRel Target"
[PROOF STATE]
proof (prove)
using this:
weak_reduction_bisimulation (indRelTEQ TRel) (STCal Source Target)
TRel\<^sup>* = TRel

goal (1 subgoal):
 1. weak_reduction_bisimulation TRel Target
[PROOF STEP]
using indRelTEQ_impl_TRel_is_weak_reduction_bisimulation[where TRel="TRel"]
[PROOF STATE]
proof (prove)
using this:
weak_reduction_bisimulation (indRelTEQ TRel) (STCal Source Target)
TRel\<^sup>* = TRel
weak_reduction_bisimulation (indRelTEQ TRel) (STCal Source Target) \<Longrightarrow> weak_reduction_bisimulation (TRel\<^sup>*) Target

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
weak_reduction_bisimulation TRel Target

goal (1 subgoal):
 1. weak_reduction_bisimulation (indRelTEQ TRel) (STCal Source Target) \<Longrightarrow> operational_corresponding TRel \<and> weak_reduction_bisimulation TRel Target
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
operational_corresponding TRel
weak_reduction_bisimulation TRel Target
[PROOF STEP]
show "operational_corresponding TRel \<and> weak_reduction_bisimulation TRel Target"
[PROOF STATE]
proof (prove)
using this:
operational_corresponding TRel
weak_reduction_bisimulation TRel Target

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

goal:
No subgoals!
[PROOF STEP]
qed