[STATEMENT]
lemma (in encoding_wrt_barbs) rel_with_target_impl_TRel_weakly_reflects_barbs:
  fixes TRel :: "('procT \<times> 'procT) set"
    and Rel  :: "(('procS, 'procT) Proc \<times> ('procS, 'procT) Proc) set"
  assumes reflection: "rel_weakly_reflects_barbs Rel (STCalWB SWB TWB)"
      and targetInRel:  "\<forall>T1 T2. (T1, T2) \<in> TRel \<longrightarrow> (TargetTerm T1, TargetTerm T2) \<in> Rel"
  shows "rel_weakly_reflects_barbs TRel TWB"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_weakly_reflects_barbs TRel TWB
[PROOF STEP]
proof clarify
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b x P'. (a, b) \<in> TRel \<and> b \<longmapsto>Calculus TWB* P' \<and> P'\<down><TWB>x \<Longrightarrow> a\<Down><TWB>x
[PROOF STEP]
fix TP TQ a TQ'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b x P'. (a, b) \<in> TRel \<and> b \<longmapsto>Calculus TWB* P' \<and> P'\<down><TWB>x \<Longrightarrow> a\<Down><TWB>x
[PROOF STEP]
assume "(TP, TQ) \<in> TRel"
[PROOF STATE]
proof (state)
this:
(TP, TQ) \<in> TRel

goal (1 subgoal):
 1. \<And>a b x P'. (a, b) \<in> TRel \<and> b \<longmapsto>Calculus TWB* P' \<and> P'\<down><TWB>x \<Longrightarrow> a\<Down><TWB>x
[PROOF STEP]
with targetInRel
[PROOF STATE]
proof (chain)
picking this:
\<forall>T1 T2. (T1, T2) \<in> TRel \<longrightarrow> (TargetTerm T1, TargetTerm T2) \<in> Rel
(TP, TQ) \<in> TRel
[PROOF STEP]
have "(TargetTerm TP, TargetTerm TQ) \<in> Rel"
[PROOF STATE]
proof (prove)
using this:
\<forall>T1 T2. (T1, T2) \<in> TRel \<longrightarrow> (TargetTerm T1, TargetTerm T2) \<in> Rel
(TP, TQ) \<in> TRel

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

goal (1 subgoal):
 1. \<And>a b x P'. (a, b) \<in> TRel \<and> b \<longmapsto>Calculus TWB* P' \<and> P'\<down><TWB>x \<Longrightarrow> a\<Down><TWB>x
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(TargetTerm TP, TargetTerm TQ) \<in> Rel

goal (1 subgoal):
 1. \<And>a b x P'. (a, b) \<in> TRel \<and> b \<longmapsto>Calculus TWB* P' \<and> P'\<down><TWB>x \<Longrightarrow> a\<Down><TWB>x
[PROOF STEP]
assume "TQ \<longmapsto>(Calculus TWB)* TQ'" and "TQ'\<down><TWB>a"
[PROOF STATE]
proof (state)
this:
TQ \<longmapsto>Calculus TWB* TQ'
TQ'\<down><TWB>a

goal (1 subgoal):
 1. \<And>a b x P'. (a, b) \<in> TRel \<and> b \<longmapsto>Calculus TWB* P' \<and> P'\<down><TWB>x \<Longrightarrow> a\<Down><TWB>x
[PROOF STEP]
hence "TargetTerm TQ\<Down>.a"
[PROOF STATE]
proof (prove)
using this:
TQ \<longmapsto>Calculus TWB* TQ'
TQ'\<down><TWB>a

goal (1 subgoal):
 1. (\<exists>S. S \<in>S TargetTerm TQ \<and> S\<Down><SWB>a) \<or> (\<exists>T. T \<in>T TargetTerm TQ \<and> T\<Down><TWB>a)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(\<exists>S. S \<in>S TargetTerm TQ \<and> S\<Down><SWB>a) \<or> (\<exists>T. T \<in>T TargetTerm TQ \<and> T\<Down><TWB>a)

goal (1 subgoal):
 1. \<And>a b x P'. (a, b) \<in> TRel \<and> b \<longmapsto>Calculus TWB* P' \<and> P'\<down><TWB>x \<Longrightarrow> a\<Down><TWB>x
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(TargetTerm TP, TargetTerm TQ) \<in> Rel
(\<exists>S. S \<in>S TargetTerm TQ \<and> S\<Down><SWB>a) \<or> (\<exists>T. T \<in>T TargetTerm TQ \<and> T\<Down><TWB>a)
[PROOF STEP]
have "TargetTerm TP\<Down>.a"
[PROOF STATE]
proof (prove)
using this:
(TargetTerm TP, TargetTerm TQ) \<in> Rel
(\<exists>S. S \<in>S TargetTerm TQ \<and> S\<Down><SWB>a) \<or> (\<exists>T. T \<in>T TargetTerm TQ \<and> T\<Down><TWB>a)

goal (1 subgoal):
 1. (\<exists>S. S \<in>S TargetTerm TP \<and> S\<Down><SWB>a) \<or> (\<exists>T. T \<in>T TargetTerm TP \<and> T\<Down><TWB>a)
[PROOF STEP]
using reflection weak_reflection_of_barbs_in_barbed_encoding[where Rel="Rel"]
[PROOF STATE]
proof (prove)
using this:
(TargetTerm TP, TargetTerm TQ) \<in> Rel
(\<exists>S. S \<in>S TargetTerm TQ \<and> S\<Down><SWB>a) \<or> (\<exists>T. T \<in>T TargetTerm TQ \<and> T\<Down><TWB>a)
rel_weakly_reflects_barbs Rel (STCalWB SWB TWB)
rel_weakly_reflects_barbs Rel (STCalWB SWB TWB) \<and> (?P, ?Q) \<in> Rel \<and> ((\<exists>S. S \<in>S ?Q \<and> S\<Down><SWB>?a) \<or> (\<exists>T. T \<in>T ?Q \<and> T\<Down><TWB>?a)) \<Longrightarrow> (\<exists>S. S \<in>S ?P \<and> S\<Down><SWB>?a) \<or> (\<exists>T. T \<in>T ?P \<and> T\<Down><TWB>?a)

goal (1 subgoal):
 1. (\<exists>S. S \<in>S TargetTerm TP \<and> S\<Down><SWB>a) \<or> (\<exists>T. T \<in>T TargetTerm TP \<and> T\<Down><TWB>a)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(\<exists>S. S \<in>S TargetTerm TP \<and> S\<Down><SWB>a) \<or> (\<exists>T. T \<in>T TargetTerm TP \<and> T\<Down><TWB>a)

goal (1 subgoal):
 1. \<And>a b x P'. (a, b) \<in> TRel \<and> b \<longmapsto>Calculus TWB* P' \<and> P'\<down><TWB>x \<Longrightarrow> a\<Down><TWB>x
[PROOF STEP]
thus "TP\<Down><TWB>a"
[PROOF STATE]
proof (prove)
using this:
(\<exists>S. S \<in>S TargetTerm TP \<and> S\<Down><SWB>a) \<or> (\<exists>T. T \<in>T TargetTerm TP \<and> T\<Down><TWB>a)

goal (1 subgoal):
 1. TP\<Down><TWB>a
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
TP\<Down><TWB>a

goal:
No subgoals!
[PROOF STEP]
qed