[STATEMENT]
lemma  boxed_b_eq:
  assumes "boxed_b \<Theta> s1 b bv b' s1'" and "\<turnstile>\<^sub>w\<^sub>f \<Theta>"
  shows "wfTh \<Theta> \<Longrightarrow> boxed_b \<Theta> s2 b bv b' s2' \<Longrightarrow> ( s1 = s2 ) = ( s1' = s2' )"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>   \<turnstile>\<^sub>w\<^sub>f \<Theta> ;  \<Theta>  \<turnstile> s2 ~ b [ bv ::= b' ] \<setminus> s2' \<rbrakk> \<Longrightarrow> (s1 = s2) = (s1' = s2')
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
 \<Theta>  \<turnstile> s1 ~ b [ bv ::= b' ] \<setminus> s1'
   \<turnstile>\<^sub>w\<^sub>f \<Theta>

goal (1 subgoal):
 1. \<lbrakk>   \<turnstile>\<^sub>w\<^sub>f \<Theta> ;  \<Theta>  \<turnstile> s2 ~ b [ bv ::= b' ] \<setminus> s2' \<rbrakk> \<Longrightarrow> (s1 = s2) = (s1' = s2')
[PROOF STEP]
proof(induct arbitrary: s2 s2'  rule: boxed_b.inducts )
[PROOF STATE]
proof (state)
goal (9 subgoals):
 1. \<And>bv bv' P s b s2 s2'. \<lbrakk>bv = bv';  P  \<turnstile> s : b;    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ B_var bv' [ bv ::= b ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s = s2) = (SUt s = s2')
 2. \<And>bv bv' P s b s2 s2'. \<lbrakk>bv \<noteq> bv';  P  \<turnstile> s : B_var bv';    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ B_var bv' [ bv ::= b ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s = s2) = (s = s2')
 3. \<And>P s uu_ uv_ s2 s2'. \<lbrakk> P  \<turnstile> s : B_int;    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ B_int [ uu_ ::= uv_ ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s = s2) = (s = s2')
 4. \<And>P s uw_ ux_ s2 s2'. \<lbrakk> P  \<turnstile> s : B_bool;    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ B_bool [ uw_ ::= ux_ ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s = s2) = (s = s2')
 5. \<And>P s uy_ uz_ s2 s2'. \<lbrakk> P  \<turnstile> s : B_unit;    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ B_unit [ uy_ ::= uz_ ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s = s2) = (s = s2')
 6. \<And>P s1 b1 bv b s1' s2 b2 s2' s2a s2'a. \<lbrakk> P  \<turnstile> s1 ~ b1 [ bv ::= b ] \<setminus> s1' ; \<And>s2 s2'. \<lbrakk>   \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ b1 [ bv ::= b ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s1 = s2) = (s1' = s2');  P  \<turnstile> s2 ~ b2 [ bv ::= b ] \<setminus> s2' ; \<And>s2a s2'a. \<lbrakk>   \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2a ~ b2 [ bv ::= b ] \<setminus> s2'a ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s2 = s2a) = (s2' = s2'a);    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2a ~ [ b1 , b2 ]\<^sup>b [ bv ::= b ] \<setminus> s2'a ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (SPair s1 s2 = s2a) = (SPair s1' s2' = s2'a)
 7. \<And>tyid dclist P dc x b c s1 bv b' s1' s2 s2'. \<lbrakk>AF_typedef tyid dclist \<in> set P; (dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist;  P  \<turnstile> s1 ~ b [ bv ::= b' ] \<setminus> s1' ; \<And>s2 s2'. \<lbrakk>   \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ b [ bv ::= b' ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s1 = s2) = (s1' = s2');    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ B_id tyid [ bv ::= b' ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (SCons tyid dc s1 = s2) = (SCons tyid dc s1' = s2')
 8. \<And>tyid bva dclist P b1 bv b' s1 s1' dc x b c s2 s2'. \<lbrakk>AF_typedef_poly tyid bva dclist \<in> set P; atom bva \<sharp> (b1, bv, b', s1, s1'); (dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist;  P  \<turnstile> s1 ~ b[bva::=b1]\<^sub>b\<^sub>b [ bv ::= b' ] \<setminus> s1' ; \<And>s2 s2'. \<lbrakk>   \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ b[bva::=b1]\<^sub>b\<^sub>b [ bv ::= b' ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s1 = s2) = (s1' = s2');    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ B_app tyid b1 [ bv ::= b' ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (SConsp tyid dc b1[bv::=b']\<^sub>b\<^sub>b s1 = s2) = (SConsp tyid dc b1 s1' = s2')
 9. \<And>P s bv b s2 s2'. \<lbrakk> P  \<turnstile> s : B_bitvec;    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ B_bitvec [ bv ::= b ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s = s2) = (s = s2')
[PROOF STEP]
case (boxed_b_BVar1I bv bv'  P s b )
[PROOF STATE]
proof (state)
this:
bv = bv'
 P  \<turnstile> s : b
   \<turnstile>\<^sub>w\<^sub>f P
 P  \<turnstile> s2 ~ B_var bv' [ bv ::= b ] \<setminus> s2'
   \<turnstile>\<^sub>w\<^sub>f P

goal (9 subgoals):
 1. \<And>bv bv' P s b s2 s2'. \<lbrakk>bv = bv';  P  \<turnstile> s : b;    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ B_var bv' [ bv ::= b ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s = s2) = (SUt s = s2')
 2. \<And>bv bv' P s b s2 s2'. \<lbrakk>bv \<noteq> bv';  P  \<turnstile> s : B_var bv';    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ B_var bv' [ bv ::= b ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s = s2) = (s = s2')
 3. \<And>P s uu_ uv_ s2 s2'. \<lbrakk> P  \<turnstile> s : B_int;    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ B_int [ uu_ ::= uv_ ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s = s2) = (s = s2')
 4. \<And>P s uw_ ux_ s2 s2'. \<lbrakk> P  \<turnstile> s : B_bool;    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ B_bool [ uw_ ::= ux_ ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s = s2) = (s = s2')
 5. \<And>P s uy_ uz_ s2 s2'. \<lbrakk> P  \<turnstile> s : B_unit;    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ B_unit [ uy_ ::= uz_ ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s = s2) = (s = s2')
 6. \<And>P s1 b1 bv b s1' s2 b2 s2' s2a s2'a. \<lbrakk> P  \<turnstile> s1 ~ b1 [ bv ::= b ] \<setminus> s1' ; \<And>s2 s2'. \<lbrakk>   \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ b1 [ bv ::= b ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s1 = s2) = (s1' = s2');  P  \<turnstile> s2 ~ b2 [ bv ::= b ] \<setminus> s2' ; \<And>s2a s2'a. \<lbrakk>   \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2a ~ b2 [ bv ::= b ] \<setminus> s2'a ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s2 = s2a) = (s2' = s2'a);    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2a ~ [ b1 , b2 ]\<^sup>b [ bv ::= b ] \<setminus> s2'a ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (SPair s1 s2 = s2a) = (SPair s1' s2' = s2'a)
 7. \<And>tyid dclist P dc x b c s1 bv b' s1' s2 s2'. \<lbrakk>AF_typedef tyid dclist \<in> set P; (dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist;  P  \<turnstile> s1 ~ b [ bv ::= b' ] \<setminus> s1' ; \<And>s2 s2'. \<lbrakk>   \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ b [ bv ::= b' ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s1 = s2) = (s1' = s2');    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ B_id tyid [ bv ::= b' ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (SCons tyid dc s1 = s2) = (SCons tyid dc s1' = s2')
 8. \<And>tyid bva dclist P b1 bv b' s1 s1' dc x b c s2 s2'. \<lbrakk>AF_typedef_poly tyid bva dclist \<in> set P; atom bva \<sharp> (b1, bv, b', s1, s1'); (dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist;  P  \<turnstile> s1 ~ b[bva::=b1]\<^sub>b\<^sub>b [ bv ::= b' ] \<setminus> s1' ; \<And>s2 s2'. \<lbrakk>   \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ b[bva::=b1]\<^sub>b\<^sub>b [ bv ::= b' ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s1 = s2) = (s1' = s2');    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ B_app tyid b1 [ bv ::= b' ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (SConsp tyid dc b1[bv::=b']\<^sub>b\<^sub>b s1 = s2) = (SConsp tyid dc b1 s1' = s2')
 9. \<And>P s bv b s2 s2'. \<lbrakk> P  \<turnstile> s : B_bitvec;    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ B_bitvec [ bv ::= b ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s = s2) = (s = s2')
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
bv = bv'
 P  \<turnstile> s : b
   \<turnstile>\<^sub>w\<^sub>f P
 P  \<turnstile> s2 ~ B_var bv' [ bv ::= b ] \<setminus> s2'
   \<turnstile>\<^sub>w\<^sub>f P
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
bv = bv'
 P  \<turnstile> s : b
   \<turnstile>\<^sub>w\<^sub>f P
 P  \<turnstile> s2 ~ B_var bv' [ bv ::= b ] \<setminus> s2'
   \<turnstile>\<^sub>w\<^sub>f P

goal (1 subgoal):
 1. (s = s2) = (SUt s = s2')
[PROOF STEP]
using boxed_b_elims(1) rcl_val.eq_iff
[PROOF STATE]
proof (prove)
using this:
bv = bv'
 P  \<turnstile> s : b
   \<turnstile>\<^sub>w\<^sub>f P
 P  \<turnstile> s2 ~ B_var bv' [ bv ::= b ] \<setminus> s2'
   \<turnstile>\<^sub>w\<^sub>f P
\<lbrakk> ?P  \<turnstile> ?s ~ B_var ?bv [ ?bv' ::= ?b ] \<setminus> ?s' ; \<lbrakk>?bv' = ?bv; ?s' = SUt ?s;  ?P  \<turnstile> ?s : ?b\<rbrakk> \<Longrightarrow> ?Pa; \<lbrakk>?s' = ?s; ?bv' \<noteq> ?bv;  ?P  \<turnstile> ?s : B_var ?bv\<rbrakk> \<Longrightarrow> ?Pa\<rbrakk> \<Longrightarrow> ?Pa
(SBitvec ?list = SBitvec ?lista) = (?list = ?lista)
(SNum ?int = SNum ?inta) = (?int = ?inta)
(SBool ?bool = SBool ?boola) = (?bool = ?boola)
(SPair ?rcl_val1.0 ?rcl_val2.0 = SPair ?rcl_val1a ?rcl_val2a) = (?rcl_val1.0 = ?rcl_val1a \<and> ?rcl_val2.0 = ?rcl_val2a)
(SCons ?list1.0 ?list2.0 ?rcl_val = SCons ?list1a ?list2a ?rcl_vala) = (?list1.0 = ?list1a \<and> ?list2.0 = ?list2a \<and> ?rcl_val = ?rcl_vala)
(SConsp ?list1.0 ?list2.0 ?b ?rcl_val = SConsp ?list1a ?list2a ?ba ?rcl_vala) = (?list1.0 = ?list1a \<and> ?list2.0 = ?list2a \<and> ?b = ?ba \<and> ?rcl_val = ?rcl_vala)
(SUnit = SUnit) = True
(SUt ?rcl_val = SUt ?rcl_vala) = (?rcl_val = ?rcl_vala)

goal (1 subgoal):
 1. (s = s2) = (SUt s = s2')
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
(s = s2) = (SUt s = s2')

goal (8 subgoals):
 1. \<And>bv bv' P s b s2 s2'. \<lbrakk>bv \<noteq> bv';  P  \<turnstile> s : B_var bv';    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ B_var bv' [ bv ::= b ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s = s2) = (s = s2')
 2. \<And>P s uu_ uv_ s2 s2'. \<lbrakk> P  \<turnstile> s : B_int;    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ B_int [ uu_ ::= uv_ ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s = s2) = (s = s2')
 3. \<And>P s uw_ ux_ s2 s2'. \<lbrakk> P  \<turnstile> s : B_bool;    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ B_bool [ uw_ ::= ux_ ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s = s2) = (s = s2')
 4. \<And>P s uy_ uz_ s2 s2'. \<lbrakk> P  \<turnstile> s : B_unit;    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ B_unit [ uy_ ::= uz_ ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s = s2) = (s = s2')
 5. \<And>P s1 b1 bv b s1' s2 b2 s2' s2a s2'a. \<lbrakk> P  \<turnstile> s1 ~ b1 [ bv ::= b ] \<setminus> s1' ; \<And>s2 s2'. \<lbrakk>   \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ b1 [ bv ::= b ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s1 = s2) = (s1' = s2');  P  \<turnstile> s2 ~ b2 [ bv ::= b ] \<setminus> s2' ; \<And>s2a s2'a. \<lbrakk>   \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2a ~ b2 [ bv ::= b ] \<setminus> s2'a ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s2 = s2a) = (s2' = s2'a);    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2a ~ [ b1 , b2 ]\<^sup>b [ bv ::= b ] \<setminus> s2'a ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (SPair s1 s2 = s2a) = (SPair s1' s2' = s2'a)
 6. \<And>tyid dclist P dc x b c s1 bv b' s1' s2 s2'. \<lbrakk>AF_typedef tyid dclist \<in> set P; (dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist;  P  \<turnstile> s1 ~ b [ bv ::= b' ] \<setminus> s1' ; \<And>s2 s2'. \<lbrakk>   \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ b [ bv ::= b' ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s1 = s2) = (s1' = s2');    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ B_id tyid [ bv ::= b' ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (SCons tyid dc s1 = s2) = (SCons tyid dc s1' = s2')
 7. \<And>tyid bva dclist P b1 bv b' s1 s1' dc x b c s2 s2'. \<lbrakk>AF_typedef_poly tyid bva dclist \<in> set P; atom bva \<sharp> (b1, bv, b', s1, s1'); (dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist;  P  \<turnstile> s1 ~ b[bva::=b1]\<^sub>b\<^sub>b [ bv ::= b' ] \<setminus> s1' ; \<And>s2 s2'. \<lbrakk>   \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ b[bva::=b1]\<^sub>b\<^sub>b [ bv ::= b' ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s1 = s2) = (s1' = s2');    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ B_app tyid b1 [ bv ::= b' ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (SConsp tyid dc b1[bv::=b']\<^sub>b\<^sub>b s1 = s2) = (SConsp tyid dc b1 s1' = s2')
 8. \<And>P s bv b s2 s2'. \<lbrakk> P  \<turnstile> s : B_bitvec;    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ B_bitvec [ bv ::= b ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s = s2) = (s = s2')
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (8 subgoals):
 1. \<And>bv bv' P s b s2 s2'. \<lbrakk>bv \<noteq> bv';  P  \<turnstile> s : B_var bv';    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ B_var bv' [ bv ::= b ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s = s2) = (s = s2')
 2. \<And>P s uu_ uv_ s2 s2'. \<lbrakk> P  \<turnstile> s : B_int;    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ B_int [ uu_ ::= uv_ ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s = s2) = (s = s2')
 3. \<And>P s uw_ ux_ s2 s2'. \<lbrakk> P  \<turnstile> s : B_bool;    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ B_bool [ uw_ ::= ux_ ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s = s2) = (s = s2')
 4. \<And>P s uy_ uz_ s2 s2'. \<lbrakk> P  \<turnstile> s : B_unit;    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ B_unit [ uy_ ::= uz_ ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s = s2) = (s = s2')
 5. \<And>P s1 b1 bv b s1' s2 b2 s2' s2a s2'a. \<lbrakk> P  \<turnstile> s1 ~ b1 [ bv ::= b ] \<setminus> s1' ; \<And>s2 s2'. \<lbrakk>   \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ b1 [ bv ::= b ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s1 = s2) = (s1' = s2');  P  \<turnstile> s2 ~ b2 [ bv ::= b ] \<setminus> s2' ; \<And>s2a s2'a. \<lbrakk>   \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2a ~ b2 [ bv ::= b ] \<setminus> s2'a ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s2 = s2a) = (s2' = s2'a);    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2a ~ [ b1 , b2 ]\<^sup>b [ bv ::= b ] \<setminus> s2'a ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (SPair s1 s2 = s2a) = (SPair s1' s2' = s2'a)
 6. \<And>tyid dclist P dc x b c s1 bv b' s1' s2 s2'. \<lbrakk>AF_typedef tyid dclist \<in> set P; (dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist;  P  \<turnstile> s1 ~ b [ bv ::= b' ] \<setminus> s1' ; \<And>s2 s2'. \<lbrakk>   \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ b [ bv ::= b' ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s1 = s2) = (s1' = s2');    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ B_id tyid [ bv ::= b' ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (SCons tyid dc s1 = s2) = (SCons tyid dc s1' = s2')
 7. \<And>tyid bva dclist P b1 bv b' s1 s1' dc x b c s2 s2'. \<lbrakk>AF_typedef_poly tyid bva dclist \<in> set P; atom bva \<sharp> (b1, bv, b', s1, s1'); (dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist;  P  \<turnstile> s1 ~ b[bva::=b1]\<^sub>b\<^sub>b [ bv ::= b' ] \<setminus> s1' ; \<And>s2 s2'. \<lbrakk>   \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ b[bva::=b1]\<^sub>b\<^sub>b [ bv ::= b' ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s1 = s2) = (s1' = s2');    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ B_app tyid b1 [ bv ::= b' ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (SConsp tyid dc b1[bv::=b']\<^sub>b\<^sub>b s1 = s2) = (SConsp tyid dc b1 s1' = s2')
 8. \<And>P s bv b s2 s2'. \<lbrakk> P  \<turnstile> s : B_bitvec;    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ B_bitvec [ bv ::= b ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s = s2) = (s = s2')
[PROOF STEP]
case (boxed_b_BVar2I bv bv' P s b)
[PROOF STATE]
proof (state)
this:
bv \<noteq> bv'
 P  \<turnstile> s : B_var bv'
   \<turnstile>\<^sub>w\<^sub>f P
 P  \<turnstile> s2 ~ B_var bv' [ bv ::= b ] \<setminus> s2'
   \<turnstile>\<^sub>w\<^sub>f P

goal (8 subgoals):
 1. \<And>bv bv' P s b s2 s2'. \<lbrakk>bv \<noteq> bv';  P  \<turnstile> s : B_var bv';    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ B_var bv' [ bv ::= b ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s = s2) = (s = s2')
 2. \<And>P s uu_ uv_ s2 s2'. \<lbrakk> P  \<turnstile> s : B_int;    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ B_int [ uu_ ::= uv_ ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s = s2) = (s = s2')
 3. \<And>P s uw_ ux_ s2 s2'. \<lbrakk> P  \<turnstile> s : B_bool;    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ B_bool [ uw_ ::= ux_ ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s = s2) = (s = s2')
 4. \<And>P s uy_ uz_ s2 s2'. \<lbrakk> P  \<turnstile> s : B_unit;    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ B_unit [ uy_ ::= uz_ ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s = s2) = (s = s2')
 5. \<And>P s1 b1 bv b s1' s2 b2 s2' s2a s2'a. \<lbrakk> P  \<turnstile> s1 ~ b1 [ bv ::= b ] \<setminus> s1' ; \<And>s2 s2'. \<lbrakk>   \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ b1 [ bv ::= b ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s1 = s2) = (s1' = s2');  P  \<turnstile> s2 ~ b2 [ bv ::= b ] \<setminus> s2' ; \<And>s2a s2'a. \<lbrakk>   \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2a ~ b2 [ bv ::= b ] \<setminus> s2'a ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s2 = s2a) = (s2' = s2'a);    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2a ~ [ b1 , b2 ]\<^sup>b [ bv ::= b ] \<setminus> s2'a ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (SPair s1 s2 = s2a) = (SPair s1' s2' = s2'a)
 6. \<And>tyid dclist P dc x b c s1 bv b' s1' s2 s2'. \<lbrakk>AF_typedef tyid dclist \<in> set P; (dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist;  P  \<turnstile> s1 ~ b [ bv ::= b' ] \<setminus> s1' ; \<And>s2 s2'. \<lbrakk>   \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ b [ bv ::= b' ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s1 = s2) = (s1' = s2');    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ B_id tyid [ bv ::= b' ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (SCons tyid dc s1 = s2) = (SCons tyid dc s1' = s2')
 7. \<And>tyid bva dclist P b1 bv b' s1 s1' dc x b c s2 s2'. \<lbrakk>AF_typedef_poly tyid bva dclist \<in> set P; atom bva \<sharp> (b1, bv, b', s1, s1'); (dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist;  P  \<turnstile> s1 ~ b[bva::=b1]\<^sub>b\<^sub>b [ bv ::= b' ] \<setminus> s1' ; \<And>s2 s2'. \<lbrakk>   \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ b[bva::=b1]\<^sub>b\<^sub>b [ bv ::= b' ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s1 = s2) = (s1' = s2');    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ B_app tyid b1 [ bv ::= b' ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (SConsp tyid dc b1[bv::=b']\<^sub>b\<^sub>b s1 = s2) = (SConsp tyid dc b1 s1' = s2')
 8. \<And>P s bv b s2 s2'. \<lbrakk> P  \<turnstile> s : B_bitvec;    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ B_bitvec [ bv ::= b ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s = s2) = (s = s2')
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
bv \<noteq> bv'
 P  \<turnstile> s : B_var bv'
   \<turnstile>\<^sub>w\<^sub>f P
 P  \<turnstile> s2 ~ B_var bv' [ bv ::= b ] \<setminus> s2'
   \<turnstile>\<^sub>w\<^sub>f P
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
bv \<noteq> bv'
 P  \<turnstile> s : B_var bv'
   \<turnstile>\<^sub>w\<^sub>f P
 P  \<turnstile> s2 ~ B_var bv' [ bv ::= b ] \<setminus> s2'
   \<turnstile>\<^sub>w\<^sub>f P

goal (1 subgoal):
 1. (s = s2) = (s = s2')
[PROOF STEP]
using boxed_b_elims(1)
[PROOF STATE]
proof (prove)
using this:
bv \<noteq> bv'
 P  \<turnstile> s : B_var bv'
   \<turnstile>\<^sub>w\<^sub>f P
 P  \<turnstile> s2 ~ B_var bv' [ bv ::= b ] \<setminus> s2'
   \<turnstile>\<^sub>w\<^sub>f P
\<lbrakk> ?P  \<turnstile> ?s ~ B_var ?bv [ ?bv' ::= ?b ] \<setminus> ?s' ; \<lbrakk>?bv' = ?bv; ?s' = SUt ?s;  ?P  \<turnstile> ?s : ?b\<rbrakk> \<Longrightarrow> ?Pa; \<lbrakk>?s' = ?s; ?bv' \<noteq> ?bv;  ?P  \<turnstile> ?s : B_var ?bv\<rbrakk> \<Longrightarrow> ?Pa\<rbrakk> \<Longrightarrow> ?Pa

goal (1 subgoal):
 1. (s = s2) = (s = s2')
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
(s = s2) = (s = s2')

goal (7 subgoals):
 1. \<And>P s uu_ uv_ s2 s2'. \<lbrakk> P  \<turnstile> s : B_int;    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ B_int [ uu_ ::= uv_ ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s = s2) = (s = s2')
 2. \<And>P s uw_ ux_ s2 s2'. \<lbrakk> P  \<turnstile> s : B_bool;    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ B_bool [ uw_ ::= ux_ ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s = s2) = (s = s2')
 3. \<And>P s uy_ uz_ s2 s2'. \<lbrakk> P  \<turnstile> s : B_unit;    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ B_unit [ uy_ ::= uz_ ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s = s2) = (s = s2')
 4. \<And>P s1 b1 bv b s1' s2 b2 s2' s2a s2'a. \<lbrakk> P  \<turnstile> s1 ~ b1 [ bv ::= b ] \<setminus> s1' ; \<And>s2 s2'. \<lbrakk>   \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ b1 [ bv ::= b ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s1 = s2) = (s1' = s2');  P  \<turnstile> s2 ~ b2 [ bv ::= b ] \<setminus> s2' ; \<And>s2a s2'a. \<lbrakk>   \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2a ~ b2 [ bv ::= b ] \<setminus> s2'a ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s2 = s2a) = (s2' = s2'a);    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2a ~ [ b1 , b2 ]\<^sup>b [ bv ::= b ] \<setminus> s2'a ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (SPair s1 s2 = s2a) = (SPair s1' s2' = s2'a)
 5. \<And>tyid dclist P dc x b c s1 bv b' s1' s2 s2'. \<lbrakk>AF_typedef tyid dclist \<in> set P; (dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist;  P  \<turnstile> s1 ~ b [ bv ::= b' ] \<setminus> s1' ; \<And>s2 s2'. \<lbrakk>   \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ b [ bv ::= b' ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s1 = s2) = (s1' = s2');    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ B_id tyid [ bv ::= b' ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (SCons tyid dc s1 = s2) = (SCons tyid dc s1' = s2')
 6. \<And>tyid bva dclist P b1 bv b' s1 s1' dc x b c s2 s2'. \<lbrakk>AF_typedef_poly tyid bva dclist \<in> set P; atom bva \<sharp> (b1, bv, b', s1, s1'); (dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist;  P  \<turnstile> s1 ~ b[bva::=b1]\<^sub>b\<^sub>b [ bv ::= b' ] \<setminus> s1' ; \<And>s2 s2'. \<lbrakk>   \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ b[bva::=b1]\<^sub>b\<^sub>b [ bv ::= b' ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s1 = s2) = (s1' = s2');    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ B_app tyid b1 [ bv ::= b' ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (SConsp tyid dc b1[bv::=b']\<^sub>b\<^sub>b s1 = s2) = (SConsp tyid dc b1 s1' = s2')
 7. \<And>P s bv b s2 s2'. \<lbrakk> P  \<turnstile> s : B_bitvec;    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ B_bitvec [ bv ::= b ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s = s2) = (s = s2')
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. \<And>P s uu_ uv_ s2 s2'. \<lbrakk> P  \<turnstile> s : B_int;    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ B_int [ uu_ ::= uv_ ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s = s2) = (s = s2')
 2. \<And>P s uw_ ux_ s2 s2'. \<lbrakk> P  \<turnstile> s : B_bool;    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ B_bool [ uw_ ::= ux_ ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s = s2) = (s = s2')
 3. \<And>P s uy_ uz_ s2 s2'. \<lbrakk> P  \<turnstile> s : B_unit;    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ B_unit [ uy_ ::= uz_ ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s = s2) = (s = s2')
 4. \<And>P s1 b1 bv b s1' s2 b2 s2' s2a s2'a. \<lbrakk> P  \<turnstile> s1 ~ b1 [ bv ::= b ] \<setminus> s1' ; \<And>s2 s2'. \<lbrakk>   \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ b1 [ bv ::= b ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s1 = s2) = (s1' = s2');  P  \<turnstile> s2 ~ b2 [ bv ::= b ] \<setminus> s2' ; \<And>s2a s2'a. \<lbrakk>   \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2a ~ b2 [ bv ::= b ] \<setminus> s2'a ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s2 = s2a) = (s2' = s2'a);    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2a ~ [ b1 , b2 ]\<^sup>b [ bv ::= b ] \<setminus> s2'a ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (SPair s1 s2 = s2a) = (SPair s1' s2' = s2'a)
 5. \<And>tyid dclist P dc x b c s1 bv b' s1' s2 s2'. \<lbrakk>AF_typedef tyid dclist \<in> set P; (dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist;  P  \<turnstile> s1 ~ b [ bv ::= b' ] \<setminus> s1' ; \<And>s2 s2'. \<lbrakk>   \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ b [ bv ::= b' ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s1 = s2) = (s1' = s2');    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ B_id tyid [ bv ::= b' ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (SCons tyid dc s1 = s2) = (SCons tyid dc s1' = s2')
 6. \<And>tyid bva dclist P b1 bv b' s1 s1' dc x b c s2 s2'. \<lbrakk>AF_typedef_poly tyid bva dclist \<in> set P; atom bva \<sharp> (b1, bv, b', s1, s1'); (dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist;  P  \<turnstile> s1 ~ b[bva::=b1]\<^sub>b\<^sub>b [ bv ::= b' ] \<setminus> s1' ; \<And>s2 s2'. \<lbrakk>   \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ b[bva::=b1]\<^sub>b\<^sub>b [ bv ::= b' ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s1 = s2) = (s1' = s2');    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ B_app tyid b1 [ bv ::= b' ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (SConsp tyid dc b1[bv::=b']\<^sub>b\<^sub>b s1 = s2) = (SConsp tyid dc b1 s1' = s2')
 7. \<And>P s bv b s2 s2'. \<lbrakk> P  \<turnstile> s : B_bitvec;    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ B_bitvec [ bv ::= b ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s = s2) = (s = s2')
[PROOF STEP]
case (boxed_b_BIntI P s uu uv)
[PROOF STATE]
proof (state)
this:
 P  \<turnstile> s : B_int
   \<turnstile>\<^sub>w\<^sub>f P
 P  \<turnstile> s2 ~ B_int [ uu ::= uv ] \<setminus> s2'
   \<turnstile>\<^sub>w\<^sub>f P

goal (7 subgoals):
 1. \<And>P s uu_ uv_ s2 s2'. \<lbrakk> P  \<turnstile> s : B_int;    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ B_int [ uu_ ::= uv_ ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s = s2) = (s = s2')
 2. \<And>P s uw_ ux_ s2 s2'. \<lbrakk> P  \<turnstile> s : B_bool;    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ B_bool [ uw_ ::= ux_ ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s = s2) = (s = s2')
 3. \<And>P s uy_ uz_ s2 s2'. \<lbrakk> P  \<turnstile> s : B_unit;    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ B_unit [ uy_ ::= uz_ ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s = s2) = (s = s2')
 4. \<And>P s1 b1 bv b s1' s2 b2 s2' s2a s2'a. \<lbrakk> P  \<turnstile> s1 ~ b1 [ bv ::= b ] \<setminus> s1' ; \<And>s2 s2'. \<lbrakk>   \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ b1 [ bv ::= b ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s1 = s2) = (s1' = s2');  P  \<turnstile> s2 ~ b2 [ bv ::= b ] \<setminus> s2' ; \<And>s2a s2'a. \<lbrakk>   \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2a ~ b2 [ bv ::= b ] \<setminus> s2'a ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s2 = s2a) = (s2' = s2'a);    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2a ~ [ b1 , b2 ]\<^sup>b [ bv ::= b ] \<setminus> s2'a ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (SPair s1 s2 = s2a) = (SPair s1' s2' = s2'a)
 5. \<And>tyid dclist P dc x b c s1 bv b' s1' s2 s2'. \<lbrakk>AF_typedef tyid dclist \<in> set P; (dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist;  P  \<turnstile> s1 ~ b [ bv ::= b' ] \<setminus> s1' ; \<And>s2 s2'. \<lbrakk>   \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ b [ bv ::= b' ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s1 = s2) = (s1' = s2');    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ B_id tyid [ bv ::= b' ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (SCons tyid dc s1 = s2) = (SCons tyid dc s1' = s2')
 6. \<And>tyid bva dclist P b1 bv b' s1 s1' dc x b c s2 s2'. \<lbrakk>AF_typedef_poly tyid bva dclist \<in> set P; atom bva \<sharp> (b1, bv, b', s1, s1'); (dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist;  P  \<turnstile> s1 ~ b[bva::=b1]\<^sub>b\<^sub>b [ bv ::= b' ] \<setminus> s1' ; \<And>s2 s2'. \<lbrakk>   \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ b[bva::=b1]\<^sub>b\<^sub>b [ bv ::= b' ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s1 = s2) = (s1' = s2');    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ B_app tyid b1 [ bv ::= b' ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (SConsp tyid dc b1[bv::=b']\<^sub>b\<^sub>b s1 = s2) = (SConsp tyid dc b1 s1' = s2')
 7. \<And>P s bv b s2 s2'. \<lbrakk> P  \<turnstile> s : B_bitvec;    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ B_bitvec [ bv ::= b ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s = s2) = (s = s2')
[PROOF STEP]
hence "s2 = s2'"
[PROOF STATE]
proof (prove)
using this:
 P  \<turnstile> s : B_int
   \<turnstile>\<^sub>w\<^sub>f P
 P  \<turnstile> s2 ~ B_int [ uu ::= uv ] \<setminus> s2'
   \<turnstile>\<^sub>w\<^sub>f P

goal (1 subgoal):
 1. s2 = s2'
[PROOF STEP]
using boxed_b_elims
[PROOF STATE]
proof (prove)
using this:
 P  \<turnstile> s : B_int
   \<turnstile>\<^sub>w\<^sub>f P
 P  \<turnstile> s2 ~ B_int [ uu ::= uv ] \<setminus> s2'
   \<turnstile>\<^sub>w\<^sub>f P
\<lbrakk> ?P  \<turnstile> ?s ~ B_var ?bv [ ?bv' ::= ?b ] \<setminus> ?s' ; \<lbrakk>?bv' = ?bv; ?s' = SUt ?s;  ?P  \<turnstile> ?s : ?b\<rbrakk> \<Longrightarrow> ?Pa; \<lbrakk>?s' = ?s; ?bv' \<noteq> ?bv;  ?P  \<turnstile> ?s : B_var ?bv\<rbrakk> \<Longrightarrow> ?Pa\<rbrakk> \<Longrightarrow> ?Pa
\<lbrakk> ?P  \<turnstile> ?s ~ B_int [ ?bv ::= ?b ] \<setminus> ?s' ; \<lbrakk>?s' = ?s;  ?P  \<turnstile> ?s : B_int\<rbrakk> \<Longrightarrow> ?Pa\<rbrakk> \<Longrightarrow> ?Pa
\<lbrakk> ?P  \<turnstile> ?s ~ B_bool [ ?bv ::= ?b ] \<setminus> ?s' ; \<lbrakk>?s' = ?s;  ?P  \<turnstile> ?s : B_bool\<rbrakk> \<Longrightarrow> ?Pa\<rbrakk> \<Longrightarrow> ?Pa
\<lbrakk> ?P  \<turnstile> ?s ~ B_unit [ ?bv ::= ?b ] \<setminus> ?s' ; \<lbrakk>?s' = ?s;  ?P  \<turnstile> ?s : B_unit\<rbrakk> \<Longrightarrow> ?Pa\<rbrakk> \<Longrightarrow> ?Pa
\<lbrakk> ?P  \<turnstile> ?s ~ [ ?b1.0 , ?b2.0 ]\<^sup>b [ ?bv ::= ?b ] \<setminus> ?s' ; \<And>s1 s1' s2 s2'. \<lbrakk>?s = SPair s1 s2; ?s' = SPair s1' s2';  ?P  \<turnstile> s1 ~ ?b1.0 [ ?bv ::= ?b ] \<setminus> s1' ;  ?P  \<turnstile> s2 ~ ?b2.0 [ ?bv ::= ?b ] \<setminus> s2' \<rbrakk> \<Longrightarrow> ?Pa\<rbrakk> \<Longrightarrow> ?Pa
\<lbrakk> ?P  \<turnstile> ?s ~ B_id ?dc [ ?bv ::= ?b ] \<setminus> ?s' ; \<And>dclist dc x b c s1 s1'. \<lbrakk>?s = SCons ?dc dc s1; ?s' = SCons ?dc dc s1'; AF_typedef ?dc dclist \<in> set ?P; (dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist;  ?P  \<turnstile> s1 ~ b [ ?bv ::= ?b ] \<setminus> s1' \<rbrakk> \<Longrightarrow> ?Pa\<rbrakk> \<Longrightarrow> ?Pa
\<lbrakk> ?P  \<turnstile> ?s ~ B_bitvec [ ?bv ::= ?b ] \<setminus> ?s' ; \<lbrakk>?s' = ?s;  ?P  \<turnstile> ?s : B_bitvec\<rbrakk> \<Longrightarrow> ?Pa\<rbrakk> \<Longrightarrow> ?Pa
\<lbrakk> ?P  \<turnstile> ?s ~ B_app ?dc ?b' [ ?bv ::= ?b ] \<setminus> ?s' ; \<And>bva dclist s1 s1' dc x b c. \<lbrakk>?s = SConsp ?dc dc ?b'[?bv::=?b]\<^sub>b\<^sub>b s1; ?s' = SConsp ?dc dc ?b' s1'; AF_typedef_poly ?dc bva dclist \<in> set ?P; atom bva \<sharp> (?b', ?bv, ?b, s1, s1'); (dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist;  ?P  \<turnstile> s1 ~ b[bva::=?b']\<^sub>b\<^sub>b [ ?bv ::= ?b ] \<setminus> s1' \<rbrakk> \<Longrightarrow> ?Pa\<rbrakk> \<Longrightarrow> ?Pa

goal (1 subgoal):
 1. s2 = s2'
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
s2 = s2'

goal (7 subgoals):
 1. \<And>P s uu_ uv_ s2 s2'. \<lbrakk> P  \<turnstile> s : B_int;    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ B_int [ uu_ ::= uv_ ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s = s2) = (s = s2')
 2. \<And>P s uw_ ux_ s2 s2'. \<lbrakk> P  \<turnstile> s : B_bool;    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ B_bool [ uw_ ::= ux_ ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s = s2) = (s = s2')
 3. \<And>P s uy_ uz_ s2 s2'. \<lbrakk> P  \<turnstile> s : B_unit;    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ B_unit [ uy_ ::= uz_ ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s = s2) = (s = s2')
 4. \<And>P s1 b1 bv b s1' s2 b2 s2' s2a s2'a. \<lbrakk> P  \<turnstile> s1 ~ b1 [ bv ::= b ] \<setminus> s1' ; \<And>s2 s2'. \<lbrakk>   \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ b1 [ bv ::= b ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s1 = s2) = (s1' = s2');  P  \<turnstile> s2 ~ b2 [ bv ::= b ] \<setminus> s2' ; \<And>s2a s2'a. \<lbrakk>   \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2a ~ b2 [ bv ::= b ] \<setminus> s2'a ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s2 = s2a) = (s2' = s2'a);    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2a ~ [ b1 , b2 ]\<^sup>b [ bv ::= b ] \<setminus> s2'a ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (SPair s1 s2 = s2a) = (SPair s1' s2' = s2'a)
 5. \<And>tyid dclist P dc x b c s1 bv b' s1' s2 s2'. \<lbrakk>AF_typedef tyid dclist \<in> set P; (dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist;  P  \<turnstile> s1 ~ b [ bv ::= b' ] \<setminus> s1' ; \<And>s2 s2'. \<lbrakk>   \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ b [ bv ::= b' ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s1 = s2) = (s1' = s2');    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ B_id tyid [ bv ::= b' ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (SCons tyid dc s1 = s2) = (SCons tyid dc s1' = s2')
 6. \<And>tyid bva dclist P b1 bv b' s1 s1' dc x b c s2 s2'. \<lbrakk>AF_typedef_poly tyid bva dclist \<in> set P; atom bva \<sharp> (b1, bv, b', s1, s1'); (dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist;  P  \<turnstile> s1 ~ b[bva::=b1]\<^sub>b\<^sub>b [ bv ::= b' ] \<setminus> s1' ; \<And>s2 s2'. \<lbrakk>   \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ b[bva::=b1]\<^sub>b\<^sub>b [ bv ::= b' ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s1 = s2) = (s1' = s2');    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ B_app tyid b1 [ bv ::= b' ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (SConsp tyid dc b1[bv::=b']\<^sub>b\<^sub>b s1 = s2) = (SConsp tyid dc b1 s1' = s2')
 7. \<And>P s bv b s2 s2'. \<lbrakk> P  \<turnstile> s : B_bitvec;    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ B_bitvec [ bv ::= b ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s = s2) = (s = s2')
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
s2 = s2'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
s2 = s2'

goal (1 subgoal):
 1. (s = s2) = (s = s2')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(s = s2) = (s = s2')

goal (6 subgoals):
 1. \<And>P s uw_ ux_ s2 s2'. \<lbrakk> P  \<turnstile> s : B_bool;    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ B_bool [ uw_ ::= ux_ ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s = s2) = (s = s2')
 2. \<And>P s uy_ uz_ s2 s2'. \<lbrakk> P  \<turnstile> s : B_unit;    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ B_unit [ uy_ ::= uz_ ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s = s2) = (s = s2')
 3. \<And>P s1 b1 bv b s1' s2 b2 s2' s2a s2'a. \<lbrakk> P  \<turnstile> s1 ~ b1 [ bv ::= b ] \<setminus> s1' ; \<And>s2 s2'. \<lbrakk>   \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ b1 [ bv ::= b ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s1 = s2) = (s1' = s2');  P  \<turnstile> s2 ~ b2 [ bv ::= b ] \<setminus> s2' ; \<And>s2a s2'a. \<lbrakk>   \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2a ~ b2 [ bv ::= b ] \<setminus> s2'a ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s2 = s2a) = (s2' = s2'a);    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2a ~ [ b1 , b2 ]\<^sup>b [ bv ::= b ] \<setminus> s2'a ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (SPair s1 s2 = s2a) = (SPair s1' s2' = s2'a)
 4. \<And>tyid dclist P dc x b c s1 bv b' s1' s2 s2'. \<lbrakk>AF_typedef tyid dclist \<in> set P; (dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist;  P  \<turnstile> s1 ~ b [ bv ::= b' ] \<setminus> s1' ; \<And>s2 s2'. \<lbrakk>   \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ b [ bv ::= b' ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s1 = s2) = (s1' = s2');    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ B_id tyid [ bv ::= b' ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (SCons tyid dc s1 = s2) = (SCons tyid dc s1' = s2')
 5. \<And>tyid bva dclist P b1 bv b' s1 s1' dc x b c s2 s2'. \<lbrakk>AF_typedef_poly tyid bva dclist \<in> set P; atom bva \<sharp> (b1, bv, b', s1, s1'); (dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist;  P  \<turnstile> s1 ~ b[bva::=b1]\<^sub>b\<^sub>b [ bv ::= b' ] \<setminus> s1' ; \<And>s2 s2'. \<lbrakk>   \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ b[bva::=b1]\<^sub>b\<^sub>b [ bv ::= b' ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s1 = s2) = (s1' = s2');    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ B_app tyid b1 [ bv ::= b' ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (SConsp tyid dc b1[bv::=b']\<^sub>b\<^sub>b s1 = s2) = (SConsp tyid dc b1 s1' = s2')
 6. \<And>P s bv b s2 s2'. \<lbrakk> P  \<turnstile> s : B_bitvec;    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ B_bitvec [ bv ::= b ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s = s2) = (s = s2')
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<And>P s uw_ ux_ s2 s2'. \<lbrakk> P  \<turnstile> s : B_bool;    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ B_bool [ uw_ ::= ux_ ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s = s2) = (s = s2')
 2. \<And>P s uy_ uz_ s2 s2'. \<lbrakk> P  \<turnstile> s : B_unit;    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ B_unit [ uy_ ::= uz_ ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s = s2) = (s = s2')
 3. \<And>P s1 b1 bv b s1' s2 b2 s2' s2a s2'a. \<lbrakk> P  \<turnstile> s1 ~ b1 [ bv ::= b ] \<setminus> s1' ; \<And>s2 s2'. \<lbrakk>   \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ b1 [ bv ::= b ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s1 = s2) = (s1' = s2');  P  \<turnstile> s2 ~ b2 [ bv ::= b ] \<setminus> s2' ; \<And>s2a s2'a. \<lbrakk>   \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2a ~ b2 [ bv ::= b ] \<setminus> s2'a ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s2 = s2a) = (s2' = s2'a);    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2a ~ [ b1 , b2 ]\<^sup>b [ bv ::= b ] \<setminus> s2'a ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (SPair s1 s2 = s2a) = (SPair s1' s2' = s2'a)
 4. \<And>tyid dclist P dc x b c s1 bv b' s1' s2 s2'. \<lbrakk>AF_typedef tyid dclist \<in> set P; (dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist;  P  \<turnstile> s1 ~ b [ bv ::= b' ] \<setminus> s1' ; \<And>s2 s2'. \<lbrakk>   \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ b [ bv ::= b' ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s1 = s2) = (s1' = s2');    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ B_id tyid [ bv ::= b' ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (SCons tyid dc s1 = s2) = (SCons tyid dc s1' = s2')
 5. \<And>tyid bva dclist P b1 bv b' s1 s1' dc x b c s2 s2'. \<lbrakk>AF_typedef_poly tyid bva dclist \<in> set P; atom bva \<sharp> (b1, bv, b', s1, s1'); (dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist;  P  \<turnstile> s1 ~ b[bva::=b1]\<^sub>b\<^sub>b [ bv ::= b' ] \<setminus> s1' ; \<And>s2 s2'. \<lbrakk>   \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ b[bva::=b1]\<^sub>b\<^sub>b [ bv ::= b' ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s1 = s2) = (s1' = s2');    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ B_app tyid b1 [ bv ::= b' ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (SConsp tyid dc b1[bv::=b']\<^sub>b\<^sub>b s1 = s2) = (SConsp tyid dc b1 s1' = s2')
 6. \<And>P s bv b s2 s2'. \<lbrakk> P  \<turnstile> s : B_bitvec;    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ B_bitvec [ bv ::= b ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s = s2) = (s = s2')
[PROOF STEP]
case (boxed_b_BBoolI P s uw ux)
[PROOF STATE]
proof (state)
this:
 P  \<turnstile> s : B_bool
   \<turnstile>\<^sub>w\<^sub>f P
 P  \<turnstile> s2 ~ B_bool [ uw ::= ux ] \<setminus> s2'
   \<turnstile>\<^sub>w\<^sub>f P

goal (6 subgoals):
 1. \<And>P s uw_ ux_ s2 s2'. \<lbrakk> P  \<turnstile> s : B_bool;    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ B_bool [ uw_ ::= ux_ ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s = s2) = (s = s2')
 2. \<And>P s uy_ uz_ s2 s2'. \<lbrakk> P  \<turnstile> s : B_unit;    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ B_unit [ uy_ ::= uz_ ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s = s2) = (s = s2')
 3. \<And>P s1 b1 bv b s1' s2 b2 s2' s2a s2'a. \<lbrakk> P  \<turnstile> s1 ~ b1 [ bv ::= b ] \<setminus> s1' ; \<And>s2 s2'. \<lbrakk>   \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ b1 [ bv ::= b ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s1 = s2) = (s1' = s2');  P  \<turnstile> s2 ~ b2 [ bv ::= b ] \<setminus> s2' ; \<And>s2a s2'a. \<lbrakk>   \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2a ~ b2 [ bv ::= b ] \<setminus> s2'a ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s2 = s2a) = (s2' = s2'a);    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2a ~ [ b1 , b2 ]\<^sup>b [ bv ::= b ] \<setminus> s2'a ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (SPair s1 s2 = s2a) = (SPair s1' s2' = s2'a)
 4. \<And>tyid dclist P dc x b c s1 bv b' s1' s2 s2'. \<lbrakk>AF_typedef tyid dclist \<in> set P; (dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist;  P  \<turnstile> s1 ~ b [ bv ::= b' ] \<setminus> s1' ; \<And>s2 s2'. \<lbrakk>   \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ b [ bv ::= b' ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s1 = s2) = (s1' = s2');    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ B_id tyid [ bv ::= b' ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (SCons tyid dc s1 = s2) = (SCons tyid dc s1' = s2')
 5. \<And>tyid bva dclist P b1 bv b' s1 s1' dc x b c s2 s2'. \<lbrakk>AF_typedef_poly tyid bva dclist \<in> set P; atom bva \<sharp> (b1, bv, b', s1, s1'); (dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist;  P  \<turnstile> s1 ~ b[bva::=b1]\<^sub>b\<^sub>b [ bv ::= b' ] \<setminus> s1' ; \<And>s2 s2'. \<lbrakk>   \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ b[bva::=b1]\<^sub>b\<^sub>b [ bv ::= b' ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s1 = s2) = (s1' = s2');    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ B_app tyid b1 [ bv ::= b' ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (SConsp tyid dc b1[bv::=b']\<^sub>b\<^sub>b s1 = s2) = (SConsp tyid dc b1 s1' = s2')
 6. \<And>P s bv b s2 s2'. \<lbrakk> P  \<turnstile> s : B_bitvec;    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ B_bitvec [ bv ::= b ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s = s2) = (s = s2')
[PROOF STEP]
hence "s2 = s2'"
[PROOF STATE]
proof (prove)
using this:
 P  \<turnstile> s : B_bool
   \<turnstile>\<^sub>w\<^sub>f P
 P  \<turnstile> s2 ~ B_bool [ uw ::= ux ] \<setminus> s2'
   \<turnstile>\<^sub>w\<^sub>f P

goal (1 subgoal):
 1. s2 = s2'
[PROOF STEP]
using boxed_b_elims
[PROOF STATE]
proof (prove)
using this:
 P  \<turnstile> s : B_bool
   \<turnstile>\<^sub>w\<^sub>f P
 P  \<turnstile> s2 ~ B_bool [ uw ::= ux ] \<setminus> s2'
   \<turnstile>\<^sub>w\<^sub>f P
\<lbrakk> ?P  \<turnstile> ?s ~ B_var ?bv [ ?bv' ::= ?b ] \<setminus> ?s' ; \<lbrakk>?bv' = ?bv; ?s' = SUt ?s;  ?P  \<turnstile> ?s : ?b\<rbrakk> \<Longrightarrow> ?Pa; \<lbrakk>?s' = ?s; ?bv' \<noteq> ?bv;  ?P  \<turnstile> ?s : B_var ?bv\<rbrakk> \<Longrightarrow> ?Pa\<rbrakk> \<Longrightarrow> ?Pa
\<lbrakk> ?P  \<turnstile> ?s ~ B_int [ ?bv ::= ?b ] \<setminus> ?s' ; \<lbrakk>?s' = ?s;  ?P  \<turnstile> ?s : B_int\<rbrakk> \<Longrightarrow> ?Pa\<rbrakk> \<Longrightarrow> ?Pa
\<lbrakk> ?P  \<turnstile> ?s ~ B_bool [ ?bv ::= ?b ] \<setminus> ?s' ; \<lbrakk>?s' = ?s;  ?P  \<turnstile> ?s : B_bool\<rbrakk> \<Longrightarrow> ?Pa\<rbrakk> \<Longrightarrow> ?Pa
\<lbrakk> ?P  \<turnstile> ?s ~ B_unit [ ?bv ::= ?b ] \<setminus> ?s' ; \<lbrakk>?s' = ?s;  ?P  \<turnstile> ?s : B_unit\<rbrakk> \<Longrightarrow> ?Pa\<rbrakk> \<Longrightarrow> ?Pa
\<lbrakk> ?P  \<turnstile> ?s ~ [ ?b1.0 , ?b2.0 ]\<^sup>b [ ?bv ::= ?b ] \<setminus> ?s' ; \<And>s1 s1' s2 s2'. \<lbrakk>?s = SPair s1 s2; ?s' = SPair s1' s2';  ?P  \<turnstile> s1 ~ ?b1.0 [ ?bv ::= ?b ] \<setminus> s1' ;  ?P  \<turnstile> s2 ~ ?b2.0 [ ?bv ::= ?b ] \<setminus> s2' \<rbrakk> \<Longrightarrow> ?Pa\<rbrakk> \<Longrightarrow> ?Pa
\<lbrakk> ?P  \<turnstile> ?s ~ B_id ?dc [ ?bv ::= ?b ] \<setminus> ?s' ; \<And>dclist dc x b c s1 s1'. \<lbrakk>?s = SCons ?dc dc s1; ?s' = SCons ?dc dc s1'; AF_typedef ?dc dclist \<in> set ?P; (dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist;  ?P  \<turnstile> s1 ~ b [ ?bv ::= ?b ] \<setminus> s1' \<rbrakk> \<Longrightarrow> ?Pa\<rbrakk> \<Longrightarrow> ?Pa
\<lbrakk> ?P  \<turnstile> ?s ~ B_bitvec [ ?bv ::= ?b ] \<setminus> ?s' ; \<lbrakk>?s' = ?s;  ?P  \<turnstile> ?s : B_bitvec\<rbrakk> \<Longrightarrow> ?Pa\<rbrakk> \<Longrightarrow> ?Pa
\<lbrakk> ?P  \<turnstile> ?s ~ B_app ?dc ?b' [ ?bv ::= ?b ] \<setminus> ?s' ; \<And>bva dclist s1 s1' dc x b c. \<lbrakk>?s = SConsp ?dc dc ?b'[?bv::=?b]\<^sub>b\<^sub>b s1; ?s' = SConsp ?dc dc ?b' s1'; AF_typedef_poly ?dc bva dclist \<in> set ?P; atom bva \<sharp> (?b', ?bv, ?b, s1, s1'); (dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist;  ?P  \<turnstile> s1 ~ b[bva::=?b']\<^sub>b\<^sub>b [ ?bv ::= ?b ] \<setminus> s1' \<rbrakk> \<Longrightarrow> ?Pa\<rbrakk> \<Longrightarrow> ?Pa

goal (1 subgoal):
 1. s2 = s2'
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
s2 = s2'

goal (6 subgoals):
 1. \<And>P s uw_ ux_ s2 s2'. \<lbrakk> P  \<turnstile> s : B_bool;    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ B_bool [ uw_ ::= ux_ ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s = s2) = (s = s2')
 2. \<And>P s uy_ uz_ s2 s2'. \<lbrakk> P  \<turnstile> s : B_unit;    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ B_unit [ uy_ ::= uz_ ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s = s2) = (s = s2')
 3. \<And>P s1 b1 bv b s1' s2 b2 s2' s2a s2'a. \<lbrakk> P  \<turnstile> s1 ~ b1 [ bv ::= b ] \<setminus> s1' ; \<And>s2 s2'. \<lbrakk>   \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ b1 [ bv ::= b ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s1 = s2) = (s1' = s2');  P  \<turnstile> s2 ~ b2 [ bv ::= b ] \<setminus> s2' ; \<And>s2a s2'a. \<lbrakk>   \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2a ~ b2 [ bv ::= b ] \<setminus> s2'a ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s2 = s2a) = (s2' = s2'a);    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2a ~ [ b1 , b2 ]\<^sup>b [ bv ::= b ] \<setminus> s2'a ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (SPair s1 s2 = s2a) = (SPair s1' s2' = s2'a)
 4. \<And>tyid dclist P dc x b c s1 bv b' s1' s2 s2'. \<lbrakk>AF_typedef tyid dclist \<in> set P; (dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist;  P  \<turnstile> s1 ~ b [ bv ::= b' ] \<setminus> s1' ; \<And>s2 s2'. \<lbrakk>   \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ b [ bv ::= b' ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s1 = s2) = (s1' = s2');    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ B_id tyid [ bv ::= b' ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (SCons tyid dc s1 = s2) = (SCons tyid dc s1' = s2')
 5. \<And>tyid bva dclist P b1 bv b' s1 s1' dc x b c s2 s2'. \<lbrakk>AF_typedef_poly tyid bva dclist \<in> set P; atom bva \<sharp> (b1, bv, b', s1, s1'); (dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist;  P  \<turnstile> s1 ~ b[bva::=b1]\<^sub>b\<^sub>b [ bv ::= b' ] \<setminus> s1' ; \<And>s2 s2'. \<lbrakk>   \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ b[bva::=b1]\<^sub>b\<^sub>b [ bv ::= b' ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s1 = s2) = (s1' = s2');    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ B_app tyid b1 [ bv ::= b' ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (SConsp tyid dc b1[bv::=b']\<^sub>b\<^sub>b s1 = s2) = (SConsp tyid dc b1 s1' = s2')
 6. \<And>P s bv b s2 s2'. \<lbrakk> P  \<turnstile> s : B_bitvec;    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ B_bitvec [ bv ::= b ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s = s2) = (s = s2')
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
s2 = s2'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
s2 = s2'

goal (1 subgoal):
 1. (s = s2) = (s = s2')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(s = s2) = (s = s2')

goal (5 subgoals):
 1. \<And>P s uy_ uz_ s2 s2'. \<lbrakk> P  \<turnstile> s : B_unit;    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ B_unit [ uy_ ::= uz_ ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s = s2) = (s = s2')
 2. \<And>P s1 b1 bv b s1' s2 b2 s2' s2a s2'a. \<lbrakk> P  \<turnstile> s1 ~ b1 [ bv ::= b ] \<setminus> s1' ; \<And>s2 s2'. \<lbrakk>   \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ b1 [ bv ::= b ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s1 = s2) = (s1' = s2');  P  \<turnstile> s2 ~ b2 [ bv ::= b ] \<setminus> s2' ; \<And>s2a s2'a. \<lbrakk>   \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2a ~ b2 [ bv ::= b ] \<setminus> s2'a ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s2 = s2a) = (s2' = s2'a);    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2a ~ [ b1 , b2 ]\<^sup>b [ bv ::= b ] \<setminus> s2'a ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (SPair s1 s2 = s2a) = (SPair s1' s2' = s2'a)
 3. \<And>tyid dclist P dc x b c s1 bv b' s1' s2 s2'. \<lbrakk>AF_typedef tyid dclist \<in> set P; (dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist;  P  \<turnstile> s1 ~ b [ bv ::= b' ] \<setminus> s1' ; \<And>s2 s2'. \<lbrakk>   \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ b [ bv ::= b' ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s1 = s2) = (s1' = s2');    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ B_id tyid [ bv ::= b' ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (SCons tyid dc s1 = s2) = (SCons tyid dc s1' = s2')
 4. \<And>tyid bva dclist P b1 bv b' s1 s1' dc x b c s2 s2'. \<lbrakk>AF_typedef_poly tyid bva dclist \<in> set P; atom bva \<sharp> (b1, bv, b', s1, s1'); (dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist;  P  \<turnstile> s1 ~ b[bva::=b1]\<^sub>b\<^sub>b [ bv ::= b' ] \<setminus> s1' ; \<And>s2 s2'. \<lbrakk>   \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ b[bva::=b1]\<^sub>b\<^sub>b [ bv ::= b' ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s1 = s2) = (s1' = s2');    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ B_app tyid b1 [ bv ::= b' ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (SConsp tyid dc b1[bv::=b']\<^sub>b\<^sub>b s1 = s2) = (SConsp tyid dc b1 s1' = s2')
 5. \<And>P s bv b s2 s2'. \<lbrakk> P  \<turnstile> s : B_bitvec;    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ B_bitvec [ bv ::= b ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s = s2) = (s = s2')
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>P s uy_ uz_ s2 s2'. \<lbrakk> P  \<turnstile> s : B_unit;    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ B_unit [ uy_ ::= uz_ ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s = s2) = (s = s2')
 2. \<And>P s1 b1 bv b s1' s2 b2 s2' s2a s2'a. \<lbrakk> P  \<turnstile> s1 ~ b1 [ bv ::= b ] \<setminus> s1' ; \<And>s2 s2'. \<lbrakk>   \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ b1 [ bv ::= b ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s1 = s2) = (s1' = s2');  P  \<turnstile> s2 ~ b2 [ bv ::= b ] \<setminus> s2' ; \<And>s2a s2'a. \<lbrakk>   \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2a ~ b2 [ bv ::= b ] \<setminus> s2'a ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s2 = s2a) = (s2' = s2'a);    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2a ~ [ b1 , b2 ]\<^sup>b [ bv ::= b ] \<setminus> s2'a ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (SPair s1 s2 = s2a) = (SPair s1' s2' = s2'a)
 3. \<And>tyid dclist P dc x b c s1 bv b' s1' s2 s2'. \<lbrakk>AF_typedef tyid dclist \<in> set P; (dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist;  P  \<turnstile> s1 ~ b [ bv ::= b' ] \<setminus> s1' ; \<And>s2 s2'. \<lbrakk>   \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ b [ bv ::= b' ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s1 = s2) = (s1' = s2');    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ B_id tyid [ bv ::= b' ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (SCons tyid dc s1 = s2) = (SCons tyid dc s1' = s2')
 4. \<And>tyid bva dclist P b1 bv b' s1 s1' dc x b c s2 s2'. \<lbrakk>AF_typedef_poly tyid bva dclist \<in> set P; atom bva \<sharp> (b1, bv, b', s1, s1'); (dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist;  P  \<turnstile> s1 ~ b[bva::=b1]\<^sub>b\<^sub>b [ bv ::= b' ] \<setminus> s1' ; \<And>s2 s2'. \<lbrakk>   \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ b[bva::=b1]\<^sub>b\<^sub>b [ bv ::= b' ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s1 = s2) = (s1' = s2');    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ B_app tyid b1 [ bv ::= b' ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (SConsp tyid dc b1[bv::=b']\<^sub>b\<^sub>b s1 = s2) = (SConsp tyid dc b1 s1' = s2')
 5. \<And>P s bv b s2 s2'. \<lbrakk> P  \<turnstile> s : B_bitvec;    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ B_bitvec [ bv ::= b ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s = s2) = (s = s2')
[PROOF STEP]
case (boxed_b_BUnitI P s uy uz)
[PROOF STATE]
proof (state)
this:
 P  \<turnstile> s : B_unit
   \<turnstile>\<^sub>w\<^sub>f P
 P  \<turnstile> s2 ~ B_unit [ uy ::= uz ] \<setminus> s2'
   \<turnstile>\<^sub>w\<^sub>f P

goal (5 subgoals):
 1. \<And>P s uy_ uz_ s2 s2'. \<lbrakk> P  \<turnstile> s : B_unit;    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ B_unit [ uy_ ::= uz_ ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s = s2) = (s = s2')
 2. \<And>P s1 b1 bv b s1' s2 b2 s2' s2a s2'a. \<lbrakk> P  \<turnstile> s1 ~ b1 [ bv ::= b ] \<setminus> s1' ; \<And>s2 s2'. \<lbrakk>   \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ b1 [ bv ::= b ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s1 = s2) = (s1' = s2');  P  \<turnstile> s2 ~ b2 [ bv ::= b ] \<setminus> s2' ; \<And>s2a s2'a. \<lbrakk>   \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2a ~ b2 [ bv ::= b ] \<setminus> s2'a ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s2 = s2a) = (s2' = s2'a);    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2a ~ [ b1 , b2 ]\<^sup>b [ bv ::= b ] \<setminus> s2'a ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (SPair s1 s2 = s2a) = (SPair s1' s2' = s2'a)
 3. \<And>tyid dclist P dc x b c s1 bv b' s1' s2 s2'. \<lbrakk>AF_typedef tyid dclist \<in> set P; (dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist;  P  \<turnstile> s1 ~ b [ bv ::= b' ] \<setminus> s1' ; \<And>s2 s2'. \<lbrakk>   \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ b [ bv ::= b' ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s1 = s2) = (s1' = s2');    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ B_id tyid [ bv ::= b' ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (SCons tyid dc s1 = s2) = (SCons tyid dc s1' = s2')
 4. \<And>tyid bva dclist P b1 bv b' s1 s1' dc x b c s2 s2'. \<lbrakk>AF_typedef_poly tyid bva dclist \<in> set P; atom bva \<sharp> (b1, bv, b', s1, s1'); (dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist;  P  \<turnstile> s1 ~ b[bva::=b1]\<^sub>b\<^sub>b [ bv ::= b' ] \<setminus> s1' ; \<And>s2 s2'. \<lbrakk>   \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ b[bva::=b1]\<^sub>b\<^sub>b [ bv ::= b' ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s1 = s2) = (s1' = s2');    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ B_app tyid b1 [ bv ::= b' ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (SConsp tyid dc b1[bv::=b']\<^sub>b\<^sub>b s1 = s2) = (SConsp tyid dc b1 s1' = s2')
 5. \<And>P s bv b s2 s2'. \<lbrakk> P  \<turnstile> s : B_bitvec;    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ B_bitvec [ bv ::= b ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s = s2) = (s = s2')
[PROOF STEP]
hence "s2 = s2'"
[PROOF STATE]
proof (prove)
using this:
 P  \<turnstile> s : B_unit
   \<turnstile>\<^sub>w\<^sub>f P
 P  \<turnstile> s2 ~ B_unit [ uy ::= uz ] \<setminus> s2'
   \<turnstile>\<^sub>w\<^sub>f P

goal (1 subgoal):
 1. s2 = s2'
[PROOF STEP]
using boxed_b_elims
[PROOF STATE]
proof (prove)
using this:
 P  \<turnstile> s : B_unit
   \<turnstile>\<^sub>w\<^sub>f P
 P  \<turnstile> s2 ~ B_unit [ uy ::= uz ] \<setminus> s2'
   \<turnstile>\<^sub>w\<^sub>f P
\<lbrakk> ?P  \<turnstile> ?s ~ B_var ?bv [ ?bv' ::= ?b ] \<setminus> ?s' ; \<lbrakk>?bv' = ?bv; ?s' = SUt ?s;  ?P  \<turnstile> ?s : ?b\<rbrakk> \<Longrightarrow> ?Pa; \<lbrakk>?s' = ?s; ?bv' \<noteq> ?bv;  ?P  \<turnstile> ?s : B_var ?bv\<rbrakk> \<Longrightarrow> ?Pa\<rbrakk> \<Longrightarrow> ?Pa
\<lbrakk> ?P  \<turnstile> ?s ~ B_int [ ?bv ::= ?b ] \<setminus> ?s' ; \<lbrakk>?s' = ?s;  ?P  \<turnstile> ?s : B_int\<rbrakk> \<Longrightarrow> ?Pa\<rbrakk> \<Longrightarrow> ?Pa
\<lbrakk> ?P  \<turnstile> ?s ~ B_bool [ ?bv ::= ?b ] \<setminus> ?s' ; \<lbrakk>?s' = ?s;  ?P  \<turnstile> ?s : B_bool\<rbrakk> \<Longrightarrow> ?Pa\<rbrakk> \<Longrightarrow> ?Pa
\<lbrakk> ?P  \<turnstile> ?s ~ B_unit [ ?bv ::= ?b ] \<setminus> ?s' ; \<lbrakk>?s' = ?s;  ?P  \<turnstile> ?s : B_unit\<rbrakk> \<Longrightarrow> ?Pa\<rbrakk> \<Longrightarrow> ?Pa
\<lbrakk> ?P  \<turnstile> ?s ~ [ ?b1.0 , ?b2.0 ]\<^sup>b [ ?bv ::= ?b ] \<setminus> ?s' ; \<And>s1 s1' s2 s2'. \<lbrakk>?s = SPair s1 s2; ?s' = SPair s1' s2';  ?P  \<turnstile> s1 ~ ?b1.0 [ ?bv ::= ?b ] \<setminus> s1' ;  ?P  \<turnstile> s2 ~ ?b2.0 [ ?bv ::= ?b ] \<setminus> s2' \<rbrakk> \<Longrightarrow> ?Pa\<rbrakk> \<Longrightarrow> ?Pa
\<lbrakk> ?P  \<turnstile> ?s ~ B_id ?dc [ ?bv ::= ?b ] \<setminus> ?s' ; \<And>dclist dc x b c s1 s1'. \<lbrakk>?s = SCons ?dc dc s1; ?s' = SCons ?dc dc s1'; AF_typedef ?dc dclist \<in> set ?P; (dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist;  ?P  \<turnstile> s1 ~ b [ ?bv ::= ?b ] \<setminus> s1' \<rbrakk> \<Longrightarrow> ?Pa\<rbrakk> \<Longrightarrow> ?Pa
\<lbrakk> ?P  \<turnstile> ?s ~ B_bitvec [ ?bv ::= ?b ] \<setminus> ?s' ; \<lbrakk>?s' = ?s;  ?P  \<turnstile> ?s : B_bitvec\<rbrakk> \<Longrightarrow> ?Pa\<rbrakk> \<Longrightarrow> ?Pa
\<lbrakk> ?P  \<turnstile> ?s ~ B_app ?dc ?b' [ ?bv ::= ?b ] \<setminus> ?s' ; \<And>bva dclist s1 s1' dc x b c. \<lbrakk>?s = SConsp ?dc dc ?b'[?bv::=?b]\<^sub>b\<^sub>b s1; ?s' = SConsp ?dc dc ?b' s1'; AF_typedef_poly ?dc bva dclist \<in> set ?P; atom bva \<sharp> (?b', ?bv, ?b, s1, s1'); (dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist;  ?P  \<turnstile> s1 ~ b[bva::=?b']\<^sub>b\<^sub>b [ ?bv ::= ?b ] \<setminus> s1' \<rbrakk> \<Longrightarrow> ?Pa\<rbrakk> \<Longrightarrow> ?Pa

goal (1 subgoal):
 1. s2 = s2'
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
s2 = s2'

goal (5 subgoals):
 1. \<And>P s uy_ uz_ s2 s2'. \<lbrakk> P  \<turnstile> s : B_unit;    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ B_unit [ uy_ ::= uz_ ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s = s2) = (s = s2')
 2. \<And>P s1 b1 bv b s1' s2 b2 s2' s2a s2'a. \<lbrakk> P  \<turnstile> s1 ~ b1 [ bv ::= b ] \<setminus> s1' ; \<And>s2 s2'. \<lbrakk>   \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ b1 [ bv ::= b ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s1 = s2) = (s1' = s2');  P  \<turnstile> s2 ~ b2 [ bv ::= b ] \<setminus> s2' ; \<And>s2a s2'a. \<lbrakk>   \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2a ~ b2 [ bv ::= b ] \<setminus> s2'a ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s2 = s2a) = (s2' = s2'a);    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2a ~ [ b1 , b2 ]\<^sup>b [ bv ::= b ] \<setminus> s2'a ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (SPair s1 s2 = s2a) = (SPair s1' s2' = s2'a)
 3. \<And>tyid dclist P dc x b c s1 bv b' s1' s2 s2'. \<lbrakk>AF_typedef tyid dclist \<in> set P; (dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist;  P  \<turnstile> s1 ~ b [ bv ::= b' ] \<setminus> s1' ; \<And>s2 s2'. \<lbrakk>   \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ b [ bv ::= b' ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s1 = s2) = (s1' = s2');    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ B_id tyid [ bv ::= b' ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (SCons tyid dc s1 = s2) = (SCons tyid dc s1' = s2')
 4. \<And>tyid bva dclist P b1 bv b' s1 s1' dc x b c s2 s2'. \<lbrakk>AF_typedef_poly tyid bva dclist \<in> set P; atom bva \<sharp> (b1, bv, b', s1, s1'); (dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist;  P  \<turnstile> s1 ~ b[bva::=b1]\<^sub>b\<^sub>b [ bv ::= b' ] \<setminus> s1' ; \<And>s2 s2'. \<lbrakk>   \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ b[bva::=b1]\<^sub>b\<^sub>b [ bv ::= b' ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s1 = s2) = (s1' = s2');    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ B_app tyid b1 [ bv ::= b' ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (SConsp tyid dc b1[bv::=b']\<^sub>b\<^sub>b s1 = s2) = (SConsp tyid dc b1 s1' = s2')
 5. \<And>P s bv b s2 s2'. \<lbrakk> P  \<turnstile> s : B_bitvec;    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ B_bitvec [ bv ::= b ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s = s2) = (s = s2')
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
s2 = s2'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
s2 = s2'

goal (1 subgoal):
 1. (s = s2) = (s = s2')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(s = s2) = (s = s2')

goal (4 subgoals):
 1. \<And>P s1 b1 bv b s1' s2 b2 s2' s2a s2'a. \<lbrakk> P  \<turnstile> s1 ~ b1 [ bv ::= b ] \<setminus> s1' ; \<And>s2 s2'. \<lbrakk>   \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ b1 [ bv ::= b ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s1 = s2) = (s1' = s2');  P  \<turnstile> s2 ~ b2 [ bv ::= b ] \<setminus> s2' ; \<And>s2a s2'a. \<lbrakk>   \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2a ~ b2 [ bv ::= b ] \<setminus> s2'a ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s2 = s2a) = (s2' = s2'a);    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2a ~ [ b1 , b2 ]\<^sup>b [ bv ::= b ] \<setminus> s2'a ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (SPair s1 s2 = s2a) = (SPair s1' s2' = s2'a)
 2. \<And>tyid dclist P dc x b c s1 bv b' s1' s2 s2'. \<lbrakk>AF_typedef tyid dclist \<in> set P; (dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist;  P  \<turnstile> s1 ~ b [ bv ::= b' ] \<setminus> s1' ; \<And>s2 s2'. \<lbrakk>   \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ b [ bv ::= b' ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s1 = s2) = (s1' = s2');    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ B_id tyid [ bv ::= b' ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (SCons tyid dc s1 = s2) = (SCons tyid dc s1' = s2')
 3. \<And>tyid bva dclist P b1 bv b' s1 s1' dc x b c s2 s2'. \<lbrakk>AF_typedef_poly tyid bva dclist \<in> set P; atom bva \<sharp> (b1, bv, b', s1, s1'); (dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist;  P  \<turnstile> s1 ~ b[bva::=b1]\<^sub>b\<^sub>b [ bv ::= b' ] \<setminus> s1' ; \<And>s2 s2'. \<lbrakk>   \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ b[bva::=b1]\<^sub>b\<^sub>b [ bv ::= b' ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s1 = s2) = (s1' = s2');    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ B_app tyid b1 [ bv ::= b' ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (SConsp tyid dc b1[bv::=b']\<^sub>b\<^sub>b s1 = s2) = (SConsp tyid dc b1 s1' = s2')
 4. \<And>P s bv b s2 s2'. \<lbrakk> P  \<turnstile> s : B_bitvec;    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ B_bitvec [ bv ::= b ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s = s2) = (s = s2')
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>P s1 b1 bv b s1' s2 b2 s2' s2a s2'a. \<lbrakk> P  \<turnstile> s1 ~ b1 [ bv ::= b ] \<setminus> s1' ; \<And>s2 s2'. \<lbrakk>   \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ b1 [ bv ::= b ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s1 = s2) = (s1' = s2');  P  \<turnstile> s2 ~ b2 [ bv ::= b ] \<setminus> s2' ; \<And>s2a s2'a. \<lbrakk>   \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2a ~ b2 [ bv ::= b ] \<setminus> s2'a ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s2 = s2a) = (s2' = s2'a);    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2a ~ [ b1 , b2 ]\<^sup>b [ bv ::= b ] \<setminus> s2'a ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (SPair s1 s2 = s2a) = (SPair s1' s2' = s2'a)
 2. \<And>tyid dclist P dc x b c s1 bv b' s1' s2 s2'. \<lbrakk>AF_typedef tyid dclist \<in> set P; (dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist;  P  \<turnstile> s1 ~ b [ bv ::= b' ] \<setminus> s1' ; \<And>s2 s2'. \<lbrakk>   \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ b [ bv ::= b' ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s1 = s2) = (s1' = s2');    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ B_id tyid [ bv ::= b' ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (SCons tyid dc s1 = s2) = (SCons tyid dc s1' = s2')
 3. \<And>tyid bva dclist P b1 bv b' s1 s1' dc x b c s2 s2'. \<lbrakk>AF_typedef_poly tyid bva dclist \<in> set P; atom bva \<sharp> (b1, bv, b', s1, s1'); (dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist;  P  \<turnstile> s1 ~ b[bva::=b1]\<^sub>b\<^sub>b [ bv ::= b' ] \<setminus> s1' ; \<And>s2 s2'. \<lbrakk>   \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ b[bva::=b1]\<^sub>b\<^sub>b [ bv ::= b' ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s1 = s2) = (s1' = s2');    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ B_app tyid b1 [ bv ::= b' ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (SConsp tyid dc b1[bv::=b']\<^sub>b\<^sub>b s1 = s2) = (SConsp tyid dc b1 s1' = s2')
 4. \<And>P s bv b s2 s2'. \<lbrakk> P  \<turnstile> s : B_bitvec;    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ B_bitvec [ bv ::= b ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s = s2) = (s = s2')
[PROOF STEP]
case (boxed_b_BPairI P s1 b1 bv b s1' s2a b2 s2a')
[PROOF STATE]
proof (state)
this:
 P  \<turnstile> s1 ~ b1 [ bv ::= b ] \<setminus> s1'
\<lbrakk>   \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> ?s2.0 ~ b1 [ bv ::= b ] \<setminus> ?s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s1 = ?s2.0) = (s1' = ?s2')
 P  \<turnstile> s2a ~ b2 [ bv ::= b ] \<setminus> s2a'
\<lbrakk>   \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> ?s2.0 ~ b2 [ bv ::= b ] \<setminus> ?s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s2a = ?s2.0) = (s2a' = ?s2')
   \<turnstile>\<^sub>w\<^sub>f P
 P  \<turnstile> s2 ~ [ b1 , b2 ]\<^sup>b [ bv ::= b ] \<setminus> s2'
   \<turnstile>\<^sub>w\<^sub>f P

