[STATEMENT]
lemma eval_c_weakening_x:
  fixes c::c
  assumes  "i' \<lbrakk> c \<rbrakk> ~ s" and "atom x \<sharp> c" and "i = i' (x \<mapsto> s')"
  shows "i \<lbrakk> c \<rbrakk> ~ s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  i \<lbrakk> c \<rbrakk> ~ s
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
 i' \<lbrakk> c \<rbrakk> ~ s
atom x \<sharp> c
i = i'(x \<mapsto> s')

goal (1 subgoal):
 1.  i \<lbrakk> c \<rbrakk> ~ s
[PROOF STEP]
proof(induct rule: eval_c.induct)
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. \<And>ia. \<lbrakk>atom x \<sharp> (TRUE); i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> TRUE \<rbrakk> ~ True
 2. \<And>ia. \<lbrakk>atom x \<sharp> (FALSE); i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> FALSE \<rbrakk> ~ False
 3. \<And>ia c1 b1 c2 b2. \<lbrakk> ia \<lbrakk> c1 \<rbrakk> ~ b1 ; \<lbrakk>atom x \<sharp> c1; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c1 \<rbrakk> ~ b1 ;  ia \<lbrakk> c2 \<rbrakk> ~ b2 ; \<lbrakk>atom x \<sharp> c2; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c2 \<rbrakk> ~ b2 ; atom x \<sharp> (c1  AND  c2 ); i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c1  AND  c2  \<rbrakk> ~ b1 \<and> b2
 4. \<And>ia c1 b1 c2 b2. \<lbrakk> ia \<lbrakk> c1 \<rbrakk> ~ b1 ; \<lbrakk>atom x \<sharp> c1; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c1 \<rbrakk> ~ b1 ;  ia \<lbrakk> c2 \<rbrakk> ~ b2 ; \<lbrakk>atom x \<sharp> c2; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c2 \<rbrakk> ~ b2 ; atom x \<sharp> (c1 OR c2 ); i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c1 OR c2  \<rbrakk> ~ b1 \<or> b2
 5. \<And>ia c1 b1 c2 b2. \<lbrakk> ia \<lbrakk> c1 \<rbrakk> ~ b1 ; \<lbrakk>atom x \<sharp> c1; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c1 \<rbrakk> ~ b1 ;  ia \<lbrakk> c2 \<rbrakk> ~ b2 ; \<lbrakk>atom x \<sharp> c2; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c2 \<rbrakk> ~ b2 ; atom x \<sharp> (c1  IMP  c2 ); i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c1  IMP  c2  \<rbrakk> ~ b1 \<longrightarrow> b2
 6. \<And>ia c b. \<lbrakk> ia \<lbrakk> c \<rbrakk> ~ b ; \<lbrakk>atom x \<sharp> c; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c \<rbrakk> ~ b ; atom x \<sharp> (\<not> c ); i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> \<not> c  \<rbrakk> ~ \<not> b
 7. \<And>ia e1 sv1 e2 sv2. \<lbrakk>ia \<lbrakk> e1 \<rbrakk> ~ sv1 ; ia \<lbrakk> e2 \<rbrakk> ~ sv2 ; atom x \<sharp> (e1  ==  e2 ); i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> e1  ==  e2  \<rbrakk> ~ sv1 = sv2
