[STATEMENT]
lemma eval_c_exist:
  fixes \<Gamma>::\<Gamma> and c::c
  assumes "P ; \<Gamma>  \<turnstile> i" and "P ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f c"
  shows "\<exists>s. i \<lbrakk> c \<rbrakk> ~ s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>s.  i \<lbrakk> c \<rbrakk> ~ s
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
 P ; \<Gamma> \<turnstile> i
 P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f c

goal (1 subgoal):
 1. \<exists>s.  i \<lbrakk> c \<rbrakk> ~ s
[PROOF STEP]
proof(nominal_induct c  rule: c.strong_induct)
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f TRUE \<rbrakk> \<Longrightarrow> Ex (eval_c i (TRUE))
 2. \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f FALSE \<rbrakk> \<Longrightarrow> Ex (eval_c i (FALSE))
 3. \<And>x1 x2. \<lbrakk>\<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1 \<rbrakk> \<Longrightarrow> Ex (eval_c i x1); \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x2 \<rbrakk> \<Longrightarrow> Ex (eval_c i x2);  P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1  AND  x2  \<rbrakk> \<Longrightarrow> Ex (eval_c i (x1  AND  x2 ))
 4. \<And>x1 x2. \<lbrakk>\<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1 \<rbrakk> \<Longrightarrow> Ex (eval_c i x1); \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x2 \<rbrakk> \<Longrightarrow> Ex (eval_c i x2);  P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1 OR x2  \<rbrakk> \<Longrightarrow> Ex (eval_c i (x1 OR x2 ))
 5. \<And>x. \<lbrakk>\<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x \<rbrakk> \<Longrightarrow> Ex (eval_c i x);  P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f \<not> x  \<rbrakk> \<Longrightarrow> Ex (eval_c i (\<not> x ))
 6. \<And>x1 x2. \<lbrakk>\<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1 \<rbrakk> \<Longrightarrow> Ex (eval_c i x1); \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x2 \<rbrakk> \<Longrightarrow> Ex (eval_c i x2);  P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1  IMP  x2  \<rbrakk> \<Longrightarrow> Ex (eval_c i (x1  IMP  x2 ))
 7. \<And>x1 x2. \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1  ==  x2  \<rbrakk> \<Longrightarrow> Ex (eval_c i (x1  ==  x2 ))
[PROOF STEP]
case C_true
[PROOF STATE]
proof (state)
this:
 P ; \<Gamma> \<turnstile> i
 P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f TRUE

goal (7 subgoals):
 1. \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f TRUE \<rbrakk> \<Longrightarrow> Ex (eval_c i (TRUE))
 2. \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f FALSE \<rbrakk> \<Longrightarrow> Ex (eval_c i (FALSE))
 3. \<And>x1 x2. \<lbrakk>\<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1 \<rbrakk> \<Longrightarrow> Ex (eval_c i x1); \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x2 \<rbrakk> \<Longrightarrow> Ex (eval_c i x2);  P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1  AND  x2  \<rbrakk> \<Longrightarrow> Ex (eval_c i (x1  AND  x2 ))
 4. \<And>x1 x2. \<lbrakk>\<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1 \<rbrakk> \<Longrightarrow> Ex (eval_c i x1); \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x2 \<rbrakk> \<Longrightarrow> Ex (eval_c i x2);  P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1 OR x2  \<rbrakk> \<Longrightarrow> Ex (eval_c i (x1 OR x2 ))
 5. \<And>x. \<lbrakk>\<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x \<rbrakk> \<Longrightarrow> Ex (eval_c i x);  P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f \<not> x  \<rbrakk> \<Longrightarrow> Ex (eval_c i (\<not> x ))
 6. \<And>x1 x2. \<lbrakk>\<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1 \<rbrakk> \<Longrightarrow> Ex (eval_c i x1); \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x2 \<rbrakk> \<Longrightarrow> Ex (eval_c i x2);  P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1  IMP  x2  \<rbrakk> \<Longrightarrow> Ex (eval_c i (x1  IMP  x2 ))
 7. \<And>x1 x2. \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1  ==  x2  \<rbrakk> \<Longrightarrow> Ex (eval_c i (x1  ==  x2 ))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
 P ; \<Gamma> \<turnstile> i
 P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f TRUE
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
 P ; \<Gamma> \<turnstile> i
 P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f TRUE

goal (1 subgoal):
 1. \<exists>a.  i \<lbrakk> TRUE \<rbrakk> ~ a
[PROOF STEP]
using eval_c.intros wfC_elims
[PROOF STATE]
proof (prove)
using this:
 P ; \<Gamma> \<turnstile> i
 P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f TRUE
 ?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
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f TRUE ;  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma>  \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f FALSE ;  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma>  \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?e1.0  ==  ?e2.0  ; \<And>b. \<lbrakk>  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?e1.0 : b ;   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?e2.0 : b \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c1.0  AND  ?c2.0  ; \<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c1.0 ;  ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c2.0 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c1.0 OR ?c2.0  ; \<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c1.0 ;  ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c2.0 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f \<not> ?c1.0  ;  ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c1.0  \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c1.0  IMP  ?c2.0  ; \<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c1.0 ;  ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c2.0 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

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

goal (6 subgoals):
 1. \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f FALSE \<rbrakk> \<Longrightarrow> Ex (eval_c i (FALSE))
 2. \<And>x1 x2. \<lbrakk>\<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1 \<rbrakk> \<Longrightarrow> Ex (eval_c i x1); \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x2 \<rbrakk> \<Longrightarrow> Ex (eval_c i x2);  P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1  AND  x2  \<rbrakk> \<Longrightarrow> Ex (eval_c i (x1  AND  x2 ))
 3. \<And>x1 x2. \<lbrakk>\<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1 \<rbrakk> \<Longrightarrow> Ex (eval_c i x1); \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x2 \<rbrakk> \<Longrightarrow> Ex (eval_c i x2);  P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1 OR x2  \<rbrakk> \<Longrightarrow> Ex (eval_c i (x1 OR x2 ))
 4. \<And>x. \<lbrakk>\<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x \<rbrakk> \<Longrightarrow> Ex (eval_c i x);  P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f \<not> x  \<rbrakk> \<Longrightarrow> Ex (eval_c i (\<not> x ))
 5. \<And>x1 x2. \<lbrakk>\<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1 \<rbrakk> \<Longrightarrow> Ex (eval_c i x1); \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x2 \<rbrakk> \<Longrightarrow> Ex (eval_c i x2);  P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1  IMP  x2  \<rbrakk> \<Longrightarrow> Ex (eval_c i (x1  IMP  x2 ))
 6. \<And>x1 x2. \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1  ==  x2  \<rbrakk> \<Longrightarrow> Ex (eval_c i (x1  ==  x2 ))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f FALSE \<rbrakk> \<Longrightarrow> Ex (eval_c i (FALSE))
 2. \<And>x1 x2. \<lbrakk>\<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1 \<rbrakk> \<Longrightarrow> Ex (eval_c i x1); \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x2 \<rbrakk> \<Longrightarrow> Ex (eval_c i x2);  P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1  AND  x2  \<rbrakk> \<Longrightarrow> Ex (eval_c i (x1  AND  x2 ))
 3. \<And>x1 x2. \<lbrakk>\<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1 \<rbrakk> \<Longrightarrow> Ex (eval_c i x1); \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x2 \<rbrakk> \<Longrightarrow> Ex (eval_c i x2);  P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1 OR x2  \<rbrakk> \<Longrightarrow> Ex (eval_c i (x1 OR x2 ))
 4. \<And>x. \<lbrakk>\<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x \<rbrakk> \<Longrightarrow> Ex (eval_c i x);  P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f \<not> x  \<rbrakk> \<Longrightarrow> Ex (eval_c i (\<not> x ))
 5. \<And>x1 x2. \<lbrakk>\<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1 \<rbrakk> \<Longrightarrow> Ex (eval_c i x1); \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x2 \<rbrakk> \<Longrightarrow> Ex (eval_c i x2);  P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1  IMP  x2  \<rbrakk> \<Longrightarrow> Ex (eval_c i (x1  IMP  x2 ))
 6. \<And>x1 x2. \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1  ==  x2  \<rbrakk> \<Longrightarrow> Ex (eval_c i (x1  ==  x2 ))
[PROOF STEP]
case C_false
[PROOF STATE]
proof (state)
this:
 P ; \<Gamma> \<turnstile> i
 P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f FALSE

goal (6 subgoals):
 1. \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f FALSE \<rbrakk> \<Longrightarrow> Ex (eval_c i (FALSE))
 2. \<And>x1 x2. \<lbrakk>\<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1 \<rbrakk> \<Longrightarrow> Ex (eval_c i x1); \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x2 \<rbrakk> \<Longrightarrow> Ex (eval_c i x2);  P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1  AND  x2  \<rbrakk> \<Longrightarrow> Ex (eval_c i (x1  AND  x2 ))
 3. \<And>x1 x2. \<lbrakk>\<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1 \<rbrakk> \<Longrightarrow> Ex (eval_c i x1); \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x2 \<rbrakk> \<Longrightarrow> Ex (eval_c i x2);  P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1 OR x2  \<rbrakk> \<Longrightarrow> Ex (eval_c i (x1 OR x2 ))
 4. \<And>x. \<lbrakk>\<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x \<rbrakk> \<Longrightarrow> Ex (eval_c i x);  P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f \<not> x  \<rbrakk> \<Longrightarrow> Ex (eval_c i (\<not> x ))
 5. \<And>x1 x2. \<lbrakk>\<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1 \<rbrakk> \<Longrightarrow> Ex (eval_c i x1); \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x2 \<rbrakk> \<Longrightarrow> Ex (eval_c i x2);  P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1  IMP  x2  \<rbrakk> \<Longrightarrow> Ex (eval_c i (x1  IMP  x2 ))
 6. \<And>x1 x2. \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1  ==  x2  \<rbrakk> \<Longrightarrow> Ex (eval_c i (x1  ==  x2 ))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
 P ; \<Gamma> \<turnstile> i
 P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f FALSE
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
 P ; \<Gamma> \<turnstile> i
 P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f FALSE

goal (1 subgoal):
 1. \<exists>a.  i \<lbrakk> FALSE \<rbrakk> ~ a