goal (4 subgoals):
 1. \<And>P s1 b1 bv b s1' s2 b2 s2' s2a s2'a. \<lbrakk> P  \<turnstile> s1 ~ b1 [ bv ::= b ] \<setminus> s1' ; \<And>s2 s2'. \<lbrakk>   \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ b1 [ bv ::= b ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s1 = s2) = (s1' = s2');  P  \<turnstile> s2 ~ b2 [ bv ::= b ] \<setminus> s2' ; \<And>s2a s2'a. \<lbrakk>   \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2a ~ b2 [ bv ::= b ] \<setminus> s2'a ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s2 = s2a) = (s2' = s2'a);    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2a ~ [ b1 , b2 ]\<^sup>b [ bv ::= b ] \<setminus> s2'a ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (SPair s1 s2 = s2a) = (SPair s1' s2' = s2'a)
 2. \<And>tyid dclist P dc x b c s1 bv b' s1' s2 s2'. \<lbrakk>AF_typedef tyid dclist \<in> set P; (dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist;  P  \<turnstile> s1 ~ b [ bv ::= b' ] \<setminus> s1' ; \<And>s2 s2'. \<lbrakk>   \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ b [ bv ::= b' ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s1 = s2) = (s1' = s2');    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ B_id tyid [ bv ::= b' ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (SCons tyid dc s1 = s2) = (SCons tyid dc s1' = s2')
 3. \<And>tyid bva dclist P b1 bv b' s1 s1' dc x b c s2 s2'. \<lbrakk>AF_typedef_poly tyid bva dclist \<in> set P; atom bva \<sharp> (b1, bv, b', s1, s1'); (dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist;  P  \<turnstile> s1 ~ b[bva::=b1]\<^sub>b\<^sub>b [ bv ::= b' ] \<setminus> s1' ; \<And>s2 s2'. \<lbrakk>   \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ b[bva::=b1]\<^sub>b\<^sub>b [ bv ::= b' ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s1 = s2) = (s1' = s2');    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ B_app tyid b1 [ bv ::= b' ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (SConsp tyid dc b1[bv::=b']\<^sub>b\<^sub>b s1 = s2) = (SConsp tyid dc b1 s1' = s2')
 4. \<And>P s bv b s2 s2'. \<lbrakk> P  \<turnstile> s : B_bitvec;    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ B_bitvec [ bv ::= b ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s = s2) = (s = s2')
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
 P  \<turnstile> s1 ~ b1 [ bv ::= b ] \<setminus> s1'
\<lbrakk>   \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> ?s2.0 ~ b1 [ bv ::= b ] \<setminus> ?s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s1 = ?s2.0) = (s1' = ?s2')
 P  \<turnstile> s2a ~ b2 [ bv ::= b ] \<setminus> s2a'
\<lbrakk>   \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> ?s2.0 ~ b2 [ bv ::= b ] \<setminus> ?s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s2a = ?s2.0) = (s2a' = ?s2')
   \<turnstile>\<^sub>w\<^sub>f P
 P  \<turnstile> s2 ~ [ b1 , b2 ]\<^sup>b [ bv ::= b ] \<setminus> s2'
   \<turnstile>\<^sub>w\<^sub>f P
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
 P  \<turnstile> s1 ~ b1 [ bv ::= b ] \<setminus> s1'
