[STATEMENT]
theorem Subject_reductions:
assumes wf: "wf_J_prog P" and reds: "P \<turnstile> \<langle>e,s,b\<rangle> \<rightarrow>* \<langle>e',s',b'\<rangle>"
shows "\<And>T. P,E,s \<turnstile> e:T \<surd> \<Longrightarrow> \<exists>T'. P,E,s' \<turnstile> e':T' \<surd> \<and> P \<turnstile> T' \<le> T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>T. P,E,s \<turnstile> e : T \<surd> \<Longrightarrow> \<exists>T'. P,E,s' \<turnstile> e' : T' \<surd> \<and> P \<turnstile> T' \<le> T
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>T. P,E,s \<turnstile> e : T \<surd> \<Longrightarrow> \<exists>T'. P,E,s' \<turnstile> e' : T' \<surd> \<and> P \<turnstile> T' \<le> T
[PROOF STEP]
using reds
[PROOF STATE]
proof (prove)
using this:
P \<turnstile> \<langle>e,s,b\<rangle> \<rightarrow>* \<langle>e',s',b'\<rangle>

goal (1 subgoal):
 1. \<And>T. P,E,s \<turnstile> e : T \<surd> \<Longrightarrow> \<exists>T'. P,E,s' \<turnstile> e' : T' \<surd> \<and> P \<turnstile> T' \<le> T
[PROOF STEP]
proof (induct rule:converse_rtrancl_induct3)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>T. P,E,s' \<turnstile> e' : T \<surd> \<Longrightarrow> \<exists>T'. P,E,s' \<turnstile> e' : T' \<surd> \<and> P \<turnstile> T' \<le> T
 2. \<And>a aa b ab ac ba T. \<lbrakk>P \<turnstile> \<langle>a,aa,b\<rangle> \<rightarrow> \<langle>ab,ac,ba\<rangle>; P \<turnstile> \<langle>ab,ac,ba\<rangle> \<rightarrow>* \<langle>e',s',b'\<rangle>; \<And>T. P,E,ac \<turnstile> ab : T \<surd> \<Longrightarrow> \<exists>T'. P,E,s' \<turnstile> e' : T' \<surd> \<and> P \<turnstile> T' \<le> T; P,E,aa \<turnstile> a : T \<surd>\<rbrakk> \<Longrightarrow> \<exists>T'. P,E,s' \<turnstile> e' : T' \<surd> \<and> P \<turnstile> T' \<le> T
[PROOF STEP]
case refl
[PROOF STATE]
proof (state)
this:
P,E,s' \<turnstile> e' : T \<surd>

goal (2 subgoals):
 1. \<And>T. P,E,s' \<turnstile> e' : T \<surd> \<Longrightarrow> \<exists>T'. P,E,s' \<turnstile> e' : T' \<surd> \<and> P \<turnstile> T' \<le> T
 2. \<And>a aa b ab ac ba T. \<lbrakk>P \<turnstile> \<langle>a,aa,b\<rangle> \<rightarrow> \<langle>ab,ac,ba\<rangle>; P \<turnstile> \<langle>ab,ac,ba\<rangle> \<rightarrow>* \<langle>e',s',b'\<rangle>; \<And>T. P,E,ac \<turnstile> ab : T \<surd> \<Longrightarrow> \<exists>T'. P,E,s' \<turnstile> e' : T' \<surd> \<and> P \<turnstile> T' \<le> T; P,E,aa \<turnstile> a : T \<surd>\<rbrakk> \<Longrightarrow> \<exists>T'. P,E,s' \<turnstile> e' : T' \<surd> \<and> P \<turnstile> T' \<le> T
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
P,E,s' \<turnstile> e' : T \<surd>

goal (1 subgoal):
 1. \<exists>T'. P,E,s' \<turnstile> e' : T' \<surd> \<and> P \<turnstile> T' \<le> T
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>T'. P,E,s' \<turnstile> e' : T' \<surd> \<and> P \<turnstile> T' \<le> T

goal (1 subgoal):
 1. \<And>a aa b ab ac ba T. \<lbrakk>P \<turnstile> \<langle>a,aa,b\<rangle> \<rightarrow> \<langle>ab,ac,ba\<rangle>; P \<turnstile> \<langle>ab,ac,ba\<rangle> \<rightarrow>* \<langle>e',s',b'\<rangle>; \<And>T. P,E,ac \<turnstile> ab : T \<surd> \<Longrightarrow> \<exists>T'. P,E,s' \<turnstile> e' : T' \<surd> \<and> P \<turnstile> T' \<le> T; P,E,aa \<turnstile> a : T \<surd>\<rbrakk> \<Longrightarrow> \<exists>T'. P,E,s' \<turnstile> e' : T' \<surd> \<and> P \<turnstile> T' \<le> T
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a aa b ab ac ba T. \<lbrakk>P \<turnstile> \<langle>a,aa,b\<rangle> \<rightarrow> \<langle>ab,ac,ba\<rangle>; P \<turnstile> \<langle>ab,ac,ba\<rangle> \<rightarrow>* \<langle>e',s',b'\<rangle>; \<And>T. P,E,ac \<turnstile> ab : T \<surd> \<Longrightarrow> \<exists>T'. P,E,s' \<turnstile> e' : T' \<surd> \<and> P \<turnstile> T' \<le> T; P,E,aa \<turnstile> a : T \<surd>\<rbrakk> \<Longrightarrow> \<exists>T'. P,E,s' \<turnstile> e' : T' \<surd> \<and> P \<turnstile> T' \<le> T
[PROOF STEP]
case step
[PROOF STATE]
proof (state)
this:
P \<turnstile> \<langle>a___,aa___,ba___\<rangle> \<rightarrow> \<langle>ab___,a_,b_\<rangle>
P \<turnstile> \<langle>ab___,a_,b_\<rangle> \<rightarrow>* \<langle>e',s',b'\<rangle>
P,E,a_ \<turnstile> ab___ : ?T \<surd> \<Longrightarrow> \<exists>T'. P,E,s' \<turnstile> e' : T' \<surd> \<and> P \<turnstile> T' \<le> ?T
P,E,aa___ \<turnstile> a___ : T \<surd>

goal (1 subgoal):
 1. \<And>a aa b ab ac ba T. \<lbrakk>P \<turnstile> \<langle>a,aa,b\<rangle> \<rightarrow> \<langle>ab,ac,ba\<rangle>; P \<turnstile> \<langle>ab,ac,ba\<rangle> \<rightarrow>* \<langle>e',s',b'\<rangle>; \<And>T. P,E,ac \<turnstile> ab : T \<surd> \<Longrightarrow> \<exists>T'. P,E,s' \<turnstile> e' : T' \<surd> \<and> P \<turnstile> T' \<le> T; P,E,aa \<turnstile> a : T \<surd>\<rbrakk> \<Longrightarrow> \<exists>T'. P,E,s' \<turnstile> e' : T' \<surd> \<and> P \<turnstile> T' \<le> T
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
P \<turnstile> \<langle>a___,aa___,ba___\<rangle> \<rightarrow> \<langle>ab___,a_,b_\<rangle>
P \<turnstile> \<langle>ab___,a_,b_\<rangle> \<rightarrow>* \<langle>e',s',b'\<rangle>
P,E,a_ \<turnstile> ab___ : ?T \<surd> \<Longrightarrow> \<exists>T'. P,E,s' \<turnstile> e' : T' \<surd> \<and> P \<turnstile> T' \<le> ?T
P,E,aa___ \<turnstile> a___ : T \<surd>

goal (1 subgoal):
 1. \<exists>T'. P,E,s' \<turnstile> e' : T' \<surd> \<and> P \<turnstile> T' \<le> T
[PROOF STEP]
by(blast dest:Subject_reduction[OF wf] intro:widen_trans)
[PROOF STATE]
proof (state)
this:
\<exists>T'. P,E,s' \<turnstile> e' : T' \<surd> \<and> P \<turnstile> T' \<le> T

goal:
No subgoals!
[PROOF STEP]
qed