[PROOF STEP]
using eval_c.intros wfC_elims
[PROOF STATE]
proof (prove)
using this:
 P ; \<Gamma> \<turnstile> i
 P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f FALSE
 ?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
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f TRUE ;  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma>  \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f FALSE ;  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma>  \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?e1.0  ==  ?e2.0  ; \<And>b. \<lbrakk>  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?e1.0 : b ;   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?e2.0 : b \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c1.0  AND  ?c2.0  ; \<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c1.0 ;  ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c2.0 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c1.0 OR ?c2.0  ; \<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c1.0 ;  ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c2.0 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f \<not> ?c1.0  ;  ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c1.0  \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c1.0  IMP  ?c2.0  ; \<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c1.0 ;  ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c2.0 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

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

goal (5 subgoals):
 1. \<And>x1 x2. \<lbrakk>\<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1 \<rbrakk> \<Longrightarrow> Ex (eval_c i x1); \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x2 \<rbrakk> \<Longrightarrow> Ex (eval_c i x2);  P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1  AND  x2  \<rbrakk> \<Longrightarrow> Ex (eval_c i (x1  AND  x2 ))
 2. \<And>x1 x2. \<lbrakk>\<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1 \<rbrakk> \<Longrightarrow> Ex (eval_c i x1); \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x2 \<rbrakk> \<Longrightarrow> Ex (eval_c i x2);  P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1 OR x2  \<rbrakk> \<Longrightarrow> Ex (eval_c i (x1 OR x2 ))
 3. \<And>x. \<lbrakk>\<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x \<rbrakk> \<Longrightarrow> Ex (eval_c i x);  P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f \<not> x  \<rbrakk> \<Longrightarrow> Ex (eval_c i (\<not> x ))
 4. \<And>x1 x2. \<lbrakk>\<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1 \<rbrakk> \<Longrightarrow> Ex (eval_c i x1); \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x2 \<rbrakk> \<Longrightarrow> Ex (eval_c i x2);  P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1  IMP  x2  \<rbrakk> \<Longrightarrow> Ex (eval_c i (x1  IMP  x2 ))
 5. \<And>x1 x2. \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1  ==  x2  \<rbrakk> \<Longrightarrow> Ex (eval_c i (x1  ==  x2 ))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>x1 x2. \<lbrakk>\<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1 \<rbrakk> \<Longrightarrow> Ex (eval_c i x1); \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x2 \<rbrakk> \<Longrightarrow> Ex (eval_c i x2);  P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1  AND  x2  \<rbrakk> \<Longrightarrow> Ex (eval_c i (x1  AND  x2 ))
 2. \<And>x1 x2. \<lbrakk>\<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1 \<rbrakk> \<Longrightarrow> Ex (eval_c i x1); \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x2 \<rbrakk> \<Longrightarrow> Ex (eval_c i x2);  P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1 OR x2  \<rbrakk> \<Longrightarrow> Ex (eval_c i (x1 OR x2 ))
 3. \<And>x. \<lbrakk>\<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x \<rbrakk> \<Longrightarrow> Ex (eval_c i x);  P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f \<not> x  \<rbrakk> \<Longrightarrow> Ex (eval_c i (\<not> x ))
 4. \<And>x1 x2. \<lbrakk>\<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1 \<rbrakk> \<Longrightarrow> Ex (eval_c i x1); \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x2 \<rbrakk> \<Longrightarrow> Ex (eval_c i x2);  P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1  IMP  x2  \<rbrakk> \<Longrightarrow> Ex (eval_c i (x1  IMP  x2 ))
 5. \<And>x1 x2. \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1  ==  x2  \<rbrakk> \<Longrightarrow> Ex (eval_c i (x1  ==  x2 ))
[PROOF STEP]
case (C_conj c1 c2)
[PROOF STATE]
proof (state)
this:
\<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f c1 \<rbrakk> \<Longrightarrow> \<exists>a.  i \<lbrakk> c1 \<rbrakk> ~ a
\<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f c2 \<rbrakk> \<Longrightarrow> \<exists>a.  i \<lbrakk> c2 \<rbrakk> ~ a
 P ; \<Gamma> \<turnstile> i
 P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f c1  AND  c2

goal (5 subgoals):
 1. \<And>x1 x2. \<lbrakk>\<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1 \<rbrakk> \<Longrightarrow> Ex (eval_c i x1); \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x2 \<rbrakk> \<Longrightarrow> Ex (eval_c i x2);  P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1  AND  x2  \<rbrakk> \<Longrightarrow> Ex (eval_c i (x1  AND  x2 ))
 2. \<And>x1 x2. \<lbrakk>\<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1 \<rbrakk> \<Longrightarrow> Ex (eval_c i x1); \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x2 \<rbrakk> \<Longrightarrow> Ex (eval_c i x2);  P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1 OR x2  \<rbrakk> \<Longrightarrow> Ex (eval_c i (x1 OR x2 ))
 3. \<And>x. \<lbrakk>\<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x \<rbrakk> \<Longrightarrow> Ex (eval_c i x);  P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f \<not> x  \<rbrakk> \<Longrightarrow> Ex (eval_c i (\<not> x ))
 4. \<And>x1 x2. \<lbrakk>\<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1 \<rbrakk> \<Longrightarrow> Ex (eval_c i x1); \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x2 \<rbrakk> \<Longrightarrow> Ex (eval_c i x2);  P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1  IMP  x2  \<rbrakk> \<Longrightarrow> Ex (eval_c i (x1  IMP  x2 ))
 5. \<And>x1 x2. \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1  ==  x2  \<rbrakk> \<Longrightarrow> Ex (eval_c i (x1  ==  x2 ))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f c1 \<rbrakk> \<Longrightarrow> \<exists>a.  i \<lbrakk> c1 \<rbrakk> ~ a
\<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f c2 \<rbrakk> \<Longrightarrow> \<exists>a.  i \<lbrakk> c2 \<rbrakk> ~ a
 P ; \<Gamma> \<turnstile> i
 P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f c1  AND  c2
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f c1 \<rbrakk> \<Longrightarrow> \<exists>a.  i \<lbrakk> c1 \<rbrakk> ~ a
\<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f c2 \<rbrakk> \<Longrightarrow> \<exists>a.  i \<lbrakk> c2 \<rbrakk> ~ a
 P ; \<Gamma> \<turnstile> i
 P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f c1  AND  c2

goal (1 subgoal):
 1. \<exists>a.  i \<lbrakk> c1  AND  c2  \<rbrakk> ~ a
[PROOF STEP]
using eval_c.intros wfC_elims
[PROOF STATE]
proof (prove)
using this:
\<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f c1 \<rbrakk> \<Longrightarrow> \<exists>a.  i \<lbrakk> c1 \<rbrakk> ~ a
\<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f c2 \<rbrakk> \<Longrightarrow> \<exists>a.  i \<lbrakk> c2 \<rbrakk> ~ a
 P ; \<Gamma> \<turnstile> i
 P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f c1  AND  c2
 ?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
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f TRUE ;  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma>  \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f FALSE ;  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma>  \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?e1.0  ==  ?e2.0  ; \<And>b. \<lbrakk>  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?e1.0 : b ;   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?e2.0 : b \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c1.0  AND  ?c2.0  ; \<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c1.0 ;  ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c2.0 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c1.0 OR ?c2.0  ; \<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c1.0 ;  ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c2.0 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f \<not> ?c1.0  ;  ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c1.0  \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c1.0  IMP  ?c2.0  ; \<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c1.0 ;  ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c2.0 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

goal (1 subgoal):
 1. \<exists>a.  i \<lbrakk> c1  AND  c2  \<rbrakk> ~ a
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<exists>a.  i \<lbrakk> c1  AND  c2  \<rbrakk> ~ a

goal (4 subgoals):
 1. \<And>x1 x2. \<lbrakk>\<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1 \<rbrakk> \<Longrightarrow> Ex (eval_c i x1); \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x2 \<rbrakk> \<Longrightarrow> Ex (eval_c i x2);  P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1 OR x2  \<rbrakk> \<Longrightarrow> Ex (eval_c i (x1 OR x2 ))
 2. \<And>x. \<lbrakk>\<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x \<rbrakk> \<Longrightarrow> Ex (eval_c i x);  P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f \<not> x  \<rbrakk> \<Longrightarrow> Ex (eval_c i (\<not> x ))
 3. \<And>x1 x2. \<lbrakk>\<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1 \<rbrakk> \<Longrightarrow> Ex (eval_c i x1); \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x2 \<rbrakk> \<Longrightarrow> Ex (eval_c i x2);  P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1  IMP  x2  \<rbrakk> \<Longrightarrow> Ex (eval_c i (x1  IMP  x2 ))
 4. \<And>x1 x2. \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1  ==  x2  \<rbrakk> \<Longrightarrow> Ex (eval_c i (x1  ==  x2 ))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>x1 x2. \<lbrakk>\<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1 \<rbrakk> \<Longrightarrow> Ex (eval_c i x1); \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x2 \<rbrakk> \<Longrightarrow> Ex (eval_c i x2);  P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1 OR x2  \<rbrakk> \<Longrightarrow> Ex (eval_c i (x1 OR x2 ))
 2. \<And>x. \<lbrakk>\<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x \<rbrakk> \<Longrightarrow> Ex (eval_c i x);  P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f \<not> x  \<rbrakk> \<Longrightarrow> Ex (eval_c i (\<not> x ))
 3. \<And>x1 x2. \<lbrakk>\<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1 \<rbrakk> \<Longrightarrow> Ex (eval_c i x1); \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x2 \<rbrakk> \<Longrightarrow> Ex (eval_c i x2);  P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1  IMP  x2  \<rbrakk> \<Longrightarrow> Ex (eval_c i (x1  IMP  x2 ))
 4. \<And>x1 x2. \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1  ==  x2  \<rbrakk> \<Longrightarrow> Ex (eval_c i (x1  ==  x2 ))
[PROOF STEP]
case (C_disj x1 x2)
[PROOF STATE]
proof (state)
this:
\<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1 \<rbrakk> \<Longrightarrow> \<exists>a.  i \<lbrakk> x1 \<rbrakk> ~ a
\<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x2 \<rbrakk> \<Longrightarrow> \<exists>a.  i \<lbrakk> x2 \<rbrakk> ~ a
 P ; \<Gamma> \<turnstile> i
 P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1 OR x2

goal (4 subgoals):
 1. \<And>x1 x2. \<lbrakk>\<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1 \<rbrakk> \<Longrightarrow> Ex (eval_c i x1); \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x2 \<rbrakk> \<Longrightarrow> Ex (eval_c i x2);  P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1 OR x2  \<rbrakk> \<Longrightarrow> Ex (eval_c i (x1 OR x2 ))
 2. \<And>x. \<lbrakk>\<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x \<rbrakk> \<Longrightarrow> Ex (eval_c i x);  P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f \<not> x  \<rbrakk> \<Longrightarrow> Ex (eval_c i (\<not> x ))
 3. \<And>x1 x2. \<lbrakk>\<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1 \<rbrakk> \<Longrightarrow> Ex (eval_c i x1); \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x2 \<rbrakk> \<Longrightarrow> Ex (eval_c i x2);  P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1  IMP  x2  \<rbrakk> \<Longrightarrow> Ex (eval_c i (x1  IMP  x2 ))
 4. \<And>x1 x2. \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1  ==  x2  \<rbrakk> \<Longrightarrow> Ex (eval_c i (x1  ==  x2 ))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1 \<rbrakk> \<Longrightarrow> \<exists>a.  i \<lbrakk> x1 \<rbrakk> ~ a
\<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x2 \<rbrakk> \<Longrightarrow> \<exists>a.  i \<lbrakk> x2 \<rbrakk> ~ a
 P ; \<Gamma> \<turnstile> i
 P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1 OR x2
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1 \<rbrakk> \<Longrightarrow> \<exists>a.  i \<lbrakk> x1 \<rbrakk> ~ a
\<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x2 \<rbrakk> \<Longrightarrow> \<exists>a.  i \<lbrakk> x2 \<rbrakk> ~ a
 P ; \<Gamma> \<turnstile> i
 P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1 OR x2

goal (1 subgoal):
 1. \<exists>a.  i \<lbrakk> x1 OR x2  \<rbrakk> ~ a
[PROOF STEP]
using eval_c.intros wfC_elims
[PROOF STATE]
proof (prove)
using this:
\<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1 \<rbrakk> \<Longrightarrow> \<exists>a.  i \<lbrakk> x1 \<rbrakk> ~ a
\<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x2 \<rbrakk> \<Longrightarrow> \<exists>a.  i \<lbrakk> x2 \<rbrakk> ~ a
 P ; \<Gamma> \<turnstile> i
 P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1 OR x2
 ?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
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f TRUE ;  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma>  \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f FALSE ;  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma>  \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?e1.0  ==  ?e2.0  ; \<And>b. \<lbrakk>  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?e1.0 : b ;   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?e2.0 : b \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c1.0  AND  ?c2.0  ; \<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c1.0 ;  ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c2.0 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c1.0 OR ?c2.0  ; \<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c1.0 ;  ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c2.0 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f \<not> ?c1.0  ;  ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c1.0  \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c1.0  IMP  ?c2.0  ; \<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c1.0 ;  ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c2.0 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

goal (1 subgoal):
 1. \<exists>a.  i \<lbrakk> x1 OR x2  \<rbrakk> ~ a
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<exists>a.  i \<lbrakk> x1 OR x2  \<rbrakk> ~ a

goal (3 subgoals):
 1. \<And>x. \<lbrakk>\<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x \<rbrakk> \<Longrightarrow> Ex (eval_c i x);  P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f \<not> x  \<rbrakk> \<Longrightarrow> Ex (eval_c i (\<not> x ))
 2. \<And>x1 x2. \<lbrakk>\<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1 \<rbrakk> \<Longrightarrow> Ex (eval_c i x1); \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x2 \<rbrakk> \<Longrightarrow> Ex (eval_c i x2);  P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1  IMP  x2  \<rbrakk> \<Longrightarrow> Ex (eval_c i (x1  IMP  x2 ))
 3. \<And>x1 x2. \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1  ==  x2  \<rbrakk> \<Longrightarrow> Ex (eval_c i (x1  ==  x2 ))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>\<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x \<rbrakk> \<Longrightarrow> Ex (eval_c i x);  P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f \<not> x  \<rbrakk> \<Longrightarrow> Ex (eval_c i (\<not> x ))
 2. \<And>x1 x2. \<lbrakk>\<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1 \<rbrakk> \<Longrightarrow> Ex (eval_c i x1); \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x2 \<rbrakk> \<Longrightarrow> Ex (eval_c i x2);  P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1  IMP  x2  \<rbrakk> \<Longrightarrow> Ex (eval_c i (x1  IMP  x2 ))
 3. \<And>x1 x2. \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1  ==  x2  \<rbrakk> \<Longrightarrow> Ex (eval_c i (x1  ==  x2 ))
[PROOF STEP]
case (C_not x)
[PROOF STATE]
proof (state)
this:
\<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x \<rbrakk> \<Longrightarrow> \<exists>a.  i \<lbrakk> x \<rbrakk> ~ a
 P ; \<Gamma> \<turnstile> i
 P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f \<not> x

goal (3 subgoals):
 1. \<And>x. \<lbrakk>\<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x \<rbrakk> \<Longrightarrow> Ex (eval_c i x);  P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f \<not> x  \<rbrakk> \<Longrightarrow> Ex (eval_c i (\<not> x ))
 2. \<And>x1 x2. \<lbrakk>\<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1 \<rbrakk> \<Longrightarrow> Ex (eval_c i x1); \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x2 \<rbrakk> \<Longrightarrow> Ex (eval_c i x2);  P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1  IMP  x2  \<rbrakk> \<Longrightarrow> Ex (eval_c i (x1  IMP  x2 ))
 3. \<And>x1 x2. \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1  ==  x2  \<rbrakk> \<Longrightarrow> Ex (eval_c i (x1  ==  x2 ))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x \<rbrakk> \<Longrightarrow> \<exists>a.  i \<lbrakk> x \<rbrakk> ~ a
 P ; \<Gamma> \<turnstile> i
 P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f \<not> x
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x \<rbrakk> \<Longrightarrow> \<exists>a.  i \<lbrakk> x \<rbrakk> ~ a
 P ; \<Gamma> \<turnstile> i
 P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f \<not> x

goal (1 subgoal):
 1. \<exists>a.  i \<lbrakk> \<not> x  \<rbrakk> ~ a
[PROOF STEP]
using eval_c.intros wfC_elims
[PROOF STATE]
proof (prove)
using this:
\<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x \<rbrakk> \<Longrightarrow> \<exists>a.  i \<lbrakk> x \<rbrakk> ~ a
 P ; \<Gamma> \<turnstile> i
 P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f \<not> x
 ?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
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f TRUE ;  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma>  \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f FALSE ;  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma>  \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?e1.0  ==  ?e2.0  ; \<And>b. \<lbrakk>  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?e1.0 : b ;   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?e2.0 : b \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c1.0  AND  ?c2.0  ; \<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c1.0 ;  ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c2.0 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c1.0 OR ?c2.0  ; \<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c1.0 ;  ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c2.0 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f \<not> ?c1.0  ;  ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c1.0  \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c1.0  IMP  ?c2.0  ; \<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c1.0 ;  ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c2.0 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

goal (1 subgoal):
 1. \<exists>a.  i \<lbrakk> \<not> x  \<rbrakk> ~ a
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<exists>a.  i \<lbrakk> \<not> x  \<rbrakk> ~ a

goal (2 subgoals):
 1. \<And>x1 x2. \<lbrakk>\<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1 \<rbrakk> \<Longrightarrow> Ex (eval_c i x1); \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x2 \<rbrakk> \<Longrightarrow> Ex (eval_c i x2);  P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1  IMP  x2  \<rbrakk> \<Longrightarrow> Ex (eval_c i (x1  IMP  x2 ))
 2. \<And>x1 x2. \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1  ==  x2  \<rbrakk> \<Longrightarrow> Ex (eval_c i (x1  ==  x2 ))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x1 x2. \<lbrakk>\<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1 \<rbrakk> \<Longrightarrow> Ex (eval_c i x1); \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x2 \<rbrakk> \<Longrightarrow> Ex (eval_c i x2);  P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1  IMP  x2  \<rbrakk> \<Longrightarrow> Ex (eval_c i (x1  IMP  x2 ))
 2. \<And>x1 x2. \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1  ==  x2  \<rbrakk> \<Longrightarrow> Ex (eval_c i (x1  ==  x2 ))
[PROOF STEP]
case (C_imp x1 x2)
[PROOF STATE]
proof (state)
this:
\<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1 \<rbrakk> \<Longrightarrow> \<exists>a.  i \<lbrakk> x1 \<rbrakk> ~ a
\<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x2 \<rbrakk> \<Longrightarrow> \<exists>a.  i \<lbrakk> x2 \<rbrakk> ~ a
 P ; \<Gamma> \<turnstile> i
 P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1  IMP  x2

goal (2 subgoals):
 1. \<And>x1 x2. \<lbrakk>\<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1 \<rbrakk> \<Longrightarrow> Ex (eval_c i x1); \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x2 \<rbrakk> \<Longrightarrow> Ex (eval_c i x2);  P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1  IMP  x2  \<rbrakk> \<Longrightarrow> Ex (eval_c i (x1  IMP  x2 ))
 2. \<And>x1 x2. \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1  ==  x2  \<rbrakk> \<Longrightarrow> Ex (eval_c i (x1  ==  x2 ))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1 \<rbrakk> \<Longrightarrow> \<exists>a.  i \<lbrakk> x1 \<rbrakk> ~ a
\<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x2 \<rbrakk> \<Longrightarrow> \<exists>a.  i \<lbrakk> x2 \<rbrakk> ~ a
 P ; \<Gamma> \<turnstile> i
 P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1  IMP  x2
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1 \<rbrakk> \<Longrightarrow> \<exists>a.  i \<lbrakk> x1 \<rbrakk> ~ a
\<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x2 \<rbrakk> \<Longrightarrow> \<exists>a.  i \<lbrakk> x2 \<rbrakk> ~ a
 P ; \<Gamma> \<turnstile> i
 P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1  IMP  x2

goal (1 subgoal):
 1. \<exists>a.  i \<lbrakk> x1  IMP  x2  \<rbrakk> ~ a
[PROOF STEP]
using eval_c.intros eval_e_exist wfC_elims
[PROOF STATE]
proof (prove)
using this:
\<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1 \<rbrakk> \<Longrightarrow> \<exists>a.  i \<lbrakk> x1 \<rbrakk> ~ a
\<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x2 \<rbrakk> \<Longrightarrow> \<exists>a.  i \<lbrakk> x2 \<rbrakk> ~ a
 P ; \<Gamma> \<turnstile> i
 P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1  IMP  x2
 ?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
\<lbrakk> ?P ; ?\<Gamma> \<turnstile> ?i;   ?P ; ?B ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?e : ?b \<rbrakk> \<Longrightarrow> \<exists>s. ?i \<lbrakk> ?e \<rbrakk> ~ s
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f TRUE ;  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma>  \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f FALSE ;  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma>  \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?e1.0  ==  ?e2.0  ; \<And>b. \<lbrakk>  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?e1.0 : b ;   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?e2.0 : b \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c1.0  AND  ?c2.0  ; \<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c1.0 ;  ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c2.0 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c1.0 OR ?c2.0  ; \<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c1.0 ;  ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c2.0 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f \<not> ?c1.0  ;  ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c1.0  \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c1.0  IMP  ?c2.0  ; \<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c1.0 ;  ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c2.0 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

goal (1 subgoal):
 1. \<exists>a.  i \<lbrakk> x1  IMP  x2  \<rbrakk> ~ a
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<exists>a.  i \<lbrakk> x1  IMP  x2  \<rbrakk> ~ a

goal (1 subgoal):
 1. \<And>x1 x2. \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1  ==  x2  \<rbrakk> \<Longrightarrow> Ex (eval_c i (x1  ==  x2 ))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x1 x2. \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1  ==  x2  \<rbrakk> \<Longrightarrow> Ex (eval_c i (x1  ==  x2 ))
[PROOF STEP]
case (C_eq x1 x2)
[PROOF STATE]
proof (state)
this:
 P ; \<Gamma> \<turnstile> i
 P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1  ==  x2

goal (1 subgoal):
 1. \<And>x1 x2. \<lbrakk> P ; \<Gamma> \<turnstile> i;  P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1  ==  x2  \<rbrakk> \<Longrightarrow> Ex (eval_c i (x1  ==  x2 ))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
 P ; \<Gamma> \<turnstile> i
 P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1  ==  x2
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
 P ; \<Gamma> \<turnstile> i
 P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1  ==  x2

goal (1 subgoal):
 1. \<exists>a.  i \<lbrakk> x1  ==  x2  \<rbrakk> ~ a
[PROOF STEP]
using eval_c.intros eval_e_exist wfC_elims
[PROOF STATE]
proof (prove)
using this:
 P ; \<Gamma> \<turnstile> i
 P ; B ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f x1  ==  x2
 ?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
\<lbrakk> ?P ; ?\<Gamma> \<turnstile> ?i;   ?P ; ?B ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?e : ?b \<rbrakk> \<Longrightarrow> \<exists>s. ?i \<lbrakk> ?e \<rbrakk> ~ s
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f TRUE ;  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma>  \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f FALSE ;  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma>  \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?e1.0  ==  ?e2.0  ; \<And>b. \<lbrakk>  ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?e1.0 : b ;   ?\<Theta> ; ?\<B> ; ?\<Gamma> \<turnstile>\<^sub>w\<^sub>f ?e2.0 : b \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c1.0  AND  ?c2.0  ; \<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c1.0 ;  ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c2.0 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c1.0 OR ?c2.0  ; \<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c1.0 ;  ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c2.0 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f \<not> ?c1.0  ;  ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c1.0  \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c1.0  IMP  ?c2.0  ; \<lbrakk> ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c1.0 ;  ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?c2.0 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

goal (1 subgoal):
 1. \<exists>a.  i \<lbrakk> x1  ==  x2  \<rbrakk> ~ a
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<exists>a.  i \<lbrakk> x1  ==  x2  \<rbrakk> ~ a

goal:
No subgoals!
[PROOF STEP]
qed


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

goal (1 subgoal):
 1. s = s'
[PROOF STEP]
proof(nominal_induct c arbitrary: s s' rule:c.strong_induct)
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. \<And>s s'. \<lbrakk> i \<lbrakk> TRUE \<rbrakk> ~ s ;  i \<lbrakk> TRUE \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 2. \<And>s s'. \<lbrakk> i \<lbrakk> FALSE \<rbrakk> ~ s ;  i \<lbrakk> FALSE \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 3. \<And>x1 x2 s s'. \<lbrakk>\<And>s s'. \<lbrakk> i \<lbrakk> x1 \<rbrakk> ~ s ;  i \<lbrakk> x1 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; \<And>s s'. \<lbrakk> i \<lbrakk> x2 \<rbrakk> ~ s ;  i \<lbrakk> x2 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s';  i \<lbrakk> x1  AND  x2  \<rbrakk> ~ s ;  i \<lbrakk> x1  AND  x2  \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 4. \<And>x1 x2 s s'. \<lbrakk>\<And>s s'. \<lbrakk> i \<lbrakk> x1 \<rbrakk> ~ s ;  i \<lbrakk> x1 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; \<And>s s'. \<lbrakk> i \<lbrakk> x2 \<rbrakk> ~ s ;  i \<lbrakk> x2 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s';  i \<lbrakk> x1 OR x2  \<rbrakk> ~ s ;  i \<lbrakk> x1 OR x2  \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 5. \<And>x s s'. \<lbrakk>\<And>s s'. \<lbrakk> i \<lbrakk> x \<rbrakk> ~ s ;  i \<lbrakk> x \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s';  i \<lbrakk> \<not> x  \<rbrakk> ~ s ;  i \<lbrakk> \<not> x  \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 6. \<And>x1 x2 s s'. \<lbrakk>\<And>s s'. \<lbrakk> i \<lbrakk> x1 \<rbrakk> ~ s ;  i \<lbrakk> x1 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; \<And>s s'. \<lbrakk> i \<lbrakk> x2 \<rbrakk> ~ s ;  i \<lbrakk> x2 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s';  i \<lbrakk> x1  IMP  x2  \<rbrakk> ~ s ;  i \<lbrakk> x1  IMP  x2  \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 7. \<And>x1 x2 s s'. \<lbrakk> i \<lbrakk> x1  ==  x2  \<rbrakk> ~ s ;  i \<lbrakk> x1  ==  x2  \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
[PROOF STEP]
case C_true
[PROOF STATE]
proof (state)
this:
 i \<lbrakk> TRUE \<rbrakk> ~ s
 i \<lbrakk> TRUE \<rbrakk> ~ s'

goal (7 subgoals):
 1. \<And>s s'. \<lbrakk> i \<lbrakk> TRUE \<rbrakk> ~ s ;  i \<lbrakk> TRUE \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 2. \<And>s s'. \<lbrakk> i \<lbrakk> FALSE \<rbrakk> ~ s ;  i \<lbrakk> FALSE \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 3. \<And>x1 x2 s s'. \<lbrakk>\<And>s s'. \<lbrakk> i \<lbrakk> x1 \<rbrakk> ~ s ;  i \<lbrakk> x1 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; \<And>s s'. \<lbrakk> i \<lbrakk> x2 \<rbrakk> ~ s ;  i \<lbrakk> x2 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s';  i \<lbrakk> x1  AND  x2  \<rbrakk> ~ s ;  i \<lbrakk> x1  AND  x2  \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 4. \<And>x1 x2 s s'. \<lbrakk>\<And>s s'. \<lbrakk> i \<lbrakk> x1 \<rbrakk> ~ s ;  i \<lbrakk> x1 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; \<And>s s'. \<lbrakk> i \<lbrakk> x2 \<rbrakk> ~ s ;  i \<lbrakk> x2 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s';  i \<lbrakk> x1 OR x2  \<rbrakk> ~ s ;  i \<lbrakk> x1 OR x2  \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 5. \<And>x s s'. \<lbrakk>\<And>s s'. \<lbrakk> i \<lbrakk> x \<rbrakk> ~ s ;  i \<lbrakk> x \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s';  i \<lbrakk> \<not> x  \<rbrakk> ~ s ;  i \<lbrakk> \<not> x  \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 6. \<And>x1 x2 s s'. \<lbrakk>\<And>s s'. \<lbrakk> i \<lbrakk> x1 \<rbrakk> ~ s ;  i \<lbrakk> x1 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; \<And>s s'. \<lbrakk> i \<lbrakk> x2 \<rbrakk> ~ s ;  i \<lbrakk> x2 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s';  i \<lbrakk> x1  IMP  x2  \<rbrakk> ~ s ;  i \<lbrakk> x1  IMP  x2  \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 7. \<And>x1 x2 s s'. \<lbrakk> i \<lbrakk> x1  ==  x2  \<rbrakk> ~ s ;  i \<lbrakk> x1  ==  x2  \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
 i \<lbrakk> TRUE \<rbrakk> ~ s
 i \<lbrakk> TRUE \<rbrakk> ~ s'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
 i \<lbrakk> TRUE \<rbrakk> ~ s
 i \<lbrakk> TRUE \<rbrakk> ~ s'

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

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

goal (6 subgoals):
 1. \<And>s s'. \<lbrakk> i \<lbrakk> FALSE \<rbrakk> ~ s ;  i \<lbrakk> FALSE \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 2. \<And>x1 x2 s s'. \<lbrakk>\<And>s s'. \<lbrakk> i \<lbrakk> x1 \<rbrakk> ~ s ;  i \<lbrakk> x1 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; \<And>s s'. \<lbrakk> i \<lbrakk> x2 \<rbrakk> ~ s ;  i \<lbrakk> x2 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s';  i \<lbrakk> x1  AND  x2  \<rbrakk> ~ s ;  i \<lbrakk> x1  AND  x2  \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 3. \<And>x1 x2 s s'. \<lbrakk>\<And>s s'. \<lbrakk> i \<lbrakk> x1 \<rbrakk> ~ s ;  i \<lbrakk> x1 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; \<And>s s'. \<lbrakk> i \<lbrakk> x2 \<rbrakk> ~ s ;  i \<lbrakk> x2 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s';  i \<lbrakk> x1 OR x2  \<rbrakk> ~ s ;  i \<lbrakk> x1 OR x2  \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 4. \<And>x s s'. \<lbrakk>\<And>s s'. \<lbrakk> i \<lbrakk> x \<rbrakk> ~ s ;  i \<lbrakk> x \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s';  i \<lbrakk> \<not> x  \<rbrakk> ~ s ;  i \<lbrakk> \<not> x  \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 5. \<And>x1 x2 s s'. \<lbrakk>\<And>s s'. \<lbrakk> i \<lbrakk> x1 \<rbrakk> ~ s ;  i \<lbrakk> x1 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; \<And>s s'. \<lbrakk> i \<lbrakk> x2 \<rbrakk> ~ s ;  i \<lbrakk> x2 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s';  i \<lbrakk> x1  IMP  x2  \<rbrakk> ~ s ;  i \<lbrakk> x1  IMP  x2  \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 6. \<And>x1 x2 s s'. \<lbrakk> i \<lbrakk> x1  ==  x2  \<rbrakk> ~ s ;  i \<lbrakk> x1  ==  x2  \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<And>s s'. \<lbrakk> i \<lbrakk> FALSE \<rbrakk> ~ s ;  i \<lbrakk> FALSE \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 2. \<And>x1 x2 s s'. \<lbrakk>\<And>s s'. \<lbrakk> i \<lbrakk> x1 \<rbrakk> ~ s ;  i \<lbrakk> x1 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; \<And>s s'. \<lbrakk> i \<lbrakk> x2 \<rbrakk> ~ s ;  i \<lbrakk> x2 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s';  i \<lbrakk> x1  AND  x2  \<rbrakk> ~ s ;  i \<lbrakk> x1  AND  x2  \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 3. \<And>x1 x2 s s'. \<lbrakk>\<And>s s'. \<lbrakk> i \<lbrakk> x1 \<rbrakk> ~ s ;  i \<lbrakk> x1 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; \<And>s s'. \<lbrakk> i \<lbrakk> x2 \<rbrakk> ~ s ;  i \<lbrakk> x2 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s';  i \<lbrakk> x1 OR x2  \<rbrakk> ~ s ;  i \<lbrakk> x1 OR x2  \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 4. \<And>x s s'. \<lbrakk>\<And>s s'. \<lbrakk> i \<lbrakk> x \<rbrakk> ~ s ;  i \<lbrakk> x \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s';  i \<lbrakk> \<not> x  \<rbrakk> ~ s ;  i \<lbrakk> \<not> x  \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 5. \<And>x1 x2 s s'. \<lbrakk>\<And>s s'. \<lbrakk> i \<lbrakk> x1 \<rbrakk> ~ s ;  i \<lbrakk> x1 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; \<And>s s'. \<lbrakk> i \<lbrakk> x2 \<rbrakk> ~ s ;  i \<lbrakk> x2 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s';  i \<lbrakk> x1  IMP  x2  \<rbrakk> ~ s ;  i \<lbrakk> x1  IMP  x2  \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 6. \<And>x1 x2 s s'. \<lbrakk> i \<lbrakk> x1  ==  x2  \<rbrakk> ~ s ;  i \<lbrakk> x1  ==  x2  \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
[PROOF STEP]
case C_false
[PROOF STATE]
proof (state)
this:
 i \<lbrakk> FALSE \<rbrakk> ~ s
 i \<lbrakk> FALSE \<rbrakk> ~ s'

goal (6 subgoals):
 1. \<And>s s'. \<lbrakk> i \<lbrakk> FALSE \<rbrakk> ~ s ;  i \<lbrakk> FALSE \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 2. \<And>x1 x2 s s'. \<lbrakk>\<And>s s'. \<lbrakk> i \<lbrakk> x1 \<rbrakk> ~ s ;  i \<lbrakk> x1 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; \<And>s s'. \<lbrakk> i \<lbrakk> x2 \<rbrakk> ~ s ;  i \<lbrakk> x2 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s';  i \<lbrakk> x1  AND  x2  \<rbrakk> ~ s ;  i \<lbrakk> x1  AND  x2  \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 3. \<And>x1 x2 s s'. \<lbrakk>\<And>s s'. \<lbrakk> i \<lbrakk> x1 \<rbrakk> ~ s ;  i \<lbrakk> x1 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; \<And>s s'. \<lbrakk> i \<lbrakk> x2 \<rbrakk> ~ s ;  i \<lbrakk> x2 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s';  i \<lbrakk> x1 OR x2  \<rbrakk> ~ s ;  i \<lbrakk> x1 OR x2  \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 4. \<And>x s s'. \<lbrakk>\<And>s s'. \<lbrakk> i \<lbrakk> x \<rbrakk> ~ s ;  i \<lbrakk> x \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s';  i \<lbrakk> \<not> x  \<rbrakk> ~ s ;  i \<lbrakk> \<not> x  \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 5. \<And>x1 x2 s s'. \<lbrakk>\<And>s s'. \<lbrakk> i \<lbrakk> x1 \<rbrakk> ~ s ;  i \<lbrakk> x1 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; \<And>s s'. \<lbrakk> i \<lbrakk> x2 \<rbrakk> ~ s ;  i \<lbrakk> x2 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s';  i \<lbrakk> x1  IMP  x2  \<rbrakk> ~ s ;  i \<lbrakk> x1  IMP  x2  \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 6. \<And>x1 x2 s s'. \<lbrakk> i \<lbrakk> x1  ==  x2  \<rbrakk> ~ s ;  i \<lbrakk> x1  ==  x2  \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
 i \<lbrakk> FALSE \<rbrakk> ~ s
 i \<lbrakk> FALSE \<rbrakk> ~ s'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
 i \<lbrakk> FALSE \<rbrakk> ~ s
 i \<lbrakk> FALSE \<rbrakk> ~ s'

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

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

goal (5 subgoals):
 1. \<And>x1 x2 s s'. \<lbrakk>\<And>s s'. \<lbrakk> i \<lbrakk> x1 \<rbrakk> ~ s ;  i \<lbrakk> x1 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; \<And>s s'. \<lbrakk> i \<lbrakk> x2 \<rbrakk> ~ s ;  i \<lbrakk> x2 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s';  i \<lbrakk> x1  AND  x2  \<rbrakk> ~ s ;  i \<lbrakk> x1  AND  x2  \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 2. \<And>x1 x2 s s'. \<lbrakk>\<And>s s'. \<lbrakk> i \<lbrakk> x1 \<rbrakk> ~ s ;  i \<lbrakk> x1 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; \<And>s s'. \<lbrakk> i \<lbrakk> x2 \<rbrakk> ~ s ;  i \<lbrakk> x2 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s';  i \<lbrakk> x1 OR x2  \<rbrakk> ~ s ;  i \<lbrakk> x1 OR x2  \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 3. \<And>x s s'. \<lbrakk>\<And>s s'. \<lbrakk> i \<lbrakk> x \<rbrakk> ~ s ;  i \<lbrakk> x \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s';  i \<lbrakk> \<not> x  \<rbrakk> ~ s ;  i \<lbrakk> \<not> x  \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 4. \<And>x1 x2 s s'. \<lbrakk>\<And>s s'. \<lbrakk> i \<lbrakk> x1 \<rbrakk> ~ s ;  i \<lbrakk> x1 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; \<And>s s'. \<lbrakk> i \<lbrakk> x2 \<rbrakk> ~ s ;  i \<lbrakk> x2 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s';  i \<lbrakk> x1  IMP  x2  \<rbrakk> ~ s ;  i \<lbrakk> x1  IMP  x2  \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 5. \<And>x1 x2 s s'. \<lbrakk> i \<lbrakk> x1  ==  x2  \<rbrakk> ~ s ;  i \<lbrakk> x1  ==  x2  \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>x1 x2 s s'. \<lbrakk>\<And>s s'. \<lbrakk> i \<lbrakk> x1 \<rbrakk> ~ s ;  i \<lbrakk> x1 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; \<And>s s'. \<lbrakk> i \<lbrakk> x2 \<rbrakk> ~ s ;  i \<lbrakk> x2 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s';  i \<lbrakk> x1  AND  x2  \<rbrakk> ~ s ;  i \<lbrakk> x1  AND  x2  \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 2. \<And>x1 x2 s s'. \<lbrakk>\<And>s s'. \<lbrakk> i \<lbrakk> x1 \<rbrakk> ~ s ;  i \<lbrakk> x1 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; \<And>s s'. \<lbrakk> i \<lbrakk> x2 \<rbrakk> ~ s ;  i \<lbrakk> x2 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s';  i \<lbrakk> x1 OR x2  \<rbrakk> ~ s ;  i \<lbrakk> x1 OR x2  \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 3. \<And>x s s'. \<lbrakk>\<And>s s'. \<lbrakk> i \<lbrakk> x \<rbrakk> ~ s ;  i \<lbrakk> x \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s';  i \<lbrakk> \<not> x  \<rbrakk> ~ s ;  i \<lbrakk> \<not> x  \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 4. \<And>x1 x2 s s'. \<lbrakk>\<And>s s'. \<lbrakk> i \<lbrakk> x1 \<rbrakk> ~ s ;  i \<lbrakk> x1 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; \<And>s s'. \<lbrakk> i \<lbrakk> x2 \<rbrakk> ~ s ;  i \<lbrakk> x2 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s';  i \<lbrakk> x1  IMP  x2  \<rbrakk> ~ s ;  i \<lbrakk> x1  IMP  x2  \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 5. \<And>x1 x2 s s'. \<lbrakk> i \<lbrakk> x1  ==  x2  \<rbrakk> ~ s ;  i \<lbrakk> x1  ==  x2  \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
[PROOF STEP]
case (C_conj x1 x2)
[PROOF STATE]
proof (state)
this:
\<lbrakk> i \<lbrakk> x1 \<rbrakk> ~ ?s ;  i \<lbrakk> x1 \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> ?s = ?s'
\<lbrakk> i \<lbrakk> x2 \<rbrakk> ~ ?s ;  i \<lbrakk> x2 \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> ?s = ?s'
 i \<lbrakk> x1  AND  x2  \<rbrakk> ~ s
 i \<lbrakk> x1  AND  x2  \<rbrakk> ~ s'

goal (5 subgoals):
 1. \<And>x1 x2 s s'. \<lbrakk>\<And>s s'. \<lbrakk> i \<lbrakk> x1 \<rbrakk> ~ s ;  i \<lbrakk> x1 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; \<And>s s'. \<lbrakk> i \<lbrakk> x2 \<rbrakk> ~ s ;  i \<lbrakk> x2 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s';  i \<lbrakk> x1  AND  x2  \<rbrakk> ~ s ;  i \<lbrakk> x1  AND  x2  \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 2. \<And>x1 x2 s s'. \<lbrakk>\<And>s s'. \<lbrakk> i \<lbrakk> x1 \<rbrakk> ~ s ;  i \<lbrakk> x1 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; \<And>s s'. \<lbrakk> i \<lbrakk> x2 \<rbrakk> ~ s ;  i \<lbrakk> x2 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s';  i \<lbrakk> x1 OR x2  \<rbrakk> ~ s ;  i \<lbrakk> x1 OR x2  \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 3. \<And>x s s'. \<lbrakk>\<And>s s'. \<lbrakk> i \<lbrakk> x \<rbrakk> ~ s ;  i \<lbrakk> x \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s';  i \<lbrakk> \<not> x  \<rbrakk> ~ s ;  i \<lbrakk> \<not> x  \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 4. \<And>x1 x2 s s'. \<lbrakk>\<And>s s'. \<lbrakk> i \<lbrakk> x1 \<rbrakk> ~ s ;  i \<lbrakk> x1 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; \<And>s s'. \<lbrakk> i \<lbrakk> x2 \<rbrakk> ~ s ;  i \<lbrakk> x2 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s';  i \<lbrakk> x1  IMP  x2  \<rbrakk> ~ s ;  i \<lbrakk> x1  IMP  x2  \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 5. \<And>x1 x2 s s'. \<lbrakk> i \<lbrakk> x1  ==  x2  \<rbrakk> ~ s ;  i \<lbrakk> x1  ==  x2  \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk> i \<lbrakk> x1 \<rbrakk> ~ ?s ;  i \<lbrakk> x1 \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> ?s = ?s'
\<lbrakk> i \<lbrakk> x2 \<rbrakk> ~ ?s ;  i \<lbrakk> x2 \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> ?s = ?s'
 i \<lbrakk> x1  AND  x2  \<rbrakk> ~ s
 i \<lbrakk> x1  AND  x2  \<rbrakk> ~ s'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk> i \<lbrakk> x1 \<rbrakk> ~ ?s ;  i \<lbrakk> x1 \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> ?s = ?s'
\<lbrakk> i \<lbrakk> x2 \<rbrakk> ~ ?s ;  i \<lbrakk> x2 \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> ?s = ?s'
 i \<lbrakk> x1  AND  x2  \<rbrakk> ~ s
 i \<lbrakk> x1  AND  x2  \<rbrakk> ~ s'

goal (1 subgoal):
 1. s = s'
[PROOF STEP]
using  eval_c_elims(3)
[PROOF STATE]
proof (prove)
using this:
\<lbrakk> i \<lbrakk> x1 \<rbrakk> ~ ?s ;  i \<lbrakk> x1 \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> ?s = ?s'
\<lbrakk> i \<lbrakk> x2 \<rbrakk> ~ ?s ;  i \<lbrakk> x2 \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> ?s = ?s'
 i \<lbrakk> x1  AND  x2  \<rbrakk> ~ s
 i \<lbrakk> x1  AND  x2  \<rbrakk> ~ s'
\<lbrakk> ?i \<lbrakk> ?c1.0  AND  ?c2.0  \<rbrakk> ~ ?s ; \<And>b1 b2. \<lbrakk>?s = (b1 \<and> b2);  ?i \<lbrakk> ?c1.0 \<rbrakk> ~ b1 ;  ?i \<lbrakk> ?c2.0 \<rbrakk> ~ b2 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

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

goal (4 subgoals):
 1. \<And>x1 x2 s s'. \<lbrakk>\<And>s s'. \<lbrakk> i \<lbrakk> x1 \<rbrakk> ~ s ;  i \<lbrakk> x1 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; \<And>s s'. \<lbrakk> i \<lbrakk> x2 \<rbrakk> ~ s ;  i \<lbrakk> x2 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s';  i \<lbrakk> x1 OR x2  \<rbrakk> ~ s ;  i \<lbrakk> x1 OR x2  \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 2. \<And>x s s'. \<lbrakk>\<And>s s'. \<lbrakk> i \<lbrakk> x \<rbrakk> ~ s ;  i \<lbrakk> x \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s';  i \<lbrakk> \<not> x  \<rbrakk> ~ s ;  i \<lbrakk> \<not> x  \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 3. \<And>x1 x2 s s'. \<lbrakk>\<And>s s'. \<lbrakk> i \<lbrakk> x1 \<rbrakk> ~ s ;  i \<lbrakk> x1 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; \<And>s s'. \<lbrakk> i \<lbrakk> x2 \<rbrakk> ~ s ;  i \<lbrakk> x2 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s';  i \<lbrakk> x1  IMP  x2  \<rbrakk> ~ s ;  i \<lbrakk> x1  IMP  x2  \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 4. \<And>x1 x2 s s'. \<lbrakk> i \<lbrakk> x1  ==  x2  \<rbrakk> ~ s ;  i \<lbrakk> x1  ==  x2  \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>x1 x2 s s'. \<lbrakk>\<And>s s'. \<lbrakk> i \<lbrakk> x1 \<rbrakk> ~ s ;  i \<lbrakk> x1 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; \<And>s s'. \<lbrakk> i \<lbrakk> x2 \<rbrakk> ~ s ;  i \<lbrakk> x2 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s';  i \<lbrakk> x1 OR x2  \<rbrakk> ~ s ;  i \<lbrakk> x1 OR x2  \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 2. \<And>x s s'. \<lbrakk>\<And>s s'. \<lbrakk> i \<lbrakk> x \<rbrakk> ~ s ;  i \<lbrakk> x \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s';  i \<lbrakk> \<not> x  \<rbrakk> ~ s ;  i \<lbrakk> \<not> x  \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 3. \<And>x1 x2 s s'. \<lbrakk>\<And>s s'. \<lbrakk> i \<lbrakk> x1 \<rbrakk> ~ s ;  i \<lbrakk> x1 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; \<And>s s'. \<lbrakk> i \<lbrakk> x2 \<rbrakk> ~ s ;  i \<lbrakk> x2 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s';  i \<lbrakk> x1  IMP  x2  \<rbrakk> ~ s ;  i \<lbrakk> x1  IMP  x2  \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 4. \<And>x1 x2 s s'. \<lbrakk> i \<lbrakk> x1  ==  x2  \<rbrakk> ~ s ;  i \<lbrakk> x1  ==  x2  \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
[PROOF STEP]
case (C_disj x1 x2)
[PROOF STATE]
proof (state)
this:
\<lbrakk> i \<lbrakk> x1 \<rbrakk> ~ ?s ;  i \<lbrakk> x1 \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> ?s = ?s'
\<lbrakk> i \<lbrakk> x2 \<rbrakk> ~ ?s ;  i \<lbrakk> x2 \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> ?s = ?s'
 i \<lbrakk> x1 OR x2  \<rbrakk> ~ s
 i \<lbrakk> x1 OR x2  \<rbrakk> ~ s'

goal (4 subgoals):
 1. \<And>x1 x2 s s'. \<lbrakk>\<And>s s'. \<lbrakk> i \<lbrakk> x1 \<rbrakk> ~ s ;  i \<lbrakk> x1 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; \<And>s s'. \<lbrakk> i \<lbrakk> x2 \<rbrakk> ~ s ;  i \<lbrakk> x2 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s';  i \<lbrakk> x1 OR x2  \<rbrakk> ~ s ;  i \<lbrakk> x1 OR x2  \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 2. \<And>x s s'. \<lbrakk>\<And>s s'. \<lbrakk> i \<lbrakk> x \<rbrakk> ~ s ;  i \<lbrakk> x \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s';  i \<lbrakk> \<not> x  \<rbrakk> ~ s ;  i \<lbrakk> \<not> x  \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 3. \<And>x1 x2 s s'. \<lbrakk>\<And>s s'. \<lbrakk> i \<lbrakk> x1 \<rbrakk> ~ s ;  i \<lbrakk> x1 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; \<And>s s'. \<lbrakk> i \<lbrakk> x2 \<rbrakk> ~ s ;  i \<lbrakk> x2 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s';  i \<lbrakk> x1  IMP  x2  \<rbrakk> ~ s ;  i \<lbrakk> x1  IMP  x2  \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 4. \<And>x1 x2 s s'. \<lbrakk> i \<lbrakk> x1  ==  x2  \<rbrakk> ~ s ;  i \<lbrakk> x1  ==  x2  \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk> i \<lbrakk> x1 \<rbrakk> ~ ?s ;  i \<lbrakk> x1 \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> ?s = ?s'
\<lbrakk> i \<lbrakk> x2 \<rbrakk> ~ ?s ;  i \<lbrakk> x2 \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> ?s = ?s'
 i \<lbrakk> x1 OR x2  \<rbrakk> ~ s
 i \<lbrakk> x1 OR x2  \<rbrakk> ~ s'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk> i \<lbrakk> x1 \<rbrakk> ~ ?s ;  i \<lbrakk> x1 \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> ?s = ?s'
\<lbrakk> i \<lbrakk> x2 \<rbrakk> ~ ?s ;  i \<lbrakk> x2 \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> ?s = ?s'
 i \<lbrakk> x1 OR x2  \<rbrakk> ~ s
 i \<lbrakk> x1 OR x2  \<rbrakk> ~ s'

goal (1 subgoal):
 1. s = s'
[PROOF STEP]
using eval_c_elims(4)
[PROOF STATE]
proof (prove)
using this:
\<lbrakk> i \<lbrakk> x1 \<rbrakk> ~ ?s ;  i \<lbrakk> x1 \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> ?s = ?s'
\<lbrakk> i \<lbrakk> x2 \<rbrakk> ~ ?s ;  i \<lbrakk> x2 \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> ?s = ?s'
 i \<lbrakk> x1 OR x2  \<rbrakk> ~ s
 i \<lbrakk> x1 OR x2  \<rbrakk> ~ s'
\<lbrakk> ?i \<lbrakk> ?c1.0 OR ?c2.0  \<rbrakk> ~ ?s ; \<And>b1 b2. \<lbrakk>?s = (b1 \<or> b2);  ?i \<lbrakk> ?c1.0 \<rbrakk> ~ b1 ;  ?i \<lbrakk> ?c2.0 \<rbrakk> ~ b2 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

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

goal (3 subgoals):
 1. \<And>x s s'. \<lbrakk>\<And>s s'. \<lbrakk> i \<lbrakk> x \<rbrakk> ~ s ;  i \<lbrakk> x \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s';  i \<lbrakk> \<not> x  \<rbrakk> ~ s ;  i \<lbrakk> \<not> x  \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 2. \<And>x1 x2 s s'. \<lbrakk>\<And>s s'. \<lbrakk> i \<lbrakk> x1 \<rbrakk> ~ s ;  i \<lbrakk> x1 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; \<And>s s'. \<lbrakk> i \<lbrakk> x2 \<rbrakk> ~ s ;  i \<lbrakk> x2 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s';  i \<lbrakk> x1  IMP  x2  \<rbrakk> ~ s ;  i \<lbrakk> x1  IMP  x2  \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 3. \<And>x1 x2 s s'. \<lbrakk> i \<lbrakk> x1  ==  x2  \<rbrakk> ~ s ;  i \<lbrakk> x1  ==  x2  \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x s s'. \<lbrakk>\<And>s s'. \<lbrakk> i \<lbrakk> x \<rbrakk> ~ s ;  i \<lbrakk> x \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s';  i \<lbrakk> \<not> x  \<rbrakk> ~ s ;  i \<lbrakk> \<not> x  \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 2. \<And>x1 x2 s s'. \<lbrakk>\<And>s s'. \<lbrakk> i \<lbrakk> x1 \<rbrakk> ~ s ;  i \<lbrakk> x1 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; \<And>s s'. \<lbrakk> i \<lbrakk> x2 \<rbrakk> ~ s ;  i \<lbrakk> x2 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s';  i \<lbrakk> x1  IMP  x2  \<rbrakk> ~ s ;  i \<lbrakk> x1  IMP  x2  \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 3. \<And>x1 x2 s s'. \<lbrakk> i \<lbrakk> x1  ==  x2  \<rbrakk> ~ s ;  i \<lbrakk> x1  ==  x2  \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
[PROOF STEP]
case (C_not x)
[PROOF STATE]
proof (state)
this:
\<lbrakk> i \<lbrakk> x \<rbrakk> ~ ?s ;  i \<lbrakk> x \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> ?s = ?s'
 i \<lbrakk> \<not> x  \<rbrakk> ~ s
 i \<lbrakk> \<not> x  \<rbrakk> ~ s'

goal (3 subgoals):
 1. \<And>x s s'. \<lbrakk>\<And>s s'. \<lbrakk> i \<lbrakk> x \<rbrakk> ~ s ;  i \<lbrakk> x \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s';  i \<lbrakk> \<not> x  \<rbrakk> ~ s ;  i \<lbrakk> \<not> x  \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 2. \<And>x1 x2 s s'. \<lbrakk>\<And>s s'. \<lbrakk> i \<lbrakk> x1 \<rbrakk> ~ s ;  i \<lbrakk> x1 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; \<And>s s'. \<lbrakk> i \<lbrakk> x2 \<rbrakk> ~ s ;  i \<lbrakk> x2 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s';  i \<lbrakk> x1  IMP  x2  \<rbrakk> ~ s ;  i \<lbrakk> x1  IMP  x2  \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 3. \<And>x1 x2 s s'. \<lbrakk> i \<lbrakk> x1  ==  x2  \<rbrakk> ~ s ;  i \<lbrakk> x1  ==  x2  \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk> i \<lbrakk> x \<rbrakk> ~ ?s ;  i \<lbrakk> x \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> ?s = ?s'
 i \<lbrakk> \<not> x  \<rbrakk> ~ s
 i \<lbrakk> \<not> x  \<rbrakk> ~ s'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk> i \<lbrakk> x \<rbrakk> ~ ?s ;  i \<lbrakk> x \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> ?s = ?s'
 i \<lbrakk> \<not> x  \<rbrakk> ~ s
 i \<lbrakk> \<not> x  \<rbrakk> ~ s'

goal (1 subgoal):
 1. s = s'
[PROOF STEP]
using eval_c_elims(6)
[PROOF STATE]
proof (prove)
using this:
\<lbrakk> i \<lbrakk> x \<rbrakk> ~ ?s ;  i \<lbrakk> x \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> ?s = ?s'
 i \<lbrakk> \<not> x  \<rbrakk> ~ s
 i \<lbrakk> \<not> x  \<rbrakk> ~ s'
\<lbrakk> ?i \<lbrakk> \<not> ?c  \<rbrakk> ~ ?s ; \<And>b. \<lbrakk>?s = (\<not> b);  ?i \<lbrakk> ?c \<rbrakk> ~ b \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

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

goal (2 subgoals):
 1. \<And>x1 x2 s s'. \<lbrakk>\<And>s s'. \<lbrakk> i \<lbrakk> x1 \<rbrakk> ~ s ;  i \<lbrakk> x1 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; \<And>s s'. \<lbrakk> i \<lbrakk> x2 \<rbrakk> ~ s ;  i \<lbrakk> x2 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s';  i \<lbrakk> x1  IMP  x2  \<rbrakk> ~ s ;  i \<lbrakk> x1  IMP  x2  \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 2. \<And>x1 x2 s s'. \<lbrakk> i \<lbrakk> x1  ==  x2  \<rbrakk> ~ s ;  i \<lbrakk> x1  ==  x2  \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x1 x2 s s'. \<lbrakk>\<And>s s'. \<lbrakk> i \<lbrakk> x1 \<rbrakk> ~ s ;  i \<lbrakk> x1 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; \<And>s s'. \<lbrakk> i \<lbrakk> x2 \<rbrakk> ~ s ;  i \<lbrakk> x2 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s';  i \<lbrakk> x1  IMP  x2  \<rbrakk> ~ s ;  i \<lbrakk> x1  IMP  x2  \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 2. \<And>x1 x2 s s'. \<lbrakk> i \<lbrakk> x1  ==  x2  \<rbrakk> ~ s ;  i \<lbrakk> x1  ==  x2  \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
[PROOF STEP]
case (C_imp x1 x2)
[PROOF STATE]
proof (state)
this:
\<lbrakk> i \<lbrakk> x1 \<rbrakk> ~ ?s ;  i \<lbrakk> x1 \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> ?s = ?s'
\<lbrakk> i \<lbrakk> x2 \<rbrakk> ~ ?s ;  i \<lbrakk> x2 \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> ?s = ?s'
 i \<lbrakk> x1  IMP  x2  \<rbrakk> ~ s
 i \<lbrakk> x1  IMP  x2  \<rbrakk> ~ s'

goal (2 subgoals):
 1. \<And>x1 x2 s s'. \<lbrakk>\<And>s s'. \<lbrakk> i \<lbrakk> x1 \<rbrakk> ~ s ;  i \<lbrakk> x1 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; \<And>s s'. \<lbrakk> i \<lbrakk> x2 \<rbrakk> ~ s ;  i \<lbrakk> x2 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s';  i \<lbrakk> x1  IMP  x2  \<rbrakk> ~ s ;  i \<lbrakk> x1  IMP  x2  \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 2. \<And>x1 x2 s s'. \<lbrakk> i \<lbrakk> x1  ==  x2  \<rbrakk> ~ s ;  i \<lbrakk> x1  ==  x2  \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk> i \<lbrakk> x1 \<rbrakk> ~ ?s ;  i \<lbrakk> x1 \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> ?s = ?s'
\<lbrakk> i \<lbrakk> x2 \<rbrakk> ~ ?s ;  i \<lbrakk> x2 \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> ?s = ?s'
 i \<lbrakk> x1  IMP  x2  \<rbrakk> ~ s
 i \<lbrakk> x1  IMP  x2  \<rbrakk> ~ s'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk> i \<lbrakk> x1 \<rbrakk> ~ ?s ;  i \<lbrakk> x1 \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> ?s = ?s'
\<lbrakk> i \<lbrakk> x2 \<rbrakk> ~ ?s ;  i \<lbrakk> x2 \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> ?s = ?s'
 i \<lbrakk> x1  IMP  x2  \<rbrakk> ~ s
 i \<lbrakk> x1  IMP  x2  \<rbrakk> ~ s'

goal (1 subgoal):
 1. s = s'
[PROOF STEP]
using eval_c_elims(5)
[PROOF STATE]
proof (prove)
using this:
\<lbrakk> i \<lbrakk> x1 \<rbrakk> ~ ?s ;  i \<lbrakk> x1 \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> ?s = ?s'
\<lbrakk> i \<lbrakk> x2 \<rbrakk> ~ ?s ;  i \<lbrakk> x2 \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> ?s = ?s'
 i \<lbrakk> x1  IMP  x2  \<rbrakk> ~ s
 i \<lbrakk> x1  IMP  x2  \<rbrakk> ~ s'
\<lbrakk> ?i \<lbrakk> ?c1.0  IMP  ?c2.0  \<rbrakk> ~ ?s ; \<And>b1 b2. \<lbrakk>?s = (b1 \<longrightarrow> b2);  ?i \<lbrakk> ?c1.0 \<rbrakk> ~ b1 ;  ?i \<lbrakk> ?c2.0 \<rbrakk> ~ b2 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

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

goal (1 subgoal):
 1. \<And>x1 x2 s s'. \<lbrakk> i \<lbrakk> x1  ==  x2  \<rbrakk> ~ s ;  i \<lbrakk> x1  ==  x2  \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x1 x2 s s'. \<lbrakk> i \<lbrakk> x1  ==  x2  \<rbrakk> ~ s ;  i \<lbrakk> x1  ==  x2  \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
[PROOF STEP]
case (C_eq x1 x2)
[PROOF STATE]
proof (state)
this:
 i \<lbrakk> x1  ==  x2  \<rbrakk> ~ s
 i \<lbrakk> x1  ==  x2  \<rbrakk> ~ s'

goal (1 subgoal):
 1. \<And>x1 x2 s s'. \<lbrakk> i \<lbrakk> x1  ==  x2  \<rbrakk> ~ s ;  i \<lbrakk> x1  ==  x2  \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
 i \<lbrakk> x1  ==  x2  \<rbrakk> ~ s
 i \<lbrakk> x1  ==  x2  \<rbrakk> ~ s'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
 i \<lbrakk> x1  ==  x2  \<rbrakk> ~ s
 i \<lbrakk> x1  ==  x2  \<rbrakk> ~ s'

goal (1 subgoal):
 1. s = s'
[PROOF STEP]
using eval_e_uniqueness eval_c_elims(7)
[PROOF STATE]
proof (prove)
using this:
 i \<lbrakk> x1  ==  x2  \<rbrakk> ~ s
 i \<lbrakk> x1  ==  x2  \<rbrakk> ~ s'
\<lbrakk>?i \<lbrakk> ?e \<rbrakk> ~ ?s ; ?i \<lbrakk> ?e \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> ?s = ?s'
\<lbrakk> ?i \<lbrakk> ?e1.0  ==  ?e2.0  \<rbrakk> ~ ?s ; \<And>sv1 sv2. \<lbrakk>?s = (sv1 = sv2); ?i \<lbrakk> ?e1.0 \<rbrakk> ~ sv1 ; ?i \<lbrakk> ?e2.0 \<rbrakk> ~ sv2 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma wfI_wfC_eval_c:
  fixes c::c
  assumes "wfC P B G c" and "P ; G \<turnstile> i"
  shows "\<exists>s. i \<lbrakk> c \<rbrakk> ~ s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>s.  i \<lbrakk> c \<rbrakk> ~ s
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
 P ; B ; G   \<turnstile>\<^sub>w\<^sub>f c
 P ; G \<turnstile> i

goal (1 subgoal):
 1. \<exists>s.  i \<lbrakk> c \<rbrakk> ~ s
[PROOF STEP]
proof(nominal_induct c  rule: c.strong_induct)
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. \<lbrakk> P ; B ; G   \<turnstile>\<^sub>w\<^sub>f TRUE ;  P ; G \<turnstile> i\<rbrakk> \<Longrightarrow> Ex (eval_c i (TRUE))
 2. \<lbrakk> P ; B ; G   \<turnstile>\<^sub>w\<^sub>f FALSE ;  P ; G \<turnstile> i\<rbrakk> \<Longrightarrow> Ex (eval_c i (FALSE))
 3. \<And>x1 x2. \<lbrakk>\<lbrakk> P ; B ; G   \<turnstile>\<^sub>w\<^sub>f x1 ;  P ; G \<turnstile> i\<rbrakk> \<Longrightarrow> Ex (eval_c i x1); \<lbrakk> P ; B ; G   \<turnstile>\<^sub>w\<^sub>f x2 ;  P ; G \<turnstile> i\<rbrakk> \<Longrightarrow> Ex (eval_c i x2);  P ; B ; G   \<turnstile>\<^sub>w\<^sub>f x1  AND  x2  ;  P ; G \<turnstile> i\<rbrakk> \<Longrightarrow> Ex (eval_c i (x1  AND  x2 ))
 4. \<And>x1 x2. \<lbrakk>\<lbrakk> P ; B ; G   \<turnstile>\<^sub>w\<^sub>f x1 ;  P ; G \<turnstile> i\<rbrakk> \<Longrightarrow> Ex (eval_c i x1); \<lbrakk> P ; B ; G   \<turnstile>\<^sub>w\<^sub>f x2 ;  P ; G \<turnstile> i\<rbrakk> \<Longrightarrow> Ex (eval_c i x2);  P ; B ; G   \<turnstile>\<^sub>w\<^sub>f x1 OR x2  ;  P ; G \<turnstile> i\<rbrakk> \<Longrightarrow> Ex (eval_c i (x1 OR x2 ))
 5. \<And>x. \<lbrakk>\<lbrakk> P ; B ; G   \<turnstile>\<^sub>w\<^sub>f x ;  P ; G \<turnstile> i\<rbrakk> \<Longrightarrow> Ex (eval_c i x);  P ; B ; G   \<turnstile>\<^sub>w\<^sub>f \<not> x  ;  P ; G \<turnstile> i\<rbrakk> \<Longrightarrow> Ex (eval_c i (\<not> x ))
 6. \<And>x1 x2. \<lbrakk>\<lbrakk> P ; B ; G   \<turnstile>\<^sub>w\<^sub>f x1 ;  P ; G \<turnstile> i\<rbrakk> \<Longrightarrow> Ex (eval_c i x1); \<lbrakk> P ; B ; G   \<turnstile>\<^sub>w\<^sub>f x2 ;  P ; G \<turnstile> i\<rbrakk> \<Longrightarrow> Ex (eval_c i x2);  P ; B ; G   \<turnstile>\<^sub>w\<^sub>f x1  IMP  x2  ;  P ; G \<turnstile> i\<rbrakk> \<Longrightarrow> Ex (eval_c i (x1  IMP  x2 ))
 7. \<And>x1 x2. \<lbrakk> P ; B ; G   \<turnstile>\<^sub>w\<^sub>f x1  ==  x2  ;  P ; G \<turnstile> i\<rbrakk> \<Longrightarrow> Ex (eval_c i (x1  ==  x2 ))
[PROOF STEP]
qed(metis wfC_elims wfI_wfCE_eval_e eval_c.intros)+


[STATEMENT]
lemma satis_reflI:
  fixes c::c
  assumes "i \<Turnstile> ((x, b, c) #\<^sub>\<Gamma> G)"
  shows "i \<Turnstile> c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  i \<Turnstile> c
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
 i \<Turnstile> (x, b, c) #\<^sub>\<Gamma> G

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


[STATEMENT]
lemma is_satis_mp:
  fixes c1::c and c2::c
  assumes "i \<Turnstile> (c1 IMP c2)" and "i \<Turnstile> c1"
  shows "i \<Turnstile> c2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  i \<Turnstile> c2
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
 i \<Turnstile> c1  IMP  c2
 i \<Turnstile> c1

goal (1 subgoal):
 1.  i \<Turnstile> c2
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk> i \<Turnstile> c1  IMP  c2  ;  i \<Turnstile> c1 \<rbrakk> \<Longrightarrow>  i \<Turnstile> c2
[PROOF STEP]
have "eval_c i (c1 IMP c2) True"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  i \<lbrakk> c1  IMP  c2  \<rbrakk> ~ True
[PROOF STEP]
using is_satis.simps
[PROOF STATE]
proof (prove)
using this:
 ?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 \<lbrakk> c1  IMP  c2  \<rbrakk> ~ True
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
 ?a1.0 \<Turnstile> ?a2.0  = (\<exists>i c. ?a1.0 = i \<and> ?a2.0 = c \<and>  i \<lbrakk> c \<rbrakk> ~ True )
 i \<Turnstile> c1  IMP  c2
 i \<Turnstile> c1

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

goal (1 subgoal):
 1. \<lbrakk> i \<Turnstile> c1  IMP  c2  ;  i \<Turnstile> c1 \<rbrakk> \<Longrightarrow>  i \<Turnstile> c2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
 i \<lbrakk> c1  IMP  c2  \<rbrakk> ~ True
[PROOF STEP]
obtain b1 and b2 where "True = (b1 \<longrightarrow> b2) \<and> eval_c i c1 b1 \<and> eval_c i c2 b2"
[PROOF STATE]
proof (prove)
using this:
 i \<lbrakk> c1  IMP  c2  \<rbrakk> ~ True

goal (1 subgoal):
 1. (\<And>b1 b2. True = (b1 \<longrightarrow> b2) \<and>  i \<lbrakk> c1 \<rbrakk> ~ b1  \<and>  i \<lbrakk> c2 \<rbrakk> ~ b2  \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using eval_c_elims(5)
[PROOF STATE]
proof (prove)
using this:
 i \<lbrakk> c1  IMP  c2  \<rbrakk> ~ True
\<lbrakk> ?i \<lbrakk> ?c1.0  IMP  ?c2.0  \<rbrakk> ~ ?s ; \<And>b1 b2. \<lbrakk>?s = (b1 \<longrightarrow> b2);  ?i \<lbrakk> ?c1.0 \<rbrakk> ~ b1 ;  ?i \<lbrakk> ?c2.0 \<rbrakk> ~ b2 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

goal (1 subgoal):
 1. (\<And>b1 b2. True = (b1 \<longrightarrow> b2) \<and>  i \<lbrakk> c1 \<rbrakk> ~ b1  \<and>  i \<lbrakk> c2 \<rbrakk> ~ b2  \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
True = (b1 \<longrightarrow> b2) \<and>  i \<lbrakk> c1 \<rbrakk> ~ b1  \<and>  i \<lbrakk> c2 \<rbrakk> ~ b2

goal (1 subgoal):
 1. \<lbrakk> i \<Turnstile> c1  IMP  c2  ;  i \<Turnstile> c1 \<rbrakk> \<Longrightarrow>  i \<Turnstile> c2
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
True = (b1 \<longrightarrow> b2) \<and>  i \<lbrakk> c1 \<rbrakk> ~ b1  \<and>  i \<lbrakk> c2 \<rbrakk> ~ b2

goal (1 subgoal):
 1. \<lbrakk> i \<Turnstile> c1  IMP  c2  ;  i \<Turnstile> c1 \<rbrakk> \<Longrightarrow>  i \<Turnstile> c2
[PROOF STEP]
have "eval_c i c1 True"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  i \<lbrakk> c1 \<rbrakk> ~ True
[PROOF STEP]
using is_satis.simps
[PROOF STATE]
proof (prove)
using this:
 ?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 \<lbrakk> c1 \<rbrakk> ~ True
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
 ?a1.0 \<Turnstile> ?a2.0  = (\<exists>i c. ?a1.0 = i \<and> ?a2.0 = c \<and>  i \<lbrakk> c \<rbrakk> ~ True )
 i \<Turnstile> c1  IMP  c2
 i \<Turnstile> c1

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

goal (1 subgoal):
 1. \<lbrakk> i \<Turnstile> c1  IMP  c2  ;  i \<Turnstile> c1 \<rbrakk> \<Longrightarrow>  i \<Turnstile> c2
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
 i \<lbrakk> c1 \<rbrakk> ~ True

goal (1 subgoal):
 1. \<lbrakk> i \<Turnstile> c1  IMP  c2  ;  i \<Turnstile> c1 \<rbrakk> \<Longrightarrow>  i \<Turnstile> c2
[PROOF STEP]
have "b1 = True"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b1 = True
[PROOF STEP]
using calculation eval_c_uniqueness
[PROOF STATE]
proof (prove)
using this:
True = (b1 \<longrightarrow> b2) \<and>  i \<lbrakk> c1 \<rbrakk> ~ b1  \<and>  i \<lbrakk> c2 \<rbrakk> ~ b2
 i \<lbrakk> c1 \<rbrakk> ~ True
\<lbrakk> ?i \<lbrakk> ?c \<rbrakk> ~ ?s ;  ?i \<lbrakk> ?c \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> ?s = ?s'

goal (1 subgoal):
 1. b1 = True
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
b1 = True

goal (1 subgoal):
 1. \<lbrakk> i \<Turnstile> c1  IMP  c2  ;  i \<Turnstile> c1 \<rbrakk> \<Longrightarrow>  i \<Turnstile> c2
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
True = (b1 \<longrightarrow> b2) \<and>  i \<lbrakk> c1 \<rbrakk> ~ b1  \<and>  i \<lbrakk> c2 \<rbrakk> ~ b2
 i \<lbrakk> c1 \<rbrakk> ~ True
b1 = True
[PROOF STEP]
have "eval_c i c2 True"
[PROOF STATE]
proof (prove)
using this:
True = (b1 \<longrightarrow> b2) \<and>  i \<lbrakk> c1 \<rbrakk> ~ b1  \<and>  i \<lbrakk> c2 \<rbrakk> ~ b2
 i \<lbrakk> c1 \<rbrakk> ~ True
b1 = True

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

goal (1 subgoal):
 1. \<lbrakk> i \<Turnstile> c1  IMP  c2  ;  i \<Turnstile> c1 \<rbrakk> \<Longrightarrow>  i \<Turnstile> c2
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
 i \<lbrakk> c2 \<rbrakk> ~ True

goal (1 subgoal):
 1.  i \<Turnstile> c2
[PROOF STEP]
using is_satis.intros
[PROOF STATE]
proof (prove)
using this:
 i \<lbrakk> c2 \<rbrakk> ~ True
 ?i \<lbrakk> ?c \<rbrakk> ~ True  \<Longrightarrow>  ?i \<Turnstile> ?c

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

goal:
No subgoals!
[PROOF STEP]
qed