[PROOF STEP]
case (eval_c_trueI i)
[PROOF STATE]
proof (state)
this:
atom x \<sharp> (TRUE)
i = i(x \<mapsto> s')

goal (7 subgoals):
 1. \<And>ia. \<lbrakk>atom x \<sharp> (TRUE); i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> TRUE \<rbrakk> ~ True
 2. \<And>ia. \<lbrakk>atom x \<sharp> (FALSE); i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> FALSE \<rbrakk> ~ False
 3. \<And>ia c1 b1 c2 b2. \<lbrakk> ia \<lbrakk> c1 \<rbrakk> ~ b1 ; \<lbrakk>atom x \<sharp> c1; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c1 \<rbrakk> ~ b1 ;  ia \<lbrakk> c2 \<rbrakk> ~ b2 ; \<lbrakk>atom x \<sharp> c2; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c2 \<rbrakk> ~ b2 ; atom x \<sharp> (c1  AND  c2 ); i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c1  AND  c2  \<rbrakk> ~ b1 \<and> b2
 4. \<And>ia c1 b1 c2 b2. \<lbrakk> ia \<lbrakk> c1 \<rbrakk> ~ b1 ; \<lbrakk>atom x \<sharp> c1; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c1 \<rbrakk> ~ b1 ;  ia \<lbrakk> c2 \<rbrakk> ~ b2 ; \<lbrakk>atom x \<sharp> c2; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c2 \<rbrakk> ~ b2 ; atom x \<sharp> (c1 OR c2 ); i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c1 OR c2  \<rbrakk> ~ b1 \<or> b2
 5. \<And>ia c1 b1 c2 b2. \<lbrakk> ia \<lbrakk> c1 \<rbrakk> ~ b1 ; \<lbrakk>atom x \<sharp> c1; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c1 \<rbrakk> ~ b1 ;  ia \<lbrakk> c2 \<rbrakk> ~ b2 ; \<lbrakk>atom x \<sharp> c2; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c2 \<rbrakk> ~ b2 ; atom x \<sharp> (c1  IMP  c2 ); i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c1  IMP  c2  \<rbrakk> ~ b1 \<longrightarrow> b2
 6. \<And>ia c b. \<lbrakk> ia \<lbrakk> c \<rbrakk> ~ b ; \<lbrakk>atom x \<sharp> c; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c \<rbrakk> ~ b ; atom x \<sharp> (\<not> c ); i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> \<not> c  \<rbrakk> ~ \<not> b
 7. \<And>ia e1 sv1 e2 sv2. \<lbrakk>ia \<lbrakk> e1 \<rbrakk> ~ sv1 ; ia \<lbrakk> e2 \<rbrakk> ~ sv2 ; atom x \<sharp> (e1  ==  e2 ); i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> e1  ==  e2  \<rbrakk> ~ sv1 = sv2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
atom x \<sharp> (TRUE)
i = i(x \<mapsto> s')
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
atom x \<sharp> (TRUE)
i = i(x \<mapsto> s')

goal (1 subgoal):
 1.  i \<lbrakk> TRUE \<rbrakk> ~ True
[PROOF STEP]
using eval_c.intros
[PROOF STATE]
proof (prove)
using this:
atom x \<sharp> (TRUE)
i = i(x \<mapsto> s')
 ?i \<lbrakk> TRUE \<rbrakk> ~ True
 ?i \<lbrakk> FALSE \<rbrakk> ~ False
\<lbrakk> ?i \<lbrakk> ?c1.0 \<rbrakk> ~ ?b1.0 ;  ?i \<lbrakk> ?c2.0 \<rbrakk> ~ ?b2.0 \<rbrakk> \<Longrightarrow>  ?i \<lbrakk> ?c1.0  AND  ?c2.0  \<rbrakk> ~ ?b1.0 \<and> ?b2.0
\<lbrakk> ?i \<lbrakk> ?c1.0 \<rbrakk> ~ ?b1.0 ;  ?i \<lbrakk> ?c2.0 \<rbrakk> ~ ?b2.0 \<rbrakk> \<Longrightarrow>  ?i \<lbrakk> ?c1.0 OR ?c2.0  \<rbrakk> ~ ?b1.0 \<or> ?b2.0
\<lbrakk> ?i \<lbrakk> ?c1.0 \<rbrakk> ~ ?b1.0 ;  ?i \<lbrakk> ?c2.0 \<rbrakk> ~ ?b2.0 \<rbrakk> \<Longrightarrow>  ?i \<lbrakk> ?c1.0  IMP  ?c2.0  \<rbrakk> ~ ?b1.0 \<longrightarrow> ?b2.0
 ?i \<lbrakk> ?c \<rbrakk> ~ ?b  \<Longrightarrow>  ?i \<lbrakk> \<not> ?c  \<rbrakk> ~ \<not> ?b
\<lbrakk>?i \<lbrakk> ?e1.0 \<rbrakk> ~ ?sv1.0 ; ?i \<lbrakk> ?e2.0 \<rbrakk> ~ ?sv2.0 \<rbrakk> \<Longrightarrow>  ?i \<lbrakk> ?e1.0  ==  ?e2.0  \<rbrakk> ~ ?sv1.0 = ?sv2.0

goal (1 subgoal):
 1.  i \<lbrakk> TRUE \<rbrakk> ~ True
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
 i \<lbrakk> TRUE \<rbrakk> ~ True

goal (6 subgoals):
 1. \<And>ia. \<lbrakk>atom x \<sharp> (FALSE); i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> FALSE \<rbrakk> ~ False
 2. \<And>ia c1 b1 c2 b2. \<lbrakk> ia \<lbrakk> c1 \<rbrakk> ~ b1 ; \<lbrakk>atom x \<sharp> c1; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c1 \<rbrakk> ~ b1 ;  ia \<lbrakk> c2 \<rbrakk> ~ b2 ; \<lbrakk>atom x \<sharp> c2; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c2 \<rbrakk> ~ b2 ; atom x \<sharp> (c1  AND  c2 ); i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c1  AND  c2  \<rbrakk> ~ b1 \<and> b2
 3. \<And>ia c1 b1 c2 b2. \<lbrakk> ia \<lbrakk> c1 \<rbrakk> ~ b1 ; \<lbrakk>atom x \<sharp> c1; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c1 \<rbrakk> ~ b1 ;  ia \<lbrakk> c2 \<rbrakk> ~ b2 ; \<lbrakk>atom x \<sharp> c2; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c2 \<rbrakk> ~ b2 ; atom x \<sharp> (c1 OR c2 ); i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c1 OR c2  \<rbrakk> ~ b1 \<or> b2
 4. \<And>ia c1 b1 c2 b2. \<lbrakk> ia \<lbrakk> c1 \<rbrakk> ~ b1 ; \<lbrakk>atom x \<sharp> c1; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c1 \<rbrakk> ~ b1 ;  ia \<lbrakk> c2 \<rbrakk> ~ b2 ; \<lbrakk>atom x \<sharp> c2; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c2 \<rbrakk> ~ b2 ; atom x \<sharp> (c1  IMP  c2 ); i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c1  IMP  c2  \<rbrakk> ~ b1 \<longrightarrow> b2
 5. \<And>ia c b. \<lbrakk> ia \<lbrakk> c \<rbrakk> ~ b ; \<lbrakk>atom x \<sharp> c; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c \<rbrakk> ~ b ; atom x \<sharp> (\<not> c ); i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> \<not> c  \<rbrakk> ~ \<not> b
 6. \<And>ia e1 sv1 e2 sv2. \<lbrakk>ia \<lbrakk> e1 \<rbrakk> ~ sv1 ; ia \<lbrakk> e2 \<rbrakk> ~ sv2 ; atom x \<sharp> (e1  ==  e2 ); i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> e1  ==  e2  \<rbrakk> ~ sv1 = sv2
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<And>ia. \<lbrakk>atom x \<sharp> (FALSE); i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> FALSE \<rbrakk> ~ False
 2. \<And>ia c1 b1 c2 b2. \<lbrakk> ia \<lbrakk> c1 \<rbrakk> ~ b1 ; \<lbrakk>atom x \<sharp> c1; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c1 \<rbrakk> ~ b1 ;  ia \<lbrakk> c2 \<rbrakk> ~ b2 ; \<lbrakk>atom x \<sharp> c2; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c2 \<rbrakk> ~ b2 ; atom x \<sharp> (c1  AND  c2 ); i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c1  AND  c2  \<rbrakk> ~ b1 \<and> b2
 3. \<And>ia c1 b1 c2 b2. \<lbrakk> ia \<lbrakk> c1 \<rbrakk> ~ b1 ; \<lbrakk>atom x \<sharp> c1; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c1 \<rbrakk> ~ b1 ;  ia \<lbrakk> c2 \<rbrakk> ~ b2 ; \<lbrakk>atom x \<sharp> c2; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c2 \<rbrakk> ~ b2 ; atom x \<sharp> (c1 OR c2 ); i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c1 OR c2  \<rbrakk> ~ b1 \<or> b2
 4. \<And>ia c1 b1 c2 b2. \<lbrakk> ia \<lbrakk> c1 \<rbrakk> ~ b1 ; \<lbrakk>atom x \<sharp> c1; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c1 \<rbrakk> ~ b1 ;  ia \<lbrakk> c2 \<rbrakk> ~ b2 ; \<lbrakk>atom x \<sharp> c2; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c2 \<rbrakk> ~ b2 ; atom x \<sharp> (c1  IMP  c2 ); i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c1  IMP  c2  \<rbrakk> ~ b1 \<longrightarrow> b2
 5. \<And>ia c b. \<lbrakk> ia \<lbrakk> c \<rbrakk> ~ b ; \<lbrakk>atom x \<sharp> c; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c \<rbrakk> ~ b ; atom x \<sharp> (\<not> c ); i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> \<not> c  \<rbrakk> ~ \<not> b
 6. \<And>ia e1 sv1 e2 sv2. \<lbrakk>ia \<lbrakk> e1 \<rbrakk> ~ sv1 ; ia \<lbrakk> e2 \<rbrakk> ~ sv2 ; atom x \<sharp> (e1  ==  e2 ); i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> e1  ==  e2  \<rbrakk> ~ sv1 = sv2
[PROOF STEP]
case (eval_c_falseI i)
[PROOF STATE]
proof (state)
this:
atom x \<sharp> (FALSE)
i = i(x \<mapsto> s')

goal (6 subgoals):
 1. \<And>ia. \<lbrakk>atom x \<sharp> (FALSE); i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> FALSE \<rbrakk> ~ False
 2. \<And>ia c1 b1 c2 b2. \<lbrakk> ia \<lbrakk> c1 \<rbrakk> ~ b1 ; \<lbrakk>atom x \<sharp> c1; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c1 \<rbrakk> ~ b1 ;  ia \<lbrakk> c2 \<rbrakk> ~ b2 ; \<lbrakk>atom x \<sharp> c2; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c2 \<rbrakk> ~ b2 ; atom x \<sharp> (c1  AND  c2 ); i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c1  AND  c2  \<rbrakk> ~ b1 \<and> b2
 3. \<And>ia c1 b1 c2 b2. \<lbrakk> ia \<lbrakk> c1 \<rbrakk> ~ b1 ; \<lbrakk>atom x \<sharp> c1; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c1 \<rbrakk> ~ b1 ;  ia \<lbrakk> c2 \<rbrakk> ~ b2 ; \<lbrakk>atom x \<sharp> c2; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c2 \<rbrakk> ~ b2 ; atom x \<sharp> (c1 OR c2 ); i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c1 OR c2  \<rbrakk> ~ b1 \<or> b2
 4. \<And>ia c1 b1 c2 b2. \<lbrakk> ia \<lbrakk> c1 \<rbrakk> ~ b1 ; \<lbrakk>atom x \<sharp> c1; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c1 \<rbrakk> ~ b1 ;  ia \<lbrakk> c2 \<rbrakk> ~ b2 ; \<lbrakk>atom x \<sharp> c2; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c2 \<rbrakk> ~ b2 ; atom x \<sharp> (c1  IMP  c2 ); i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c1  IMP  c2  \<rbrakk> ~ b1 \<longrightarrow> b2
 5. \<And>ia c b. \<lbrakk> ia \<lbrakk> c \<rbrakk> ~ b ; \<lbrakk>atom x \<sharp> c; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c \<rbrakk> ~ b ; atom x \<sharp> (\<not> c ); i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> \<not> c  \<rbrakk> ~ \<not> b
 6. \<And>ia e1 sv1 e2 sv2. \<lbrakk>ia \<lbrakk> e1 \<rbrakk> ~ sv1 ; ia \<lbrakk> e2 \<rbrakk> ~ sv2 ; atom x \<sharp> (e1  ==  e2 ); i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> e1  ==  e2  \<rbrakk> ~ sv1 = sv2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
atom x \<sharp> (FALSE)
i = i(x \<mapsto> s')
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
atom x \<sharp> (FALSE)
i = i(x \<mapsto> s')

goal (1 subgoal):
 1.  i \<lbrakk> FALSE \<rbrakk> ~ False
[PROOF STEP]
using eval_c.intros
[PROOF STATE]
proof (prove)
using this:
atom x \<sharp> (FALSE)
i = i(x \<mapsto> s')
 ?i \<lbrakk> TRUE \<rbrakk> ~ True
 ?i \<lbrakk> FALSE \<rbrakk> ~ False
\<lbrakk> ?i \<lbrakk> ?c1.0 \<rbrakk> ~ ?b1.0 ;  ?i \<lbrakk> ?c2.0 \<rbrakk> ~ ?b2.0 \<rbrakk> \<Longrightarrow>  ?i \<lbrakk> ?c1.0  AND  ?c2.0  \<rbrakk> ~ ?b1.0 \<and> ?b2.0
\<lbrakk> ?i \<lbrakk> ?c1.0 \<rbrakk> ~ ?b1.0 ;  ?i \<lbrakk> ?c2.0 \<rbrakk> ~ ?b2.0 \<rbrakk> \<Longrightarrow>  ?i \<lbrakk> ?c1.0 OR ?c2.0  \<rbrakk> ~ ?b1.0 \<or> ?b2.0
\<lbrakk> ?i \<lbrakk> ?c1.0 \<rbrakk> ~ ?b1.0 ;  ?i \<lbrakk> ?c2.0 \<rbrakk> ~ ?b2.0 \<rbrakk> \<Longrightarrow>  ?i \<lbrakk> ?c1.0  IMP  ?c2.0  \<rbrakk> ~ ?b1.0 \<longrightarrow> ?b2.0
 ?i \<lbrakk> ?c \<rbrakk> ~ ?b  \<Longrightarrow>  ?i \<lbrakk> \<not> ?c  \<rbrakk> ~ \<not> ?b
\<lbrakk>?i \<lbrakk> ?e1.0 \<rbrakk> ~ ?sv1.0 ; ?i \<lbrakk> ?e2.0 \<rbrakk> ~ ?sv2.0 \<rbrakk> \<Longrightarrow>  ?i \<lbrakk> ?e1.0  ==  ?e2.0  \<rbrakk> ~ ?sv1.0 = ?sv2.0

goal (1 subgoal):
 1.  i \<lbrakk> FALSE \<rbrakk> ~ False
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
 i \<lbrakk> FALSE \<rbrakk> ~ False

goal (5 subgoals):
 1. \<And>ia c1 b1 c2 b2. \<lbrakk> ia \<lbrakk> c1 \<rbrakk> ~ b1 ; \<lbrakk>atom x \<sharp> c1; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c1 \<rbrakk> ~ b1 ;  ia \<lbrakk> c2 \<rbrakk> ~ b2 ; \<lbrakk>atom x \<sharp> c2; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c2 \<rbrakk> ~ b2 ; atom x \<sharp> (c1  AND  c2 ); i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c1  AND  c2  \<rbrakk> ~ b1 \<and> b2
 2. \<And>ia c1 b1 c2 b2. \<lbrakk> ia \<lbrakk> c1 \<rbrakk> ~ b1 ; \<lbrakk>atom x \<sharp> c1; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c1 \<rbrakk> ~ b1 ;  ia \<lbrakk> c2 \<rbrakk> ~ b2 ; \<lbrakk>atom x \<sharp> c2; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c2 \<rbrakk> ~ b2 ; atom x \<sharp> (c1 OR c2 ); i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c1 OR c2  \<rbrakk> ~ b1 \<or> b2
 3. \<And>ia c1 b1 c2 b2. \<lbrakk> ia \<lbrakk> c1 \<rbrakk> ~ b1 ; \<lbrakk>atom x \<sharp> c1; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c1 \<rbrakk> ~ b1 ;  ia \<lbrakk> c2 \<rbrakk> ~ b2 ; \<lbrakk>atom x \<sharp> c2; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c2 \<rbrakk> ~ b2 ; atom x \<sharp> (c1  IMP  c2 ); i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c1  IMP  c2  \<rbrakk> ~ b1 \<longrightarrow> b2
 4. \<And>ia c b. \<lbrakk> ia \<lbrakk> c \<rbrakk> ~ b ; \<lbrakk>atom x \<sharp> c; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c \<rbrakk> ~ b ; atom x \<sharp> (\<not> c ); i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> \<not> c  \<rbrakk> ~ \<not> b
 5. \<And>ia e1 sv1 e2 sv2. \<lbrakk>ia \<lbrakk> e1 \<rbrakk> ~ sv1 ; ia \<lbrakk> e2 \<rbrakk> ~ sv2 ; atom x \<sharp> (e1  ==  e2 ); i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> e1  ==  e2  \<rbrakk> ~ sv1 = sv2
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>ia c1 b1 c2 b2. \<lbrakk> ia \<lbrakk> c1 \<rbrakk> ~ b1 ; \<lbrakk>atom x \<sharp> c1; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c1 \<rbrakk> ~ b1 ;  ia \<lbrakk> c2 \<rbrakk> ~ b2 ; \<lbrakk>atom x \<sharp> c2; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c2 \<rbrakk> ~ b2 ; atom x \<sharp> (c1  AND  c2 ); i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c1  AND  c2  \<rbrakk> ~ b1 \<and> b2
 2. \<And>ia c1 b1 c2 b2. \<lbrakk> ia \<lbrakk> c1 \<rbrakk> ~ b1 ; \<lbrakk>atom x \<sharp> c1; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c1 \<rbrakk> ~ b1 ;  ia \<lbrakk> c2 \<rbrakk> ~ b2 ; \<lbrakk>atom x \<sharp> c2; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c2 \<rbrakk> ~ b2 ; atom x \<sharp> (c1 OR c2 ); i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c1 OR c2  \<rbrakk> ~ b1 \<or> b2
 3. \<And>ia c1 b1 c2 b2. \<lbrakk> ia \<lbrakk> c1 \<rbrakk> ~ b1 ; \<lbrakk>atom x \<sharp> c1; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c1 \<rbrakk> ~ b1 ;  ia \<lbrakk> c2 \<rbrakk> ~ b2 ; \<lbrakk>atom x \<sharp> c2; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c2 \<rbrakk> ~ b2 ; atom x \<sharp> (c1  IMP  c2 ); i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c1  IMP  c2  \<rbrakk> ~ b1 \<longrightarrow> b2
 4. \<And>ia c b. \<lbrakk> ia \<lbrakk> c \<rbrakk> ~ b ; \<lbrakk>atom x \<sharp> c; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c \<rbrakk> ~ b ; atom x \<sharp> (\<not> c ); i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> \<not> c  \<rbrakk> ~ \<not> b
 5. \<And>ia e1 sv1 e2 sv2. \<lbrakk>ia \<lbrakk> e1 \<rbrakk> ~ sv1 ; ia \<lbrakk> e2 \<rbrakk> ~ sv2 ; atom x \<sharp> (e1  ==  e2 ); i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> e1  ==  e2  \<rbrakk> ~ sv1 = sv2
[PROOF STEP]
case (eval_c_conjI i c1 b1 c2 b2)
[PROOF STATE]
proof (state)
this:
 i \<lbrakk> c1 \<rbrakk> ~ b1
\<lbrakk>atom x \<sharp> c1; i = i(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c1 \<rbrakk> ~ b1
 i \<lbrakk> c2 \<rbrakk> ~ b2
\<lbrakk>atom x \<sharp> c2; i = i(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c2 \<rbrakk> ~ b2
atom x \<sharp> (c1  AND  c2 )
i = i(x \<mapsto> s')

goal (5 subgoals):
 1. \<And>ia c1 b1 c2 b2. \<lbrakk> ia \<lbrakk> c1 \<rbrakk> ~ b1 ; \<lbrakk>atom x \<sharp> c1; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c1 \<rbrakk> ~ b1 ;  ia \<lbrakk> c2 \<rbrakk> ~ b2 ; \<lbrakk>atom x \<sharp> c2; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c2 \<rbrakk> ~ b2 ; atom x \<sharp> (c1  AND  c2 ); i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c1  AND  c2  \<rbrakk> ~ b1 \<and> b2
 2. \<And>ia c1 b1 c2 b2. \<lbrakk> ia \<lbrakk> c1 \<rbrakk> ~ b1 ; \<lbrakk>atom x \<sharp> c1; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c1 \<rbrakk> ~ b1 ;  ia \<lbrakk> c2 \<rbrakk> ~ b2 ; \<lbrakk>atom x \<sharp> c2; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c2 \<rbrakk> ~ b2 ; atom x \<sharp> (c1 OR c2 ); i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c1 OR c2  \<rbrakk> ~ b1 \<or> b2
 3. \<And>ia c1 b1 c2 b2. \<lbrakk> ia \<lbrakk> c1 \<rbrakk> ~ b1 ; \<lbrakk>atom x \<sharp> c1; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c1 \<rbrakk> ~ b1 ;  ia \<lbrakk> c2 \<rbrakk> ~ b2 ; \<lbrakk>atom x \<sharp> c2; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c2 \<rbrakk> ~ b2 ; atom x \<sharp> (c1  IMP  c2 ); i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c1  IMP  c2  \<rbrakk> ~ b1 \<longrightarrow> b2
 4. \<And>ia c b. \<lbrakk> ia \<lbrakk> c \<rbrakk> ~ b ; \<lbrakk>atom x \<sharp> c; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c \<rbrakk> ~ b ; atom x \<sharp> (\<not> c ); i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> \<not> c  \<rbrakk> ~ \<not> b
 5. \<And>ia e1 sv1 e2 sv2. \<lbrakk>ia \<lbrakk> e1 \<rbrakk> ~ sv1 ; ia \<lbrakk> e2 \<rbrakk> ~ sv2 ; atom x \<sharp> (e1  ==  e2 ); i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> e1  ==  e2  \<rbrakk> ~ sv1 = sv2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
 i \<lbrakk> c1 \<rbrakk> ~ b1
\<lbrakk>atom x \<sharp> c1; i = i(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c1 \<rbrakk> ~ b1
 i \<lbrakk> c2 \<rbrakk> ~ b2
\<lbrakk>atom x \<sharp> c2; i = i(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c2 \<rbrakk> ~ b2
atom x \<sharp> (c1  AND  c2 )
i = i(x \<mapsto> s')
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
 i \<lbrakk> c1 \<rbrakk> ~ b1
\<lbrakk>atom x \<sharp> c1; i = i(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c1 \<rbrakk> ~ b1
 i \<lbrakk> c2 \<rbrakk> ~ b2
\<lbrakk>atom x \<sharp> c2; i = i(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c2 \<rbrakk> ~ b2
atom x \<sharp> (c1  AND  c2 )
i = i(x \<mapsto> s')

goal (1 subgoal):
 1.  i \<lbrakk> c1  AND  c2  \<rbrakk> ~ b1 \<and> b2
[PROOF STEP]
using eval_c.intros
[PROOF STATE]
proof (prove)
using this:
 i \<lbrakk> c1 \<rbrakk> ~ b1
\<lbrakk>atom x \<sharp> c1; i = i(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c1 \<rbrakk> ~ b1
 i \<lbrakk> c2 \<rbrakk> ~ b2
\<lbrakk>atom x \<sharp> c2; i = i(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c2 \<rbrakk> ~ b2
atom x \<sharp> (c1  AND  c2 )
i = i(x \<mapsto> s')
 ?i \<lbrakk> TRUE \<rbrakk> ~ True
 ?i \<lbrakk> FALSE \<rbrakk> ~ False
\<lbrakk> ?i \<lbrakk> ?c1.0 \<rbrakk> ~ ?b1.0 ;  ?i \<lbrakk> ?c2.0 \<rbrakk> ~ ?b2.0 \<rbrakk> \<Longrightarrow>  ?i \<lbrakk> ?c1.0  AND  ?c2.0  \<rbrakk> ~ ?b1.0 \<and> ?b2.0
\<lbrakk> ?i \<lbrakk> ?c1.0 \<rbrakk> ~ ?b1.0 ;  ?i \<lbrakk> ?c2.0 \<rbrakk> ~ ?b2.0 \<rbrakk> \<Longrightarrow>  ?i \<lbrakk> ?c1.0 OR ?c2.0  \<rbrakk> ~ ?b1.0 \<or> ?b2.0
\<lbrakk> ?i \<lbrakk> ?c1.0 \<rbrakk> ~ ?b1.0 ;  ?i \<lbrakk> ?c2.0 \<rbrakk> ~ ?b2.0 \<rbrakk> \<Longrightarrow>  ?i \<lbrakk> ?c1.0  IMP  ?c2.0  \<rbrakk> ~ ?b1.0 \<longrightarrow> ?b2.0
 ?i \<lbrakk> ?c \<rbrakk> ~ ?b  \<Longrightarrow>  ?i \<lbrakk> \<not> ?c  \<rbrakk> ~ \<not> ?b
\<lbrakk>?i \<lbrakk> ?e1.0 \<rbrakk> ~ ?sv1.0 ; ?i \<lbrakk> ?e2.0 \<rbrakk> ~ ?sv2.0 \<rbrakk> \<Longrightarrow>  ?i \<lbrakk> ?e1.0  ==  ?e2.0  \<rbrakk> ~ ?sv1.0 = ?sv2.0

goal (1 subgoal):
 1.  i \<lbrakk> c1  AND  c2  \<rbrakk> ~ b1 \<and> b2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
 i \<lbrakk> c1  AND  c2  \<rbrakk> ~ b1 \<and> b2

goal (4 subgoals):
 1. \<And>ia c1 b1 c2 b2. \<lbrakk> ia \<lbrakk> c1 \<rbrakk> ~ b1 ; \<lbrakk>atom x \<sharp> c1; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c1 \<rbrakk> ~ b1 ;  ia \<lbrakk> c2 \<rbrakk> ~ b2 ; \<lbrakk>atom x \<sharp> c2; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c2 \<rbrakk> ~ b2 ; atom x \<sharp> (c1 OR c2 ); i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c1 OR c2  \<rbrakk> ~ b1 \<or> b2
 2. \<And>ia c1 b1 c2 b2. \<lbrakk> ia \<lbrakk> c1 \<rbrakk> ~ b1 ; \<lbrakk>atom x \<sharp> c1; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c1 \<rbrakk> ~ b1 ;  ia \<lbrakk> c2 \<rbrakk> ~ b2 ; \<lbrakk>atom x \<sharp> c2; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c2 \<rbrakk> ~ b2 ; atom x \<sharp> (c1  IMP  c2 ); i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c1  IMP  c2  \<rbrakk> ~ b1 \<longrightarrow> b2
 3. \<And>ia c b. \<lbrakk> ia \<lbrakk> c \<rbrakk> ~ b ; \<lbrakk>atom x \<sharp> c; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c \<rbrakk> ~ b ; atom x \<sharp> (\<not> c ); i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> \<not> c  \<rbrakk> ~ \<not> b
 4. \<And>ia e1 sv1 e2 sv2. \<lbrakk>ia \<lbrakk> e1 \<rbrakk> ~ sv1 ; ia \<lbrakk> e2 \<rbrakk> ~ sv2 ; atom x \<sharp> (e1  ==  e2 ); i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> e1  ==  e2  \<rbrakk> ~ sv1 = sv2
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>ia c1 b1 c2 b2. \<lbrakk> ia \<lbrakk> c1 \<rbrakk> ~ b1 ; \<lbrakk>atom x \<sharp> c1; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c1 \<rbrakk> ~ b1 ;  ia \<lbrakk> c2 \<rbrakk> ~ b2 ; \<lbrakk>atom x \<sharp> c2; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c2 \<rbrakk> ~ b2 ; atom x \<sharp> (c1 OR c2 ); i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c1 OR c2  \<rbrakk> ~ b1 \<or> b2
 2. \<And>ia c1 b1 c2 b2. \<lbrakk> ia \<lbrakk> c1 \<rbrakk> ~ b1 ; \<lbrakk>atom x \<sharp> c1; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c1 \<rbrakk> ~ b1 ;  ia \<lbrakk> c2 \<rbrakk> ~ b2 ; \<lbrakk>atom x \<sharp> c2; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c2 \<rbrakk> ~ b2 ; atom x \<sharp> (c1  IMP  c2 ); i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c1  IMP  c2  \<rbrakk> ~ b1 \<longrightarrow> b2
 3. \<And>ia c b. \<lbrakk> ia \<lbrakk> c \<rbrakk> ~ b ; \<lbrakk>atom x \<sharp> c; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c \<rbrakk> ~ b ; atom x \<sharp> (\<not> c ); i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> \<not> c  \<rbrakk> ~ \<not> b
 4. \<And>ia e1 sv1 e2 sv2. \<lbrakk>ia \<lbrakk> e1 \<rbrakk> ~ sv1 ; ia \<lbrakk> e2 \<rbrakk> ~ sv2 ; atom x \<sharp> (e1  ==  e2 ); i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> e1  ==  e2  \<rbrakk> ~ sv1 = sv2
[PROOF STEP]
case (eval_c_disjI i c1 b1 c2 b2)
[PROOF STATE]
proof (state)
this:
 i \<lbrakk> c1 \<rbrakk> ~ b1
\<lbrakk>atom x \<sharp> c1; i = i(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c1 \<rbrakk> ~ b1
 i \<lbrakk> c2 \<rbrakk> ~ b2
\<lbrakk>atom x \<sharp> c2; i = i(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c2 \<rbrakk> ~ b2
atom x \<sharp> (c1 OR c2 )
i = i(x \<mapsto> s')

goal (4 subgoals):
 1. \<And>ia c1 b1 c2 b2. \<lbrakk> ia \<lbrakk> c1 \<rbrakk> ~ b1 ; \<lbrakk>atom x \<sharp> c1; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c1 \<rbrakk> ~ b1 ;  ia \<lbrakk> c2 \<rbrakk> ~ b2 ; \<lbrakk>atom x \<sharp> c2; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c2 \<rbrakk> ~ b2 ; atom x \<sharp> (c1 OR c2 ); i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c1 OR c2  \<rbrakk> ~ b1 \<or> b2
 2. \<And>ia c1 b1 c2 b2. \<lbrakk> ia \<lbrakk> c1 \<rbrakk> ~ b1 ; \<lbrakk>atom x \<sharp> c1; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c1 \<rbrakk> ~ b1 ;  ia \<lbrakk> c2 \<rbrakk> ~ b2 ; \<lbrakk>atom x \<sharp> c2; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c2 \<rbrakk> ~ b2 ; atom x \<sharp> (c1  IMP  c2 ); i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c1  IMP  c2  \<rbrakk> ~ b1 \<longrightarrow> b2
 3. \<And>ia c b. \<lbrakk> ia \<lbrakk> c \<rbrakk> ~ b ; \<lbrakk>atom x \<sharp> c; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c \<rbrakk> ~ b ; atom x \<sharp> (\<not> c ); i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> \<not> c  \<rbrakk> ~ \<not> b
 4. \<And>ia e1 sv1 e2 sv2. \<lbrakk>ia \<lbrakk> e1 \<rbrakk> ~ sv1 ; ia \<lbrakk> e2 \<rbrakk> ~ sv2 ; atom x \<sharp> (e1  ==  e2 ); i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> e1  ==  e2  \<rbrakk> ~ sv1 = sv2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
 i \<lbrakk> c1 \<rbrakk> ~ b1
\<lbrakk>atom x \<sharp> c1; i = i(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c1 \<rbrakk> ~ b1
 i \<lbrakk> c2 \<rbrakk> ~ b2
\<lbrakk>atom x \<sharp> c2; i = i(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c2 \<rbrakk> ~ b2
atom x \<sharp> (c1 OR c2 )
i = i(x \<mapsto> s')
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
 i \<lbrakk> c1 \<rbrakk> ~ b1
\<lbrakk>atom x \<sharp> c1; i = i(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c1 \<rbrakk> ~ b1
 i \<lbrakk> c2 \<rbrakk> ~ b2
\<lbrakk>atom x \<sharp> c2; i = i(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c2 \<rbrakk> ~ b2
atom x \<sharp> (c1 OR c2 )
i = i(x \<mapsto> s')

goal (1 subgoal):
 1.  i \<lbrakk> c1 OR c2  \<rbrakk> ~ b1 \<or> b2
[PROOF STEP]
using eval_c.intros
[PROOF STATE]
proof (prove)
using this:
 i \<lbrakk> c1 \<rbrakk> ~ b1
\<lbrakk>atom x \<sharp> c1; i = i(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c1 \<rbrakk> ~ b1
 i \<lbrakk> c2 \<rbrakk> ~ b2
\<lbrakk>atom x \<sharp> c2; i = i(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c2 \<rbrakk> ~ b2
atom x \<sharp> (c1 OR c2 )
i = i(x \<mapsto> s')
 ?i \<lbrakk> TRUE \<rbrakk> ~ True
 ?i \<lbrakk> FALSE \<rbrakk> ~ False
\<lbrakk> ?i \<lbrakk> ?c1.0 \<rbrakk> ~ ?b1.0 ;  ?i \<lbrakk> ?c2.0 \<rbrakk> ~ ?b2.0 \<rbrakk> \<Longrightarrow>  ?i \<lbrakk> ?c1.0  AND  ?c2.0  \<rbrakk> ~ ?b1.0 \<and> ?b2.0
\<lbrakk> ?i \<lbrakk> ?c1.0 \<rbrakk> ~ ?b1.0 ;  ?i \<lbrakk> ?c2.0 \<rbrakk> ~ ?b2.0 \<rbrakk> \<Longrightarrow>  ?i \<lbrakk> ?c1.0 OR ?c2.0  \<rbrakk> ~ ?b1.0 \<or> ?b2.0
\<lbrakk> ?i \<lbrakk> ?c1.0 \<rbrakk> ~ ?b1.0 ;  ?i \<lbrakk> ?c2.0 \<rbrakk> ~ ?b2.0 \<rbrakk> \<Longrightarrow>  ?i \<lbrakk> ?c1.0  IMP  ?c2.0  \<rbrakk> ~ ?b1.0 \<longrightarrow> ?b2.0
 ?i \<lbrakk> ?c \<rbrakk> ~ ?b  \<Longrightarrow>  ?i \<lbrakk> \<not> ?c  \<rbrakk> ~ \<not> ?b
\<lbrakk>?i \<lbrakk> ?e1.0 \<rbrakk> ~ ?sv1.0 ; ?i \<lbrakk> ?e2.0 \<rbrakk> ~ ?sv2.0 \<rbrakk> \<Longrightarrow>  ?i \<lbrakk> ?e1.0  ==  ?e2.0  \<rbrakk> ~ ?sv1.0 = ?sv2.0

goal (1 subgoal):
 1.  i \<lbrakk> c1 OR c2  \<rbrakk> ~ b1 \<or> b2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
 i \<lbrakk> c1 OR c2  \<rbrakk> ~ b1 \<or> b2

goal (3 subgoals):
 1. \<And>ia c1 b1 c2 b2. \<lbrakk> ia \<lbrakk> c1 \<rbrakk> ~ b1 ; \<lbrakk>atom x \<sharp> c1; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c1 \<rbrakk> ~ b1 ;  ia \<lbrakk> c2 \<rbrakk> ~ b2 ; \<lbrakk>atom x \<sharp> c2; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c2 \<rbrakk> ~ b2 ; atom x \<sharp> (c1  IMP  c2 ); i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c1  IMP  c2  \<rbrakk> ~ b1 \<longrightarrow> b2
 2. \<And>ia c b. \<lbrakk> ia \<lbrakk> c \<rbrakk> ~ b ; \<lbrakk>atom x \<sharp> c; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c \<rbrakk> ~ b ; atom x \<sharp> (\<not> c ); i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> \<not> c  \<rbrakk> ~ \<not> b
 3. \<And>ia e1 sv1 e2 sv2. \<lbrakk>ia \<lbrakk> e1 \<rbrakk> ~ sv1 ; ia \<lbrakk> e2 \<rbrakk> ~ sv2 ; atom x \<sharp> (e1  ==  e2 ); i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> e1  ==  e2  \<rbrakk> ~ sv1 = sv2
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>ia c1 b1 c2 b2. \<lbrakk> ia \<lbrakk> c1 \<rbrakk> ~ b1 ; \<lbrakk>atom x \<sharp> c1; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c1 \<rbrakk> ~ b1 ;  ia \<lbrakk> c2 \<rbrakk> ~ b2 ; \<lbrakk>atom x \<sharp> c2; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c2 \<rbrakk> ~ b2 ; atom x \<sharp> (c1  IMP  c2 ); i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c1  IMP  c2  \<rbrakk> ~ b1 \<longrightarrow> b2
 2. \<And>ia c b. \<lbrakk> ia \<lbrakk> c \<rbrakk> ~ b ; \<lbrakk>atom x \<sharp> c; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c \<rbrakk> ~ b ; atom x \<sharp> (\<not> c ); i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> \<not> c  \<rbrakk> ~ \<not> b
 3. \<And>ia e1 sv1 e2 sv2. \<lbrakk>ia \<lbrakk> e1 \<rbrakk> ~ sv1 ; ia \<lbrakk> e2 \<rbrakk> ~ sv2 ; atom x \<sharp> (e1  ==  e2 ); i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> e1  ==  e2  \<rbrakk> ~ sv1 = sv2
[PROOF STEP]
case (eval_c_impI i c1 b1 c2 b2)
[PROOF STATE]
proof (state)
this:
 i \<lbrakk> c1 \<rbrakk> ~ b1
\<lbrakk>atom x \<sharp> c1; i = i(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c1 \<rbrakk> ~ b1
 i \<lbrakk> c2 \<rbrakk> ~ b2
\<lbrakk>atom x \<sharp> c2; i = i(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c2 \<rbrakk> ~ b2
atom x \<sharp> (c1  IMP  c2 )
i = i(x \<mapsto> s')

goal (3 subgoals):
 1. \<And>ia c1 b1 c2 b2. \<lbrakk> ia \<lbrakk> c1 \<rbrakk> ~ b1 ; \<lbrakk>atom x \<sharp> c1; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c1 \<rbrakk> ~ b1 ;  ia \<lbrakk> c2 \<rbrakk> ~ b2 ; \<lbrakk>atom x \<sharp> c2; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c2 \<rbrakk> ~ b2 ; atom x \<sharp> (c1  IMP  c2 ); i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c1  IMP  c2  \<rbrakk> ~ b1 \<longrightarrow> b2
 2. \<And>ia c b. \<lbrakk> ia \<lbrakk> c \<rbrakk> ~ b ; \<lbrakk>atom x \<sharp> c; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c \<rbrakk> ~ b ; atom x \<sharp> (\<not> c ); i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> \<not> c  \<rbrakk> ~ \<not> b
 3. \<And>ia e1 sv1 e2 sv2. \<lbrakk>ia \<lbrakk> e1 \<rbrakk> ~ sv1 ; ia \<lbrakk> e2 \<rbrakk> ~ sv2 ; atom x \<sharp> (e1  ==  e2 ); i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> e1  ==  e2  \<rbrakk> ~ sv1 = sv2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
 i \<lbrakk> c1 \<rbrakk> ~ b1
\<lbrakk>atom x \<sharp> c1; i = i(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c1 \<rbrakk> ~ b1
 i \<lbrakk> c2 \<rbrakk> ~ b2
\<lbrakk>atom x \<sharp> c2; i = i(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c2 \<rbrakk> ~ b2
atom x \<sharp> (c1  IMP  c2 )
i = i(x \<mapsto> s')
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
 i \<lbrakk> c1 \<rbrakk> ~ b1
\<lbrakk>atom x \<sharp> c1; i = i(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c1 \<rbrakk> ~ b1
 i \<lbrakk> c2 \<rbrakk> ~ b2
\<lbrakk>atom x \<sharp> c2; i = i(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c2 \<rbrakk> ~ b2
atom x \<sharp> (c1  IMP  c2 )
i = i(x \<mapsto> s')

goal (1 subgoal):
 1.  i \<lbrakk> c1  IMP  c2  \<rbrakk> ~ b1 \<longrightarrow> b2
[PROOF STEP]
using eval_c.intros
[PROOF STATE]
proof (prove)
using this:
 i \<lbrakk> c1 \<rbrakk> ~ b1
\<lbrakk>atom x \<sharp> c1; i = i(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c1 \<rbrakk> ~ b1
 i \<lbrakk> c2 \<rbrakk> ~ b2
\<lbrakk>atom x \<sharp> c2; i = i(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c2 \<rbrakk> ~ b2
atom x \<sharp> (c1  IMP  c2 )
i = i(x \<mapsto> s')
 ?i \<lbrakk> TRUE \<rbrakk> ~ True
 ?i \<lbrakk> FALSE \<rbrakk> ~ False
\<lbrakk> ?i \<lbrakk> ?c1.0 \<rbrakk> ~ ?b1.0 ;  ?i \<lbrakk> ?c2.0 \<rbrakk> ~ ?b2.0 \<rbrakk> \<Longrightarrow>  ?i \<lbrakk> ?c1.0  AND  ?c2.0  \<rbrakk> ~ ?b1.0 \<and> ?b2.0
\<lbrakk> ?i \<lbrakk> ?c1.0 \<rbrakk> ~ ?b1.0 ;  ?i \<lbrakk> ?c2.0 \<rbrakk> ~ ?b2.0 \<rbrakk> \<Longrightarrow>  ?i \<lbrakk> ?c1.0 OR ?c2.0  \<rbrakk> ~ ?b1.0 \<or> ?b2.0
\<lbrakk> ?i \<lbrakk> ?c1.0 \<rbrakk> ~ ?b1.0 ;  ?i \<lbrakk> ?c2.0 \<rbrakk> ~ ?b2.0 \<rbrakk> \<Longrightarrow>  ?i \<lbrakk> ?c1.0  IMP  ?c2.0  \<rbrakk> ~ ?b1.0 \<longrightarrow> ?b2.0
 ?i \<lbrakk> ?c \<rbrakk> ~ ?b  \<Longrightarrow>  ?i \<lbrakk> \<not> ?c  \<rbrakk> ~ \<not> ?b
\<lbrakk>?i \<lbrakk> ?e1.0 \<rbrakk> ~ ?sv1.0 ; ?i \<lbrakk> ?e2.0 \<rbrakk> ~ ?sv2.0 \<rbrakk> \<Longrightarrow>  ?i \<lbrakk> ?e1.0  ==  ?e2.0  \<rbrakk> ~ ?sv1.0 = ?sv2.0

goal (1 subgoal):
 1.  i \<lbrakk> c1  IMP  c2  \<rbrakk> ~ b1 \<longrightarrow> b2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
 i \<lbrakk> c1  IMP  c2  \<rbrakk> ~ b1 \<longrightarrow> b2

goal (2 subgoals):
 1. \<And>ia c b. \<lbrakk> ia \<lbrakk> c \<rbrakk> ~ b ; \<lbrakk>atom x \<sharp> c; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c \<rbrakk> ~ b ; atom x \<sharp> (\<not> c ); i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> \<not> c  \<rbrakk> ~ \<not> b
 2. \<And>ia e1 sv1 e2 sv2. \<lbrakk>ia \<lbrakk> e1 \<rbrakk> ~ sv1 ; ia \<lbrakk> e2 \<rbrakk> ~ sv2 ; atom x \<sharp> (e1  ==  e2 ); i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> e1  ==  e2  \<rbrakk> ~ sv1 = sv2
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>ia c b. \<lbrakk> ia \<lbrakk> c \<rbrakk> ~ b ; \<lbrakk>atom x \<sharp> c; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c \<rbrakk> ~ b ; atom x \<sharp> (\<not> c ); i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> \<not> c  \<rbrakk> ~ \<not> b
 2. \<And>ia e1 sv1 e2 sv2. \<lbrakk>ia \<lbrakk> e1 \<rbrakk> ~ sv1 ; ia \<lbrakk> e2 \<rbrakk> ~ sv2 ; atom x \<sharp> (e1  ==  e2 ); i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> e1  ==  e2  \<rbrakk> ~ sv1 = sv2
[PROOF STEP]
case (eval_c_notI i c b)
[PROOF STATE]
proof (state)
this:
 i \<lbrakk> c \<rbrakk> ~ b
\<lbrakk>atom x \<sharp> c; i = i(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c \<rbrakk> ~ b
atom x \<sharp> (\<not> c )
i = i(x \<mapsto> s')

goal (2 subgoals):
 1. \<And>ia c b. \<lbrakk> ia \<lbrakk> c \<rbrakk> ~ b ; \<lbrakk>atom x \<sharp> c; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c \<rbrakk> ~ b ; atom x \<sharp> (\<not> c ); i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> \<not> c  \<rbrakk> ~ \<not> b
 2. \<And>ia e1 sv1 e2 sv2. \<lbrakk>ia \<lbrakk> e1 \<rbrakk> ~ sv1 ; ia \<lbrakk> e2 \<rbrakk> ~ sv2 ; atom x \<sharp> (e1  ==  e2 ); i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> e1  ==  e2  \<rbrakk> ~ sv1 = sv2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
 i \<lbrakk> c \<rbrakk> ~ b
\<lbrakk>atom x \<sharp> c; i = i(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c \<rbrakk> ~ b
atom x \<sharp> (\<not> c )
i = i(x \<mapsto> s')
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
 i \<lbrakk> c \<rbrakk> ~ b
\<lbrakk>atom x \<sharp> c; i = i(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c \<rbrakk> ~ b
atom x \<sharp> (\<not> c )
i = i(x \<mapsto> s')

goal (1 subgoal):
 1.  i \<lbrakk> \<not> c  \<rbrakk> ~ \<not> b
[PROOF STEP]
using eval_c.intros
[PROOF STATE]
proof (prove)
using this:
 i \<lbrakk> c \<rbrakk> ~ b
\<lbrakk>atom x \<sharp> c; i = i(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> c \<rbrakk> ~ b
atom x \<sharp> (\<not> c )
i = i(x \<mapsto> s')
 ?i \<lbrakk> TRUE \<rbrakk> ~ True
 ?i \<lbrakk> FALSE \<rbrakk> ~ False
\<lbrakk> ?i \<lbrakk> ?c1.0 \<rbrakk> ~ ?b1.0 ;  ?i \<lbrakk> ?c2.0 \<rbrakk> ~ ?b2.0 \<rbrakk> \<Longrightarrow>  ?i \<lbrakk> ?c1.0  AND  ?c2.0  \<rbrakk> ~ ?b1.0 \<and> ?b2.0
\<lbrakk> ?i \<lbrakk> ?c1.0 \<rbrakk> ~ ?b1.0 ;  ?i \<lbrakk> ?c2.0 \<rbrakk> ~ ?b2.0 \<rbrakk> \<Longrightarrow>  ?i \<lbrakk> ?c1.0 OR ?c2.0  \<rbrakk> ~ ?b1.0 \<or> ?b2.0
\<lbrakk> ?i \<lbrakk> ?c1.0 \<rbrakk> ~ ?b1.0 ;  ?i \<lbrakk> ?c2.0 \<rbrakk> ~ ?b2.0 \<rbrakk> \<Longrightarrow>  ?i \<lbrakk> ?c1.0  IMP  ?c2.0  \<rbrakk> ~ ?b1.0 \<longrightarrow> ?b2.0
 ?i \<lbrakk> ?c \<rbrakk> ~ ?b  \<Longrightarrow>  ?i \<lbrakk> \<not> ?c  \<rbrakk> ~ \<not> ?b
\<lbrakk>?i \<lbrakk> ?e1.0 \<rbrakk> ~ ?sv1.0 ; ?i \<lbrakk> ?e2.0 \<rbrakk> ~ ?sv2.0 \<rbrakk> \<Longrightarrow>  ?i \<lbrakk> ?e1.0  ==  ?e2.0  \<rbrakk> ~ ?sv1.0 = ?sv2.0

goal (1 subgoal):
 1.  i \<lbrakk> \<not> c  \<rbrakk> ~ \<not> b
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
 i \<lbrakk> \<not> c  \<rbrakk> ~ \<not> b

goal (1 subgoal):
 1. \<And>ia e1 sv1 e2 sv2. \<lbrakk>ia \<lbrakk> e1 \<rbrakk> ~ sv1 ; ia \<lbrakk> e2 \<rbrakk> ~ sv2 ; atom x \<sharp> (e1  ==  e2 ); i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> e1  ==  e2  \<rbrakk> ~ sv1 = sv2
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>ia e1 sv1 e2 sv2. \<lbrakk>ia \<lbrakk> e1 \<rbrakk> ~ sv1 ; ia \<lbrakk> e2 \<rbrakk> ~ sv2 ; atom x \<sharp> (e1  ==  e2 ); i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> e1  ==  e2  \<rbrakk> ~ sv1 = sv2
[PROOF STEP]
case (eval_c_eqI i e1 sv1 e2 sv2)
[PROOF STATE]
proof (state)
this:
i \<lbrakk> e1 \<rbrakk> ~ sv1
i \<lbrakk> e2 \<rbrakk> ~ sv2
atom x \<sharp> (e1  ==  e2 )
i = i(x \<mapsto> s')

goal (1 subgoal):
 1. \<And>ia e1 sv1 e2 sv2. \<lbrakk>ia \<lbrakk> e1 \<rbrakk> ~ sv1 ; ia \<lbrakk> e2 \<rbrakk> ~ sv2 ; atom x \<sharp> (e1  ==  e2 ); i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow>  i \<lbrakk> e1  ==  e2  \<rbrakk> ~ sv1 = sv2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i \<lbrakk> e1 \<rbrakk> ~ sv1
i \<lbrakk> e2 \<rbrakk> ~ sv2
atom x \<sharp> (e1  ==  e2 )
i = i(x \<mapsto> s')
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> e1 \<rbrakk> ~ sv1
i \<lbrakk> e2 \<rbrakk> ~ sv2
atom x \<sharp> (e1  ==  e2 )
i = i(x \<mapsto> s')

goal (1 subgoal):
 1.  i \<lbrakk> e1  ==  e2  \<rbrakk> ~ sv1 = sv2
[PROOF STEP]
using eval_e_weakening_x c.fresh eval_c.intros
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> e1 \<rbrakk> ~ sv1
i \<lbrakk> e2 \<rbrakk> ~ sv2
atom x \<sharp> (e1  ==  e2 )
i = i(x \<mapsto> s')
\<lbrakk>?i' \<lbrakk> ?c \<rbrakk> ~ ?s ; atom ?x \<sharp> ?c; ?i = ?i'(?x \<mapsto> ?s')\<rbrakk> \<Longrightarrow> ?i \<lbrakk> ?c \<rbrakk> ~ ?s
?a \<sharp> (TRUE)
?a \<sharp> (FALSE)
?a \<sharp> (?c1.0  AND  ?c2.0 ) = (?a \<sharp> ?c1.0 \<and> ?a \<sharp> ?c2.0)
?a \<sharp> (?c1.0 OR ?c2.0 ) = (?a \<sharp> ?c1.0 \<and> ?a \<sharp> ?c2.0)
?a \<sharp> (\<not> ?c ) = ?a \<sharp> ?c
?a \<sharp> (?c1.0  IMP  ?c2.0 ) = (?a \<sharp> ?c1.0 \<and> ?a \<sharp> ?c2.0)
?a \<sharp> (?ce1.0  ==  ?ce2.0 ) = (?a \<sharp> ?ce1.0 \<and> ?a \<sharp> ?ce2.0)
 ?i \<lbrakk> TRUE \<rbrakk> ~ True
 ?i \<lbrakk> FALSE \<rbrakk> ~ False
\<lbrakk> ?i \<lbrakk> ?c1.0 \<rbrakk> ~ ?b1.0 ;  ?i \<lbrakk> ?c2.0 \<rbrakk> ~ ?b2.0 \<rbrakk> \<Longrightarrow>  ?i \<lbrakk> ?c1.0  AND  ?c2.0  \<rbrakk> ~ ?b1.0 \<and> ?b2.0
\<lbrakk> ?i \<lbrakk> ?c1.0 \<rbrakk> ~ ?b1.0 ;  ?i \<lbrakk> ?c2.0 \<rbrakk> ~ ?b2.0 \<rbrakk> \<Longrightarrow>  ?i \<lbrakk> ?c1.0 OR ?c2.0  \<rbrakk> ~ ?b1.0 \<or> ?b2.0
\<lbrakk> ?i \<lbrakk> ?c1.0 \<rbrakk> ~ ?b1.0 ;  ?i \<lbrakk> ?c2.0 \<rbrakk> ~ ?b2.0 \<rbrakk> \<Longrightarrow>  ?i \<lbrakk> ?c1.0  IMP  ?c2.0  \<rbrakk> ~ ?b1.0 \<longrightarrow> ?b2.0
 ?i \<lbrakk> ?c \<rbrakk> ~ ?b  \<Longrightarrow>  ?i \<lbrakk> \<not> ?c  \<rbrakk> ~ \<not> ?b
\<lbrakk>?i \<lbrakk> ?e1.0 \<rbrakk> ~ ?sv1.0 ; ?i \<lbrakk> ?e2.0 \<rbrakk> ~ ?sv2.0 \<rbrakk> \<Longrightarrow>  ?i \<lbrakk> ?e1.0  ==  ?e2.0  \<rbrakk> ~ ?sv1.0 = ?sv2.0

goal (1 subgoal):
 1.  i \<lbrakk> e1  ==  e2  \<rbrakk> ~ sv1 = sv2
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
 i \<lbrakk> e1  ==  e2  \<rbrakk> ~ sv1 = sv2

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma is_satis_weakening_x:
  fixes c::c
  assumes "i' \<Turnstile> c" and "atom x \<sharp> c" and "i = i' (x \<mapsto> s)"
  shows "i \<Turnstile> c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  i \<Turnstile> c
[PROOF STEP]
using eval_c_weakening_x assms is_satis.simps
[PROOF STATE]
proof (prove)
using this:
\<lbrakk> ?i' \<lbrakk> ?c \<rbrakk> ~ ?s ; atom ?x \<sharp> ?c; ?i = ?i'(?x \<mapsto> ?s')\<rbrakk> \<Longrightarrow>  ?i \<lbrakk> ?c \<rbrakk> ~ ?s
 i' \<Turnstile> c
atom x \<sharp> c
i = i'(x \<mapsto> s)
 ?a1.0 \<Turnstile> ?a2.0  = (\<exists>i c. ?a1.0 = i \<and> ?a2.0 = c \<and>  i \<lbrakk> c \<rbrakk> ~ True )

goal (1 subgoal):
 1.  i \<Turnstile> c
[PROOF STEP]
by simp


[STATEMENT]
lemma is_satis_g_weakening_x:
  fixes G::\<Gamma>
  assumes "i' \<Turnstile> G" and "atom x \<sharp> G" and "i = i' (x \<mapsto> s)"
  shows "i \<Turnstile> G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  i \<Turnstile> G
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
 i' \<Turnstile> G
atom x \<sharp> G
i = i'(x \<mapsto> s)

goal (1 subgoal):
 1.  i \<Turnstile> G
[PROOF STEP]
proof(induct G rule: \<Gamma>_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk> i' \<Turnstile> GNil ; atom x \<sharp> GNil; i = i'(x \<mapsto> s)\<rbrakk> \<Longrightarrow>  i \<Turnstile> GNil
 2. \<And>xa b c \<Gamma>'. \<lbrakk>\<lbrakk> i' \<Turnstile> \<Gamma>' ; atom x \<sharp> \<Gamma>'; i = i'(x \<mapsto> s)\<rbrakk> \<Longrightarrow>  i \<Turnstile> \<Gamma>' ;  i' \<Turnstile> (xa, b, c) #\<^sub>\<Gamma> \<Gamma>' ; atom x \<sharp> (xa, b, c) #\<^sub>\<Gamma> \<Gamma>'; i = i'(x \<mapsto> s)\<rbrakk> \<Longrightarrow>  i \<Turnstile> (xa, b, c) #\<^sub>\<Gamma> \<Gamma>'
[PROOF STEP]
case GNil
[PROOF STATE]
proof (state)
this:
 i' \<Turnstile> GNil
atom x \<sharp> GNil
i = i'(x \<mapsto> s)

goal (2 subgoals):
 1. \<lbrakk> i' \<Turnstile> GNil ; atom x \<sharp> GNil; i = i'(x \<mapsto> s)\<rbrakk> \<Longrightarrow>  i \<Turnstile> GNil
 2. \<And>xa b c \<Gamma>'. \<lbrakk>\<lbrakk> i' \<Turnstile> \<Gamma>' ; atom x \<sharp> \<Gamma>'; i = i'(x \<mapsto> s)\<rbrakk> \<Longrightarrow>  i \<Turnstile> \<Gamma>' ;  i' \<Turnstile> (xa, b, c) #\<^sub>\<Gamma> \<Gamma>' ; atom x \<sharp> (xa, b, c) #\<^sub>\<Gamma> \<Gamma>'; i = i'(x \<mapsto> s)\<rbrakk> \<Longrightarrow>  i \<Turnstile> (xa, b, c) #\<^sub>\<Gamma> \<Gamma>'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
 i' \<Turnstile> GNil
atom x \<sharp> GNil
i = i'(x \<mapsto> s)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
 i' \<Turnstile> GNil
atom x \<sharp> GNil
i = i'(x \<mapsto> s)

goal (1 subgoal):
 1.  i \<Turnstile> GNil
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
 i \<Turnstile> GNil

goal (1 subgoal):
 1. \<And>xa b c \<Gamma>'. \<lbrakk>\<lbrakk> i' \<Turnstile> \<Gamma>' ; atom x \<sharp> \<Gamma>'; i = i'(x \<mapsto> s)\<rbrakk> \<Longrightarrow>  i \<Turnstile> \<Gamma>' ;  i' \<Turnstile> (xa, b, c) #\<^sub>\<Gamma> \<Gamma>' ; atom x \<sharp> (xa, b, c) #\<^sub>\<Gamma> \<Gamma>'; i = i'(x \<mapsto> s)\<rbrakk> \<Longrightarrow>  i \<Turnstile> (xa, b, c) #\<^sub>\<Gamma> \<Gamma>'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa b c \<Gamma>'. \<lbrakk>\<lbrakk> i' \<Turnstile> \<Gamma>' ; atom x \<sharp> \<Gamma>'; i = i'(x \<mapsto> s)\<rbrakk> \<Longrightarrow>  i \<Turnstile> \<Gamma>' ;  i' \<Turnstile> (xa, b, c) #\<^sub>\<Gamma> \<Gamma>' ; atom x \<sharp> (xa, b, c) #\<^sub>\<Gamma> \<Gamma>'; i = i'(x \<mapsto> s)\<rbrakk> \<Longrightarrow>  i \<Turnstile> (xa, b, c) #\<^sub>\<Gamma> \<Gamma>'
[PROOF STEP]
case (GCons x' b' c' \<Gamma>')
[PROOF STATE]
proof (state)
this:
\<lbrakk> i' \<Turnstile> \<Gamma>' ; atom x \<sharp> \<Gamma>'; i = i'(x \<mapsto> s)\<rbrakk> \<Longrightarrow>  i \<Turnstile> \<Gamma>'
 i' \<Turnstile> (x', b', c') #\<^sub>\<Gamma> \<Gamma>'
atom x \<sharp> (x', b', c') #\<^sub>\<Gamma> \<Gamma>'
i = i'(x \<mapsto> s)

goal (1 subgoal):
 1. \<And>xa b c \<Gamma>'. \<lbrakk>\<lbrakk> i' \<Turnstile> \<Gamma>' ; atom x \<sharp> \<Gamma>'; i = i'(x \<mapsto> s)\<rbrakk> \<Longrightarrow>  i \<Turnstile> \<Gamma>' ;  i' \<Turnstile> (xa, b, c) #\<^sub>\<Gamma> \<Gamma>' ; atom x \<sharp> (xa, b, c) #\<^sub>\<Gamma> \<Gamma>'; i = i'(x \<mapsto> s)\<rbrakk> \<Longrightarrow>  i \<Turnstile> (xa, b, c) #\<^sub>\<Gamma> \<Gamma>'
[PROOF STEP]
hence "atom x \<sharp> c'"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk> i' \<Turnstile> \<Gamma>' ; atom x \<sharp> \<Gamma>'; i = i'(x \<mapsto> s)\<rbrakk> \<Longrightarrow>  i \<Turnstile> \<Gamma>'
 i' \<Turnstile> (x', b', c') #\<^sub>\<Gamma> \<Gamma>'
atom x \<sharp> (x', b', c') #\<^sub>\<Gamma> \<Gamma>'
i = i'(x \<mapsto> s)

goal (1 subgoal):
 1. atom x \<sharp> c'
[PROOF STEP]
using fresh_GCons fresh_prodN
[PROOF STATE]
proof (prove)
using this:
\<lbrakk> i' \<Turnstile> \<Gamma>' ; atom x \<sharp> \<Gamma>'; i = i'(x \<mapsto> s)\<rbrakk> \<Longrightarrow>  i \<Turnstile> \<Gamma>'
 i' \<Turnstile> (x', b', c') #\<^sub>\<Gamma> \<Gamma>'
atom x \<sharp> (x', b', c') #\<^sub>\<Gamma> \<Gamma>'
i = i'(x \<mapsto> s)
?a \<sharp> ?x #\<^sub>\<Gamma> ?xs = (?a \<sharp> ?x \<and> ?a \<sharp> ?xs)
?a \<sharp> (?x, ?y) = (?a \<sharp> ?x \<and> ?a \<sharp> ?y)
?x \<sharp> (?a, ?b, ?c) = (?x \<sharp> ?a \<and> ?x \<sharp> ?b \<and> ?x \<sharp> ?c)
?x \<sharp> (?a, ?b, ?c, ?d) = (?x \<sharp> ?a \<and> ?x \<sharp> ?b \<and> ?x \<sharp> ?c \<and> ?x \<sharp> ?d)
?x \<sharp> (?a, ?b, ?c, ?d, ?e) = (?x \<sharp> ?a \<and> ?x \<sharp> ?b \<and> ?x \<sharp> ?c \<and> ?x \<sharp> ?d \<and> ?x \<sharp> ?e)
?x \<sharp> (?a, ?b, ?c, ?d, ?e, ?f) = (?x \<sharp> ?a \<and> ?x \<sharp> ?b \<and> ?x \<sharp> ?c \<and> ?x \<sharp> ?d \<and> ?x \<sharp> ?e \<and> ?x \<sharp> ?f)
?x \<sharp> (?a, ?b, ?c, ?d, ?e, ?f, ?g) = (?x \<sharp> ?a \<and> ?x \<sharp> ?b \<and> ?x \<sharp> ?c \<and> ?x \<sharp> ?d \<and> ?x \<sharp> ?e \<and> ?x \<sharp> ?f \<and> ?x \<sharp> ?g)
?x \<sharp> (?a, ?b, ?c, ?d, ?e, ?f, ?g, ?h) = (?x \<sharp> ?a \<and> ?x \<sharp> ?b \<and> ?x \<sharp> ?c \<and> ?x \<sharp> ?d \<and> ?x \<sharp> ?e \<and> ?x \<sharp> ?f \<and> ?x \<sharp> ?g \<and> ?x \<sharp> ?h)
?x \<sharp> (?a, ?b, ?c, ?d, ?e, ?f, ?g, ?h, ?i) = (?x \<sharp> ?a \<and> ?x \<sharp> ?b \<and> ?x \<sharp> ?c \<and> ?x \<sharp> ?d \<and> ?x \<sharp> ?e \<and> ?x \<sharp> ?f \<and> ?x \<sharp> ?g \<and> ?x \<sharp> ?h \<and> ?x \<sharp> ?i)
?x \<sharp> (?a, ?b, ?c, ?d, ?e, ?f, ?g, ?h, ?i, ?j) = (?x \<sharp> ?a \<and> ?x \<sharp> ?b \<and> ?x \<sharp> ?c \<and> ?x \<sharp> ?d \<and> ?x \<sharp> ?e \<and> ?x \<sharp> ?f \<and> ?x \<sharp> ?g \<and> ?x \<sharp> ?h \<and> ?x \<sharp> ?i \<and> ?x \<sharp> ?j)
?x \<sharp> (?a, ?b, ?c, ?d, ?e, ?f, ?g, ?h, ?i, ?j, ?k, ?l) = (?x \<sharp> ?a \<and> ?x \<sharp> ?b \<and> ?x \<sharp> ?c \<and> ?x \<sharp> ?d \<and> ?x \<sharp> ?e \<and> ?x \<sharp> ?f \<and> ?x \<sharp> ?g \<and> ?x \<sharp> ?h \<and> ?x \<sharp> ?i \<and> ?x \<sharp> ?j \<and> ?x \<sharp> ?k \<and> ?x \<sharp> ?l)

goal (1 subgoal):
 1. atom x \<sharp> c'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
atom x \<sharp> c'

goal (1 subgoal):
 1. \<And>xa b c \<Gamma>'. \<lbrakk>\<lbrakk> i' \<Turnstile> \<Gamma>' ; atom x \<sharp> \<Gamma>'; i = i'(x \<mapsto> s)\<rbrakk> \<Longrightarrow>  i \<Turnstile> \<Gamma>' ;  i' \<Turnstile> (xa, b, c) #\<^sub>\<Gamma> \<Gamma>' ; atom x \<sharp> (xa, b, c) #\<^sub>\<Gamma> \<Gamma>'; i = i'(x \<mapsto> s)\<rbrakk> \<Longrightarrow>  i \<Turnstile> (xa, b, c) #\<^sub>\<Gamma> \<Gamma>'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
atom x \<sharp> c'

goal (1 subgoal):
 1. \<And>xa b c \<Gamma>'. \<lbrakk>\<lbrakk> i' \<Turnstile> \<Gamma>' ; atom x \<sharp> \<Gamma>'; i = i'(x \<mapsto> s)\<rbrakk> \<Longrightarrow>  i \<Turnstile> \<Gamma>' ;  i' \<Turnstile> (xa, b, c) #\<^sub>\<Gamma> \<Gamma>' ; atom x \<sharp> (xa, b, c) #\<^sub>\<Gamma> \<Gamma>'; i = i'(x \<mapsto> s)\<rbrakk> \<Longrightarrow>  i \<Turnstile> (xa, b, c) #\<^sub>\<Gamma> \<Gamma>'
[PROOF STEP]
hence "i \<Turnstile> c'"
[PROOF STATE]
proof (prove)
using this:
atom x \<sharp> c'

goal (1 subgoal):
 1.  i \<Turnstile> c'
[PROOF STEP]
using is_satis_weakening_x  is_satis_g.simps(2) GCons
[PROOF STATE]
proof (prove)
using this:
atom x \<sharp> c'
\<lbrakk> ?i' \<Turnstile> ?c ; atom ?x \<sharp> ?c; ?i = ?i'(?x \<mapsto> ?s)\<rbrakk> \<Longrightarrow>  ?i \<Turnstile> ?c
 ?i \<Turnstile> (?x, ?b, ?c) #\<^sub>\<Gamma> ?G  = ( ?i \<Turnstile> ?c  \<and>  ?i \<Turnstile> ?G )
\<lbrakk> i' \<Turnstile> \<Gamma>' ; atom x \<sharp> \<Gamma>'; i = i'(x \<mapsto> s)\<rbrakk> \<Longrightarrow>  i \<Turnstile> \<Gamma>'
 i' \<Turnstile> (x', b', c') #\<^sub>\<Gamma> \<Gamma>'
atom x \<sharp> (x', b', c') #\<^sub>\<Gamma> \<Gamma>'
i = i'(x \<mapsto> s)

goal (1 subgoal):
 1.  i \<Turnstile> c'
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
 i \<Turnstile> c'

goal (1 subgoal):
 1. \<And>xa b c \<Gamma>'. \<lbrakk>\<lbrakk> i' \<Turnstile> \<Gamma>' ; atom x \<sharp> \<Gamma>'; i = i'(x \<mapsto> s)\<rbrakk> \<Longrightarrow>  i \<Turnstile> \<Gamma>' ;  i' \<Turnstile> (xa, b, c) #\<^sub>\<Gamma> \<Gamma>' ; atom x \<sharp> (xa, b, c) #\<^sub>\<Gamma> \<Gamma>'; i = i'(x \<mapsto> s)\<rbrakk> \<Longrightarrow>  i \<Turnstile> (xa, b, c) #\<^sub>\<Gamma> \<Gamma>'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
 i \<Turnstile> c'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
 i \<Turnstile> c'

goal (1 subgoal):
 1.  i \<Turnstile> (x', b', c') #\<^sub>\<Gamma> \<Gamma>'
[PROOF STEP]
using   is_satis_g.simps(2)[of i x' b' c' \<Gamma>'] GCons fresh_GCons
[PROOF STATE]
proof (prove)
using this:
 i \<Turnstile> c'
 i \<Turnstile> (x', b', c') #\<^sub>\<Gamma> \<Gamma>'  = ( i \<Turnstile> c'  \<and>  i \<Turnstile> \<Gamma>' )
\<lbrakk> i' \<Turnstile> \<Gamma>' ; atom x \<sharp> \<Gamma>'; i = i'(x \<mapsto> s)\<rbrakk> \<Longrightarrow>  i \<Turnstile> \<Gamma>'
 i' \<Turnstile> (x', b', c') #\<^sub>\<Gamma> \<Gamma>'
atom x \<sharp> (x', b', c') #\<^sub>\<Gamma> \<Gamma>'
i = i'(x \<mapsto> s)
?a \<sharp> ?x #\<^sub>\<Gamma> ?xs = (?a \<sharp> ?x \<and> ?a \<sharp> ?xs)

goal (1 subgoal):
 1.  i \<Turnstile> (x', b', c') #\<^sub>\<Gamma> \<Gamma>'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
 i \<Turnstile> (x', b', c') #\<^sub>\<Gamma> \<Gamma>'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma subst_b_var:
  assumes  "B_var bv2 = b[bv::=b']\<^sub>b\<^sub>b"
  shows  "(b = B_var bv \<and> b' = B_var bv2) \<or> (b=B_var bv2 \<and> bv \<noteq> bv2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b = B_var bv \<and> b' = B_var bv2 \<or> b = B_var bv2 \<and> bv \<noteq> bv2
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
B_var bv2 = b[bv::=b']\<^sub>b\<^sub>b

goal (1 subgoal):
 1. b = B_var bv \<and> b' = B_var bv2 \<or> b = B_var bv2 \<and> bv \<noteq> bv2
[PROOF STEP]
by(nominal_induct b rule: b.strong_induct,auto+)


[STATEMENT]
lemma wfRCV_poly_elims:
  fixes tm::"'a::fs" and b::b
  assumes "T  \<turnstile> SConsp typid dc bdc s : b"
  obtains bva dclist x1 b1 c1 where "b = B_app typid bdc \<and>
    AF_typedef_poly typid bva dclist \<in> set T \<and> (dc, \<lbrace> x1 : b1  | c1 \<rbrace>) \<in> set dclist \<and>  T  \<turnstile> s : b1[bva::=bdc]\<^sub>b\<^sub>b \<and> atom bva \<sharp> tm"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>bva dclist x1 b1 c1. b = B_app typid bdc \<and> AF_typedef_poly typid bva dclist \<in> set T \<and> (dc, \<lbrace> x1 : b1  | c1 \<rbrace>) \<in> set dclist \<and>  T  \<turnstile> s : b1[bva::=bdc]\<^sub>b\<^sub>b \<and> atom bva \<sharp> tm \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
 T  \<turnstile> SConsp typid dc bdc s : b

goal (1 subgoal):
 1. (\<And>bva dclist x1 b1 c1. b = B_app typid bdc \<and> AF_typedef_poly typid bva dclist \<in> set T \<and> (dc, \<lbrace> x1 : b1  | c1 \<rbrace>) \<in> set dclist \<and>  T  \<turnstile> s : b1[bva::=bdc]\<^sub>b\<^sub>b \<and> atom bva \<sharp> tm \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof(nominal_induct "SConsp typid dc bdc s" b avoiding: tm rule:wfRCV.strong_induct)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>bv dclist \<Theta> x b c tm. \<lbrakk>atom bv \<sharp> tm; AF_typedef_poly typid bv dclist \<in> set \<Theta>; (dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist; atom bv \<sharp> \<Theta>; atom bv \<sharp> SConsp typid dc bdc s; atom bv \<sharp> B_app typid bdc;  \<Theta>  \<turnstile> s : b[bv::=bdc]\<^sub>b\<^sub>b; \<And>ba. \<lbrakk>s = SConsp typid dc bdc s; \<And>bva dclist x1 b1 c1. b[bv::=bdc]\<^sub>b\<^sub>b = B_app typid bdc \<and> AF_typedef_poly typid bva dclist \<in> set \<Theta> \<and> (dc, \<lbrace> x1 : b1  | c1 \<rbrace>) \<in> set dclist \<and>  \<Theta>  \<turnstile> s : b1[bva::=bdc]\<^sub>b\<^sub>b \<and> atom bva \<sharp> ba \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis; \<And>bva dclist x1 b1 c1. B_app typid bdc = B_app typid bdc \<and> AF_typedef_poly typid bva dclist \<in> set \<Theta> \<and> (dc, \<lbrace> x1 : b1  | c1 \<rbrace>) \<in> set dclist \<and>  \<Theta>  \<turnstile> s : b1[bva::=bdc]\<^sub>b\<^sub>b \<and> atom bva \<sharp> tm \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
case (wfRCV_BConsPI bv dclist \<Theta> x b c)
[PROOF STATE]
proof (state)
this:
atom bv \<sharp> tm
AF_typedef_poly typid bv dclist \<in> set \<Theta>
(dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist
atom bv \<sharp> \<Theta>
atom bv \<sharp> SConsp typid dc bdc s
atom bv \<sharp> B_app typid bdc
 \<Theta>  \<turnstile> s : b[bv::=bdc]\<^sub>b\<^sub>b
\<lbrakk>s = SConsp typid dc bdc s; \<And>bva dclist x1 b1 c1. b[bv::=bdc]\<^sub>b\<^sub>b = B_app typid bdc \<and> AF_typedef_poly typid bva dclist \<in> set \<Theta> \<and> (dc, \<lbrace> x1 : b1  | c1 \<rbrace>) \<in> set dclist \<and>  \<Theta>  \<turnstile> s : b1[bva::=bdc]\<^sub>b\<^sub>b \<and> atom bva \<sharp> ?b \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
B_app typid bdc = B_app typid bdc \<and> AF_typedef_poly typid ?bva ?dclist \<in> set \<Theta> \<and> (dc, \<lbrace> ?x1.0 : ?b1.0  | ?c1.0 \<rbrace>) \<in> set ?dclist \<and>  \<Theta>  \<turnstile> s : ?b1.0[?bva::=bdc]\<^sub>b\<^sub>b \<and> atom ?bva \<sharp> tm \<Longrightarrow> thesis

goal (1 subgoal):
 1. \<And>bv dclist \<Theta> x b c tm. \<lbrakk>atom bv \<sharp> tm; AF_typedef_poly typid bv dclist \<in> set \<Theta>; (dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist; atom bv \<sharp> \<Theta>; atom bv \<sharp> SConsp typid dc bdc s; atom bv \<sharp> B_app typid bdc;  \<Theta>  \<turnstile> s : b[bv::=bdc]\<^sub>b\<^sub>b; \<And>ba. \<lbrakk>s = SConsp typid dc bdc s; \<And>bva dclist x1 b1 c1. b[bv::=bdc]\<^sub>b\<^sub>b = B_app typid bdc \<and> AF_typedef_poly typid bva dclist \<in> set \<Theta> \<and> (dc, \<lbrace> x1 : b1  | c1 \<rbrace>) \<in> set dclist \<and>  \<Theta>  \<turnstile> s : b1[bva::=bdc]\<^sub>b\<^sub>b \<and> atom bva \<sharp> ba \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis; \<And>bva dclist x1 b1 c1. B_app typid bdc = B_app typid bdc \<and> AF_typedef_poly typid bva dclist \<in> set \<Theta> \<and> (dc, \<lbrace> x1 : b1  | c1 \<rbrace>) \<in> set dclist \<and>  \<Theta>  \<turnstile> s : b1[bva::=bdc]\<^sub>b\<^sub>b \<and> atom bva \<sharp> tm \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
atom bv \<sharp> tm
AF_typedef_poly typid bv dclist \<in> set \<Theta>
(dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist
atom bv \<sharp> \<Theta>
atom bv \<sharp> SConsp typid dc bdc s
atom bv \<sharp> B_app typid bdc
 \<Theta>  \<turnstile> s : b[bv::=bdc]\<^sub>b\<^sub>b
\<lbrakk>s = SConsp typid dc bdc s; \<And>bva dclist x1 b1 c1. b[bv::=bdc]\<^sub>b\<^sub>b = B_app typid bdc \<and> AF_typedef_poly typid bva dclist \<in> set \<Theta> \<and> (dc, \<lbrace> x1 : b1  | c1 \<rbrace>) \<in> set dclist \<and>  \<Theta>  \<turnstile> s : b1[bva::=bdc]\<^sub>b\<^sub>b \<and> atom bva \<sharp> ?b \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
B_app typid bdc = B_app typid bdc \<and> AF_typedef_poly typid ?bva ?dclist \<in> set \<Theta> \<and> (dc, \<lbrace> ?x1.0 : ?b1.0  | ?c1.0 \<rbrace>) \<in> set ?dclist \<and>  \<Theta>  \<turnstile> s : ?b1.0[?bva::=bdc]\<^sub>b\<^sub>b \<and> atom ?bva \<sharp> tm \<Longrightarrow> thesis
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
atom bv \<sharp> tm
AF_typedef_poly typid bv dclist \<in> set \<Theta>
(dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist
atom bv \<sharp> \<Theta>
atom bv \<sharp> SConsp typid dc bdc s
atom bv \<sharp> B_app typid bdc
 \<Theta>  \<turnstile> s : b[bv::=bdc]\<^sub>b\<^sub>b
\<lbrakk>s = SConsp typid dc bdc s; \<And>bva dclist x1 b1 c1. b[bv::=bdc]\<^sub>b\<^sub>b = B_app typid bdc \<and> AF_typedef_poly typid bva dclist \<in> set \<Theta> \<and> (dc, \<lbrace> x1 : b1  | c1 \<rbrace>) \<in> set dclist \<and>  \<Theta>  \<turnstile> s : b1[bva::=bdc]\<^sub>b\<^sub>b \<and> atom bva \<sharp> ?b \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
B_app typid bdc = B_app typid bdc \<and> AF_typedef_poly typid ?bva ?dclist \<in> set \<Theta> \<and> (dc, \<lbrace> ?x1.0 : ?b1.0  | ?c1.0 \<rbrace>) \<in> set ?dclist \<and>  \<Theta>  \<turnstile> s : ?b1.0[?bva::=bdc]\<^sub>b\<^sub>b \<and> atom ?bva \<sharp> tm \<Longrightarrow> thesis

goal (1 subgoal):
 1. thesis
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed