theory Corres_UL_C

lemma exec_handlers_Seq_cases0':
  assumes eh: "\<Gamma> \<turnstile>\<^sub>h \<langle>h, s\<rangle> \<Rightarrow> (n, t)"
  and     hv: "h = (a ;; b) # hs"
  and     r1: "\<And>z t'. \<lbrakk>\<Gamma> \<turnstile> \<langle>a, Normal s\<rangle> \<Rightarrow> t';  \<Gamma> \<turnstile> \<langle>b, t'\<rangle> \<Rightarrow> z;
  ((\<not> isAbr z \<or> hs = []) \<and> n = length hs \<and> z = t) \<or> (\<exists>q. z = Abrupt q \<and> \<Gamma> \<turnstile>\<^sub>h \<langle>hs, q\<rangle> \<Rightarrow> (n, t));  \<not> isAbr t'  \<rbrakk> \<Longrightarrow> P"
  and     r2: "\<And>t'. \<lbrakk>\<Gamma> \<turnstile> \<langle>a, Normal s\<rangle> \<Rightarrow> Abrupt t'; \<Gamma> \<turnstile>\<^sub>h \<langle>hs, t'\<rangle> \<Rightarrow> (n, t) \<rbrakk> \<Longrightarrow> P"
  shows P using eh hv r1 r2 proof induct case (EHOther h s t hs') hence ex: "\<Gamma> \<turnstile> \<langle>a ;; b, Normal s\<rangle> \<Rightarrow> t" by simp then obtain t'' where ae: "\<Gamma> \<turnstile> \<langle>a, Normal s\<rangle> \<Rightarrow> t''" and be: "\<Gamma> \<turnstile> \<langle>b, t''\<rangle> \<Rightarrow> t" by (auto elim: exec_Normal_elim_cases) have r: "\<And>z t'. \<lbrakk>\<Gamma> \<turnstile> \<langle>a, Normal s\<rangle> \<Rightarrow> t';  \<Gamma> \<turnstile> \<langle>b, t'\<rangle> \<Rightarrow> z;
    ((\<not> isAbr z \<or> hs = []) \<and> length hs' = length hs \<and> z = t) \<or> (\<exists>q. z = Abrupt q \<and> \<Gamma> \<turnstile>\<^sub>h \<langle>hs, q\<rangle> \<Rightarrow> (length hs', t));  \<not> isAbr t' \<rbrakk> \<Longrightarrow> P" by fact+ show ?case proof (rule r) show "\<not> isAbr t''" using EHOther(2) be by (cases t) (auto elim: Normal_resultE Fault_resultE Stuck_resultE) show "((\<not> isAbr t \<or> hs = []) \<and> length hs' = length hs \<and> t = t)
        \<or> (\<exists>q. t = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (length hs', t))" using EHOther by simp qed fact+ next case (EHAbrupt h s z hs' n t) hence ex: "\<Gamma> \<turnstile> \<langle>a ;; b, Normal s\<rangle> \<Rightarrow> Abrupt z" and hs: "hs' = hs" by simp_all have ra: "\<And>z t'. \<lbrakk>\<Gamma> \<turnstile> \<langle>a, Normal s\<rangle> \<Rightarrow> t';  \<Gamma> \<turnstile> \<langle>b, t'\<rangle> \<Rightarrow> z;
    ((\<not> isAbr z \<or> hs = []) \<and> n = length hs \<and> z = t) \<or> (\<exists>q. z = Abrupt q \<and> \<Gamma> \<turnstile>\<^sub>h \<langle>hs, q\<rangle> \<Rightarrow> (n, t));  \<not> isAbr t' \<rbrakk> \<Longrightarrow> P" by fact+ have rb: "\<And>t'. \<lbrakk>\<Gamma> \<turnstile> \<langle>a, Normal s\<rangle> \<Rightarrow> Abrupt t'; \<Gamma> \<turnstile>\<^sub>h \<langle>hs, t'\<rangle> \<Rightarrow> (n, t) \<rbrakk> \<Longrightarrow> P" by fact+ { assume "\<Gamma> \<turnstile> \<langle>a, Normal s\<rangle> \<Rightarrow> Abrupt z" hence ?case proof (rule rb) show "\<Gamma>\<turnstile>\<^sub>h \<langle>hs,z\<rangle> \<Rightarrow> (n, t)" by (fold hs) fact+ qed } moreover { fix s'' assume "\<Gamma> \<turnstile> \<langle>a, Normal s\<rangle> \<Rightarrow> Normal s''" and
      "\<Gamma> \<turnstile> \<langle>b, Normal s''\<rangle> \<Rightarrow> Abrupt z" hence ?case proof (rule ra) show "((\<not> isAbr (Abrupt z) \<or> hs = []) \<and> n = length hs \<and> Abrupt z = t)
               \<or> (\<exists>q. Abrupt z = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (n, t))" using EHAbrupt(2) by (simp add: hs) show "\<not> isAbr (Normal s'')" by simp qed } ultimately show ?case using ex apply - apply (erule exec_Normal_elim_cases) apply (erule Abrupt_resultE) apply simp apply simp apply (drule Abrupt_end [OF _ refl]) apply simp done next case (EHEmpty s) thus ?case by simp qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. P proof (prove)
using this:
\<Gamma>\<turnstile>\<^sub>h \<langle>h,s\<rangle> \<Rightarrow> (n, t)
h = (a;;
b) # hs
\<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> ?t'; \<Gamma>\<turnstile> \<langle>b,?t'\<rangle> \<Rightarrow> ?z; (\<not> isAbr ?z \<or> hs = []) \<and> n = length hs \<and> ?z = t \<or> (\<exists>q. ?z = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (n, t)); \<not> isAbr ?t'\<rbrakk> \<Longrightarrow> P
\<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> Abrupt ?t'; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,?t'\<rangle> \<Rightarrow> (n, t)\<rbrakk> \<Longrightarrow> P

goal (1 subgoal):
 1. P proof (state)
goal (3 subgoals):
 1. \<And>h s z hsa n t. \<lbrakk>\<Gamma>\<turnstile> \<langle>h,Normal s\<rangle> \<Rightarrow> Abrupt z; \<Gamma>\<turnstile>\<^sub>h \<langle>hsa,z\<rangle> \<Rightarrow> (n, t); \<lbrakk>hsa = (a;;
b) # hs; \<And>t' za. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal z\<rangle> \<Rightarrow> t'; \<Gamma>\<turnstile> \<langle>b,t'\<rangle> \<Rightarrow> za; (\<not> isAbr za \<or> hs = []) \<and> n = length hs \<and> za = t \<or> (\<exists>q. za = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (n, t)); \<not> isAbr t'\<rbrakk> \<Longrightarrow> P; \<And>t'. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal z\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,t'\<rangle> \<Rightarrow> (n, t)\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P; h # hsa = (a;;
b) # hs; \<And>t' z. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> t'; \<Gamma>\<turnstile> \<langle>b,t'\<rangle> \<Rightarrow> z; (\<not> isAbr z \<or> hs = []) \<and> n = length hs \<and> z = t \<or> (\<exists>q. z = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (n, t)); \<not> isAbr t'\<rbrakk> \<Longrightarrow> P; \<And>t'. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,t'\<rangle> \<Rightarrow> (n, t)\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
 2. \<And>h s t hsa. \<lbrakk>\<Gamma>\<turnstile> \<langle>h,Normal s\<rangle> \<Rightarrow> t; \<not> isAbr t; h # hsa = (a;;