\<lbrakk>   \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> ?s2.0 ~ b1 [ bv ::= b ] \<setminus> ?s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s1 = ?s2.0) = (s1' = ?s2')
 P  \<turnstile> s2a ~ b2 [ bv ::= b ] \<setminus> s2a'
\<lbrakk>   \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> ?s2.0 ~ b2 [ bv ::= b ] \<setminus> ?s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s2a = ?s2.0) = (s2a' = ?s2')
   \<turnstile>\<^sub>w\<^sub>f P
 P  \<turnstile> s2 ~ [ b1 , b2 ]\<^sup>b [ bv ::= b ] \<setminus> s2'
   \<turnstile>\<^sub>w\<^sub>f P

goal (1 subgoal):
 1. (SPair s1 s2a = s2) = (SPair s1' s2a' = s2')
[PROOF STEP]
by (metis boxed_b_elims(5) rcl_val.eq_iff(4))
[PROOF STATE]
proof (state)
this:
(SPair s1 s2a = s2) = (SPair s1' s2a' = s2')

goal (3 subgoals):
 1. \<And>tyid dclist P dc x b c s1 bv b' s1' s2 s2'. \<lbrakk>AF_typedef tyid dclist \<in> set P; (dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist;  P  \<turnstile> s1 ~ b [ bv ::= b' ] \<setminus> s1' ; \<And>s2 s2'. \<lbrakk>   \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ b [ bv ::= b' ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s1 = s2) = (s1' = s2');    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ B_id tyid [ bv ::= b' ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (SCons tyid dc s1 = s2) = (SCons tyid dc s1' = s2')
 2. \<And>tyid bva dclist P b1 bv b' s1 s1' dc x b c s2 s2'. \<lbrakk>AF_typedef_poly tyid bva dclist \<in> set P; atom bva \<sharp> (b1, bv, b', s1, s1'); (dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist;  P  \<turnstile> s1 ~ b[bva::=b1]\<^sub>b\<^sub>b [ bv ::= b' ] \<setminus> s1' ; \<And>s2 s2'. \<lbrakk>   \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ b[bva::=b1]\<^sub>b\<^sub>b [ bv ::= b' ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s1 = s2) = (s1' = s2');    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ B_app tyid b1 [ bv ::= b' ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (SConsp tyid dc b1[bv::=b']\<^sub>b\<^sub>b s1 = s2) = (SConsp tyid dc b1 s1' = s2')
 3. \<And>P s bv b s2 s2'. \<lbrakk> P  \<turnstile> s : B_bitvec;    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ B_bitvec [ bv ::= b ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s = s2) = (s = s2')
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>tyid dclist P dc x b c s1 bv b' s1' s2 s2'. \<lbrakk>AF_typedef tyid dclist \<in> set P; (dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist;  P  \<turnstile> s1 ~ b [ bv ::= b' ] \<setminus> s1' ; \<And>s2 s2'. \<lbrakk>   \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ b [ bv ::= b' ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s1 = s2) = (s1' = s2');    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ B_id tyid [ bv ::= b' ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (SCons tyid dc s1 = s2) = (SCons tyid dc s1' = s2')
 2. \<And>tyid bva dclist P b1 bv b' s1 s1' dc x b c s2 s2'. \<lbrakk>AF_typedef_poly tyid bva dclist \<in> set P; atom bva \<sharp> (b1, bv, b', s1, s1'); (dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist;  P  \<turnstile> s1 ~ b[bva::=b1]\<^sub>b\<^sub>b [ bv ::= b' ] \<setminus> s1' ; \<And>s2 s2'. \<lbrakk>   \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ b[bva::=b1]\<^sub>b\<^sub>b [ bv ::= b' ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s1 = s2) = (s1' = s2');    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ B_app tyid b1 [ bv ::= b' ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (SConsp tyid dc b1[bv::=b']\<^sub>b\<^sub>b s1 = s2) = (SConsp tyid dc b1 s1' = s2')
 3. \<And>P s bv b s2 s2'. \<lbrakk> P  \<turnstile> s : B_bitvec;    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ B_bitvec [ bv ::= b ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s = s2) = (s = s2')
[PROOF STEP]
case (boxed_b_BConsI tyid dclist P dc x b c s1 bv b' s1')
[PROOF STATE]
proof (state)
this:
AF_typedef tyid dclist \<in> set P
(dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist
 P  \<turnstile> s1 ~ b [ bv ::= b' ] \<setminus> s1'
\<lbrakk>   \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> ?s2.0 ~ b [ bv ::= b' ] \<setminus> ?s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s1 = ?s2.0) = (s1' = ?s2')
   \<turnstile>\<^sub>w\<^sub>f P
 P  \<turnstile> s2 ~ B_id tyid [ bv ::= b' ] \<setminus> s2'
   \<turnstile>\<^sub>w\<^sub>f P

goal (3 subgoals):
 1. \<And>tyid dclist P dc x b c s1 bv b' s1' s2 s2'. \<lbrakk>AF_typedef tyid dclist \<in> set P; (dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist;  P  \<turnstile> s1 ~ b [ bv ::= b' ] \<setminus> s1' ; \<And>s2 s2'. \<lbrakk>   \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ b [ bv ::= b' ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s1 = s2) = (s1' = s2');    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ B_id tyid [ bv ::= b' ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (SCons tyid dc s1 = s2) = (SCons tyid dc s1' = s2')
 2. \<And>tyid bva dclist P b1 bv b' s1 s1' dc x b c s2 s2'. \<lbrakk>AF_typedef_poly tyid bva dclist \<in> set P; atom bva \<sharp> (b1, bv, b', s1, s1'); (dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist;  P  \<turnstile> s1 ~ b[bva::=b1]\<^sub>b\<^sub>b [ bv ::= b' ] \<setminus> s1' ; \<And>s2 s2'. \<lbrakk>   \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ b[bva::=b1]\<^sub>b\<^sub>b [ bv ::= b' ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s1 = s2) = (s1' = s2');    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ B_app tyid b1 [ bv ::= b' ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (SConsp tyid dc b1[bv::=b']\<^sub>b\<^sub>b s1 = s2) = (SConsp tyid dc b1 s1' = s2')
 3. \<And>P s bv b s2 s2'. \<lbrakk> P  \<turnstile> s : B_bitvec;    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ B_bitvec [ bv ::= b ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s = s2) = (s = s2')
[PROOF STEP]
obtain s22 and s22' dclist2 dc2 x2 b2 c2 where *:"s2 = SCons tyid dc2 s22 \<and> s2' = SCons tyid dc2 s22' \<and> boxed_b P s22 b2 bv b' s22'
      \<and> AF_typedef tyid dclist2 \<in> set P \<and> (dc2, \<lbrace> x2 : b2  | c2 \<rbrace>) \<in> set dclist2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>dc2 s22 s22' b2 dclist2 x2 c2. s2 = SCons tyid dc2 s22 \<and> s2' = SCons tyid dc2 s22' \<and>  P  \<turnstile> s22 ~ b2 [ bv ::= b' ] \<setminus> s22'  \<and> AF_typedef tyid dclist2 \<in> set P \<and> (dc2, \<lbrace> x2 : b2  | c2 \<rbrace>) \<in> set dclist2 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using boxed_b_elims(6)[OF boxed_b_BConsI(6)]
[PROOF STATE]
proof (prove)
using this:
(\<And>dclist dc x b c s1 s1'. \<lbrakk>s2 = SCons tyid dc s1; s2' = SCons tyid dc s1'; AF_typedef tyid dclist \<in> set P; (dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist;  P  \<turnstile> s1 ~ b [ bv ::= b' ] \<setminus> s1' \<rbrakk> \<Longrightarrow> ?Pa) \<Longrightarrow> ?Pa

goal (1 subgoal):
 1. (\<And>dc2 s22 s22' b2 dclist2 x2 c2. s2 = SCons tyid dc2 s22 \<and> s2' = SCons tyid dc2 s22' \<and>  P  \<turnstile> s22 ~ b2 [ bv ::= b' ] \<setminus> s22'  \<and> AF_typedef tyid dclist2 \<in> set P \<and> (dc2, \<lbrace> x2 : b2  | c2 \<rbrace>) \<in> set dclist2 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
s2 = SCons tyid dc2 s22 \<and> s2' = SCons tyid dc2 s22' \<and>  P  \<turnstile> s22 ~ b2 [ bv ::= b' ] \<setminus> s22'  \<and> AF_typedef tyid dclist2 \<in> set P \<and> (dc2, \<lbrace> x2 : b2  | c2 \<rbrace>) \<in> set dclist2

goal (3 subgoals):
 1. \<And>tyid dclist P dc x b c s1 bv b' s1' s2 s2'. \<lbrakk>AF_typedef tyid dclist \<in> set P; (dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist;  P  \<turnstile> s1 ~ b [ bv ::= b' ] \<setminus> s1' ; \<And>s2 s2'. \<lbrakk>   \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ b [ bv ::= b' ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s1 = s2) = (s1' = s2');    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ B_id tyid [ bv ::= b' ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (SCons tyid dc s1 = s2) = (SCons tyid dc s1' = s2')
 2. \<And>tyid bva dclist P b1 bv b' s1 s1' dc x b c s2 s2'. \<lbrakk>AF_typedef_poly tyid bva dclist \<in> set P; atom bva \<sharp> (b1, bv, b', s1, s1'); (dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist;  P  \<turnstile> s1 ~ b[bva::=b1]\<^sub>b\<^sub>b [ bv ::= b' ] \<setminus> s1' ; \<And>s2 s2'. \<lbrakk>   \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ b[bva::=b1]\<^sub>b\<^sub>b [ bv ::= b' ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s1 = s2) = (s1' = s2');    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ B_app tyid b1 [ bv ::= b' ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (SConsp tyid dc b1[bv::=b']\<^sub>b\<^sub>b s1 = s2) = (SConsp tyid dc b1 s1' = s2')
 3. \<And>P s bv b s2 s2'. \<lbrakk> P  \<turnstile> s : B_bitvec;    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ B_bitvec [ bv ::= b ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s = s2) = (s = s2')
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (SCons tyid dc s1 = s2) = (SCons tyid dc s1' = s2')
[PROOF STEP]
proof(cases "dc = dc2")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. dc = dc2 \<Longrightarrow> (SCons tyid dc s1 = s2) = (SCons tyid dc s1' = s2')
 2. dc \<noteq> dc2 \<Longrightarrow> (SCons tyid dc s1 = s2) = (SCons tyid dc s1' = s2')
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
dc = dc2

goal (2 subgoals):
 1. dc = dc2 \<Longrightarrow> (SCons tyid dc s1 = s2) = (SCons tyid dc s1' = s2')
 2. dc \<noteq> dc2 \<Longrightarrow> (SCons tyid dc s1 = s2) = (SCons tyid dc s1' = s2')
[PROOF STEP]
hence "b = b2"
[PROOF STATE]
proof (prove)
using this:
dc = dc2

goal (1 subgoal):
 1. b = b2
[PROOF STEP]
using wfTh_ctor_unique \<tau>.eq_iff wfTh_dclist_unique wf boxed_b_BConsI *
[PROOF STATE]
proof (prove)
using this:
dc = dc2
\<lbrakk>   \<turnstile>\<^sub>w\<^sub>f ?\<Theta> ; AF_typedef ?tid ?dclist \<in> set ?\<Theta>; (?c, ?t1.0) \<in> set ?dclist; (?c, ?t2.0) \<in> set ?dclist\<rbrakk> \<Longrightarrow> ?t1.0 = ?t2.0
(\<lbrace> ?x : ?b  | ?c \<rbrace> = \<lbrace> ?xa : ?ba  | ?ca \<rbrace>) = ([[atom ?x]]lst. ?c = [[atom ?xa]]lst. ?ca \<and> ?b = ?ba)
\<lbrakk>   \<turnstile>\<^sub>w\<^sub>f ?\<Theta> ; AF_typedef ?tid ?dclist1.0 \<in> set ?\<Theta>; AF_typedef ?tid ?dclist2.0 \<in> set ?\<Theta>\<rbrakk> \<Longrightarrow> ?dclist1.0 = ?dclist2.0
wf {(x, y). x < y}
AF_typedef tyid dclist \<in> set P
(dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist
 P  \<turnstile> s1 ~ b [ bv ::= b' ] \<setminus> s1'
\<lbrakk>   \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> ?s2.0 ~ b [ bv ::= b' ] \<setminus> ?s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s1 = ?s2.0) = (s1' = ?s2')
   \<turnstile>\<^sub>w\<^sub>f P
 P  \<turnstile> s2 ~ B_id tyid [ bv ::= b' ] \<setminus> s2'
   \<turnstile>\<^sub>w\<^sub>f P
s2 = SCons tyid dc2 s22 \<and> s2' = SCons tyid dc2 s22' \<and>  P  \<turnstile> s22 ~ b2 [ bv ::= b' ] \<setminus> s22'  \<and> AF_typedef tyid dclist2 \<in> set P \<and> (dc2, \<lbrace> x2 : b2  | c2 \<rbrace>) \<in> set dclist2

goal (1 subgoal):
 1. b = b2
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
b = b2

goal (2 subgoals):
 1. dc = dc2 \<Longrightarrow> (SCons tyid dc s1 = s2) = (SCons tyid dc s1' = s2')
 2. dc \<noteq> dc2 \<Longrightarrow> (SCons tyid dc s1 = s2) = (SCons tyid dc s1' = s2')
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
b = b2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
b = b2

goal (1 subgoal):
 1. (SCons tyid dc s1 = s2) = (SCons tyid dc s1' = s2')
[PROOF STEP]
using boxed_b_BConsI True *
[PROOF STATE]
proof (prove)
using this:
b = b2
AF_typedef tyid dclist \<in> set P
(dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist
 P  \<turnstile> s1 ~ b [ bv ::= b' ] \<setminus> s1'
\<lbrakk>   \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> ?s2.0 ~ b [ bv ::= b' ] \<setminus> ?s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s1 = ?s2.0) = (s1' = ?s2')
   \<turnstile>\<^sub>w\<^sub>f P
 P  \<turnstile> s2 ~ B_id tyid [ bv ::= b' ] \<setminus> s2'
   \<turnstile>\<^sub>w\<^sub>f P
dc = dc2
s2 = SCons tyid dc2 s22 \<and> s2' = SCons tyid dc2 s22' \<and>  P  \<turnstile> s22 ~ b2 [ bv ::= b' ] \<setminus> s22'  \<and> AF_typedef tyid dclist2 \<in> set P \<and> (dc2, \<lbrace> x2 : b2  | c2 \<rbrace>) \<in> set dclist2

goal (1 subgoal):
 1. (SCons tyid dc s1 = s2) = (SCons tyid dc s1' = s2')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(SCons tyid dc s1 = s2) = (SCons tyid dc s1' = s2')

goal (1 subgoal):
 1. dc \<noteq> dc2 \<Longrightarrow> (SCons tyid dc s1 = s2) = (SCons tyid dc s1' = s2')
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. dc \<noteq> dc2 \<Longrightarrow> (SCons tyid dc s1 = s2) = (SCons tyid dc s1' = s2')
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
dc \<noteq> dc2

goal (1 subgoal):
 1. dc \<noteq> dc2 \<Longrightarrow> (SCons tyid dc s1 = s2) = (SCons tyid dc s1' = s2')
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
dc \<noteq> dc2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
dc \<noteq> dc2

goal (1 subgoal):
 1. (SCons tyid dc s1 = s2) = (SCons tyid dc s1' = s2')
[PROOF STEP]
using * boxed_b_BConsI
[PROOF STATE]
proof (prove)
using this:
dc \<noteq> dc2
s2 = SCons tyid dc2 s22 \<and> s2' = SCons tyid dc2 s22' \<and>  P  \<turnstile> s22 ~ b2 [ bv ::= b' ] \<setminus> s22'  \<and> AF_typedef tyid dclist2 \<in> set P \<and> (dc2, \<lbrace> x2 : b2  | c2 \<rbrace>) \<in> set dclist2
AF_typedef tyid dclist \<in> set P
(dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist
 P  \<turnstile> s1 ~ b [ bv ::= b' ] \<setminus> s1'
\<lbrakk>   \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> ?s2.0 ~ b [ bv ::= b' ] \<setminus> ?s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s1 = ?s2.0) = (s1' = ?s2')
   \<turnstile>\<^sub>w\<^sub>f P
 P  \<turnstile> s2 ~ B_id tyid [ bv ::= b' ] \<setminus> s2'
   \<turnstile>\<^sub>w\<^sub>f P

goal (1 subgoal):
 1. (SCons tyid dc s1 = s2) = (SCons tyid dc s1' = s2')
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(SCons tyid dc s1 = s2) = (SCons tyid dc s1' = s2')

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(SCons tyid dc s1 = s2) = (SCons tyid dc s1' = s2')

goal (2 subgoals):
 1. \<And>tyid bva dclist P b1 bv b' s1 s1' dc x b c s2 s2'. \<lbrakk>AF_typedef_poly tyid bva dclist \<in> set P; atom bva \<sharp> (b1, bv, b', s1, s1'); (dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist;  P  \<turnstile> s1 ~ b[bva::=b1]\<^sub>b\<^sub>b [ bv ::= b' ] \<setminus> s1' ; \<And>s2 s2'. \<lbrakk>   \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ b[bva::=b1]\<^sub>b\<^sub>b [ bv ::= b' ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s1 = s2) = (s1' = s2');    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ B_app tyid b1 [ bv ::= b' ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (SConsp tyid dc b1[bv::=b']\<^sub>b\<^sub>b s1 = s2) = (SConsp tyid dc b1 s1' = s2')
 2. \<And>P s bv b s2 s2'. \<lbrakk> P  \<turnstile> s : B_bitvec;    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ B_bitvec [ bv ::= b ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s = s2) = (s = s2')
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>tyid bva dclist P b1 bv b' s1 s1' dc x b c s2 s2'. \<lbrakk>AF_typedef_poly tyid bva dclist \<in> set P; atom bva \<sharp> (b1, bv, b', s1, s1'); (dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist;  P  \<turnstile> s1 ~ b[bva::=b1]\<^sub>b\<^sub>b [ bv ::= b' ] \<setminus> s1' ; \<And>s2 s2'. \<lbrakk>   \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ b[bva::=b1]\<^sub>b\<^sub>b [ bv ::= b' ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s1 = s2) = (s1' = s2');    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ B_app tyid b1 [ bv ::= b' ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (SConsp tyid dc b1[bv::=b']\<^sub>b\<^sub>b s1 = s2) = (SConsp tyid dc b1 s1' = s2')
 2. \<And>P s bv b s2 s2'. \<lbrakk> P  \<turnstile> s : B_bitvec;    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ B_bitvec [ bv ::= b ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s = s2) = (s = s2')
[PROOF STEP]
case (boxed_b_Bbitvec P s bv b)
[PROOF STATE]
proof (state)
this:
 P  \<turnstile> s : B_bitvec
   \<turnstile>\<^sub>w\<^sub>f P
 P  \<turnstile> s2 ~ B_bitvec [ bv ::= b ] \<setminus> s2'
   \<turnstile>\<^sub>w\<^sub>f P

goal (2 subgoals):
 1. \<And>tyid bva dclist P b1 bv b' s1 s1' dc x b c s2 s2'. \<lbrakk>AF_typedef_poly tyid bva dclist \<in> set P; atom bva \<sharp> (b1, bv, b', s1, s1'); (dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist;  P  \<turnstile> s1 ~ b[bva::=b1]\<^sub>b\<^sub>b [ bv ::= b' ] \<setminus> s1' ; \<And>s2 s2'. \<lbrakk>   \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ b[bva::=b1]\<^sub>b\<^sub>b [ bv ::= b' ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s1 = s2) = (s1' = s2');    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ B_app tyid b1 [ bv ::= b' ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (SConsp tyid dc b1[bv::=b']\<^sub>b\<^sub>b s1 = s2) = (SConsp tyid dc b1 s1' = s2')
 2. \<And>P s bv b s2 s2'. \<lbrakk> P  \<turnstile> s : B_bitvec;    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ B_bitvec [ bv ::= b ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s = s2) = (s = s2')
[PROOF STEP]
hence "s2 = s2'"
[PROOF STATE]
proof (prove)
using this:
 P  \<turnstile> s : B_bitvec
   \<turnstile>\<^sub>w\<^sub>f P
 P  \<turnstile> s2 ~ B_bitvec [ bv ::= b ] \<setminus> s2'
   \<turnstile>\<^sub>w\<^sub>f P

goal (1 subgoal):
 1. s2 = s2'
[PROOF STEP]
using boxed_b_elims
[PROOF STATE]
proof (prove)
using this:
 P  \<turnstile> s : B_bitvec
   \<turnstile>\<^sub>w\<^sub>f P
 P  \<turnstile> s2 ~ B_bitvec [ bv ::= b ] \<setminus> s2'
   \<turnstile>\<^sub>w\<^sub>f P
\<lbrakk> ?P  \<turnstile> ?s ~ B_var ?bv [ ?bv' ::= ?b ] \<setminus> ?s' ; \<lbrakk>?bv' = ?bv; ?s' = SUt ?s;  ?P  \<turnstile> ?s : ?b\<rbrakk> \<Longrightarrow> ?Pa; \<lbrakk>?s' = ?s; ?bv' \<noteq> ?bv;  ?P  \<turnstile> ?s : B_var ?bv\<rbrakk> \<Longrightarrow> ?Pa\<rbrakk> \<Longrightarrow> ?Pa
\<lbrakk> ?P  \<turnstile> ?s ~ B_int [ ?bv ::= ?b ] \<setminus> ?s' ; \<lbrakk>?s' = ?s;  ?P  \<turnstile> ?s : B_int\<rbrakk> \<Longrightarrow> ?Pa\<rbrakk> \<Longrightarrow> ?Pa
\<lbrakk> ?P  \<turnstile> ?s ~ B_bool [ ?bv ::= ?b ] \<setminus> ?s' ; \<lbrakk>?s' = ?s;  ?P  \<turnstile> ?s : B_bool\<rbrakk> \<Longrightarrow> ?Pa\<rbrakk> \<Longrightarrow> ?Pa
\<lbrakk> ?P  \<turnstile> ?s ~ B_unit [ ?bv ::= ?b ] \<setminus> ?s' ; \<lbrakk>?s' = ?s;  ?P  \<turnstile> ?s : B_unit\<rbrakk> \<Longrightarrow> ?Pa\<rbrakk> \<Longrightarrow> ?Pa
\<lbrakk> ?P  \<turnstile> ?s ~ [ ?b1.0 , ?b2.0 ]\<^sup>b [ ?bv ::= ?b ] \<setminus> ?s' ; \<And>s1 s1' s2 s2'. \<lbrakk>?s = SPair s1 s2; ?s' = SPair s1' s2';  ?P  \<turnstile> s1 ~ ?b1.0 [ ?bv ::= ?b ] \<setminus> s1' ;  ?P  \<turnstile> s2 ~ ?b2.0 [ ?bv ::= ?b ] \<setminus> s2' \<rbrakk> \<Longrightarrow> ?Pa\<rbrakk> \<Longrightarrow> ?Pa
\<lbrakk> ?P  \<turnstile> ?s ~ B_id ?dc [ ?bv ::= ?b ] \<setminus> ?s' ; \<And>dclist dc x b c s1 s1'. \<lbrakk>?s = SCons ?dc dc s1; ?s' = SCons ?dc dc s1'; AF_typedef ?dc dclist \<in> set ?P; (dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist;  ?P  \<turnstile> s1 ~ b [ ?bv ::= ?b ] \<setminus> s1' \<rbrakk> \<Longrightarrow> ?Pa\<rbrakk> \<Longrightarrow> ?Pa
\<lbrakk> ?P  \<turnstile> ?s ~ B_bitvec [ ?bv ::= ?b ] \<setminus> ?s' ; \<lbrakk>?s' = ?s;  ?P  \<turnstile> ?s : B_bitvec\<rbrakk> \<Longrightarrow> ?Pa\<rbrakk> \<Longrightarrow> ?Pa
\<lbrakk> ?P  \<turnstile> ?s ~ B_app ?dc ?b' [ ?bv ::= ?b ] \<setminus> ?s' ; \<And>bva dclist s1 s1' dc x b c. \<lbrakk>?s = SConsp ?dc dc ?b'[?bv::=?b]\<^sub>b\<^sub>b s1; ?s' = SConsp ?dc dc ?b' s1'; AF_typedef_poly ?dc bva dclist \<in> set ?P; atom bva \<sharp> (?b', ?bv, ?b, s1, s1'); (dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist;  ?P  \<turnstile> s1 ~ b[bva::=?b']\<^sub>b\<^sub>b [ ?bv ::= ?b ] \<setminus> s1' \<rbrakk> \<Longrightarrow> ?Pa\<rbrakk> \<Longrightarrow> ?Pa

goal (1 subgoal):
 1. s2 = s2'
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
s2 = s2'

goal (2 subgoals):
 1. \<And>tyid bva dclist P b1 bv b' s1 s1' dc x b c s2 s2'. \<lbrakk>AF_typedef_poly tyid bva dclist \<in> set P; atom bva \<sharp> (b1, bv, b', s1, s1'); (dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist;  P  \<turnstile> s1 ~ b[bva::=b1]\<^sub>b\<^sub>b [ bv ::= b' ] \<setminus> s1' ; \<And>s2 s2'. \<lbrakk>   \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ b[bva::=b1]\<^sub>b\<^sub>b [ bv ::= b' ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s1 = s2) = (s1' = s2');    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ B_app tyid b1 [ bv ::= b' ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (SConsp tyid dc b1[bv::=b']\<^sub>b\<^sub>b s1 = s2) = (SConsp tyid dc b1 s1' = s2')
 2. \<And>P s bv b s2 s2'. \<lbrakk> P  \<turnstile> s : B_bitvec;    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ B_bitvec [ bv ::= b ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s = s2) = (s = s2')
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
s2 = s2'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
s2 = s2'

goal (1 subgoal):
 1. (s = s2) = (s = s2')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(s = s2) = (s = s2')

goal (1 subgoal):
 1. \<And>tyid bva dclist P b1 bv b' s1 s1' dc x b c s2 s2'. \<lbrakk>AF_typedef_poly tyid bva dclist \<in> set P; atom bva \<sharp> (b1, bv, b', s1, s1'); (dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist;  P  \<turnstile> s1 ~ b[bva::=b1]\<^sub>b\<^sub>b [ bv ::= b' ] \<setminus> s1' ; \<And>s2 s2'. \<lbrakk>   \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ b[bva::=b1]\<^sub>b\<^sub>b [ bv ::= b' ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s1 = s2) = (s1' = s2');    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ B_app tyid b1 [ bv ::= b' ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (SConsp tyid dc b1[bv::=b']\<^sub>b\<^sub>b s1 = s2) = (SConsp tyid dc b1 s1' = s2')
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>tyid bva dclist P b1 bv b' s1 s1' dc x b c s2 s2'. \<lbrakk>AF_typedef_poly tyid bva dclist \<in> set P; atom bva \<sharp> (b1, bv, b', s1, s1'); (dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist;  P  \<turnstile> s1 ~ b[bva::=b1]\<^sub>b\<^sub>b [ bv ::= b' ] \<setminus> s1' ; \<And>s2 s2'. \<lbrakk>   \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ b[bva::=b1]\<^sub>b\<^sub>b [ bv ::= b' ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s1 = s2) = (s1' = s2');    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ B_app tyid b1 [ bv ::= b' ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (SConsp tyid dc b1[bv::=b']\<^sub>b\<^sub>b s1 = s2) = (SConsp tyid dc b1 s1' = s2')
[PROOF STEP]
case (boxed_b_BConspI tyid bva dclist P b1 bv b' s1 s1' dc x b c)
[PROOF STATE]
proof (state)
this:
AF_typedef_poly tyid bva dclist \<in> set P
atom bva \<sharp> (b1, bv, b', s1, s1')
(dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist
 P  \<turnstile> s1 ~ b[bva::=b1]\<^sub>b\<^sub>b [ bv ::= b' ] \<setminus> s1'
\<lbrakk>   \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> ?s2.0 ~ b[bva::=b1]\<^sub>b\<^sub>b [ bv ::= b' ] \<setminus> ?s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s1 = ?s2.0) = (s1' = ?s2')
   \<turnstile>\<^sub>w\<^sub>f P
 P  \<turnstile> s2 ~ B_app tyid b1 [ bv ::= b' ] \<setminus> s2'
   \<turnstile>\<^sub>w\<^sub>f P

goal (1 subgoal):
 1. \<And>tyid bva dclist P b1 bv b' s1 s1' dc x b c s2 s2'. \<lbrakk>AF_typedef_poly tyid bva dclist \<in> set P; atom bva \<sharp> (b1, bv, b', s1, s1'); (dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist;  P  \<turnstile> s1 ~ b[bva::=b1]\<^sub>b\<^sub>b [ bv ::= b' ] \<setminus> s1' ; \<And>s2 s2'. \<lbrakk>   \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ b[bva::=b1]\<^sub>b\<^sub>b [ bv ::= b' ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s1 = s2) = (s1' = s2');    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ B_app tyid b1 [ bv ::= b' ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (SConsp tyid dc b1[bv::=b']\<^sub>b\<^sub>b s1 = s2) = (SConsp tyid dc b1 s1' = s2')
[PROOF STEP]
obtain bva2 s22  s22' dclist2 dc2 x2 b2 c2 where *:"
     s2 = SConsp tyid dc2 b1[bv::=b']\<^sub>b\<^sub>b s22 \<and>
     s2' = SConsp tyid dc2 b1 s22' \<and>
     boxed_b P s22 b2[bva2::=b1]\<^sub>b\<^sub>b  bv b' s22'  \<and>
     AF_typedef_poly tyid bva2 dclist2 \<in> set P \<and> (dc2, \<lbrace> x2 : b2  | c2 \<rbrace>) \<in> set dclist2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>dc2 s22 s22' b2 bva2 dclist2 x2 c2. s2 = SConsp tyid dc2 b1[bv::=b']\<^sub>b\<^sub>b s22 \<and> s2' = SConsp tyid dc2 b1 s22' \<and>  P  \<turnstile> s22 ~ b2[bva2::=b1]\<^sub>b\<^sub>b [ bv ::= b' ] \<setminus> s22'  \<and> AF_typedef_poly tyid bva2 dclist2 \<in> set P \<and> (dc2, \<lbrace> x2 : b2  | c2 \<rbrace>) \<in> set dclist2 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using boxed_b_elims(8)[OF boxed_b_BConspI(7)]
[PROOF STATE]
proof (prove)
using this:
(\<And>bva dclist s1 s1' dc x b c. \<lbrakk>s2 = SConsp tyid dc b1[bv::=b']\<^sub>b\<^sub>b s1; s2' = SConsp tyid dc b1 s1'; AF_typedef_poly tyid bva dclist \<in> set P; atom bva \<sharp> (b1, bv, b', s1, s1'); (dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist;  P  \<turnstile> s1 ~ b[bva::=b1]\<^sub>b\<^sub>b [ bv ::= b' ] \<setminus> s1' \<rbrakk> \<Longrightarrow> ?Pa) \<Longrightarrow> ?Pa

goal (1 subgoal):
 1. (\<And>dc2 s22 s22' b2 bva2 dclist2 x2 c2. s2 = SConsp tyid dc2 b1[bv::=b']\<^sub>b\<^sub>b s22 \<and> s2' = SConsp tyid dc2 b1 s22' \<and>  P  \<turnstile> s22 ~ b2[bva2::=b1]\<^sub>b\<^sub>b [ bv ::= b' ] \<setminus> s22'  \<and> AF_typedef_poly tyid bva2 dclist2 \<in> set P \<and> (dc2, \<lbrace> x2 : b2  | c2 \<rbrace>) \<in> set dclist2 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
s2 = SConsp tyid dc2 b1[bv::=b']\<^sub>b\<^sub>b s22 \<and> s2' = SConsp tyid dc2 b1 s22' \<and>  P  \<turnstile> s22 ~ b2[bva2::=b1]\<^sub>b\<^sub>b [ bv ::= b' ] \<setminus> s22'  \<and> AF_typedef_poly tyid bva2 dclist2 \<in> set P \<and> (dc2, \<lbrace> x2 : b2  | c2 \<rbrace>) \<in> set dclist2

goal (1 subgoal):
 1. \<And>tyid bva dclist P b1 bv b' s1 s1' dc x b c s2 s2'. \<lbrakk>AF_typedef_poly tyid bva dclist \<in> set P; atom bva \<sharp> (b1, bv, b', s1, s1'); (dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist;  P  \<turnstile> s1 ~ b[bva::=b1]\<^sub>b\<^sub>b [ bv ::= b' ] \<setminus> s1' ; \<And>s2 s2'. \<lbrakk>   \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ b[bva::=b1]\<^sub>b\<^sub>b [ bv ::= b' ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s1 = s2) = (s1' = s2');    \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> s2 ~ B_app tyid b1 [ bv ::= b' ] \<setminus> s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (SConsp tyid dc b1[bv::=b']\<^sub>b\<^sub>b s1 = s2) = (SConsp tyid dc b1 s1' = s2')
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (SConsp tyid dc b1[bv::=b']\<^sub>b\<^sub>b s1 = s2) = (SConsp tyid dc b1 s1' = s2')
[PROOF STEP]
proof(cases "dc = dc2")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. dc = dc2 \<Longrightarrow> (SConsp tyid dc b1[bv::=b']\<^sub>b\<^sub>b s1 = s2) = (SConsp tyid dc b1 s1' = s2')
 2. dc \<noteq> dc2 \<Longrightarrow> (SConsp tyid dc b1[bv::=b']\<^sub>b\<^sub>b s1 = s2) = (SConsp tyid dc b1 s1' = s2')
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
dc = dc2

goal (2 subgoals):
 1. dc = dc2 \<Longrightarrow> (SConsp tyid dc b1[bv::=b']\<^sub>b\<^sub>b s1 = s2) = (SConsp tyid dc b1 s1' = s2')
 2. dc \<noteq> dc2 \<Longrightarrow> (SConsp tyid dc b1[bv::=b']\<^sub>b\<^sub>b s1 = s2) = (SConsp tyid dc b1 s1' = s2')
[PROOF STEP]
hence "AF_typedef_poly tyid bva2 dclist2 \<in> set P \<and> (dc, \<lbrace> x2 : b2  | c2 \<rbrace>) \<in> set dclist2"
[PROOF STATE]
proof (prove)
using this:
dc = dc2

goal (1 subgoal):
 1. AF_typedef_poly tyid bva2 dclist2 \<in> set P \<and> (dc, \<lbrace> x2 : b2  | c2 \<rbrace>) \<in> set dclist2
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
dc = dc2
s2 = SConsp tyid dc2 b1[bv::=b']\<^sub>b\<^sub>b s22 \<and> s2' = SConsp tyid dc2 b1 s22' \<and>  P  \<turnstile> s22 ~ b2[bva2::=b1]\<^sub>b\<^sub>b [ bv ::= b' ] \<setminus> s22'  \<and> AF_typedef_poly tyid bva2 dclist2 \<in> set P \<and> (dc2, \<lbrace> x2 : b2  | c2 \<rbrace>) \<in> set dclist2

goal (1 subgoal):
 1. AF_typedef_poly tyid bva2 dclist2 \<in> set P \<and> (dc, \<lbrace> x2 : b2  | c2 \<rbrace>) \<in> set dclist2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
AF_typedef_poly tyid bva2 dclist2 \<in> set P \<and> (dc, \<lbrace> x2 : b2  | c2 \<rbrace>) \<in> set dclist2

goal (2 subgoals):
 1. dc = dc2 \<Longrightarrow> (SConsp tyid dc b1[bv::=b']\<^sub>b\<^sub>b s1 = s2) = (SConsp tyid dc b1 s1' = s2')
 2. dc \<noteq> dc2 \<Longrightarrow> (SConsp tyid dc b1[bv::=b']\<^sub>b\<^sub>b s1 = s2) = (SConsp tyid dc b1 s1' = s2')
[PROOF STEP]
hence "b[bva::=b1]\<^sub>b\<^sub>b = b2[bva2::=b1]\<^sub>b\<^sub>b"
[PROOF STATE]
proof (prove)
using this:
AF_typedef_poly tyid bva2 dclist2 \<in> set P \<and> (dc, \<lbrace> x2 : b2  | c2 \<rbrace>) \<in> set dclist2

goal (1 subgoal):
 1. b[bva::=b1]\<^sub>b\<^sub>b = b2[bva2::=b1]\<^sub>b\<^sub>b
[PROOF STEP]
using wfTh_typedef_poly_b_eq_iff[OF boxed_b_BConspI(1) boxed_b_BConspI(3)] * boxed_b_BConspI
[PROOF STATE]
proof (prove)
using this:
AF_typedef_poly tyid bva2 dclist2 \<in> set P \<and> (dc, \<lbrace> x2 : b2  | c2 \<rbrace>) \<in> set dclist2
\<lbrakk>AF_typedef_poly tyid ?bva2.0 ?dclist2.0 \<in> set P; (dc, \<lbrace> ?x2.0 : ?b2.0  | ?c2.0 \<rbrace>) \<in> set ?dclist2.0;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> b[bva::=?b]\<^sub>b\<^sub>b = ?b2.0[?bva2.0::=?b]\<^sub>b\<^sub>b
s2 = SConsp tyid dc2 b1[bv::=b']\<^sub>b\<^sub>b s22 \<and> s2' = SConsp tyid dc2 b1 s22' \<and>  P  \<turnstile> s22 ~ b2[bva2::=b1]\<^sub>b\<^sub>b [ bv ::= b' ] \<setminus> s22'  \<and> AF_typedef_poly tyid bva2 dclist2 \<in> set P \<and> (dc2, \<lbrace> x2 : b2  | c2 \<rbrace>) \<in> set dclist2
AF_typedef_poly tyid bva dclist \<in> set P
atom bva \<sharp> (b1, bv, b', s1, s1')
(dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist
 P  \<turnstile> s1 ~ b[bva::=b1]\<^sub>b\<^sub>b [ bv ::= b' ] \<setminus> s1'
\<lbrakk>   \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> ?s2.0 ~ b[bva::=b1]\<^sub>b\<^sub>b [ bv ::= b' ] \<setminus> ?s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s1 = ?s2.0) = (s1' = ?s2')
   \<turnstile>\<^sub>w\<^sub>f P
 P  \<turnstile> s2 ~ B_app tyid b1 [ bv ::= b' ] \<setminus> s2'
   \<turnstile>\<^sub>w\<^sub>f P

goal (1 subgoal):
 1. b[bva::=b1]\<^sub>b\<^sub>b = b2[bva2::=b1]\<^sub>b\<^sub>b
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
b[bva::=b1]\<^sub>b\<^sub>b = b2[bva2::=b1]\<^sub>b\<^sub>b

goal (2 subgoals):
 1. dc = dc2 \<Longrightarrow> (SConsp tyid dc b1[bv::=b']\<^sub>b\<^sub>b s1 = s2) = (SConsp tyid dc b1 s1' = s2')
 2. dc \<noteq> dc2 \<Longrightarrow> (SConsp tyid dc b1[bv::=b']\<^sub>b\<^sub>b s1 = s2) = (SConsp tyid dc b1 s1' = s2')
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
b[bva::=b1]\<^sub>b\<^sub>b = b2[bva2::=b1]\<^sub>b\<^sub>b
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
b[bva::=b1]\<^sub>b\<^sub>b = b2[bva2::=b1]\<^sub>b\<^sub>b

goal (1 subgoal):
 1. (SConsp tyid dc b1[bv::=b']\<^sub>b\<^sub>b s1 = s2) = (SConsp tyid dc b1 s1' = s2')
[PROOF STEP]
using boxed_b_BConspI True *
[PROOF STATE]
proof (prove)
using this:
b[bva::=b1]\<^sub>b\<^sub>b = b2[bva2::=b1]\<^sub>b\<^sub>b
AF_typedef_poly tyid bva dclist \<in> set P
atom bva \<sharp> (b1, bv, b', s1, s1')
(dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist
 P  \<turnstile> s1 ~ b[bva::=b1]\<^sub>b\<^sub>b [ bv ::= b' ] \<setminus> s1'
\<lbrakk>   \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> ?s2.0 ~ b[bva::=b1]\<^sub>b\<^sub>b [ bv ::= b' ] \<setminus> ?s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s1 = ?s2.0) = (s1' = ?s2')
   \<turnstile>\<^sub>w\<^sub>f P
 P  \<turnstile> s2 ~ B_app tyid b1 [ bv ::= b' ] \<setminus> s2'
   \<turnstile>\<^sub>w\<^sub>f P
dc = dc2
s2 = SConsp tyid dc2 b1[bv::=b']\<^sub>b\<^sub>b s22 \<and> s2' = SConsp tyid dc2 b1 s22' \<and>  P  \<turnstile> s22 ~ b2[bva2::=b1]\<^sub>b\<^sub>b [ bv ::= b' ] \<setminus> s22'  \<and> AF_typedef_poly tyid bva2 dclist2 \<in> set P \<and> (dc2, \<lbrace> x2 : b2  | c2 \<rbrace>) \<in> set dclist2

goal (1 subgoal):
 1. (SConsp tyid dc b1[bv::=b']\<^sub>b\<^sub>b s1 = s2) = (SConsp tyid dc b1 s1' = s2')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(SConsp tyid dc b1[bv::=b']\<^sub>b\<^sub>b s1 = s2) = (SConsp tyid dc b1 s1' = s2')

goal (1 subgoal):
 1. dc \<noteq> dc2 \<Longrightarrow> (SConsp tyid dc b1[bv::=b']\<^sub>b\<^sub>b s1 = s2) = (SConsp tyid dc b1 s1' = s2')
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. dc \<noteq> dc2 \<Longrightarrow> (SConsp tyid dc b1[bv::=b']\<^sub>b\<^sub>b s1 = s2) = (SConsp tyid dc b1 s1' = s2')
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
dc \<noteq> dc2

goal (1 subgoal):
 1. dc \<noteq> dc2 \<Longrightarrow> (SConsp tyid dc b1[bv::=b']\<^sub>b\<^sub>b s1 = s2) = (SConsp tyid dc b1 s1' = s2')
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
dc \<noteq> dc2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
dc \<noteq> dc2

goal (1 subgoal):
 1. (SConsp tyid dc b1[bv::=b']\<^sub>b\<^sub>b s1 = s2) = (SConsp tyid dc b1 s1' = s2')
[PROOF STEP]
using * boxed_b_BConspI
[PROOF STATE]
proof (prove)
using this:
dc \<noteq> dc2
s2 = SConsp tyid dc2 b1[bv::=b']\<^sub>b\<^sub>b s22 \<and> s2' = SConsp tyid dc2 b1 s22' \<and>  P  \<turnstile> s22 ~ b2[bva2::=b1]\<^sub>b\<^sub>b [ bv ::= b' ] \<setminus> s22'  \<and> AF_typedef_poly tyid bva2 dclist2 \<in> set P \<and> (dc2, \<lbrace> x2 : b2  | c2 \<rbrace>) \<in> set dclist2
AF_typedef_poly tyid bva dclist \<in> set P
atom bva \<sharp> (b1, bv, b', s1, s1')
(dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist
 P  \<turnstile> s1 ~ b[bva::=b1]\<^sub>b\<^sub>b [ bv ::= b' ] \<setminus> s1'
\<lbrakk>   \<turnstile>\<^sub>w\<^sub>f P ;  P  \<turnstile> ?s2.0 ~ b[bva::=b1]\<^sub>b\<^sub>b [ bv ::= b' ] \<setminus> ?s2' ;    \<turnstile>\<^sub>w\<^sub>f P \<rbrakk> \<Longrightarrow> (s1 = ?s2.0) = (s1' = ?s2')
   \<turnstile>\<^sub>w\<^sub>f P
 P  \<turnstile> s2 ~ B_app tyid b1 [ bv ::= b' ] \<setminus> s2'
   \<turnstile>\<^sub>w\<^sub>f P

goal (1 subgoal):
 1. (SConsp tyid dc b1[bv::=b']\<^sub>b\<^sub>b s1 = s2) = (SConsp tyid dc b1 s1' = s2')
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(SConsp tyid dc b1[bv::=b']\<^sub>b\<^sub>b s1 = s2) = (SConsp tyid dc b1 s1' = s2')

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(SConsp tyid dc b1[bv::=b']\<^sub>b\<^sub>b s1 = s2) = (SConsp tyid dc b1 s1' = s2')

goal:
No subgoals!
[PROOF STEP]
qed