theory Corres_UL_C

lemma ccorres_context_cong_helper:
  assumes "\<And>s. P s = P' s"
  assumes "\<And>s s'. \<lbrakk> (s, s') \<in> sr; P' s \<rbrakk> \<Longrightarrow> Q = Q'"
  assumes "hs = hs'"
  assumes "\<And>s s'. \<lbrakk> (s, s') \<in> sr; P' s; s' \<in> Q' \<rbrakk> \<Longrightarrow> a s = a' s"
  assumes "\<And>s s' s''. \<lbrakk> (s, s') \<in> sr; P' s; s' \<in> Q' \<rbrakk>  \<Longrightarrow> semantic_equiv \<Gamma> s' s'' c c'"
  assumes "\<And>s s' t'.
             \<lbrakk> (s, s') \<in> sr; P' s; s' \<in> Q'; \<Gamma> \<turnstile>\<^sub>h \<langle>c' # hs', s'\<rangle> \<Rightarrow> (size hs', Normal t') \<rbrakk> \<Longrightarrow>
             xf t' = xf' t'"
  assumes "\<And>x s t s' t'.
             \<lbrakk> (s, s') \<in> sr; P' s; s' \<in> Q'; (t, t') \<in> sr; (x, t) \<in> fst (a' s);
               \<Gamma> \<turnstile>\<^sub>h \<langle>c' # hs', s'\<rangle> \<Rightarrow> (size hs', Normal t') \<rbrakk> \<Longrightarrow>
             r x (xf' t') = r' x (xf' t')"
  assumes "\<And>s s' t' n.
             \<lbrakk> (s, s') \<in> sr; P' s; s' \<in> Q'; n \<noteq> size hs'; \<Gamma> \<turnstile>\<^sub>h \<langle>c' # hs', s'\<rangle> \<Rightarrow> (n, Normal t') \<rbrakk> \<Longrightarrow>
             axf t' = axf' t'"
  assumes "\<And>x s t s' t' n.
             \<lbrakk> (s, s') \<in> sr; P' s; s' \<in> Q'; (t, t') \<in> sr; (x, t) \<in> fst (a' s); n \<noteq> size hs';
               \<Gamma> \<turnstile>\<^sub>h \<langle>c' # hs', s'\<rangle> \<Rightarrow> (n, Normal t') \<rbrakk> \<Longrightarrow>
             ar x (axf' t') = ar' x (axf' t')"
  shows   "ccorres_underlying sr \<Gamma> r xf ar axf P Q hs a c
           = ccorres_underlying sr \<Gamma> r' xf' ar' axf' P' Q' hs' a' c'" using assms apply - apply rule apply (erule ccorres_context_cong_helper'; assumption) apply (erule ccorres_context_cong_helper') by (fastforce simp: semantic_equiv_sym exec_handlers_semantic_equiv[where a=c and b=c'])+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_underlying sr \<Gamma> r xf ar axf P Q hs a c = ccorres_underlying sr \<Gamma> r' xf' ar' axf' P' Q' hs' a' c' proof (prove)
using this:
P ?s = P' ?s
\<lbrakk>(?s, ?s') \<in> sr; P' ?s\<rbrakk> \<Longrightarrow> Q = Q'
hs = hs'
\<lbrakk>(?s, ?s') \<in> sr; P' ?s; ?s' \<in> Q'\<rbrakk> \<Longrightarrow> a ?s = a' ?s
\<lbrakk>(?s, ?s') \<in> sr; P' ?s; ?s' \<in> Q'\<rbrakk> \<Longrightarrow> semantic_equiv \<Gamma> ?s' ?s'' c c'
\<lbrakk>(?s, ?s') \<in> sr; P' ?s; ?s' \<in> Q'; \<Gamma>\<turnstile>\<^sub>h \<langle>c' # hs',?s'\<rangle> \<Rightarrow> (length hs', Normal ?t')\<rbrakk> \<Longrightarrow> xf ?t' = xf' ?t'
\<lbrakk>(?s, ?s') \<in> sr; P' ?s; ?s' \<in> Q'; (?t, ?t') \<in> sr; (?x, ?t) \<in> fst (a' ?s); \<Gamma>\<turnstile>\<^sub>h \<langle>c' # hs',?s'\<rangle> \<Rightarrow> (length hs', Normal ?t')\<rbrakk> \<Longrightarrow> r ?x (xf' ?t') = r' ?x (xf' ?t')
\<lbrakk>(?s, ?s') \<in> sr; P' ?s; ?s' \<in> Q'; ?n \<noteq> length hs'; \<Gamma>\<turnstile>\<^sub>h \<langle>c' # hs',?s'\<rangle> \<Rightarrow> (?n, Normal ?t')\<rbrakk> \<Longrightarrow> axf ?t' = axf' ?t'
\<lbrakk>(?s, ?s') \<in> sr; P' ?s; ?s' \<in> Q'; (?t, ?t') \<in> sr; (?x, ?t) \<in> fst (a' ?s); ?n \<noteq> length hs'; \<Gamma>\<turnstile>\<^sub>h \<langle>c' # hs',?s'\<rangle> \<Rightarrow> (?n, Normal ?t')\<rbrakk> \<Longrightarrow> ar ?x (axf' ?t') = ar' ?x (axf' ?t')

goal (1 subgoal):
 1. ccorres_underlying sr \<Gamma> r xf ar axf P Q hs a c = ccorres_underlying sr \<Gamma> r' xf' ar' axf' P' Q' hs' a' c' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>s. P s = P' s; \<And>s s'. \<lbrakk>(s, s') \<in> sr; P' s\<rbrakk> \<Longrightarrow> Q = Q'; hs = hs'; \<And>s s'. \<lbrakk>(s, s') \<in> sr; P' s; s' \<in> Q'\<rbrakk> \<Longrightarrow> a s = a' s; \<And>s s' s''. \<lbrakk>(s, s') \<in> sr; P' s; s' \<in> Q'\<rbrakk> \<Longrightarrow> semantic_equiv \<Gamma> s' s'' c c'; \<And>s s' t'. \<lbrakk>(s, s') \<in> sr; P' s; s' \<in> Q'; \<Gamma>\<turnstile>\<^sub>h \<langle>c' # hs',s'\<rangle> \<Rightarrow> (length hs', Normal t')\<rbrakk> \<Longrightarrow> xf t' = xf' t'; \<And>s s' t t' x. \<lbrakk>(s, s') \<in> sr; P' s; s' \<in> Q'; (t, t') \<in> sr; (x, t) \<in> fst (a' s); \<Gamma>\<turnstile>\<^sub>h \<langle>c' # hs',s'\<rangle> \<Rightarrow> (length hs', Normal t')\<rbrakk> \<Longrightarrow> r x (xf' t') = r' x (xf' t'); \<And>s s' n t'. \<lbrakk>(s, s') \<in> sr; P' s; s' \<in> Q'; n \<noteq> length hs'; \<Gamma>\<turnstile>\<^sub>h \<langle>c' # hs',s'\<rangle> \<Rightarrow> (n, Normal t')\<rbrakk> \<Longrightarrow> axf t' = axf' t'; \<And>s s' t t' x n. \<lbrakk>(s, s') \<in> sr; P' s; s' \<in> Q'; (t, t') \<in> sr; (x, t) \<in> fst (a' s); n \<noteq> length hs'; \<Gamma>\<turnstile>\<^sub>h \<langle>c' # hs',s'\<rangle> \<Rightarrow> (n, Normal t')\<rbrakk> \<Longrightarrow> ar x (axf' t') = ar' x (axf' t')\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf ar axf P Q hs a c = ccorres_underlying sr \<Gamma> r' xf' ar' axf' P' Q' hs' a' c' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<And>s. P s = P' s; \<And>s s'. \<lbrakk>(s, s') \<in> sr; P' s\<rbrakk> \<Longrightarrow> Q = Q'; hs = hs'; \<And>s s'. \<lbrakk>(s, s') \<in> sr; P' s; s' \<in> Q'\<rbrakk> \<Longrightarrow> a s = a' s; \<And>s s' s''. \<lbrakk>(s, s') \<in> sr; P' s; s' \<in> Q'\<rbrakk> \<Longrightarrow> semantic_equiv \<Gamma> s' s'' c c'; \<And>s s' t'. \<lbrakk>(s, s') \<in> sr; P' s; s' \<in> Q'; \<Gamma>\<turnstile>\<^sub>h \<langle>c' # hs',s'\<rangle> \<Rightarrow> (length hs', Normal t')\<rbrakk> \<Longrightarrow> xf t' = xf' t'; \<And>s s' t t' x. \<lbrakk>(s, s') \<in> sr; P' s; s' \<in> Q'; (t, t') \<in> sr; (x, t) \<in> fst (a' s); \<Gamma>\<turnstile>\<^sub>h \<langle>c' # hs',s'\<rangle> \<Rightarrow> (length hs', Normal t')\<rbrakk> \<Longrightarrow> r x (xf' t') = r' x (xf' t'); \<And>s s' n t'. \<lbrakk>(s, s') \<in> sr; P' s; s' \<in> Q'; n \<noteq> length hs'; \<Gamma>\<turnstile>\<^sub>h \<langle>c' # hs',s'\<rangle> \<Rightarrow> (n, Normal t')\<rbrakk> \<Longrightarrow> axf t' = axf' t'; \<And>s s' t t' x n. \<lbrakk>(s, s') \<in> sr; P' s; s' \<in> Q'; (t, t') \<in> sr; (x, t) \<in> fst (a' s); n \<noteq> length hs'; \<Gamma>\<turnstile>\<^sub>h \<langle>c' # hs',s'\<rangle> \<Rightarrow> (n, Normal t')\<rbrakk> \<Longrightarrow> ar x (axf' t') = ar' x (axf' t'); ccorres_underlying sr \<Gamma> r xf ar axf P Q hs a c\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r' xf' ar' axf' P' Q' hs' a' c'
 2. \<lbrakk>\<And>s. P s = P' s; \<And>s s'. \<lbrakk>(s, s') \<in> sr; P' s\<rbrakk> \<Longrightarrow> Q = Q'; hs = hs'; \<And>s s'. \<lbrakk>(s, s') \<in> sr; P' s; s' \<in> Q'\<rbrakk> \<Longrightarrow> a s = a' s; \<And>s s' s''. \<lbrakk>(s, s') \<in> sr; P' s; s' \<in> Q'\<rbrakk> \<Longrightarrow> semantic_equiv \<Gamma> s' s'' c c'; \<And>s s' t'. \<lbrakk>(s, s') \<in> sr; P' s; s' \<in> Q'; \<Gamma>\<turnstile>\<^sub>h \<langle>c' # hs',s'\<rangle> \<Rightarrow> (length hs', Normal t')\<rbrakk> \<Longrightarrow> xf t' = xf' t'; \<And>s s' t t' x. \<lbrakk>(s, s') \<in> sr; P' s; s' \<in> Q'; (t, t') \<in> sr; (x, t) \<in> fst (a' s); \<Gamma>\<turnstile>\<^sub>h \<langle>c' # hs',s'\<rangle> \<Rightarrow> (length hs', Normal t')\<rbrakk> \<Longrightarrow> r x (xf' t') = r' x (xf' t'); \<And>s s' n t'. \<lbrakk>(s, s') \<in> sr; P' s; s' \<in> Q'; n \<noteq> length hs'; \<Gamma>\<turnstile>\<^sub>h \<langle>c' # hs',s'\<rangle> \<Rightarrow> (n, Normal t')\<rbrakk> \<Longrightarrow> axf t' = axf' t'; \<And>s s' t t' x n. \<lbrakk>(s, s') \<in> sr; P' s; s' \<in> Q'; (t, t') \<in> sr; (x, t) \<in> fst (a' s); n \<noteq> length hs'; \<Gamma>\<turnstile>\<^sub>h \<langle>c' # hs',s'\<rangle> \<Rightarrow> (n, Normal t')\<rbrakk> \<Longrightarrow> ar x (axf' t') = ar' x (axf' t'); ccorres_underlying sr \<Gamma> r' xf' ar' axf' P' Q' hs' a' c'\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf ar axf P Q hs a c proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>s. P s = P' s; \<And>s s'. \<lbrakk>(s, s') \<in> sr; P' s\<rbrakk> \<Longrightarrow> Q = Q'; hs = hs'; \<And>s s'. \<lbrakk>(s, s') \<in> sr; P' s; s' \<in> Q'\<rbrakk> \<Longrightarrow> a s = a' s; \<And>s s' s''. \<lbrakk>(s, s') \<in> sr; P' s; s' \<in> Q'\<rbrakk> \<Longrightarrow> semantic_equiv \<Gamma> s' s'' c c'; \<And>s s' t'. \<lbrakk>(s, s') \<in> sr; P' s; s' \<in> Q'; \<Gamma>\<turnstile>\<^sub>h \<langle>c' # hs',s'\<rangle> \<Rightarrow> (length hs', Normal t')\<rbrakk> \<Longrightarrow> xf t' = xf' t'; \<And>s s' t t' x. \<lbrakk>(s, s') \<in> sr; P' s; s' \<in> Q'; (t, t') \<in> sr; (x, t) \<in> fst (a' s); \<Gamma>\<turnstile>\<^sub>h \<langle>c' # hs',s'\<rangle> \<Rightarrow> (length hs', Normal t')\<rbrakk> \<Longrightarrow> r x (xf' t') = r' x (xf' t'); \<And>s s' n t'. \<lbrakk>(s, s') \<in> sr; P' s; s' \<in> Q'; n \<noteq> length hs'; \<Gamma>\<turnstile>\<^sub>h \<langle>c' # hs',s'\<rangle> \<Rightarrow> (n, Normal t')\<rbrakk> \<Longrightarrow> axf t' = axf' t'; \<And>s s' t t' x n. \<lbrakk>(s, s') \<in> sr; P' s; s' \<in> Q'; (t, t') \<in> sr; (x, t) \<in> fst (a' s); n \<noteq> length hs'; \<Gamma>\<turnstile>\<^sub>h \<langle>c' # hs',s'\<rangle> \<Rightarrow> (n, Normal t')\<rbrakk> \<Longrightarrow> ar x (axf' t') = ar' x (axf' t'); ccorres_underlying sr \<Gamma> r' xf' ar' axf' P' Q' hs' a' c'\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf ar axf P Q hs a c proof (prove)
goal (9 subgoals):
 1. \<And>s. \<lbrakk>\<And>s. P s = P' s; \<And>s s'. \<lbrakk>(s, s') \<in> sr; P' s\<rbrakk> \<Longrightarrow> Q = Q'; hs = hs'; \<And>s s'. \<lbrakk>(s, s') \<in> sr; P' s; s' \<in> Q'\<rbrakk> \<Longrightarrow> a s = a' s; \<And>s s' s''. \<lbrakk>(s, s') \<in> sr; P' s; s' \<in> Q'\<rbrakk> \<Longrightarrow> semantic_equiv \<Gamma> s' s'' c c'; \<And>s s' t'. \<lbrakk>(s, s') \<in> sr; P' s; s' \<in> Q'; \<Gamma>\<turnstile>\<^sub>h \<langle>c' # hs',s'\<rangle> \<Rightarrow> (length hs', Normal t')\<rbrakk> \<Longrightarrow> xf t' = xf' t'; \<And>s s' t t' x. \<lbrakk>(s, s') \<in> sr; P' s; s' \<in> Q'; (t, t') \<in> sr; (x, t) \<in> fst (a' s); \<Gamma>\<turnstile>\<^sub>h \<langle>c' # hs',s'\<rangle> \<Rightarrow> (length hs', Normal t')\<rbrakk> \<Longrightarrow> r x (xf' t') = r' x (xf' t'); \<And>s s' n t'. \<lbrakk>(s, s') \<in> sr; P' s; s' \<in> Q'; n \<noteq> length hs'; \<Gamma>\<turnstile>\<^sub>h \<langle>c' # hs',s'\<rangle> \<Rightarrow> (n, Normal t')\<rbrakk> \<Longrightarrow> axf t' = axf' t'; \<And>s s' t t' x n. \<lbrakk>(s, s') \<in> sr; P' s; s' \<in> Q'; (t, t') \<in> sr; (x, t) \<in> fst (a' s); n \<noteq> length hs'; \<Gamma>\<turnstile>\<^sub>h \<langle>c' # hs',s'\<rangle> \<Rightarrow> (n, Normal t')\<rbrakk> \<Longrightarrow> ar x (axf' t') = ar' x (axf' t')\<rbrakk> \<Longrightarrow> P' s = P s
 2. \<And>s s'. \<lbrakk>\<And>s. P s = P' s; \<And>s s'. \<lbrakk>(s, s') \<in> sr; P' s\<rbrakk> \<Longrightarrow> Q = Q'; hs = hs'; \<And>s s'. \<lbrakk>(s, s') \<in> sr; P' s; s' \<in> Q'\<rbrakk> \<Longrightarrow> a s = a' s; \<And>s s' s''. \<lbrakk>(s, s') \<in> sr; P' s; s' \<in> Q'\<rbrakk> \<Longrightarrow> semantic_equiv \<Gamma> s' s'' c c'; \<And>s s' t'. \<lbrakk>(s, s') \<in> sr; P' s; s' \<in> Q'; \<Gamma>\<turnstile>\<^sub>h \<langle>c' # hs',s'\<rangle> \<Rightarrow> (length hs', Normal t')\<rbrakk> \<Longrightarrow> xf t' = xf' t'; \<And>s s' t t' x. \<lbrakk>(s, s') \<in> sr; P' s; s' \<in> Q'; (t, t') \<in> sr; (x, t) \<in> fst (a' s); \<Gamma>\<turnstile>\<^sub>h \<langle>c' # hs',s'\<rangle> \<Rightarrow> (length hs', Normal t')\<rbrakk> \<Longrightarrow> r x (xf' t') = r' x (xf' t'); \<And>s s' n t'. \<lbrakk>(s, s') \<in> sr; P' s; s' \<in> Q'; n \<noteq> length hs'; \<Gamma>\<turnstile>\<^sub>h \<langle>c' # hs',s'\<rangle> \<Rightarrow> (n, Normal t')\<rbrakk> \<Longrightarrow> axf t' = axf' t'; \<And>s s' t t' x n. \<lbrakk>(s, s') \<in> sr; P' s; s' \<in> Q'; (t, t') \<in> sr; (x, t) \<in> fst (a' s); n \<noteq> length hs'; \<Gamma>\<turnstile>\<^sub>h \<langle>c' # hs',s'\<rangle> \<Rightarrow> (n, Normal t')\<rbrakk> \<Longrightarrow> ar x (axf' t') = ar' x (axf' t'); (s, s') \<in> sr; P s\<rbrakk> \<Longrightarrow> Q' = Q
 3. \<lbrakk>\<And>s. P s = P' s; \<And>s s'. \<lbrakk>(s, s') \<in> sr; P' s\<rbrakk> \<Longrightarrow> Q = Q'; hs = hs'; \<And>s s'. \<lbrakk>(s, s') \<in> sr; P' s; s' \<in> Q'\<rbrakk> \<Longrightarrow> a s = a' s; \<And>s s' s''. \<lbrakk>(s, s') \<in> sr; P' s; s' \<in> Q'\<rbrakk> \<Longrightarrow> semantic_equiv \<Gamma> s' s'' c c'; \<And>s s' t'. \<lbrakk>(s, s') \<in> sr; P' s; s' \<in> Q'; \<Gamma>\<turnstile>\<^sub>h \<langle>c' # hs',s'\<rangle> \<Rightarrow> (length hs', Normal t')\<rbrakk> \<Longrightarrow> xf t' = xf' t'; \<And>s s' t t' x. \<lbrakk>(s, s') \<in> sr; P' s; s' \<in> Q'; (t, t') \<in> sr; (x, t) \<in> fst (a' s); \<Gamma>\<turnstile>\<^sub>h \<langle>c' # hs',s'\<rangle> \<Rightarrow> (length hs', Normal t')\<rbrakk> \<Longrightarrow> r x (xf' t') = r' x (xf' t'); \<And>s s' n t'. \<lbrakk>(s, s') \<in> sr; P' s; s' \<in> Q'; n \<noteq> length hs'; \<Gamma>\<turnstile>\<^sub>h \<langle>c' # hs',s'\<rangle> \<Rightarrow> (n, Normal t')\<rbrakk> \<Longrightarrow> axf t' = axf' t'; \<And>s s' t t' x n. \<lbrakk>(s, s') \<in> sr; P' s; s' \<in> Q'; (t, t') \<in> sr; (x, t) \<in> fst (a' s); n \<noteq> length hs'; \<Gamma>\<turnstile>\<^sub>h \<langle>c' # hs',s'\<rangle> \<Rightarrow> (n, Normal t')\<rbrakk> \<Longrightarrow> ar x (axf' t') = ar' x (axf' t')\<rbrakk> \<Longrightarrow> hs' = hs
 4. \<And>s s'. \<lbrakk>\<And>s. P s = P' s; \<And>s s'. \<lbrakk>(s, s') \<in> sr; P' s\<rbrakk> \<Longrightarrow> Q = Q'; hs = hs'; \<And>s s'. \<lbrakk>(s, s') \<in> sr; P' s; s' \<in> Q'\<rbrakk> \<Longrightarrow> a s = a' s; \<And>s s' s''. \<lbrakk>(s, s') \<in> sr; P' s; s' \<in> Q'\<rbrakk> \<Longrightarrow> semantic_equiv \<Gamma> s' s'' c c'; \<And>s s' t'. \<lbrakk>(s, s') \<in> sr; P' s; s' \<in> Q'; \<Gamma>\<turnstile>\<^sub>h \<langle>c' # hs',s'\<rangle> \<Rightarrow> (length hs', Normal t')\<rbrakk> \<Longrightarrow> xf t' = xf' t'; \<And>s s' t t' x. \<lbrakk>(s, s') \<in> sr; P' s; s' \<in> Q'; (t, t') \<in> sr; (x, t) \<in> fst (a' s); \<Gamma>\<turnstile>\<^sub>h \<langle>c' # hs',s'\<rangle> \<Rightarrow> (length hs', Normal t')\<rbrakk> \<Longrightarrow> r x (xf' t') = r' x (xf' t'); \<And>s s' n t'. \<lbrakk>(s, s') \<in> sr; P' s; s' \<in> Q'; n \<noteq> length hs'; \<Gamma>\<turnstile>\<^sub>h \<langle>c' # hs',s'\<rangle> \<Rightarrow> (n, Normal t')\<rbrakk> \<Longrightarrow> axf t' = axf' t'; \<And>s s' t t' x n. \<lbrakk>(s, s') \<in> sr; P' s; s' \<in> Q'; (t, t') \<in> sr; (x, t) \<in> fst (a' s); n \<noteq> length hs'; \<Gamma>\<turnstile>\<^sub>h \<langle>c' # hs',s'\<rangle> \<Rightarrow> (n, Normal t')\<rbrakk> \<Longrightarrow> ar x (axf' t') = ar' x (axf' t'); (s, s') \<in> sr; P s; s' \<in> Q\<rbrakk> \<Longrightarrow> a' s = a s
 5. \<And>s s' s''. \<lbrakk>\<And>s. P s = P' s; \<And>s s'. \<lbrakk>(s, s') \<in> sr; P' s\<rbrakk> \<Longrightarrow> Q = Q'; hs = hs'; \<And>s s'. \<lbrakk>(s, s') \<in> sr; P' s; s' \<in> Q'\<rbrakk> \<Longrightarrow> a s = a' s; \<And>s s' s''. \<lbrakk>(s, s') \<in> sr; P' s; s' \<in> Q'\<rbrakk> \<Longrightarrow> semantic_equiv \<Gamma> s' s'' c c'; \<And>s s' t'. \<lbrakk>(s, s') \<in> sr; P' s; s' \<in> Q'; \<Gamma>\<turnstile>\<^sub>h \<langle>c' # hs',s'\<rangle> \<Rightarrow> (length hs', Normal t')\<rbrakk> \<Longrightarrow> xf t' = xf' t'; \<And>s s' t t' x. \<lbrakk>(s, s') \<in> sr; P' s; s' \<in> Q'; (t, t') \<in> sr; (x, t) \<in> fst (a' s); \<Gamma>\<turnstile>\<^sub>h \<langle>c' # hs',s'\<rangle> \<Rightarrow> (length hs', Normal t')\<rbrakk> \<Longrightarrow> r x (xf' t') = r' x (xf' t'); \<And>s s' n t'. \<lbrakk>(s, s') \<in> sr; P' s; s' \<in> Q'; n \<noteq> length hs'; \<Gamma>\<turnstile>\<^sub>h \<langle>c' # hs',s'\<rangle> \<Rightarrow> (n, Normal t')\<rbrakk> \<Longrightarrow> axf t' = axf' t'; \<And>s s' t t' x n. \<lbrakk>(s, s') \<in> sr; P' s; s' \<in> Q'; (t, t') \<in> sr; (x, t) \<in> fst (a' s); n \<noteq> length hs'; \<Gamma>\<turnstile>\<^sub>h \<langle>c' # hs',s'\<rangle> \<Rightarrow> (n, Normal t')\<rbrakk> \<Longrightarrow> ar x (axf' t') = ar' x (axf' t'); (s, s') \<in> sr; P s; s' \<in> Q\<rbrakk> \<Longrightarrow> semantic_equiv \<Gamma> s' s'' c' c
 6. \<And>s s' t'. \<lbrakk>\<And>s. P s = P' s; \<And>s s'. \<lbrakk>(s, s') \<in> sr; P' s\<rbrakk> \<Longrightarrow> Q = Q'; hs = hs'; \<And>s s'. \<lbrakk>(s, s') \<in> sr; P' s; s' \<in> Q'\<rbrakk> \<Longrightarrow> a s = a' s; \<And>s s' s''. \<lbrakk>(s, s') \<in> sr; P' s; s' \<in> Q'\<rbrakk> \<Longrightarrow> semantic_equiv \<Gamma> s' s'' c c'; \<And>s s' t'. \<lbrakk>(s, s') \<in> sr; P' s; s' \<in> Q'; \<Gamma>\<turnstile>\<^sub>h \<langle>c' # hs',s'\<rangle> \<Rightarrow> (length hs', Normal t')\<rbrakk> \<Longrightarrow> xf t' = xf' t'; \<And>s s' t t' x. \<lbrakk>(s, s') \<in> sr; P' s; s' \<in> Q'; (t, t') \<in> sr; (x, t) \<in> fst (a' s); \<Gamma>\<turnstile>\<^sub>h \<langle>c' # hs',s'\<rangle> \<Rightarrow> (length hs', Normal t')\<rbrakk> \<Longrightarrow> r x (xf' t') = r' x (xf' t'); \<And>s s' n t'. \<lbrakk>(s, s') \<in> sr; P' s; s' \<in> Q'; n \<noteq> length hs'; \<Gamma>\<turnstile>\<^sub>h \<langle>c' # hs',s'\<rangle> \<Rightarrow> (n, Normal t')\<rbrakk> \<Longrightarrow> axf t' = axf' t'; \<And>s s' t t' x n. \<lbrakk>(s, s') \<in> sr; P' s; s' \<in> Q'; (t, t') \<in> sr; (x, t) \<in> fst (a' s); n \<noteq> length hs'; \<Gamma>\<turnstile>\<^sub>h \<langle>c' # hs',s'\<rangle> \<Rightarrow> (n, Normal t')\<rbrakk> \<Longrightarrow> ar x (axf' t') = ar' x (axf' t'); (s, s') \<in> sr; P s; s' \<in> Q; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (length hs, Normal t')\<rbrakk> \<Longrightarrow> xf' t' = xf t'
 7. \<And>x s t s' t'. \<lbrakk>\<And>s. P s = P' s; \<And>s s'. \<lbrakk>(s, s') \<in> sr; P' s\<rbrakk> \<Longrightarrow> Q = Q'; hs = hs'; \<And>s s'. \<lbrakk>(s, s') \<in> sr; P' s; s' \<in> Q'\<rbrakk> \<Longrightarrow> a s = a' s; \<And>s s' s''. \<lbrakk>(s, s') \<in> sr; P' s; s' \<in> Q'\<rbrakk> \<Longrightarrow> semantic_equiv \<Gamma> s' s'' c c'; \<And>s s' t'. \<lbrakk>(s, s') \<in> sr; P' s; s' \<in> Q'; \<Gamma>\<turnstile>\<^sub>h \<langle>c' # hs',s'\<rangle> \<Rightarrow> (length hs', Normal t')\<rbrakk> \<Longrightarrow> xf t' = xf' t'; \<And>s s' t t' x. \<lbrakk>(s, s') \<in> sr; P' s; s' \<in> Q'; (t, t') \<in> sr; (x, t) \<in> fst (a' s); \<Gamma>\<turnstile>\<^sub>h \<langle>c' # hs',s'\<rangle> \<Rightarrow> (length hs', Normal t')\<rbrakk> \<Longrightarrow> r x (xf' t') = r' x (xf' t'); \<And>s s' n t'. \<lbrakk>(s, s') \<in> sr; P' s; s' \<in> Q'; n \<noteq> length hs'; \<Gamma>\<turnstile>\<^sub>h \<langle>c' # hs',s'\<rangle> \<Rightarrow> (n, Normal t')\<rbrakk> \<Longrightarrow> axf t' = axf' t'; \<And>s s' t t' x n. \<lbrakk>(s, s') \<in> sr; P' s; s' \<in> Q'; (t, t') \<in> sr; (x, t) \<in> fst (a' s); n \<noteq> length hs'; \<Gamma>\<turnstile>\<^sub>h \<langle>c' # hs',s'\<rangle> \<Rightarrow> (n, Normal t')\<rbrakk> \<Longrightarrow> ar x (axf' t') = ar' x (axf' t'); (s, s') \<in> sr; P s; s' \<in> Q; (t, t') \<in> sr; (x, t) \<in> fst (a s); \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (length hs, Normal t')\<rbrakk> \<Longrightarrow> r' x (xf t') = r x (xf t')
 8. \<And>s s' t' n. \<lbrakk>\<And>s. P s = P' s; \<And>s s'. \<lbrakk>(s, s') \<in> sr; P' s\<rbrakk> \<Longrightarrow> Q = Q'; hs = hs'; \<And>s s'. \<lbrakk>(s, s') \<in> sr; P' s; s' \<in> Q'\<rbrakk> \<Longrightarrow> a s = a' s; \<And>s s' s''. \<lbrakk>(s, s') \<in> sr; P' s; s' \<in> Q'\<rbrakk> \<Longrightarrow> semantic_equiv \<Gamma> s' s'' c c'; \<And>s s' t'. \<lbrakk>(s, s') \<in> sr; P' s; s' \<in> Q'; \<Gamma>\<turnstile>\<^sub>h \<langle>c' # hs',s'\<rangle> \<Rightarrow> (length hs', Normal t')\<rbrakk> \<Longrightarrow> xf t' = xf' t'; \<And>s s' t t' x. \<lbrakk>(s, s') \<in> sr; P' s; s' \<in> Q'; (t, t') \<in> sr; (x, t) \<in> fst (a' s); \<Gamma>\<turnstile>\<^sub>h \<langle>c' # hs',s'\<rangle> \<Rightarrow> (length hs', Normal t')\<rbrakk> \<Longrightarrow> r x (xf' t') = r' x (xf' t'); \<And>s s' n t'. \<lbrakk>(s, s') \<in> sr; P' s; s' \<in> Q'; n \<noteq> length hs'; \<Gamma>\<turnstile>\<^sub>h \<langle>c' # hs',s'\<rangle> \<Rightarrow> (n, Normal t')\<rbrakk> \<Longrightarrow> axf t' = axf' t'; \<And>s s' t t' x n. \<lbrakk>(s, s') \<in> sr; P' s; s' \<in> Q'; (t, t') \<in> sr; (x, t) \<in> fst (a' s); n \<noteq> length hs'; \<Gamma>\<turnstile>\<^sub>h \<langle>c' # hs',s'\<rangle> \<Rightarrow> (n, Normal t')\<rbrakk> \<Longrightarrow> ar x (axf' t') = ar' x (axf' t'); (s, s') \<in> sr; P s; s' \<in> Q; n \<noteq> length hs; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, Normal t')\<rbrakk> \<Longrightarrow> axf' t' = axf t'
 9. \<And>x s t s' t' n. \<lbrakk>\<And>s. P s = P' s; \<And>s s'. \<lbrakk>(s, s') \<in> sr; P' s\<rbrakk> \<Longrightarrow> Q = Q'; hs = hs'; \<And>s s'. \<lbrakk>(s, s') \<in> sr; P' s; s' \<in> Q'\<rbrakk> \<Longrightarrow> a s = a' s; \<And>s s' s''. \<lbrakk>(s, s') \<in> sr; P' s; s' \<in> Q'\<rbrakk> \<Longrightarrow> semantic_equiv \<Gamma> s' s'' c c'; \<And>s s' t'. \<lbrakk>(s, s') \<in> sr; P' s; s' \<in> Q'; \<Gamma>\<turnstile>\<^sub>h \<langle>c' # hs',s'\<rangle> \<Rightarrow> (length hs', Normal t')\<rbrakk> \<Longrightarrow> xf t' = xf' t'; \<And>s s' t t' x. \<lbrakk>(s, s') \<in> sr; P' s; s' \<in> Q'; (t, t') \<in> sr; (x, t) \<in> fst (a' s); \<Gamma>\<turnstile>\<^sub>h \<langle>c' # hs',s'\<rangle> \<Rightarrow> (length hs', Normal t')\<rbrakk> \<Longrightarrow> r x (xf' t') = r' x (xf' t'); \<And>s s' n t'. \<lbrakk>(s, s') \<in> sr; P' s; s' \<in> Q'; n \<noteq> length hs'; \<Gamma>\<turnstile>\<^sub>h \<langle>c' # hs',s'\<rangle> \<Rightarrow> (n, Normal t')\<rbrakk> \<Longrightarrow> axf t' = axf' t'; \<And>s s' t t' x n. \<lbrakk>(s, s') \<in> sr; P' s; s' \<in> Q'; (t, t') \<in> sr; (x, t) \<in> fst (a' s); n \<noteq> length hs'; \<Gamma>\<turnstile>\<^sub>h \<langle>c' # hs',s'\<rangle> \<Rightarrow> (n, Normal t')\<rbrakk> \<Longrightarrow> ar x (axf' t') = ar' x (axf' t'); (s, s') \<in> sr; P s; s' \<in> Q; (t, t') \<in> sr; (x, t) \<in> fst (a s); n \<noteq> length hs; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, Normal t')\<rbrakk> \<Longrightarrow> ar' x (axf t') = ar x (axf t')