b) # hs; \<And>t' z. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> t'; \<Gamma>\<turnstile> \<langle>b,t'\<rangle> \<Rightarrow> z; (\<not> isAbr z \<or> hs = []) \<and> length hsa = length hs \<and> z = t \<or> (\<exists>q. z = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (length hsa, t)); \<not> isAbr t'\<rbrakk> \<Longrightarrow> P; \<And>t'. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,t'\<rangle> \<Rightarrow> (length hsa, t)\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
 3. \<And>s. \<lbrakk>[] = (a;;
b) # hs; \<And>t' z. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> t'; \<Gamma>\<turnstile> \<langle>b,t'\<rangle> \<Rightarrow> z; (\<not> isAbr z \<or> hs = []) \<and> 0 = length hs \<and> z = Abrupt s \<or> (\<exists>q. z = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (0, Abrupt s)); \<not> isAbr t'\<rbrakk> \<Longrightarrow> P; \<And>t'. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,t'\<rangle> \<Rightarrow> (0, Abrupt s)\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P proof (state)
this:
\<Gamma>\<turnstile> \<langle>h,Normal s\<rangle> \<Rightarrow> t
\<not> isAbr t
h # hs' = (a;;
b) # hs
\<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> ?t'; \<Gamma>\<turnstile> \<langle>b,?t'\<rangle> \<Rightarrow> ?z; (\<not> isAbr ?z \<or> hs = []) \<and> length hs' = length hs \<and> ?z = t \<or> (\<exists>q. ?z = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (length hs', t)); \<not> isAbr ?t'\<rbrakk> \<Longrightarrow> P
\<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> Abrupt ?t'; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,?t'\<rangle> \<Rightarrow> (length hs', t)\<rbrakk> \<Longrightarrow> P

goal (3 subgoals):
 1. \<And>h s z hsa n t. \<lbrakk>\<Gamma>\<turnstile> \<langle>h,Normal s\<rangle> \<Rightarrow> Abrupt z; \<Gamma>\<turnstile>\<^sub>h \<langle>hsa,z\<rangle> \<Rightarrow> (n, t); \<lbrakk>hsa = (a;;
b) # hs; \<And>t' za. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal z\<rangle> \<Rightarrow> t'; \<Gamma>\<turnstile> \<langle>b,t'\<rangle> \<Rightarrow> za; (\<not> isAbr za \<or> hs = []) \<and> n = length hs \<and> za = t \<or> (\<exists>q. za = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (n, t)); \<not> isAbr t'\<rbrakk> \<Longrightarrow> P; \<And>t'. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal z\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,t'\<rangle> \<Rightarrow> (n, t)\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P; h # hsa = (a;;
b) # hs; \<And>t' z. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> t'; \<Gamma>\<turnstile> \<langle>b,t'\<rangle> \<Rightarrow> z; (\<not> isAbr z \<or> hs = []) \<and> n = length hs \<and> z = t \<or> (\<exists>q. z = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (n, t)); \<not> isAbr t'\<rbrakk> \<Longrightarrow> P; \<And>t'. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,t'\<rangle> \<Rightarrow> (n, t)\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
 2. \<And>h s t hsa. \<lbrakk>\<Gamma>\<turnstile> \<langle>h,Normal s\<rangle> \<Rightarrow> t; \<not> isAbr t; h # hsa = (a;;
b) # hs; \<And>t' z. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> t'; \<Gamma>\<turnstile> \<langle>b,t'\<rangle> \<Rightarrow> z; (\<not> isAbr z \<or> hs = []) \<and> length hsa = length hs \<and> z = t \<or> (\<exists>q. z = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (length hsa, t)); \<not> isAbr t'\<rbrakk> \<Longrightarrow> P; \<And>t'. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,t'\<rangle> \<Rightarrow> (length hsa, t)\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
 3. \<And>s. \<lbrakk>[] = (a;;
b) # hs; \<And>t' z. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> t'; \<Gamma>\<turnstile> \<langle>b,t'\<rangle> \<Rightarrow> z; (\<not> isAbr z \<or> hs = []) \<and> 0 = length hs \<and> z = Abrupt s \<or> (\<exists>q. z = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (0, Abrupt s)); \<not> isAbr t'\<rbrakk> \<Longrightarrow> P; \<And>t'. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,t'\<rangle> \<Rightarrow> (0, Abrupt s)\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P proof (prove)
using this:
\<Gamma>\<turnstile> \<langle>h,Normal s\<rangle> \<Rightarrow> t
\<not> isAbr t
h # hs' = (a;;
b) # hs
\<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> ?t'; \<Gamma>\<turnstile> \<langle>b,?t'\<rangle> \<Rightarrow> ?z; (\<not> isAbr ?z \<or> hs = []) \<and> length hs' = length hs \<and> ?z = t \<or> (\<exists>q. ?z = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (length hs', t)); \<not> isAbr ?t'\<rbrakk> \<Longrightarrow> P
\<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> Abrupt ?t'; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,?t'\<rangle> \<Rightarrow> (length hs', t)\<rbrakk> \<Longrightarrow> P

goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<langle>a;;
b,Normal s\<rangle> \<Rightarrow> t proof (state)
this:
\<Gamma>\<turnstile> \<langle>a;;
b,Normal s\<rangle> \<Rightarrow> t

goal (3 subgoals):
 1. \<And>h s z hsa n t. \<lbrakk>\<Gamma>\<turnstile> \<langle>h,Normal s\<rangle> \<Rightarrow> Abrupt z; \<Gamma>\<turnstile>\<^sub>h \<langle>hsa,z\<rangle> \<Rightarrow> (n, t); \<lbrakk>hsa = (a;;
b) # hs; \<And>t' za. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal z\<rangle> \<Rightarrow> t'; \<Gamma>\<turnstile> \<langle>b,t'\<rangle> \<Rightarrow> za; (\<not> isAbr za \<or> hs = []) \<and> n = length hs \<and> za = t \<or> (\<exists>q. za = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (n, t)); \<not> isAbr t'\<rbrakk> \<Longrightarrow> P; \<And>t'. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal z\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,t'\<rangle> \<Rightarrow> (n, t)\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P; h # hsa = (a;;
b) # hs; \<And>t' z. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> t'; \<Gamma>\<turnstile> \<langle>b,t'\<rangle> \<Rightarrow> z; (\<not> isAbr z \<or> hs = []) \<and> n = length hs \<and> z = t \<or> (\<exists>q. z = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (n, t)); \<not> isAbr t'\<rbrakk> \<Longrightarrow> P; \<And>t'. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,t'\<rangle> \<Rightarrow> (n, t)\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
 2. \<And>h s t hsa. \<lbrakk>\<Gamma>\<turnstile> \<langle>h,Normal s\<rangle> \<Rightarrow> t; \<not> isAbr t; h # hsa = (a;;
b) # hs; \<And>t' z. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> t'; \<Gamma>\<turnstile> \<langle>b,t'\<rangle> \<Rightarrow> z; (\<not> isAbr z \<or> hs = []) \<and> length hsa = length hs \<and> z = t \<or> (\<exists>q. z = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (length hsa, t)); \<not> isAbr t'\<rbrakk> \<Longrightarrow> P; \<And>t'. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,t'\<rangle> \<Rightarrow> (length hsa, t)\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
 3. \<And>s. \<lbrakk>[] = (a;;
b) # hs; \<And>t' z. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> t'; \<Gamma>\<turnstile> \<langle>b,t'\<rangle> \<Rightarrow> z; (\<not> isAbr z \<or> hs = []) \<and> 0 = length hs \<and> z = Abrupt s \<or> (\<exists>q. z = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (0, Abrupt s)); \<not> isAbr t'\<rbrakk> \<Longrightarrow> P; \<And>t'. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,t'\<rangle> \<Rightarrow> (0, Abrupt s)\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P proof (chain)
picking this:
\<Gamma>\<turnstile> \<langle>a;;
b,Normal s\<rangle> \<Rightarrow> t proof (prove)
using this:
\<Gamma>\<turnstile> \<langle>a;;
b,Normal s\<rangle> \<Rightarrow> t

goal (1 subgoal):
 1. (\<And>t''. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> t''; \<Gamma>\<turnstile> \<langle>b,t''\<rangle> \<Rightarrow> t\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (state)
this:
\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> t''
\<Gamma>\<turnstile> \<langle>b,t''\<rangle> \<Rightarrow> t

goal (3 subgoals):
 1. \<And>h s z hsa n t. \<lbrakk>\<Gamma>\<turnstile> \<langle>h,Normal s\<rangle> \<Rightarrow> Abrupt z; \<Gamma>\<turnstile>\<^sub>h \<langle>hsa,z\<rangle> \<Rightarrow> (n, t); \<lbrakk>hsa = (a;;
b) # hs; \<And>t' za. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal z\<rangle> \<Rightarrow> t'; \<Gamma>\<turnstile> \<langle>b,t'\<rangle> \<Rightarrow> za; (\<not> isAbr za \<or> hs = []) \<and> n = length hs \<and> za = t \<or> (\<exists>q. za = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (n, t)); \<not> isAbr t'\<rbrakk> \<Longrightarrow> P; \<And>t'. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal z\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,t'\<rangle> \<Rightarrow> (n, t)\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P; h # hsa = (a;;
b) # hs; \<And>t' z. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> t'; \<Gamma>\<turnstile> \<langle>b,t'\<rangle> \<Rightarrow> z; (\<not> isAbr z \<or> hs = []) \<and> n = length hs \<and> z = t \<or> (\<exists>q. z = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (n, t)); \<not> isAbr t'\<rbrakk> \<Longrightarrow> P; \<And>t'. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,t'\<rangle> \<Rightarrow> (n, t)\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
 2. \<And>h s t hsa. \<lbrakk>\<Gamma>\<turnstile> \<langle>h,Normal s\<rangle> \<Rightarrow> t; \<not> isAbr t; h # hsa = (a;;
b) # hs; \<And>t' z. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> t'; \<Gamma>\<turnstile> \<langle>b,t'\<rangle> \<Rightarrow> z; (\<not> isAbr z \<or> hs = []) \<and> length hsa = length hs \<and> z = t \<or> (\<exists>q. z = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (length hsa, t)); \<not> isAbr t'\<rbrakk> \<Longrightarrow> P; \<And>t'. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,t'\<rangle> \<Rightarrow> (length hsa, t)\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
 3. \<And>s. \<lbrakk>[] = (a;;
b) # hs; \<And>t' z. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> t'; \<Gamma>\<turnstile> \<langle>b,t'\<rangle> \<Rightarrow> z; (\<not> isAbr z \<or> hs = []) \<and> 0 = length hs \<and> z = Abrupt s \<or> (\<exists>q. z = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (0, Abrupt s)); \<not> isAbr t'\<rbrakk> \<Longrightarrow> P; \<And>t'. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,t'\<rangle> \<Rightarrow> (0, Abrupt s)\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P proof (prove)
goal (1 subgoal):
 1. \<And>z t'. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> t'; \<Gamma>\<turnstile> \<langle>b,t'\<rangle> \<Rightarrow> z; (\<not> isAbr z \<or> hs = []) \<and> length hs' = length hs \<and> z = t \<or> (\<exists>q. z = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (length hs', t)); \<not> isAbr t'\<rbrakk> \<Longrightarrow> P proof (state)
this:
\<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> ?t'; \<Gamma>\<turnstile> \<langle>b,?t'\<rangle> \<Rightarrow> ?z; (\<not> isAbr ?z \<or> hs = []) \<and> length hs' = length hs \<and> ?z = t \<or> (\<exists>q. ?z = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (length hs', t)); \<not> isAbr ?t'\<rbrakk> \<Longrightarrow> P

goal (3 subgoals):
 1. \<And>h s z hsa n t. \<lbrakk>\<Gamma>\<turnstile> \<langle>h,Normal s\<rangle> \<Rightarrow> Abrupt z; \<Gamma>\<turnstile>\<^sub>h \<langle>hsa,z\<rangle> \<Rightarrow> (n, t); \<lbrakk>hsa = (a;;
b) # hs; \<And>t' za. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal z\<rangle> \<Rightarrow> t'; \<Gamma>\<turnstile> \<langle>b,t'\<rangle> \<Rightarrow> za; (\<not> isAbr za \<or> hs = []) \<and> n = length hs \<and> za = t \<or> (\<exists>q. za = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (n, t)); \<not> isAbr t'\<rbrakk> \<Longrightarrow> P; \<And>t'. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal z\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,t'\<rangle> \<Rightarrow> (n, t)\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P; h # hsa = (a;;
b) # hs; \<And>t' z. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> t'; \<Gamma>\<turnstile> \<langle>b,t'\<rangle> \<Rightarrow> z; (\<not> isAbr z \<or> hs = []) \<and> n = length hs \<and> z = t \<or> (\<exists>q. z = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (n, t)); \<not> isAbr t'\<rbrakk> \<Longrightarrow> P; \<And>t'. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,t'\<rangle> \<Rightarrow> (n, t)\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
 2. \<And>h s t hsa. \<lbrakk>\<Gamma>\<turnstile> \<langle>h,Normal s\<rangle> \<Rightarrow> t; \<not> isAbr t; h # hsa = (a;;
b) # hs; \<And>t' z. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> t'; \<Gamma>\<turnstile> \<langle>b,t'\<rangle> \<Rightarrow> z; (\<not> isAbr z \<or> hs = []) \<and> length hsa = length hs \<and> z = t \<or> (\<exists>q. z = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (length hsa, t)); \<not> isAbr t'\<rbrakk> \<Longrightarrow> P; \<And>t'. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,t'\<rangle> \<Rightarrow> (length hsa, t)\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
 3. \<And>s. \<lbrakk>[] = (a;;
b) # hs; \<And>t' z. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> t'; \<Gamma>\<turnstile> \<langle>b,t'\<rangle> \<Rightarrow> z; (\<not> isAbr z \<or> hs = []) \<and> 0 = length hs \<and> z = Abrupt s \<or> (\<exists>q. z = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (0, Abrupt s)); \<not> isAbr t'\<rbrakk> \<Longrightarrow> P; \<And>t'. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,t'\<rangle> \<Rightarrow> (0, Abrupt s)\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P proof (prove)
goal (1 subgoal):
 1. P proof (state)
goal (4 subgoals):
 1. \<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> ?t'
 2. \<Gamma>\<turnstile> \<langle>b,?t'\<rangle> \<Rightarrow> ?z
 3. (\<not> isAbr ?z \<or> hs = []) \<and> length hs' = length hs \<and> ?z = t \<or> (\<exists>q. ?z = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (length hs', t))
 4. \<not> isAbr ?t' proof (prove)
goal (1 subgoal):
 1. \<not> isAbr t'' proof (prove)
using this:
\<not> isAbr t
\<Gamma>\<turnstile> \<langle>b,t''\<rangle> \<Rightarrow> t

goal (1 subgoal):
 1. \<not> isAbr t'' proof (state)
this:
\<not> isAbr t''

goal (3 subgoals):
 1. \<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> t''
 2. \<Gamma>\<turnstile> \<langle>b,t''\<rangle> \<Rightarrow> ?z
 3. (\<not> isAbr ?z \<or> hs = []) \<and> length hs' = length hs \<and> ?z = t \<or> (\<exists>q. ?z = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (length hs', t)) proof (prove)
goal (1 subgoal):
 1. (\<not> isAbr t \<or> hs = []) \<and> length hs' = length hs \<and> t = t \<or> (\<exists>q. t = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (length hs', t)) proof (prove)
using this:
\<Gamma>\<turnstile> \<langle>h,Normal s\<rangle> \<Rightarrow> t
\<not> isAbr t
h # hs' = (a;;
b) # hs
\<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> ?t'; \<Gamma>\<turnstile> \<langle>b,?t'\<rangle> \<Rightarrow> ?z; (\<not> isAbr ?z \<or> hs = []) \<and> length hs' = length hs \<and> ?z = t \<or> (\<exists>q. ?z = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (length hs', t)); \<not> isAbr ?t'\<rbrakk> \<Longrightarrow> P
\<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> Abrupt ?t'; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,?t'\<rangle> \<Rightarrow> (length hs', t)\<rbrakk> \<Longrightarrow> P

goal (1 subgoal):
 1. (\<not> isAbr t \<or> hs = []) \<and> length hs' = length hs \<and> t = t \<or> (\<exists>q. t = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (length hs', t)) proof (state)
this:
(\<not> isAbr t \<or> hs = []) \<and> length hs' = length hs \<and> t = t \<or> (\<exists>q. t = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (length hs', t))

goal (2 subgoals):
 1. \<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> t''
 2. \<Gamma>\<turnstile> \<langle>b,t''\<rangle> \<Rightarrow> t proof (state)
this:
P

goal (2 subgoals):
 1. \<And>h s z hsa n t. \<lbrakk>\<Gamma>\<turnstile> \<langle>h,Normal s\<rangle> \<Rightarrow> Abrupt z; \<Gamma>\<turnstile>\<^sub>h \<langle>hsa,z\<rangle> \<Rightarrow> (n, t); \<lbrakk>hsa = (a;;
b) # hs; \<And>t' za. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal z\<rangle> \<Rightarrow> t'; \<Gamma>\<turnstile> \<langle>b,t'\<rangle> \<Rightarrow> za; (\<not> isAbr za \<or> hs = []) \<and> n = length hs \<and> za = t \<or> (\<exists>q. za = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (n, t)); \<not> isAbr t'\<rbrakk> \<Longrightarrow> P; \<And>t'. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal z\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,t'\<rangle> \<Rightarrow> (n, t)\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P; h # hsa = (a;;
b) # hs; \<And>t' z. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> t'; \<Gamma>\<turnstile> \<langle>b,t'\<rangle> \<Rightarrow> z; (\<not> isAbr z \<or> hs = []) \<and> n = length hs \<and> z = t \<or> (\<exists>q. z = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (n, t)); \<not> isAbr t'\<rbrakk> \<Longrightarrow> P; \<And>t'. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,t'\<rangle> \<Rightarrow> (n, t)\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
 2. \<And>s. \<lbrakk>[] = (a;;
b) # hs; \<And>t' z. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> t'; \<Gamma>\<turnstile> \<langle>b,t'\<rangle> \<Rightarrow> z; (\<not> isAbr z \<or> hs = []) \<and> 0 = length hs \<and> z = Abrupt s \<or> (\<exists>q. z = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (0, Abrupt s)); \<not> isAbr t'\<rbrakk> \<Longrightarrow> P; \<And>t'. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,t'\<rangle> \<Rightarrow> (0, Abrupt s)\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P proof (state)
goal (2 subgoals):
 1. \<And>h s z hsa n t. \<lbrakk>\<Gamma>\<turnstile> \<langle>h,Normal s\<rangle> \<Rightarrow> Abrupt z; \<Gamma>\<turnstile>\<^sub>h \<langle>hsa,z\<rangle> \<Rightarrow> (n, t); \<lbrakk>hsa = (a;;
b) # hs; \<And>t' za. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal z\<rangle> \<Rightarrow> t'; \<Gamma>\<turnstile> \<langle>b,t'\<rangle> \<Rightarrow> za; (\<not> isAbr za \<or> hs = []) \<and> n = length hs \<and> za = t \<or> (\<exists>q. za = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (n, t)); \<not> isAbr t'\<rbrakk> \<Longrightarrow> P; \<And>t'. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal z\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,t'\<rangle> \<Rightarrow> (n, t)\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P; h # hsa = (a;;
b) # hs; \<And>t' z. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> t'; \<Gamma>\<turnstile> \<langle>b,t'\<rangle> \<Rightarrow> z; (\<not> isAbr z \<or> hs = []) \<and> n = length hs \<and> z = t \<or> (\<exists>q. z = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (n, t)); \<not> isAbr t'\<rbrakk> \<Longrightarrow> P; \<And>t'. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,t'\<rangle> \<Rightarrow> (n, t)\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
 2. \<And>s. \<lbrakk>[] = (a;;
b) # hs; \<And>t' z. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> t'; \<Gamma>\<turnstile> \<langle>b,t'\<rangle> \<Rightarrow> z; (\<not> isAbr z \<or> hs = []) \<and> 0 = length hs \<and> z = Abrupt s \<or> (\<exists>q. z = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (0, Abrupt s)); \<not> isAbr t'\<rbrakk> \<Longrightarrow> P; \<And>t'. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,t'\<rangle> \<Rightarrow> (0, Abrupt s)\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P proof (state)
this:
\<Gamma>\<turnstile> \<langle>h,Normal s\<rangle> \<Rightarrow> Abrupt z
\<Gamma>\<turnstile>\<^sub>h \<langle>hs',z\<rangle> \<Rightarrow> (n, t)
\<lbrakk>hs' = (a;;
b) # hs; \<And>t' za. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal z\<rangle> \<Rightarrow> t'; \<Gamma>\<turnstile> \<langle>b,t'\<rangle> \<Rightarrow> za; (\<not> isAbr za \<or> hs = []) \<and> n = length hs \<and> za = t \<or> (\<exists>q. za = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (n, t)); \<not> isAbr t'\<rbrakk> \<Longrightarrow> P; \<And>t'. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal z\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,t'\<rangle> \<Rightarrow> (n, t)\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
h # hs' = (a;;
b) # hs
\<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> ?t'; \<Gamma>\<turnstile> \<langle>b,?t'\<rangle> \<Rightarrow> ?z; (\<not> isAbr ?z \<or> hs = []) \<and> n = length hs \<and> ?z = t \<or> (\<exists>q. ?z = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (n, t)); \<not> isAbr ?t'\<rbrakk> \<Longrightarrow> P
\<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> Abrupt ?t'; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,?t'\<rangle> \<Rightarrow> (n, t)\<rbrakk> \<Longrightarrow> P

goal (2 subgoals):
 1. \<And>h s z hsa n t. \<lbrakk>\<Gamma>\<turnstile> \<langle>h,Normal s\<rangle> \<Rightarrow> Abrupt z; \<Gamma>\<turnstile>\<^sub>h \<langle>hsa,z\<rangle> \<Rightarrow> (n, t); \<lbrakk>hsa = (a;;
b) # hs; \<And>t' za. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal z\<rangle> \<Rightarrow> t'; \<Gamma>\<turnstile> \<langle>b,t'\<rangle> \<Rightarrow> za; (\<not> isAbr za \<or> hs = []) \<and> n = length hs \<and> za = t \<or> (\<exists>q. za = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (n, t)); \<not> isAbr t'\<rbrakk> \<Longrightarrow> P; \<And>t'. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal z\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,t'\<rangle> \<Rightarrow> (n, t)\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P; h # hsa = (a;;
b) # hs; \<And>t' z. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> t'; \<Gamma>\<turnstile> \<langle>b,t'\<rangle> \<Rightarrow> z; (\<not> isAbr z \<or> hs = []) \<and> n = length hs \<and> z = t \<or> (\<exists>q. z = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (n, t)); \<not> isAbr t'\<rbrakk> \<Longrightarrow> P; \<And>t'. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,t'\<rangle> \<Rightarrow> (n, t)\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
 2. \<And>s. \<lbrakk>[] = (a;;
b) # hs; \<And>t' z. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> t'; \<Gamma>\<turnstile> \<langle>b,t'\<rangle> \<Rightarrow> z; (\<not> isAbr z \<or> hs = []) \<and> 0 = length hs \<and> z = Abrupt s \<or> (\<exists>q. z = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (0, Abrupt s)); \<not> isAbr t'\<rbrakk> \<Longrightarrow> P; \<And>t'. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,t'\<rangle> \<Rightarrow> (0, Abrupt s)\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P proof (prove)
using this:
\<Gamma>\<turnstile> \<langle>h,Normal s\<rangle> \<Rightarrow> Abrupt z
\<Gamma>\<turnstile>\<^sub>h \<langle>hs',z\<rangle> \<Rightarrow> (n, t)
\<lbrakk>hs' = (a;;
b) # hs; \<And>t' za. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal z\<rangle> \<Rightarrow> t'; \<Gamma>\<turnstile> \<langle>b,t'\<rangle> \<Rightarrow> za; (\<not> isAbr za \<or> hs = []) \<and> n = length hs \<and> za = t \<or> (\<exists>q. za = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (n, t)); \<not> isAbr t'\<rbrakk> \<Longrightarrow> P; \<And>t'. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal z\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,t'\<rangle> \<Rightarrow> (n, t)\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
h # hs' = (a;;
b) # hs
\<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> ?t'; \<Gamma>\<turnstile> \<langle>b,?t'\<rangle> \<Rightarrow> ?z; (\<not> isAbr ?z \<or> hs = []) \<and> n = length hs \<and> ?z = t \<or> (\<exists>q. ?z = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (n, t)); \<not> isAbr ?t'\<rbrakk> \<Longrightarrow> P
\<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> Abrupt ?t'; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,?t'\<rangle> \<Rightarrow> (n, t)\<rbrakk> \<Longrightarrow> P

goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<langle>a;;
b,Normal s\<rangle> \<Rightarrow> Abrupt z &&& hs' = hs proof (state)
this:
\<Gamma>\<turnstile> \<langle>a;;
b,Normal s\<rangle> \<Rightarrow> Abrupt z
hs' = hs

goal (2 subgoals):
 1. \<And>h s z hsa n t. \<lbrakk>\<Gamma>\<turnstile> \<langle>h,Normal s\<rangle> \<Rightarrow> Abrupt z; \<Gamma>\<turnstile>\<^sub>h \<langle>hsa,z\<rangle> \<Rightarrow> (n, t); \<lbrakk>hsa = (a;;
b) # hs; \<And>t' za. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal z\<rangle> \<Rightarrow> t'; \<Gamma>\<turnstile> \<langle>b,t'\<rangle> \<Rightarrow> za; (\<not> isAbr za \<or> hs = []) \<and> n = length hs \<and> za = t \<or> (\<exists>q. za = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (n, t)); \<not> isAbr t'\<rbrakk> \<Longrightarrow> P; \<And>t'. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal z\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,t'\<rangle> \<Rightarrow> (n, t)\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P; h # hsa = (a;;
b) # hs; \<And>t' z. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> t'; \<Gamma>\<turnstile> \<langle>b,t'\<rangle> \<Rightarrow> z; (\<not> isAbr z \<or> hs = []) \<and> n = length hs \<and> z = t \<or> (\<exists>q. z = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (n, t)); \<not> isAbr t'\<rbrakk> \<Longrightarrow> P; \<And>t'. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,t'\<rangle> \<Rightarrow> (n, t)\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
 2. \<And>s. \<lbrakk>[] = (a;;
b) # hs; \<And>t' z. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> t'; \<Gamma>\<turnstile> \<langle>b,t'\<rangle> \<Rightarrow> z; (\<not> isAbr z \<or> hs = []) \<and> 0 = length hs \<and> z = Abrupt s \<or> (\<exists>q. z = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (0, Abrupt s)); \<not> isAbr t'\<rbrakk> \<Longrightarrow> P; \<And>t'. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,t'\<rangle> \<Rightarrow> (0, Abrupt s)\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P proof (prove)
goal (1 subgoal):
 1. \<And>z t'. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> t'; \<Gamma>\<turnstile> \<langle>b,t'\<rangle> \<Rightarrow> z; (\<not> isAbr z \<or> hs = []) \<and> n = length hs \<and> z = t \<or> (\<exists>q. z = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (n, t)); \<not> isAbr t'\<rbrakk> \<Longrightarrow> P proof (state)
this:
\<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> ?t'; \<Gamma>\<turnstile> \<langle>b,?t'\<rangle> \<Rightarrow> ?z; (\<not> isAbr ?z \<or> hs = []) \<and> n = length hs \<and> ?z = t \<or> (\<exists>q. ?z = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (n, t)); \<not> isAbr ?t'\<rbrakk> \<Longrightarrow> P

goal (2 subgoals):
 1. \<And>h s z hsa n t. \<lbrakk>\<Gamma>\<turnstile> \<langle>h,Normal s\<rangle> \<Rightarrow> Abrupt z; \<Gamma>\<turnstile>\<^sub>h \<langle>hsa,z\<rangle> \<Rightarrow> (n, t); \<lbrakk>hsa = (a;;
b) # hs; \<And>t' za. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal z\<rangle> \<Rightarrow> t'; \<Gamma>\<turnstile> \<langle>b,t'\<rangle> \<Rightarrow> za; (\<not> isAbr za \<or> hs = []) \<and> n = length hs \<and> za = t \<or> (\<exists>q. za = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (n, t)); \<not> isAbr t'\<rbrakk> \<Longrightarrow> P; \<And>t'. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal z\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,t'\<rangle> \<Rightarrow> (n, t)\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P; h # hsa = (a;;
b) # hs; \<And>t' z. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> t'; \<Gamma>\<turnstile> \<langle>b,t'\<rangle> \<Rightarrow> z; (\<not> isAbr z \<or> hs = []) \<and> n = length hs \<and> z = t \<or> (\<exists>q. z = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (n, t)); \<not> isAbr t'\<rbrakk> \<Longrightarrow> P; \<And>t'. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,t'\<rangle> \<Rightarrow> (n, t)\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
 2. \<And>s. \<lbrakk>[] = (a;;
b) # hs; \<And>t' z. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> t'; \<Gamma>\<turnstile> \<langle>b,t'\<rangle> \<Rightarrow> z; (\<not> isAbr z \<or> hs = []) \<and> 0 = length hs \<and> z = Abrupt s \<or> (\<exists>q. z = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (0, Abrupt s)); \<not> isAbr t'\<rbrakk> \<Longrightarrow> P; \<And>t'. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,t'\<rangle> \<Rightarrow> (0, Abrupt s)\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P proof (prove)
goal (1 subgoal):
 1. \<And>t'. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,t'\<rangle> \<Rightarrow> (n, t)\<rbrakk> \<Longrightarrow> P proof (state)
this:
\<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> Abrupt ?t'; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,?t'\<rangle> \<Rightarrow> (n, t)\<rbrakk> \<Longrightarrow> P

goal (2 subgoals):
 1. \<And>h s z hsa n t. \<lbrakk>\<Gamma>\<turnstile> \<langle>h,Normal s\<rangle> \<Rightarrow> Abrupt z; \<Gamma>\<turnstile>\<^sub>h \<langle>hsa,z\<rangle> \<Rightarrow> (n, t); \<lbrakk>hsa = (a;;
b) # hs; \<And>t' za. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal z\<rangle> \<Rightarrow> t'; \<Gamma>\<turnstile> \<langle>b,t'\<rangle> \<Rightarrow> za; (\<not> isAbr za \<or> hs = []) \<and> n = length hs \<and> za = t \<or> (\<exists>q. za = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (n, t)); \<not> isAbr t'\<rbrakk> \<Longrightarrow> P; \<And>t'. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal z\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,t'\<rangle> \<Rightarrow> (n, t)\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P; h # hsa = (a;;
b) # hs; \<And>t' z. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> t'; \<Gamma>\<turnstile> \<langle>b,t'\<rangle> \<Rightarrow> z; (\<not> isAbr z \<or> hs = []) \<and> n = length hs \<and> z = t \<or> (\<exists>q. z = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (n, t)); \<not> isAbr t'\<rbrakk> \<Longrightarrow> P; \<And>t'. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,t'\<rangle> \<Rightarrow> (n, t)\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
 2. \<And>s. \<lbrakk>[] = (a;;
b) # hs; \<And>t' z. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> t'; \<Gamma>\<turnstile> \<langle>b,t'\<rangle> \<Rightarrow> z; (\<not> isAbr z \<or> hs = []) \<and> 0 = length hs \<and> z = Abrupt s \<or> (\<exists>q. z = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (0, Abrupt s)); \<not> isAbr t'\<rbrakk> \<Longrightarrow> P; \<And>t'. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,t'\<rangle> \<Rightarrow> (0, Abrupt s)\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P proof (state)
this:
\<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> Abrupt ?t'; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,?t'\<rangle> \<Rightarrow> (n, t)\<rbrakk> \<Longrightarrow> P

goal (2 subgoals):
 1. \<And>h s z hsa n t. \<lbrakk>\<Gamma>\<turnstile> \<langle>h,Normal s\<rangle> \<Rightarrow> Abrupt z; \<Gamma>\<turnstile>\<^sub>h \<langle>hsa,z\<rangle> \<Rightarrow> (n, t); \<lbrakk>hsa = (a;;
b) # hs; \<And>t' za. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal z\<rangle> \<Rightarrow> t'; \<Gamma>\<turnstile> \<langle>b,t'\<rangle> \<Rightarrow> za; (\<not> isAbr za \<or> hs = []) \<and> n = length hs \<and> za = t \<or> (\<exists>q. za = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (n, t)); \<not> isAbr t'\<rbrakk> \<Longrightarrow> P; \<And>t'. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal z\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,t'\<rangle> \<Rightarrow> (n, t)\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P; h # hsa = (a;;
b) # hs; \<And>t' z. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> t'; \<Gamma>\<turnstile> \<langle>b,t'\<rangle> \<Rightarrow> z; (\<not> isAbr z \<or> hs = []) \<and> n = length hs \<and> z = t \<or> (\<exists>q. z = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (n, t)); \<not> isAbr t'\<rbrakk> \<Longrightarrow> P; \<And>t'. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,t'\<rangle> \<Rightarrow> (n, t)\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
 2. \<And>s. \<lbrakk>[] = (a;;
b) # hs; \<And>t' z. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> t'; \<Gamma>\<turnstile> \<langle>b,t'\<rangle> \<Rightarrow> z; (\<not> isAbr z \<or> hs = []) \<and> 0 = length hs \<and> z = Abrupt s \<or> (\<exists>q. z = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (0, Abrupt s)); \<not> isAbr t'\<rbrakk> \<Longrightarrow> P; \<And>t'. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,t'\<rangle> \<Rightarrow> (0, Abrupt s)\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P proof (state)
this:
\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> Abrupt z

goal (2 subgoals):
 1. \<And>h s z hsa n t. \<lbrakk>\<Gamma>\<turnstile> \<langle>h,Normal s\<rangle> \<Rightarrow> Abrupt z; \<Gamma>\<turnstile>\<^sub>h \<langle>hsa,z\<rangle> \<Rightarrow> (n, t); \<lbrakk>hsa = (a;;
b) # hs; \<And>t' za. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal z\<rangle> \<Rightarrow> t'; \<Gamma>\<turnstile> \<langle>b,t'\<rangle> \<Rightarrow> za; (\<not> isAbr za \<or> hs = []) \<and> n = length hs \<and> za = t \<or> (\<exists>q. za = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (n, t)); \<not> isAbr t'\<rbrakk> \<Longrightarrow> P; \<And>t'. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal z\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,t'\<rangle> \<Rightarrow> (n, t)\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P; h # hsa = (a;;
b) # hs; \<And>t' z. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> t'; \<Gamma>\<turnstile> \<langle>b,t'\<rangle> \<Rightarrow> z; (\<not> isAbr z \<or> hs = []) \<and> n = length hs \<and> z = t \<or> (\<exists>q. z = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (n, t)); \<not> isAbr t'\<rbrakk> \<Longrightarrow> P; \<And>t'. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,t'\<rangle> \<Rightarrow> (n, t)\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
 2. \<And>s. \<lbrakk>[] = (a;;
b) # hs; \<And>t' z. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> t'; \<Gamma>\<turnstile> \<langle>b,t'\<rangle> \<Rightarrow> z; (\<not> isAbr z \<or> hs = []) \<and> 0 = length hs \<and> z = Abrupt s \<or> (\<exists>q. z = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (0, Abrupt s)); \<not> isAbr t'\<rbrakk> \<Longrightarrow> P; \<And>t'. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,t'\<rangle> \<Rightarrow> (0, Abrupt s)\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P proof (prove)
using this:
\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> Abrupt z

goal (1 subgoal):
 1. P proof (state)
goal (1 subgoal):
 1. \<Gamma>\<turnstile>\<^sub>h \<langle>hs,z\<rangle> \<Rightarrow> (n, t) proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile>\<^sub>h \<langle>hs,z\<rangle> \<Rightarrow> (n, t) proof (state)
this:
\<Gamma>\<turnstile>\<^sub>h \<langle>hs,z\<rangle> \<Rightarrow> (n, t)

goal:
No subgoals! proof (state)
this:
P

goal (2 subgoals):
 1. \<And>h s z hsa n t. \<lbrakk>\<Gamma>\<turnstile> \<langle>h,Normal s\<rangle> \<Rightarrow> Abrupt z; \<Gamma>\<turnstile>\<^sub>h \<langle>hsa,z\<rangle> \<Rightarrow> (n, t); \<lbrakk>hsa = (a;;
b) # hs; \<And>t' za. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal z\<rangle> \<Rightarrow> t'; \<Gamma>\<turnstile> \<langle>b,t'\<rangle> \<Rightarrow> za; (\<not> isAbr za \<or> hs = []) \<and> n = length hs \<and> za = t \<or> (\<exists>q. za = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (n, t)); \<not> isAbr t'\<rbrakk> \<Longrightarrow> P; \<And>t'. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal z\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,t'\<rangle> \<Rightarrow> (n, t)\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P; h # hsa = (a;;
b) # hs; \<And>t' z. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> t'; \<Gamma>\<turnstile> \<langle>b,t'\<rangle> \<Rightarrow> z; (\<not> isAbr z \<or> hs = []) \<and> n = length hs \<and> z = t \<or> (\<exists>q. z = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (n, t)); \<not> isAbr t'\<rbrakk> \<Longrightarrow> P; \<And>t'. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,t'\<rangle> \<Rightarrow> (n, t)\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
 2. \<And>s. \<lbrakk>[] = (a;;
b) # hs; \<And>t' z. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> t'; \<Gamma>\<turnstile> \<langle>b,t'\<rangle> \<Rightarrow> z; (\<not> isAbr z \<or> hs = []) \<and> 0 = length hs \<and> z = Abrupt s \<or> (\<exists>q. z = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (0, Abrupt s)); \<not> isAbr t'\<rbrakk> \<Longrightarrow> P; \<And>t'. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,t'\<rangle> \<Rightarrow> (0, Abrupt s)\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P proof (state)
this:
\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> Abrupt z \<Longrightarrow> P

goal (2 subgoals):
 1. \<And>h s z hsa n t. \<lbrakk>\<Gamma>\<turnstile> \<langle>h,Normal s\<rangle> \<Rightarrow> Abrupt z; \<Gamma>\<turnstile>\<^sub>h \<langle>hsa,z\<rangle> \<Rightarrow> (n, t); \<lbrakk>hsa = (a;;
b) # hs; \<And>t' za. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal z\<rangle> \<Rightarrow> t'; \<Gamma>\<turnstile> \<langle>b,t'\<rangle> \<Rightarrow> za; (\<not> isAbr za \<or> hs = []) \<and> n = length hs \<and> za = t \<or> (\<exists>q. za = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (n, t)); \<not> isAbr t'\<rbrakk> \<Longrightarrow> P; \<And>t'. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal z\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,t'\<rangle> \<Rightarrow> (n, t)\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P; h # hsa = (a;;
b) # hs; \<And>t' z. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> t'; \<Gamma>\<turnstile> \<langle>b,t'\<rangle> \<Rightarrow> z; (\<not> isAbr z \<or> hs = []) \<and> n = length hs \<and> z = t \<or> (\<exists>q. z = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (n, t)); \<not> isAbr t'\<rbrakk> \<Longrightarrow> P; \<And>t'. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,t'\<rangle> \<Rightarrow> (n, t)\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
 2. \<And>s. \<lbrakk>[] = (a;;
b) # hs; \<And>t' z. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> t'; \<Gamma>\<turnstile> \<langle>b,t'\<rangle> \<Rightarrow> z; (\<not> isAbr z \<or> hs = []) \<and> 0 = length hs \<and> z = Abrupt s \<or> (\<exists>q. z = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (0, Abrupt s)); \<not> isAbr t'\<rbrakk> \<Longrightarrow> P; \<And>t'. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,t'\<rangle> \<Rightarrow> (0, Abrupt s)\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P proof (state)
this:
\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> Abrupt z \<Longrightarrow> P

goal (2 subgoals):
 1. \<And>h s z hsa n t. \<lbrakk>\<Gamma>\<turnstile> \<langle>h,Normal s\<rangle> \<Rightarrow> Abrupt z; \<Gamma>\<turnstile>\<^sub>h \<langle>hsa,z\<rangle> \<Rightarrow> (n, t); \<lbrakk>hsa = (a;;
b) # hs; \<And>t' za. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal z\<rangle> \<Rightarrow> t'; \<Gamma>\<turnstile> \<langle>b,t'\<rangle> \<Rightarrow> za; (\<not> isAbr za \<or> hs = []) \<and> n = length hs \<and> za = t \<or> (\<exists>q. za = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (n, t)); \<not> isAbr t'\<rbrakk> \<Longrightarrow> P; \<And>t'. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal z\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,t'\<rangle> \<Rightarrow> (n, t)\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P; h # hsa = (a;;
b) # hs; \<And>t' z. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> t'; \<Gamma>\<turnstile> \<langle>b,t'\<rangle> \<Rightarrow> z; (\<not> isAbr z \<or> hs = []) \<and> n = length hs \<and> z = t \<or> (\<exists>q. z = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (n, t)); \<not> isAbr t'\<rbrakk> \<Longrightarrow> P; \<And>t'. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,t'\<rangle> \<Rightarrow> (n, t)\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
 2. \<And>s. \<lbrakk>[] = (a;;
b) # hs; \<And>t' z. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> t'; \<Gamma>\<turnstile> \<langle>b,t'\<rangle> \<Rightarrow> z; (\<not> isAbr z \<or> hs = []) \<and> 0 = length hs \<and> z = Abrupt s \<or> (\<exists>q. z = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (0, Abrupt s)); \<not> isAbr t'\<rbrakk> \<Longrightarrow> P; \<And>t'. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,t'\<rangle> \<Rightarrow> (0, Abrupt s)\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P proof (state)
this:
\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> Abrupt z \<Longrightarrow> P

goal (2 subgoals):
 1. \<And>h s z hsa n t. \<lbrakk>\<Gamma>\<turnstile> \<langle>h,Normal s\<rangle> \<Rightarrow> Abrupt z; \<Gamma>\<turnstile>\<^sub>h \<langle>hsa,z\<rangle> \<Rightarrow> (n, t); \<lbrakk>hsa = (a;;
b) # hs; \<And>t' za. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal z\<rangle> \<Rightarrow> t'; \<Gamma>\<turnstile> \<langle>b,t'\<rangle> \<Rightarrow> za; (\<not> isAbr za \<or> hs = []) \<and> n = length hs \<and> za = t \<or> (\<exists>q. za = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (n, t)); \<not> isAbr t'\<rbrakk> \<Longrightarrow> P; \<And>t'. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal z\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,t'\<rangle> \<Rightarrow> (n, t)\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P; h # hsa = (a;;
b) # hs; \<And>t' z. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> t'; \<Gamma>\<turnstile> \<langle>b,t'\<rangle> \<Rightarrow> z; (\<not> isAbr z \<or> hs = []) \<and> n = length hs \<and> z = t \<or> (\<exists>q. z = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (n, t)); \<not> isAbr t'\<rbrakk> \<Longrightarrow> P; \<And>t'. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,t'\<rangle> \<Rightarrow> (n, t)\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
 2. \<And>s. \<lbrakk>[] = (a;;
b) # hs; \<And>t' z. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> t'; \<Gamma>\<turnstile> \<langle>b,t'\<rangle> \<Rightarrow> z; (\<not> isAbr z \<or> hs = []) \<and> 0 = length hs \<and> z = Abrupt s \<or> (\<exists>q. z = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (0, Abrupt s)); \<not> isAbr t'\<rbrakk> \<Longrightarrow> P; \<And>t'. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,t'\<rangle> \<Rightarrow> (0, Abrupt s)\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P proof (state)
goal (2 subgoals):
 1. \<And>h s z hsa n t. \<lbrakk>\<Gamma>\<turnstile> \<langle>h,Normal s\<rangle> \<Rightarrow> Abrupt z; \<Gamma>\<turnstile>\<^sub>h \<langle>hsa,z\<rangle> \<Rightarrow> (n, t); \<lbrakk>hsa = (a;;
b) # hs; \<And>t' za. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal z\<rangle> \<Rightarrow> t'; \<Gamma>\<turnstile> \<langle>b,t'\<rangle> \<Rightarrow> za; (\<not> isAbr za \<or> hs = []) \<and> n = length hs \<and> za = t \<or> (\<exists>q. za = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (n, t)); \<not> isAbr t'\<rbrakk> \<Longrightarrow> P; \<And>t'. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal z\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,t'\<rangle> \<Rightarrow> (n, t)\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P; h # hsa = (a;;
b) # hs; \<And>t' z. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> t'; \<Gamma>\<turnstile> \<langle>b,t'\<rangle> \<Rightarrow> z; (\<not> isAbr z \<or> hs = []) \<and> n = length hs \<and> z = t \<or> (\<exists>q. z = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (n, t)); \<not> isAbr t'\<rbrakk> \<Longrightarrow> P; \<And>t'. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,t'\<rangle> \<Rightarrow> (n, t)\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
 2. \<And>s. \<lbrakk>[] = (a;;
b) # hs; \<And>t' z. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> t'; \<Gamma>\<turnstile> \<langle>b,t'\<rangle> \<Rightarrow> z; (\<not> isAbr z \<or> hs = []) \<and> 0 = length hs \<and> z = Abrupt s \<or> (\<exists>q. z = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (0, Abrupt s)); \<not> isAbr t'\<rbrakk> \<Longrightarrow> P; \<And>t'. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,t'\<rangle> \<Rightarrow> (0, Abrupt s)\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P proof (state)
this:
\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> Normal s''
\<Gamma>\<turnstile> \<langle>b,Normal s''\<rangle> \<Rightarrow> Abrupt z

goal (2 subgoals):
 1. \<And>h s z hsa n t. \<lbrakk>\<Gamma>\<turnstile> \<langle>h,Normal s\<rangle> \<Rightarrow> Abrupt z; \<Gamma>\<turnstile>\<^sub>h \<langle>hsa,z\<rangle> \<Rightarrow> (n, t); \<lbrakk>hsa = (a;;
b) # hs; \<And>t' za. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal z\<rangle> \<Rightarrow> t'; \<Gamma>\<turnstile> \<langle>b,t'\<rangle> \<Rightarrow> za; (\<not> isAbr za \<or> hs = []) \<and> n = length hs \<and> za = t \<or> (\<exists>q. za = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (n, t)); \<not> isAbr t'\<rbrakk> \<Longrightarrow> P; \<And>t'. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal z\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,t'\<rangle> \<Rightarrow> (n, t)\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P; h # hsa = (a;;
b) # hs; \<And>t' z. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> t'; \<Gamma>\<turnstile> \<langle>b,t'\<rangle> \<Rightarrow> z; (\<not> isAbr z \<or> hs = []) \<and> n = length hs \<and> z = t \<or> (\<exists>q. z = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (n, t)); \<not> isAbr t'\<rbrakk> \<Longrightarrow> P; \<And>t'. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,t'\<rangle> \<Rightarrow> (n, t)\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
 2. \<And>s. \<lbrakk>[] = (a;;
b) # hs; \<And>t' z. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> t'; \<Gamma>\<turnstile> \<langle>b,t'\<rangle> \<Rightarrow> z; (\<not> isAbr z \<or> hs = []) \<and> 0 = length hs \<and> z = Abrupt s \<or> (\<exists>q. z = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (0, Abrupt s)); \<not> isAbr t'\<rbrakk> \<Longrightarrow> P; \<And>t'. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,t'\<rangle> \<Rightarrow> (0, Abrupt s)\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P proof (prove)
using this:
\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> Normal s''
\<Gamma>\<turnstile> \<langle>b,Normal s''\<rangle> \<Rightarrow> Abrupt z

goal (1 subgoal):
 1. P proof (state)
goal (2 subgoals):
 1. (\<not> isAbr (Abrupt z) \<or> hs = []) \<and> n = length hs \<and> Abrupt z = t \<or> (\<exists>q. Abrupt z = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (n, t))
 2. \<not> isAbr (Normal s'') proof (prove)
goal (1 subgoal):
 1. (\<not> isAbr (Abrupt z) \<or> hs = []) \<and> n = length hs \<and> Abrupt z = t \<or> (\<exists>q. Abrupt z = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (n, t)) proof (prove)
using this:
\<Gamma>\<turnstile>\<^sub>h \<langle>hs',z\<rangle> \<Rightarrow> (n, t)

goal (1 subgoal):
 1. (\<not> isAbr (Abrupt z) \<or> hs = []) \<and> n = length hs \<and> Abrupt z = t \<or> (\<exists>q. Abrupt z = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (n, t)) proof (state)
this:
(\<not> isAbr (Abrupt z) \<or> hs = []) \<and> n = length hs \<and> Abrupt z = t \<or> (\<exists>q. Abrupt z = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (n, t))

goal (1 subgoal):
 1. \<not> isAbr (Normal s'') proof (prove)
goal (1 subgoal):
 1. \<not> isAbr (Normal s'') proof (state)
this:
\<not> isAbr (Normal s'')

goal:
No subgoals! proof (state)
this:
P

goal (2 subgoals):
 1. \<And>h s z hsa n t. \<lbrakk>\<Gamma>\<turnstile> \<langle>h,Normal s\<rangle> \<Rightarrow> Abrupt z; \<Gamma>\<turnstile>\<^sub>h \<langle>hsa,z\<rangle> \<Rightarrow> (n, t); \<lbrakk>hsa = (a;;
b) # hs; \<And>t' za. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal z\<rangle> \<Rightarrow> t'; \<Gamma>\<turnstile> \<langle>b,t'\<rangle> \<Rightarrow> za; (\<not> isAbr za \<or> hs = []) \<and> n = length hs \<and> za = t \<or> (\<exists>q. za = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (n, t)); \<not> isAbr t'\<rbrakk> \<Longrightarrow> P; \<And>t'. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal z\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,t'\<rangle> \<Rightarrow> (n, t)\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P; h # hsa = (a;;
b) # hs; \<And>t' z. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> t'; \<Gamma>\<turnstile> \<langle>b,t'\<rangle> \<Rightarrow> z; (\<not> isAbr z \<or> hs = []) \<and> n = length hs \<and> z = t \<or> (\<exists>q. z = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (n, t)); \<not> isAbr t'\<rbrakk> \<Longrightarrow> P; \<And>t'. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,t'\<rangle> \<Rightarrow> (n, t)\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
 2. \<And>s. \<lbrakk>[] = (a;;
b) # hs; \<And>t' z. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> t'; \<Gamma>\<turnstile> \<langle>b,t'\<rangle> \<Rightarrow> z; (\<not> isAbr z \<or> hs = []) \<and> 0 = length hs \<and> z = Abrupt s \<or> (\<exists>q. z = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (0, Abrupt s)); \<not> isAbr t'\<rbrakk> \<Longrightarrow> P; \<And>t'. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,t'\<rangle> \<Rightarrow> (0, Abrupt s)\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P proof (state)
this:
\<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> Normal ?s''2; \<Gamma>\<turnstile> \<langle>b,Normal ?s''2\<rangle> \<Rightarrow> Abrupt z\<rbrakk> \<Longrightarrow> P

goal (2 subgoals):
 1. \<And>h s z hsa n t. \<lbrakk>\<Gamma>\<turnstile> \<langle>h,Normal s\<rangle> \<Rightarrow> Abrupt z; \<Gamma>\<turnstile>\<^sub>h \<langle>hsa,z\<rangle> \<Rightarrow> (n, t); \<lbrakk>hsa = (a;;
b) # hs; \<And>t' za. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal z\<rangle> \<Rightarrow> t'; \<Gamma>\<turnstile> \<langle>b,t'\<rangle> \<Rightarrow> za; (\<not> isAbr za \<or> hs = []) \<and> n = length hs \<and> za = t \<or> (\<exists>q. za = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (n, t)); \<not> isAbr t'\<rbrakk> \<Longrightarrow> P; \<And>t'. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal z\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,t'\<rangle> \<Rightarrow> (n, t)\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P; h # hsa = (a;;
b) # hs; \<And>t' z. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> t'; \<Gamma>\<turnstile> \<langle>b,t'\<rangle> \<Rightarrow> z; (\<not> isAbr z \<or> hs = []) \<and> n = length hs \<and> z = t \<or> (\<exists>q. z = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (n, t)); \<not> isAbr t'\<rbrakk> \<Longrightarrow> P; \<And>t'. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,t'\<rangle> \<Rightarrow> (n, t)\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
 2. \<And>s. \<lbrakk>[] = (a;;
b) # hs; \<And>t' z. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> t'; \<Gamma>\<turnstile> \<langle>b,t'\<rangle> \<Rightarrow> z; (\<not> isAbr z \<or> hs = []) \<and> 0 = length hs \<and> z = Abrupt s \<or> (\<exists>q. z = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (0, Abrupt s)); \<not> isAbr t'\<rbrakk> \<Longrightarrow> P; \<And>t'. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,t'\<rangle> \<Rightarrow> (0, Abrupt s)\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P proof (chain)
picking this:
\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> Abrupt z \<Longrightarrow> P
\<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> Normal ?s''2; \<Gamma>\<turnstile> \<langle>b,Normal ?s''2\<rangle> \<Rightarrow> Abrupt z\<rbrakk> \<Longrightarrow> P proof (prove)
using this:
\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> Abrupt z \<Longrightarrow> P
\<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> Normal ?s''2; \<Gamma>\<turnstile> \<langle>b,Normal ?s''2\<rangle> \<Rightarrow> Abrupt z\<rbrakk> \<Longrightarrow> P

goal (1 subgoal):
 1. P proof (prove)
using this:
\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> Abrupt z \<Longrightarrow> P
\<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> Normal ?s''2; \<Gamma>\<turnstile> \<langle>b,Normal ?s''2\<rangle> \<Rightarrow> Abrupt z\<rbrakk> \<Longrightarrow> P
\<Gamma>\<turnstile> \<langle>a;;
b,Normal s\<rangle> \<Rightarrow> Abrupt z

goal (1 subgoal):
 1. P proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> Abrupt z \<Longrightarrow> P; \<And>s''. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> Normal s''; \<Gamma>\<turnstile> \<langle>b,Normal s''\<rangle> \<Rightarrow> Abrupt z\<rbrakk> \<Longrightarrow> P; \<Gamma>\<turnstile> \<langle>a;;
b,Normal s\<rangle> \<Rightarrow> Abrupt z\<rbrakk> \<Longrightarrow> P proof (prove)
goal (1 subgoal):
 1. \<And>s'. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> Abrupt z \<Longrightarrow> P; \<And>s''. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> Normal s''; \<Gamma>\<turnstile> \<langle>b,Normal s''\<rangle> \<Rightarrow> Abrupt z\<rbrakk> \<Longrightarrow> P; \<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> s'; \<Gamma>\<turnstile> \<langle>b,s'\<rangle> \<Rightarrow> Abrupt z\<rbrakk> \<Longrightarrow> P proof (prove)
goal (2 subgoals):
 1. \<And>s' t. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> Abrupt z \<Longrightarrow> P; \<And>s''. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> Normal s''; \<Gamma>\<turnstile> \<langle>b,Normal s''\<rangle> \<Rightarrow> Abrupt z\<rbrakk> \<Longrightarrow> P; \<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> s'; \<Gamma>\<turnstile> \<langle>b,Normal t\<rangle> \<Rightarrow> Abrupt z; s' = Normal t\<rbrakk> \<Longrightarrow> P
 2. \<And>s' t. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> Abrupt z \<Longrightarrow> P; \<And>s''. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> Normal s''; \<Gamma>\<turnstile> \<langle>b,Normal s''\<rangle> \<Rightarrow> Abrupt z\<rbrakk> \<Longrightarrow> P; \<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> s'; \<Gamma>\<turnstile> \<langle>b,Abrupt t\<rangle> \<Rightarrow> Abrupt z; s' = Abrupt t\<rbrakk> \<Longrightarrow> P proof (prove)
goal (1 subgoal):
 1. \<And>s' t. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> Abrupt z \<Longrightarrow> P; \<And>s''. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> Normal s''; \<Gamma>\<turnstile> \<langle>b,Normal s''\<rangle> \<Rightarrow> Abrupt z\<rbrakk> \<Longrightarrow> P; \<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> s'; \<Gamma>\<turnstile> \<langle>b,Abrupt t\<rangle> \<Rightarrow> Abrupt z; s' = Abrupt t\<rbrakk> \<Longrightarrow> P proof (prove)
goal (1 subgoal):
 1. \<And>s' t. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> Abrupt z \<Longrightarrow> P; \<And>s''. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> Normal s''; \<Gamma>\<turnstile> \<langle>b,Normal s''\<rangle> \<Rightarrow> Abrupt z\<rbrakk> \<Longrightarrow> P; \<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> Abrupt t; \<Gamma>\<turnstile> \<langle>b,Abrupt t\<rangle> \<Rightarrow> Abrupt z; s' = Abrupt t\<rbrakk> \<Longrightarrow> P proof (prove)
goal (1 subgoal):
 1. \<And>s' t. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> Abrupt z \<Longrightarrow> P; \<And>s''. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> Normal s''; \<Gamma>\<turnstile> \<langle>b,Normal s''\<rangle> \<Rightarrow> Abrupt z\<rbrakk> \<Longrightarrow> P; \<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> Abrupt t; s' = Abrupt t; Abrupt z = Abrupt t\<rbrakk> \<Longrightarrow> P proof (prove)
goal:
No subgoals! proof (state)
this:
P

goal (1 subgoal):
 1. \<And>s. \<lbrakk>[] = (a;;
b) # hs; \<And>t' z. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> t'; \<Gamma>\<turnstile> \<langle>b,t'\<rangle> \<Rightarrow> z; (\<not> isAbr z \<or> hs = []) \<and> 0 = length hs \<and> z = Abrupt s \<or> (\<exists>q. z = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (0, Abrupt s)); \<not> isAbr t'\<rbrakk> \<Longrightarrow> P; \<And>t'. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,t'\<rangle> \<Rightarrow> (0, Abrupt s)\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P proof (state)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>[] = (a;;
b) # hs; \<And>t' z. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> t'; \<Gamma>\<turnstile> \<langle>b,t'\<rangle> \<Rightarrow> z; (\<not> isAbr z \<or> hs = []) \<and> 0 = length hs \<and> z = Abrupt s \<or> (\<exists>q. z = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (0, Abrupt s)); \<not> isAbr t'\<rbrakk> \<Longrightarrow> P; \<And>t'. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,t'\<rangle> \<Rightarrow> (0, Abrupt s)\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P proof (state)
this:
[] = (a;;
b) # hs
\<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> ?t'; \<Gamma>\<turnstile> \<langle>b,?t'\<rangle> \<Rightarrow> ?z; (\<not> isAbr ?z \<or> hs = []) \<and> 0 = length hs \<and> ?z = Abrupt s \<or> (\<exists>q. ?z = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (0, Abrupt s)); \<not> isAbr ?t'\<rbrakk> \<Longrightarrow> P
\<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> Abrupt ?t'; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,?t'\<rangle> \<Rightarrow> (0, Abrupt s)\<rbrakk> \<Longrightarrow> P

goal (1 subgoal):
 1. \<And>s. \<lbrakk>[] = (a;;
b) # hs; \<And>t' z. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> t'; \<Gamma>\<turnstile> \<langle>b,t'\<rangle> \<Rightarrow> z; (\<not> isAbr z \<or> hs = []) \<and> 0 = length hs \<and> z = Abrupt s \<or> (\<exists>q. z = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (0, Abrupt s)); \<not> isAbr t'\<rbrakk> \<Longrightarrow> P; \<And>t'. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> Abrupt t'; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,t'\<rangle> \<Rightarrow> (0, Abrupt s)\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P proof (prove)
using this:
[] = (a;;
b) # hs
\<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> ?t'; \<Gamma>\<turnstile> \<langle>b,?t'\<rangle> \<Rightarrow> ?z; (\<not> isAbr ?z \<or> hs = []) \<and> 0 = length hs \<and> ?z = Abrupt s \<or> (\<exists>q. ?z = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (0, Abrupt s)); \<not> isAbr ?t'\<rbrakk> \<Longrightarrow> P
\<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> Abrupt ?t'; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,?t'\<rangle> \<Rightarrow> (0, Abrupt s)\<rbrakk> \<Longrightarrow> P

goal (1 subgoal):
 1. P proof (state)
this:
P

goal:
No subgoals!