[STATEMENT]
lemma subst_c_eval_v[simp]:
  fixes v::v and c :: c
  assumes "i \<lbrakk> v \<rbrakk> ~  s" and "i \<lbrakk> c[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1" and
    "(i ( x \<mapsto> s)) \<lbrakk> c \<rbrakk> ~ s2"
  shows "s1 = s2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s1 = s2
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> v \<rbrakk> ~ s
 i \<lbrakk> c[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1
 i(x \<mapsto> s) \<lbrakk> c \<rbrakk> ~ s2

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

goal (7 subgoals):
 1. \<And>s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> (TRUE)[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> TRUE \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2
 2. \<And>s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> (FALSE)[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> FALSE \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2
 3. \<And>x1 x2 s1 s2. \<lbrakk>\<And>s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> x1[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2; \<And>s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> x2[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x2 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2; i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> (x1  AND  x2 )[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1  AND  x2  \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2
 4. \<And>x1 x2 s1 s2. \<lbrakk>\<And>s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> x1[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2; \<And>s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> x2[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x2 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2; i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> (x1 OR x2 )[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1 OR x2  \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2
 5. \<And>xa s1 s2. \<lbrakk>\<And>s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> xa[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> xa \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2; i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> (\<not> xa )[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> \<not> xa  \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2
 6. \<And>x1 x2 s1 s2. \<lbrakk>\<And>s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> x1[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2; \<And>s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> x2[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x2 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2; i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> (x1  IMP  x2 )[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1  IMP  x2  \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2
 7. \<And>x1 x2 s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> (x1  ==  x2 )[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1  ==  x2  \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2
[PROOF STEP]
hence "s1 = True \<and> s2 = True"
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> v \<rbrakk> ~ s
 i \<lbrakk> (TRUE)[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1
 i(x \<mapsto> s) \<lbrakk> TRUE \<rbrakk> ~ s2

goal (1 subgoal):
 1. s1 = True \<and> s2 = True
[PROOF STEP]
using eval_c_elims subst_cv.simps
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> v \<rbrakk> ~ s
 i \<lbrakk> (TRUE)[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1
 i(x \<mapsto> s) \<lbrakk> TRUE \<rbrakk> ~ s2
\<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
(TRUE)[?x::=?v]\<^sub>c\<^sub>v = (TRUE)
(FALSE)[?x::=?v]\<^sub>c\<^sub>v = (FALSE)
(?c1.0  AND  ?c2.0 )[?x::=?v]\<^sub>c\<^sub>v = (?c1.0[?x::=?v]\<^sub>c\<^sub>v  AND  ?c2.0[?x::=?v]\<^sub>c\<^sub>v )
(?c1.0 OR ?c2.0 )[?x::=?v]\<^sub>c\<^sub>v = (?c1.0[?x::=?v]\<^sub>c\<^sub>v OR ?c2.0[?x::=?v]\<^sub>c\<^sub>v )
(?c1.0  IMP  ?c2.0 )[?x::=?v]\<^sub>c\<^sub>v = (?c1.0[?x::=?v]\<^sub>c\<^sub>v  IMP  ?c2.0[?x::=?v]\<^sub>c\<^sub>v )
(?e1.0  ==  ?e2.0 )[?x::=?v]\<^sub>c\<^sub>v = (?e1.0[?x::=?v]\<^sub>c\<^sub>e\<^sub>v  ==  ?e2.0[?x::=?v]\<^sub>c\<^sub>e\<^sub>v )
(\<not> ?c )[?x::=?v]\<^sub>c\<^sub>v = (\<not> ?c[?x::=?v]\<^sub>c\<^sub>v )

goal (1 subgoal):
 1. s1 = True \<and> s2 = True
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
s1 = True \<and> s2 = True

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

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

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

goal (6 subgoals):
 1. \<And>s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> (FALSE)[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> FALSE \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2
 2. \<And>x1 x2 s1 s2. \<lbrakk>\<And>s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> x1[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2; \<And>s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> x2[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x2 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2; i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> (x1  AND  x2 )[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1  AND  x2  \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2
 3. \<And>x1 x2 s1 s2. \<lbrakk>\<And>s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> x1[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2; \<And>s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> x2[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x2 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2; i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> (x1 OR x2 )[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1 OR x2  \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2
 4. \<And>xa s1 s2. \<lbrakk>\<And>s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> xa[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> xa \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2; i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> (\<not> xa )[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> \<not> xa  \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2
 5. \<And>x1 x2 s1 s2. \<lbrakk>\<And>s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> x1[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2; \<And>s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> x2[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x2 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2; i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> (x1  IMP  x2 )[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1  IMP  x2  \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2
 6. \<And>x1 x2 s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> (x1  ==  x2 )[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1  ==  x2  \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2
[PROOF STEP]
hence "s1 = False \<and> s2 = False"
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> v \<rbrakk> ~ s
 i \<lbrakk> (FALSE)[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1
 i(x \<mapsto> s) \<lbrakk> FALSE \<rbrakk> ~ s2

goal (1 subgoal):
 1. s1 = False \<and> s2 = False
[PROOF STEP]
using eval_c_elims subst_cv.simps
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> v \<rbrakk> ~ s
 i \<lbrakk> (FALSE)[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1
 i(x \<mapsto> s) \<lbrakk> FALSE \<rbrakk> ~ s2
\<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
(TRUE)[?x::=?v]\<^sub>c\<^sub>v = (TRUE)
(FALSE)[?x::=?v]\<^sub>c\<^sub>v = (FALSE)
(?c1.0  AND  ?c2.0 )[?x::=?v]\<^sub>c\<^sub>v = (?c1.0[?x::=?v]\<^sub>c\<^sub>v  AND  ?c2.0[?x::=?v]\<^sub>c\<^sub>v )
(?c1.0 OR ?c2.0 )[?x::=?v]\<^sub>c\<^sub>v = (?c1.0[?x::=?v]\<^sub>c\<^sub>v OR ?c2.0[?x::=?v]\<^sub>c\<^sub>v )
(?c1.0  IMP  ?c2.0 )[?x::=?v]\<^sub>c\<^sub>v = (?c1.0[?x::=?v]\<^sub>c\<^sub>v  IMP  ?c2.0[?x::=?v]\<^sub>c\<^sub>v )
(?e1.0  ==  ?e2.0 )[?x::=?v]\<^sub>c\<^sub>v = (?e1.0[?x::=?v]\<^sub>c\<^sub>e\<^sub>v  ==  ?e2.0[?x::=?v]\<^sub>c\<^sub>e\<^sub>v )
(\<not> ?c )[?x::=?v]\<^sub>c\<^sub>v = (\<not> ?c[?x::=?v]\<^sub>c\<^sub>v )

goal (1 subgoal):
 1. s1 = False \<and> s2 = False
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
s1 = False \<and> s2 = False

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

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

goal (5 subgoals):
 1. \<And>x1 x2 s1 s2. \<lbrakk>\<And>s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> x1[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2; \<And>s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> x2[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x2 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2; i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> (x1  AND  x2 )[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1  AND  x2  \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2
 2. \<And>x1 x2 s1 s2. \<lbrakk>\<And>s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> x1[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2; \<And>s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> x2[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x2 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2; i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> (x1 OR x2 )[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1 OR x2  \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2
 3. \<And>xa s1 s2. \<lbrakk>\<And>s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> xa[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> xa \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2; i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> (\<not> xa )[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> \<not> xa  \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2
 4. \<And>x1 x2 s1 s2. \<lbrakk>\<And>s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> x1[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2; \<And>s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> x2[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x2 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2; i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> (x1  IMP  x2 )[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1  IMP  x2  \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2
 5. \<And>x1 x2 s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> (x1  ==  x2 )[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1  ==  x2  \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>x1 x2 s1 s2. \<lbrakk>\<And>s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> x1[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2; \<And>s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> x2[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x2 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2; i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> (x1  AND  x2 )[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1  AND  x2  \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2
 2. \<And>x1 x2 s1 s2. \<lbrakk>\<And>s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> x1[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2; \<And>s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> x2[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x2 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2; i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> (x1 OR x2 )[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1 OR x2  \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2
 3. \<And>xa s1 s2. \<lbrakk>\<And>s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> xa[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> xa \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2; i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> (\<not> xa )[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> \<not> xa  \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2
 4. \<And>x1 x2 s1 s2. \<lbrakk>\<And>s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> x1[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2; \<And>s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> x2[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x2 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2; i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> (x1  IMP  x2 )[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1  IMP  x2  \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2
 5. \<And>x1 x2 s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> (x1  ==  x2 )[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1  ==  x2  \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2
[PROOF STEP]
case (C_conj c1 c2)
[PROOF STATE]
proof (state)
this:
\<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> c1[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ ?s1.0 ;  i(x \<mapsto> s) \<lbrakk> c1 \<rbrakk> ~ ?s2.0 \<rbrakk> \<Longrightarrow> ?s1.0 = ?s2.0
\<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> c2[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ ?s1.0 ;  i(x \<mapsto> s) \<lbrakk> c2 \<rbrakk> ~ ?s2.0 \<rbrakk> \<Longrightarrow> ?s1.0 = ?s2.0
i \<lbrakk> v \<rbrakk> ~ s
 i \<lbrakk> (c1  AND  c2 )[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1
 i(x \<mapsto> s) \<lbrakk> c1  AND  c2  \<rbrakk> ~ s2

goal (5 subgoals):
 1. \<And>x1 x2 s1 s2. \<lbrakk>\<And>s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> x1[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2; \<And>s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> x2[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x2 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2; i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> (x1  AND  x2 )[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1  AND  x2  \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2
 2. \<And>x1 x2 s1 s2. \<lbrakk>\<And>s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> x1[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2; \<And>s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> x2[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x2 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2; i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> (x1 OR x2 )[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1 OR x2  \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2
 3. \<And>xa s1 s2. \<lbrakk>\<And>s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> xa[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> xa \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2; i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> (\<not> xa )[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> \<not> xa  \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2
 4. \<And>x1 x2 s1 s2. \<lbrakk>\<And>s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> x1[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2; \<And>s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> x2[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x2 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2; i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> (x1  IMP  x2 )[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1  IMP  x2  \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2
 5. \<And>x1 x2 s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> (x1  ==  x2 )[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1  ==  x2  \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2
[PROOF STEP]
hence *:"eval_c i (c1[x::=v]\<^sub>c\<^sub>v AND c2[x::=v]\<^sub>c\<^sub>v) s1"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> c1[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ ?s1.0 ;  i(x \<mapsto> s) \<lbrakk> c1 \<rbrakk> ~ ?s2.0 \<rbrakk> \<Longrightarrow> ?s1.0 = ?s2.0
\<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> c2[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ ?s1.0 ;  i(x \<mapsto> s) \<lbrakk> c2 \<rbrakk> ~ ?s2.0 \<rbrakk> \<Longrightarrow> ?s1.0 = ?s2.0
i \<lbrakk> v \<rbrakk> ~ s
 i \<lbrakk> (c1  AND  c2 )[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1
 i(x \<mapsto> s) \<lbrakk> c1  AND  c2  \<rbrakk> ~ s2

goal (1 subgoal):
 1.  i \<lbrakk> c1[x::=v]\<^sub>c\<^sub>v  AND  c2[x::=v]\<^sub>c\<^sub>v  \<rbrakk> ~ s1
[PROOF STEP]
using subst_cv.simps
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> c1[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ ?s1.0 ;  i(x \<mapsto> s) \<lbrakk> c1 \<rbrakk> ~ ?s2.0 \<rbrakk> \<Longrightarrow> ?s1.0 = ?s2.0
\<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> c2[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ ?s1.0 ;  i(x \<mapsto> s) \<lbrakk> c2 \<rbrakk> ~ ?s2.0 \<rbrakk> \<Longrightarrow> ?s1.0 = ?s2.0
i \<lbrakk> v \<rbrakk> ~ s
 i \<lbrakk> (c1  AND  c2 )[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1
 i(x \<mapsto> s) \<lbrakk> c1  AND  c2  \<rbrakk> ~ s2
(TRUE)[?x::=?v]\<^sub>c\<^sub>v = (TRUE)
(FALSE)[?x::=?v]\<^sub>c\<^sub>v = (FALSE)
(?c1.0  AND  ?c2.0 )[?x::=?v]\<^sub>c\<^sub>v = (?c1.0[?x::=?v]\<^sub>c\<^sub>v  AND  ?c2.0[?x::=?v]\<^sub>c\<^sub>v )
(?c1.0 OR ?c2.0 )[?x::=?v]\<^sub>c\<^sub>v = (?c1.0[?x::=?v]\<^sub>c\<^sub>v OR ?c2.0[?x::=?v]\<^sub>c\<^sub>v )
(?c1.0  IMP  ?c2.0 )[?x::=?v]\<^sub>c\<^sub>v = (?c1.0[?x::=?v]\<^sub>c\<^sub>v  IMP  ?c2.0[?x::=?v]\<^sub>c\<^sub>v )
(?e1.0  ==  ?e2.0 )[?x::=?v]\<^sub>c\<^sub>v = (?e1.0[?x::=?v]\<^sub>c\<^sub>e\<^sub>v  ==  ?e2.0[?x::=?v]\<^sub>c\<^sub>e\<^sub>v )
(\<not> ?c )[?x::=?v]\<^sub>c\<^sub>v = (\<not> ?c[?x::=?v]\<^sub>c\<^sub>v )

goal (1 subgoal):
 1.  i \<lbrakk> c1[x::=v]\<^sub>c\<^sub>v  AND  c2[x::=v]\<^sub>c\<^sub>v  \<rbrakk> ~ s1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
 i \<lbrakk> c1[x::=v]\<^sub>c\<^sub>v  AND  c2[x::=v]\<^sub>c\<^sub>v  \<rbrakk> ~ s1

goal (5 subgoals):
 1. \<And>x1 x2 s1 s2. \<lbrakk>\<And>s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> x1[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2; \<And>s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> x2[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x2 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2; i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> (x1  AND  x2 )[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1  AND  x2  \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2
 2. \<And>x1 x2 s1 s2. \<lbrakk>\<And>s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> x1[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2; \<And>s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> x2[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x2 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2; i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> (x1 OR x2 )[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1 OR x2  \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2
 3. \<And>xa s1 s2. \<lbrakk>\<And>s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> xa[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> xa \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2; i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> (\<not> xa )[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> \<not> xa  \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2
 4. \<And>x1 x2 s1 s2. \<lbrakk>\<And>s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> x1[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2; \<And>s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> x2[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x2 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2; i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> (x1  IMP  x2 )[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1  IMP  x2  \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2
 5. \<And>x1 x2 s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> (x1  ==  x2 )[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1  ==  x2  \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
 i \<lbrakk> c1[x::=v]\<^sub>c\<^sub>v  AND  c2[x::=v]\<^sub>c\<^sub>v  \<rbrakk> ~ s1
[PROOF STEP]
obtain s11 and s12 where "(s1 = (s11 \<and> s12)) \<and> eval_c i c1[x::=v]\<^sub>c\<^sub>v s11 \<and> eval_c i c2[x::=v]\<^sub>c\<^sub>v s12"
[PROOF STATE]
proof (prove)
using this:
 i \<lbrakk> c1[x::=v]\<^sub>c\<^sub>v  AND  c2[x::=v]\<^sub>c\<^sub>v  \<rbrakk> ~ s1

goal (1 subgoal):
 1. (\<And>s11 s12. s1 = (s11 \<and> s12) \<and>  i \<lbrakk> c1[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s11  \<and>  i \<lbrakk> c2[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s12  \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using
      eval_c_elims(3)
[PROOF STATE]
proof (prove)
using this:
 i \<lbrakk> c1[x::=v]\<^sub>c\<^sub>v  AND  c2[x::=v]\<^sub>c\<^sub>v  \<rbrakk> ~ s1
\<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. (\<And>s11 s12. s1 = (s11 \<and> s12) \<and>  i \<lbrakk> c1[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s11  \<and>  i \<lbrakk> c2[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s12  \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
s1 = (s11 \<and> s12) \<and>  i \<lbrakk> c1[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s11  \<and>  i \<lbrakk> c2[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s12

goal (5 subgoals):
 1. \<And>x1 x2 s1 s2. \<lbrakk>\<And>s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> x1[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2; \<And>s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> x2[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x2 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2; i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> (x1  AND  x2 )[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1  AND  x2  \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2
 2. \<And>x1 x2 s1 s2. \<lbrakk>\<And>s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> x1[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2; \<And>s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> x2[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x2 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2; i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> (x1 OR x2 )[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1 OR x2  \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2
 3. \<And>xa s1 s2. \<lbrakk>\<And>s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> xa[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> xa \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2; i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> (\<not> xa )[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> \<not> xa  \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2
 4. \<And>x1 x2 s1 s2. \<lbrakk>\<And>s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> x1[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2; \<And>s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> x2[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x2 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2; i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> (x1  IMP  x2 )[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1  IMP  x2  \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2
 5. \<And>x1 x2 s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> (x1  ==  x2 )[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1  ==  x2  \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
s1 = (s11 \<and> s12) \<and>  i \<lbrakk> c1[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s11  \<and>  i \<lbrakk> c2[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s12

goal (5 subgoals):
 1. \<And>x1 x2 s1 s2. \<lbrakk>\<And>s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> x1[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2; \<And>s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> x2[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x2 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2; i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> (x1  AND  x2 )[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1  AND  x2  \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2
 2. \<And>x1 x2 s1 s2. \<lbrakk>\<And>s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> x1[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2; \<And>s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> x2[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x2 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2; i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> (x1 OR x2 )[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1 OR x2  \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2
 3. \<And>xa s1 s2. \<lbrakk>\<And>s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> xa[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> xa \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2; i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> (\<not> xa )[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> \<not> xa  \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2
 4. \<And>x1 x2 s1 s2. \<lbrakk>\<And>s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> x1[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2; \<And>s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> x2[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x2 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2; i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> (x1  IMP  x2 )[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1  IMP  x2  \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2
 5. \<And>x1 x2 s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> (x1  ==  x2 )[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1  ==  x2  \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2
[PROOF STEP]
obtain   s21 and s22 where "eval_c  (i ( x \<mapsto> s)) c1 s21 \<and> eval_c  (i ( x \<mapsto> s)) c2 s22 \<and> (s2 = (s21 \<and> s22))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>s21 s22.  i(x \<mapsto> s) \<lbrakk> c1 \<rbrakk> ~ s21  \<and>  i(x \<mapsto> s) \<lbrakk> c2 \<rbrakk> ~ s22  \<and> s2 = (s21 \<and> s22) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using
      eval_c_elims(3) C_conj
[PROOF STATE]
proof (prove)
using this:
\<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> v \<rbrakk> ~ s ;  i \<lbrakk> c1[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ ?s1.0 ;  i(x \<mapsto> s) \<lbrakk> c1 \<rbrakk> ~ ?s2.0 \<rbrakk> \<Longrightarrow> ?s1.0 = ?s2.0
\<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> c2[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ ?s1.0 ;  i(x \<mapsto> s) \<lbrakk> c2 \<rbrakk> ~ ?s2.0 \<rbrakk> \<Longrightarrow> ?s1.0 = ?s2.0
i \<lbrakk> v \<rbrakk> ~ s
 i \<lbrakk> (c1  AND  c2 )[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1
 i(x \<mapsto> s) \<lbrakk> c1  AND  c2  \<rbrakk> ~ s2

goal (1 subgoal):
 1. (\<And>s21 s22.  i(x \<mapsto> s) \<lbrakk> c1 \<rbrakk> ~ s21  \<and>  i(x \<mapsto> s) \<lbrakk> c2 \<rbrakk> ~ s22  \<and> s2 = (s21 \<and> s22) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
 i(x \<mapsto> s) \<lbrakk> c1 \<rbrakk> ~ s21  \<and>  i(x \<mapsto> s) \<lbrakk> c2 \<rbrakk> ~ s22  \<and> s2 = (s21 \<and> s22)

goal (5 subgoals):
 1. \<And>x1 x2 s1 s2. \<lbrakk>\<And>s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> x1[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2; \<And>s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> x2[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x2 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2; i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> (x1  AND  x2 )[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1  AND  x2  \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2
 2. \<And>x1 x2 s1 s2. \<lbrakk>\<And>s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> x1[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2; \<And>s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> x2[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x2 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2; i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> (x1 OR x2 )[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1 OR x2  \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2
 3. \<And>xa s1 s2. \<lbrakk>\<And>s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> xa[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> xa \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2; i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> (\<not> xa )[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> \<not> xa  \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2
 4. \<And>x1 x2 s1 s2. \<lbrakk>\<And>s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> x1[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2; \<And>s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> x2[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x2 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2; i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> (x1  IMP  x2 )[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1  IMP  x2  \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2
 5. \<And>x1 x2 s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> (x1  ==  x2 )[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1  ==  x2  \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
s1 = (s11 \<and> s12) \<and>  i \<lbrakk> c1[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s11  \<and>  i \<lbrakk> c2[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s12
 i(x \<mapsto> s) \<lbrakk> c1 \<rbrakk> ~ s21  \<and>  i(x \<mapsto> s) \<lbrakk> c2 \<rbrakk> ~ s22  \<and> s2 = (s21 \<and> s22)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
s1 = (s11 \<and> s12) \<and>  i \<lbrakk> c1[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s11  \<and>  i \<lbrakk> c2[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s12
 i(x \<mapsto> s) \<lbrakk> c1 \<rbrakk> ~ s21  \<and>  i(x \<mapsto> s) \<lbrakk> c2 \<rbrakk> ~ s22  \<and> s2 = (s21 \<and> s22)

goal (1 subgoal):
 1. s1 = s2
[PROOF STEP]
using C_conj
[PROOF STATE]
proof (prove)
using this:
s1 = (s11 \<and> s12) \<and>  i \<lbrakk> c1[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s11  \<and>  i \<lbrakk> c2[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s12
 i(x \<mapsto> s) \<lbrakk> c1 \<rbrakk> ~ s21  \<and>  i(x \<mapsto> s) \<lbrakk> c2 \<rbrakk> ~ s22  \<and> s2 = (s21 \<and> s22)
\<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> c1[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ ?s1.0 ;  i(x \<mapsto> s) \<lbrakk> c1 \<rbrakk> ~ ?s2.0 \<rbrakk> \<Longrightarrow> ?s1.0 = ?s2.0
\<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> c2[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ ?s1.0 ;  i(x \<mapsto> s) \<lbrakk> c2 \<rbrakk> ~ ?s2.0 \<rbrakk> \<Longrightarrow> ?s1.0 = ?s2.0
i \<lbrakk> v \<rbrakk> ~ s
 i \<lbrakk> (c1  AND  c2 )[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1
 i(x \<mapsto> s) \<lbrakk> c1  AND  c2  \<rbrakk> ~ s2

goal (1 subgoal):
 1. s1 = s2
[PROOF STEP]
by (meson eval_c_elims)
[PROOF STATE]
proof (state)
this:
s1 = s2

goal (4 subgoals):
 1. \<And>x1 x2 s1 s2. \<lbrakk>\<And>s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> x1[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2; \<And>s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> x2[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x2 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2; i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> (x1 OR x2 )[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1 OR x2  \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2
 2. \<And>xa s1 s2. \<lbrakk>\<And>s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> xa[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> xa \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2; i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> (\<not> xa )[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> \<not> xa  \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2
 3. \<And>x1 x2 s1 s2. \<lbrakk>\<And>s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> x1[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2; \<And>s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> x2[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x2 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2; i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> (x1  IMP  x2 )[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1  IMP  x2  \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2
 4. \<And>x1 x2 s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> (x1  ==  x2 )[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1  ==  x2  \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>x1 x2 s1 s2. \<lbrakk>\<And>s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> x1[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2; \<And>s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> x2[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x2 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2; i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> (x1 OR x2 )[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1 OR x2  \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2
 2. \<And>xa s1 s2. \<lbrakk>\<And>s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> xa[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> xa \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2; i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> (\<not> xa )[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> \<not> xa  \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2
 3. \<And>x1 x2 s1 s2. \<lbrakk>\<And>s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> x1[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2; \<And>s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> x2[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x2 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2; i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> (x1  IMP  x2 )[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1  IMP  x2  \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2
 4. \<And>x1 x2 s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> (x1  ==  x2 )[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1  ==  x2  \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2
[PROOF STEP]
case (C_disj c1 c2)
[PROOF STATE]
proof (state)
this:
\<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> c1[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ ?s1.0 ;  i(x \<mapsto> s) \<lbrakk> c1 \<rbrakk> ~ ?s2.0 \<rbrakk> \<Longrightarrow> ?s1.0 = ?s2.0
\<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> c2[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ ?s1.0 ;  i(x \<mapsto> s) \<lbrakk> c2 \<rbrakk> ~ ?s2.0 \<rbrakk> \<Longrightarrow> ?s1.0 = ?s2.0
i \<lbrakk> v \<rbrakk> ~ s
 i \<lbrakk> (c1 OR c2 )[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1
 i(x \<mapsto> s) \<lbrakk> c1 OR c2  \<rbrakk> ~ s2

goal (4 subgoals):
 1. \<And>x1 x2 s1 s2. \<lbrakk>\<And>s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> x1[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2; \<And>s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> x2[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x2 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2; i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> (x1 OR x2 )[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1 OR x2  \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2
 2. \<And>xa s1 s2. \<lbrakk>\<And>s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> xa[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> xa \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2; i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> (\<not> xa )[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> \<not> xa  \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2
 3. \<And>x1 x2 s1 s2. \<lbrakk>\<And>s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> x1[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2; \<And>s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> x2[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x2 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2; i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> (x1  IMP  x2 )[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1  IMP  x2  \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2
 4. \<And>x1 x2 s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> (x1  ==  x2 )[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1  ==  x2  \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2
[PROOF STEP]
hence *:"eval_c i (c1[x::=v]\<^sub>c\<^sub>v OR c2[x::=v]\<^sub>c\<^sub>v) s1"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> c1[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ ?s1.0 ;  i(x \<mapsto> s) \<lbrakk> c1 \<rbrakk> ~ ?s2.0 \<rbrakk> \<Longrightarrow> ?s1.0 = ?s2.0
\<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> c2[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ ?s1.0 ;  i(x \<mapsto> s) \<lbrakk> c2 \<rbrakk> ~ ?s2.0 \<rbrakk> \<Longrightarrow> ?s1.0 = ?s2.0
i \<lbrakk> v \<rbrakk> ~ s
 i \<lbrakk> (c1 OR c2 )[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1
 i(x \<mapsto> s) \<lbrakk> c1 OR c2  \<rbrakk> ~ s2

goal (1 subgoal):
 1.  i \<lbrakk> c1[x::=v]\<^sub>c\<^sub>v OR c2[x::=v]\<^sub>c\<^sub>v  \<rbrakk> ~ s1
[PROOF STEP]
using subst_cv.simps
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> c1[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ ?s1.0 ;  i(x \<mapsto> s) \<lbrakk> c1 \<rbrakk> ~ ?s2.0 \<rbrakk> \<Longrightarrow> ?s1.0 = ?s2.0
\<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> c2[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ ?s1.0 ;  i(x \<mapsto> s) \<lbrakk> c2 \<rbrakk> ~ ?s2.0 \<rbrakk> \<Longrightarrow> ?s1.0 = ?s2.0
i \<lbrakk> v \<rbrakk> ~ s
 i \<lbrakk> (c1 OR c2 )[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1
 i(x \<mapsto> s) \<lbrakk> c1 OR c2  \<rbrakk> ~ s2
(TRUE)[?x::=?v]\<^sub>c\<^sub>v = (TRUE)
(FALSE)[?x::=?v]\<^sub>c\<^sub>v = (FALSE)
(?c1.0  AND  ?c2.0 )[?x::=?v]\<^sub>c\<^sub>v = (?c1.0[?x::=?v]\<^sub>c\<^sub>v  AND  ?c2.0[?x::=?v]\<^sub>c\<^sub>v )
(?c1.0 OR ?c2.0 )[?x::=?v]\<^sub>c\<^sub>v = (?c1.0[?x::=?v]\<^sub>c\<^sub>v OR ?c2.0[?x::=?v]\<^sub>c\<^sub>v )
(?c1.0  IMP  ?c2.0 )[?x::=?v]\<^sub>c\<^sub>v = (?c1.0[?x::=?v]\<^sub>c\<^sub>v  IMP  ?c2.0[?x::=?v]\<^sub>c\<^sub>v )
(?e1.0  ==  ?e2.0 )[?x::=?v]\<^sub>c\<^sub>v = (?e1.0[?x::=?v]\<^sub>c\<^sub>e\<^sub>v  ==  ?e2.0[?x::=?v]\<^sub>c\<^sub>e\<^sub>v )
(\<not> ?c )[?x::=?v]\<^sub>c\<^sub>v = (\<not> ?c[?x::=?v]\<^sub>c\<^sub>v )

goal (1 subgoal):
 1.  i \<lbrakk> c1[x::=v]\<^sub>c\<^sub>v OR c2[x::=v]\<^sub>c\<^sub>v  \<rbrakk> ~ s1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
 i \<lbrakk> c1[x::=v]\<^sub>c\<^sub>v OR c2[x::=v]\<^sub>c\<^sub>v  \<rbrakk> ~ s1

goal (4 subgoals):
 1. \<And>x1 x2 s1 s2. \<lbrakk>\<And>s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> x1[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2; \<And>s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> x2[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x2 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2; i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> (x1 OR x2 )[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1 OR x2  \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2
 2. \<And>xa s1 s2. \<lbrakk>\<And>s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> xa[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> xa \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2; i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> (\<not> xa )[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> \<not> xa  \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2
 3. \<And>x1 x2 s1 s2. \<lbrakk>\<And>s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> x1[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2; \<And>s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> x2[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x2 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2; i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> (x1  IMP  x2 )[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1  IMP  x2  \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2
 4. \<And>x1 x2 s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> (x1  ==  x2 )[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1  ==  x2  \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
 i \<lbrakk> c1[x::=v]\<^sub>c\<^sub>v OR c2[x::=v]\<^sub>c\<^sub>v  \<rbrakk> ~ s1
[PROOF STEP]
obtain s11 and s12 where "(s1 = (s11 \<or> s12)) \<and> eval_c i c1[x::=v]\<^sub>c\<^sub>v s11 \<and> eval_c i c2[x::=v]\<^sub>c\<^sub>v s12"
[PROOF STATE]
proof (prove)
using this:
 i \<lbrakk> c1[x::=v]\<^sub>c\<^sub>v OR c2[x::=v]\<^sub>c\<^sub>v  \<rbrakk> ~ s1

goal (1 subgoal):
 1. (\<And>s11 s12. s1 = (s11 \<or> s12) \<and>  i \<lbrakk> c1[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s11  \<and>  i \<lbrakk> c2[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s12  \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using
      eval_c_elims(4)
[PROOF STATE]
proof (prove)
using this:
 i \<lbrakk> c1[x::=v]\<^sub>c\<^sub>v OR c2[x::=v]\<^sub>c\<^sub>v  \<rbrakk> ~ s1
\<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. (\<And>s11 s12. s1 = (s11 \<or> s12) \<and>  i \<lbrakk> c1[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s11  \<and>  i \<lbrakk> c2[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s12  \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
s1 = (s11 \<or> s12) \<and>  i \<lbrakk> c1[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s11  \<and>  i \<lbrakk> c2[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s12

goal (4 subgoals):
 1. \<And>x1 x2 s1 s2. \<lbrakk>\<And>s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> x1[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2; \<And>s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> x2[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x2 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2; i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> (x1 OR x2 )[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1 OR x2  \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2
 2. \<And>xa s1 s2. \<lbrakk>\<And>s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> xa[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> xa \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2; i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> (\<not> xa )[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> \<not> xa  \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2
 3. \<And>x1 x2 s1 s2. \<lbrakk>\<And>s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> x1[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2; \<And>s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> x2[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x2 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2; i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> (x1  IMP  x2 )[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1  IMP  x2  \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2
 4. \<And>x1 x2 s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> (x1  ==  x2 )[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1  ==  x2  \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
s1 = (s11 \<or> s12) \<and>  i \<lbrakk> c1[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s11  \<and>  i \<lbrakk> c2[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s12

goal (4 subgoals):
 1. \<And>x1 x2 s1 s2. \<lbrakk>\<And>s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> x1[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2; \<And>s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> x2[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x2 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2; i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> (x1 OR x2 )[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1 OR x2  \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2
 2. \<And>xa s1 s2. \<lbrakk>\<And>s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> xa[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> xa \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2; i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> (\<not> xa )[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> \<not> xa  \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2
 3. \<And>x1 x2 s1 s2. \<lbrakk>\<And>s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> x1[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2; \<And>s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> x2[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x2 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2; i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> (x1  IMP  x2 )[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1  IMP  x2  \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2
 4. \<And>x1 x2 s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> (x1  ==  x2 )[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1  ==  x2  \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2
[PROOF STEP]
obtain   s21 and s22 where "eval_c  (i ( x \<mapsto> s)) c1 s21 \<and> eval_c  (i ( x \<mapsto> s)) c2 s22 \<and> (s2 = (s21 \<or> s22))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>s21 s22.  i(x \<mapsto> s) \<lbrakk> c1 \<rbrakk> ~ s21  \<and>  i(x \<mapsto> s) \<lbrakk> c2 \<rbrakk> ~ s22  \<and> s2 = (s21 \<or> s22) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using
      eval_c_elims(4) C_disj
[PROOF STATE]
proof (prove)
using this:
\<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> v \<rbrakk> ~ s ;  i \<lbrakk> c1[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ ?s1.0 ;  i(x \<mapsto> s) \<lbrakk> c1 \<rbrakk> ~ ?s2.0 \<rbrakk> \<Longrightarrow> ?s1.0 = ?s2.0
\<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> c2[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ ?s1.0 ;  i(x \<mapsto> s) \<lbrakk> c2 \<rbrakk> ~ ?s2.0 \<rbrakk> \<Longrightarrow> ?s1.0 = ?s2.0
i \<lbrakk> v \<rbrakk> ~ s
 i \<lbrakk> (c1 OR c2 )[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1
 i(x \<mapsto> s) \<lbrakk> c1 OR c2  \<rbrakk> ~ s2

goal (1 subgoal):
 1. (\<And>s21 s22.  i(x \<mapsto> s) \<lbrakk> c1 \<rbrakk> ~ s21  \<and>  i(x \<mapsto> s) \<lbrakk> c2 \<rbrakk> ~ s22  \<and> s2 = (s21 \<or> s22) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
 i(x \<mapsto> s) \<lbrakk> c1 \<rbrakk> ~ s21  \<and>  i(x \<mapsto> s) \<lbrakk> c2 \<rbrakk> ~ s22  \<and> s2 = (s21 \<or> s22)

goal (4 subgoals):
 1. \<And>x1 x2 s1 s2. \<lbrakk>\<And>s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> x1[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2; \<And>s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> x2[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x2 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2; i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> (x1 OR x2 )[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1 OR x2  \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2
 2. \<And>xa s1 s2. \<lbrakk>\<And>s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> xa[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> xa \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2; i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> (\<not> xa )[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> \<not> xa  \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2
 3. \<And>x1 x2 s1 s2. \<lbrakk>\<And>s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> x1[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2; \<And>s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> x2[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x2 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2; i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> (x1  IMP  x2 )[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1  IMP  x2  \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2
 4. \<And>x1 x2 s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> (x1  ==  x2 )[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1  ==  x2  \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
s1 = (s11 \<or> s12) \<and>  i \<lbrakk> c1[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s11  \<and>  i \<lbrakk> c2[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s12
 i(x \<mapsto> s) \<lbrakk> c1 \<rbrakk> ~ s21  \<and>  i(x \<mapsto> s) \<lbrakk> c2 \<rbrakk> ~ s22  \<and> s2 = (s21 \<or> s22)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
s1 = (s11 \<or> s12) \<and>  i \<lbrakk> c1[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s11  \<and>  i \<lbrakk> c2[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s12
 i(x \<mapsto> s) \<lbrakk> c1 \<rbrakk> ~ s21  \<and>  i(x \<mapsto> s) \<lbrakk> c2 \<rbrakk> ~ s22  \<and> s2 = (s21 \<or> s22)

goal (1 subgoal):
 1. s1 = s2
[PROOF STEP]
using C_disj
[PROOF STATE]
proof (prove)
using this:
s1 = (s11 \<or> s12) \<and>  i \<lbrakk> c1[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s11  \<and>  i \<lbrakk> c2[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s12
 i(x \<mapsto> s) \<lbrakk> c1 \<rbrakk> ~ s21  \<and>  i(x \<mapsto> s) \<lbrakk> c2 \<rbrakk> ~ s22  \<and> s2 = (s21 \<or> s22)
\<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> c1[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ ?s1.0 ;  i(x \<mapsto> s) \<lbrakk> c1 \<rbrakk> ~ ?s2.0 \<rbrakk> \<Longrightarrow> ?s1.0 = ?s2.0
\<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> c2[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ ?s1.0 ;  i(x \<mapsto> s) \<lbrakk> c2 \<rbrakk> ~ ?s2.0 \<rbrakk> \<Longrightarrow> ?s1.0 = ?s2.0
i \<lbrakk> v \<rbrakk> ~ s
 i \<lbrakk> (c1 OR c2 )[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1
 i(x \<mapsto> s) \<lbrakk> c1 OR c2  \<rbrakk> ~ s2

goal (1 subgoal):
 1. s1 = s2
[PROOF STEP]
by (meson eval_c_elims)
[PROOF STATE]
proof (state)
this:
s1 = s2

goal (3 subgoals):
 1. \<And>xa s1 s2. \<lbrakk>\<And>s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> xa[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> xa \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2; i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> (\<not> xa )[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> \<not> xa  \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2
 2. \<And>x1 x2 s1 s2. \<lbrakk>\<And>s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> x1[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2; \<And>s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> x2[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x2 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2; i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> (x1  IMP  x2 )[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1  IMP  x2  \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2
 3. \<And>x1 x2 s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> (x1  ==  x2 )[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1  ==  x2  \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>xa s1 s2. \<lbrakk>\<And>s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> xa[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> xa \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2; i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> (\<not> xa )[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> \<not> xa  \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2
 2. \<And>x1 x2 s1 s2. \<lbrakk>\<And>s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> x1[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2; \<And>s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> x2[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x2 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2; i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> (x1  IMP  x2 )[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1  IMP  x2  \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2
 3. \<And>x1 x2 s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> (x1  ==  x2 )[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1  ==  x2  \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2
[PROOF STEP]
case (C_not c1)
[PROOF STATE]
proof (state)
this:
\<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> c1[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ ?s1.0 ;  i(x \<mapsto> s) \<lbrakk> c1 \<rbrakk> ~ ?s2.0 \<rbrakk> \<Longrightarrow> ?s1.0 = ?s2.0
i \<lbrakk> v \<rbrakk> ~ s
 i \<lbrakk> (\<not> c1 )[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1
 i(x \<mapsto> s) \<lbrakk> \<not> c1  \<rbrakk> ~ s2

goal (3 subgoals):
 1. \<And>xa s1 s2. \<lbrakk>\<And>s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> xa[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> xa \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2; i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> (\<not> xa )[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> \<not> xa  \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2
 2. \<And>x1 x2 s1 s2. \<lbrakk>\<And>s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> x1[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2; \<And>s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> x2[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x2 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2; i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> (x1  IMP  x2 )[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1  IMP  x2  \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2
 3. \<And>x1 x2 s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> (x1  ==  x2 )[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1  ==  x2  \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> c1[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ ?s1.0 ;  i(x \<mapsto> s) \<lbrakk> c1 \<rbrakk> ~ ?s2.0 \<rbrakk> \<Longrightarrow> ?s1.0 = ?s2.0
i \<lbrakk> v \<rbrakk> ~ s
 i \<lbrakk> (\<not> c1 )[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1
 i(x \<mapsto> s) \<lbrakk> \<not> c1  \<rbrakk> ~ s2
[PROOF STEP]
obtain s11 where "(s1 = (\<not> s11)) \<and> eval_c i c1[x::=v]\<^sub>c\<^sub>v s11"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> c1[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ ?s1.0 ;  i(x \<mapsto> s) \<lbrakk> c1 \<rbrakk> ~ ?s2.0 \<rbrakk> \<Longrightarrow> ?s1.0 = ?s2.0
i \<lbrakk> v \<rbrakk> ~ s
 i \<lbrakk> (\<not> c1 )[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1
 i(x \<mapsto> s) \<lbrakk> \<not> c1  \<rbrakk> ~ s2

goal (1 subgoal):
 1. (\<And>s11. s1 = (\<not> s11) \<and>  i \<lbrakk> c1[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s11  \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using
      eval_c_elims(6)
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> c1[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ ?s1.0 ;  i(x \<mapsto> s) \<lbrakk> c1 \<rbrakk> ~ ?s2.0 \<rbrakk> \<Longrightarrow> ?s1.0 = ?s2.0
i \<lbrakk> v \<rbrakk> ~ s
 i \<lbrakk> (\<not> c1 )[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1
 i(x \<mapsto> s) \<lbrakk> \<not> c1  \<rbrakk> ~ s2
\<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. (\<And>s11. s1 = (\<not> s11) \<and>  i \<lbrakk> c1[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s11  \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis subst_cv.simps(7))
[PROOF STATE]
proof (state)
this:
s1 = (\<not> s11) \<and>  i \<lbrakk> c1[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s11

goal (3 subgoals):
 1. \<And>xa s1 s2. \<lbrakk>\<And>s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> xa[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> xa \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2; i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> (\<not> xa )[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> \<not> xa  \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2
 2. \<And>x1 x2 s1 s2. \<lbrakk>\<And>s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> x1[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2; \<And>s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> x2[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x2 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2; i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> (x1  IMP  x2 )[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1  IMP  x2  \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2
 3. \<And>x1 x2 s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> (x1  ==  x2 )[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1  ==  x2  \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
s1 = (\<not> s11) \<and>  i \<lbrakk> c1[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s11

goal (3 subgoals):
 1. \<And>xa s1 s2. \<lbrakk>\<And>s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> xa[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> xa \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2; i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> (\<not> xa )[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> \<not> xa  \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2
 2. \<And>x1 x2 s1 s2. \<lbrakk>\<And>s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> x1[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2; \<And>s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> x2[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x2 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2; i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> (x1  IMP  x2 )[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1  IMP  x2  \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2
 3. \<And>x1 x2 s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> (x1  ==  x2 )[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1  ==  x2  \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2
[PROOF STEP]
obtain   s21 where "eval_c  (i ( x \<mapsto> s)) c1 s21 \<and> (s2 = (\<not>s21))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>s21.  i(x \<mapsto> s) \<lbrakk> c1 \<rbrakk> ~ s21  \<and> s2 = (\<not> s21) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using
      eval_c_elims(6) C_not
[PROOF STATE]
proof (prove)
using this:
\<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> v \<rbrakk> ~ s ;  i \<lbrakk> c1[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ ?s1.0 ;  i(x \<mapsto> s) \<lbrakk> c1 \<rbrakk> ~ ?s2.0 \<rbrakk> \<Longrightarrow> ?s1.0 = ?s2.0
i \<lbrakk> v \<rbrakk> ~ s
 i \<lbrakk> (\<not> c1 )[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1
 i(x \<mapsto> s) \<lbrakk> \<not> c1  \<rbrakk> ~ s2

goal (1 subgoal):
 1. (\<And>s21.  i(x \<mapsto> s) \<lbrakk> c1 \<rbrakk> ~ s21  \<and> s2 = (\<not> s21) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
 i(x \<mapsto> s) \<lbrakk> c1 \<rbrakk> ~ s21  \<and> s2 = (\<not> s21)

goal (3 subgoals):
 1. \<And>xa s1 s2. \<lbrakk>\<And>s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> xa[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> xa \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2; i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> (\<not> xa )[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> \<not> xa  \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2
 2. \<And>x1 x2 s1 s2. \<lbrakk>\<And>s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> x1[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2; \<And>s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> x2[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x2 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2; i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> (x1  IMP  x2 )[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1  IMP  x2  \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2
 3. \<And>x1 x2 s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> (x1  ==  x2 )[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1  ==  x2  \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
s1 = (\<not> s11) \<and>  i \<lbrakk> c1[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s11
 i(x \<mapsto> s) \<lbrakk> c1 \<rbrakk> ~ s21  \<and> s2 = (\<not> s21)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
s1 = (\<not> s11) \<and>  i \<lbrakk> c1[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s11
 i(x \<mapsto> s) \<lbrakk> c1 \<rbrakk> ~ s21  \<and> s2 = (\<not> s21)

goal (1 subgoal):
 1. s1 = s2
[PROOF STEP]
using C_not
[PROOF STATE]
proof (prove)
using this:
s1 = (\<not> s11) \<and>  i \<lbrakk> c1[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s11
 i(x \<mapsto> s) \<lbrakk> c1 \<rbrakk> ~ s21  \<and> s2 = (\<not> s21)
\<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> c1[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ ?s1.0 ;  i(x \<mapsto> s) \<lbrakk> c1 \<rbrakk> ~ ?s2.0 \<rbrakk> \<Longrightarrow> ?s1.0 = ?s2.0
i \<lbrakk> v \<rbrakk> ~ s
 i \<lbrakk> (\<not> c1 )[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1
 i(x \<mapsto> s) \<lbrakk> \<not> c1  \<rbrakk> ~ s2

goal (1 subgoal):
 1. s1 = s2
[PROOF STEP]
by (meson eval_c_elims)
[PROOF STATE]
proof (state)
this:
s1 = s2

goal (2 subgoals):
 1. \<And>x1 x2 s1 s2. \<lbrakk>\<And>s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> x1[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2; \<And>s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> x2[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x2 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2; i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> (x1  IMP  x2 )[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1  IMP  x2  \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2
 2. \<And>x1 x2 s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> (x1  ==  x2 )[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1  ==  x2  \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x1 x2 s1 s2. \<lbrakk>\<And>s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> x1[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2; \<And>s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> x2[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x2 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2; i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> (x1  IMP  x2 )[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1  IMP  x2  \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2
 2. \<And>x1 x2 s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> (x1  ==  x2 )[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1  ==  x2  \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2
[PROOF STEP]
case (C_imp c1 c2)
[PROOF STATE]
proof (state)
this:
\<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> c1[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ ?s1.0 ;  i(x \<mapsto> s) \<lbrakk> c1 \<rbrakk> ~ ?s2.0 \<rbrakk> \<Longrightarrow> ?s1.0 = ?s2.0
\<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> c2[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ ?s1.0 ;  i(x \<mapsto> s) \<lbrakk> c2 \<rbrakk> ~ ?s2.0 \<rbrakk> \<Longrightarrow> ?s1.0 = ?s2.0
i \<lbrakk> v \<rbrakk> ~ s
 i \<lbrakk> (c1  IMP  c2 )[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1
 i(x \<mapsto> s) \<lbrakk> c1  IMP  c2  \<rbrakk> ~ s2

goal (2 subgoals):
 1. \<And>x1 x2 s1 s2. \<lbrakk>\<And>s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> x1[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2; \<And>s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> x2[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x2 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2; i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> (x1  IMP  x2 )[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1  IMP  x2  \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2
 2. \<And>x1 x2 s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> (x1  ==  x2 )[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1  ==  x2  \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2
[PROOF STEP]
hence *:"eval_c i (c1[x::=v]\<^sub>c\<^sub>v IMP c2[x::=v]\<^sub>c\<^sub>v) s1"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> c1[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ ?s1.0 ;  i(x \<mapsto> s) \<lbrakk> c1 \<rbrakk> ~ ?s2.0 \<rbrakk> \<Longrightarrow> ?s1.0 = ?s2.0
\<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> c2[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ ?s1.0 ;  i(x \<mapsto> s) \<lbrakk> c2 \<rbrakk> ~ ?s2.0 \<rbrakk> \<Longrightarrow> ?s1.0 = ?s2.0
i \<lbrakk> v \<rbrakk> ~ s
 i \<lbrakk> (c1  IMP  c2 )[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1
 i(x \<mapsto> s) \<lbrakk> c1  IMP  c2  \<rbrakk> ~ s2

goal (1 subgoal):
 1.  i \<lbrakk> c1[x::=v]\<^sub>c\<^sub>v  IMP  c2[x::=v]\<^sub>c\<^sub>v  \<rbrakk> ~ s1
[PROOF STEP]
using subst_cv.simps
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> c1[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ ?s1.0 ;  i(x \<mapsto> s) \<lbrakk> c1 \<rbrakk> ~ ?s2.0 \<rbrakk> \<Longrightarrow> ?s1.0 = ?s2.0
\<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> c2[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ ?s1.0 ;  i(x \<mapsto> s) \<lbrakk> c2 \<rbrakk> ~ ?s2.0 \<rbrakk> \<Longrightarrow> ?s1.0 = ?s2.0
i \<lbrakk> v \<rbrakk> ~ s
 i \<lbrakk> (c1  IMP  c2 )[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1
 i(x \<mapsto> s) \<lbrakk> c1  IMP  c2  \<rbrakk> ~ s2
(TRUE)[?x::=?v]\<^sub>c\<^sub>v = (TRUE)
(FALSE)[?x::=?v]\<^sub>c\<^sub>v = (FALSE)
(?c1.0  AND  ?c2.0 )[?x::=?v]\<^sub>c\<^sub>v = (?c1.0[?x::=?v]\<^sub>c\<^sub>v  AND  ?c2.0[?x::=?v]\<^sub>c\<^sub>v )
(?c1.0 OR ?c2.0 )[?x::=?v]\<^sub>c\<^sub>v = (?c1.0[?x::=?v]\<^sub>c\<^sub>v OR ?c2.0[?x::=?v]\<^sub>c\<^sub>v )
(?c1.0  IMP  ?c2.0 )[?x::=?v]\<^sub>c\<^sub>v = (?c1.0[?x::=?v]\<^sub>c\<^sub>v  IMP  ?c2.0[?x::=?v]\<^sub>c\<^sub>v )
(?e1.0  ==  ?e2.0 )[?x::=?v]\<^sub>c\<^sub>v = (?e1.0[?x::=?v]\<^sub>c\<^sub>e\<^sub>v  ==  ?e2.0[?x::=?v]\<^sub>c\<^sub>e\<^sub>v )
(\<not> ?c )[?x::=?v]\<^sub>c\<^sub>v = (\<not> ?c[?x::=?v]\<^sub>c\<^sub>v )

goal (1 subgoal):
 1.  i \<lbrakk> c1[x::=v]\<^sub>c\<^sub>v  IMP  c2[x::=v]\<^sub>c\<^sub>v  \<rbrakk> ~ s1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
 i \<lbrakk> c1[x::=v]\<^sub>c\<^sub>v  IMP  c2[x::=v]\<^sub>c\<^sub>v  \<rbrakk> ~ s1

goal (2 subgoals):
 1. \<And>x1 x2 s1 s2. \<lbrakk>\<And>s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> x1[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2; \<And>s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> x2[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x2 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2; i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> (x1  IMP  x2 )[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1  IMP  x2  \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2
 2. \<And>x1 x2 s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> (x1  ==  x2 )[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1  ==  x2  \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
 i \<lbrakk> c1[x::=v]\<^sub>c\<^sub>v  IMP  c2[x::=v]\<^sub>c\<^sub>v  \<rbrakk> ~ s1
[PROOF STEP]
obtain s11 and s12 where "(s1 = (s11 \<longrightarrow> s12)) \<and> eval_c i c1[x::=v]\<^sub>c\<^sub>v s11 \<and> eval_c i c2[x::=v]\<^sub>c\<^sub>v s12"
[PROOF STATE]
proof (prove)
using this:
 i \<lbrakk> c1[x::=v]\<^sub>c\<^sub>v  IMP  c2[x::=v]\<^sub>c\<^sub>v  \<rbrakk> ~ s1

goal (1 subgoal):
 1. (\<And>s11 s12. s1 = (s11 \<longrightarrow> s12) \<and>  i \<lbrakk> c1[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s11  \<and>  i \<lbrakk> c2[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s12  \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using
      eval_c_elims(5)
[PROOF STATE]
proof (prove)
using this:
 i \<lbrakk> c1[x::=v]\<^sub>c\<^sub>v  IMP  c2[x::=v]\<^sub>c\<^sub>v  \<rbrakk> ~ s1
\<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>s11 s12. s1 = (s11 \<longrightarrow> s12) \<and>  i \<lbrakk> c1[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s11  \<and>  i \<lbrakk> c2[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s12  \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
s1 = (s11 \<longrightarrow> s12) \<and>  i \<lbrakk> c1[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s11  \<and>  i \<lbrakk> c2[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s12

goal (2 subgoals):
 1. \<And>x1 x2 s1 s2. \<lbrakk>\<And>s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> x1[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2; \<And>s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> x2[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x2 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2; i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> (x1  IMP  x2 )[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1  IMP  x2  \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2
 2. \<And>x1 x2 s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> (x1  ==  x2 )[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1  ==  x2  \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
s1 = (s11 \<longrightarrow> s12) \<and>  i \<lbrakk> c1[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s11  \<and>  i \<lbrakk> c2[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s12

goal (2 subgoals):
 1. \<And>x1 x2 s1 s2. \<lbrakk>\<And>s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> x1[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2; \<And>s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> x2[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x2 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2; i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> (x1  IMP  x2 )[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1  IMP  x2  \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2
 2. \<And>x1 x2 s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> (x1  ==  x2 )[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1  ==  x2  \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2
[PROOF STEP]
obtain   s21 and s22 where "eval_c  (i ( x \<mapsto> s)) c1 s21 \<and> eval_c  (i ( x \<mapsto> s)) c2 s22 \<and> (s2 = (s21 \<longrightarrow> s22))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>s21 s22.  i(x \<mapsto> s) \<lbrakk> c1 \<rbrakk> ~ s21  \<and>  i(x \<mapsto> s) \<lbrakk> c2 \<rbrakk> ~ s22  \<and> s2 = (s21 \<longrightarrow> s22) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using
      eval_c_elims(5) C_imp
[PROOF STATE]
proof (prove)
using this:
\<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> v \<rbrakk> ~ s ;  i \<lbrakk> c1[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ ?s1.0 ;  i(x \<mapsto> s) \<lbrakk> c1 \<rbrakk> ~ ?s2.0 \<rbrakk> \<Longrightarrow> ?s1.0 = ?s2.0
\<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> c2[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ ?s1.0 ;  i(x \<mapsto> s) \<lbrakk> c2 \<rbrakk> ~ ?s2.0 \<rbrakk> \<Longrightarrow> ?s1.0 = ?s2.0
i \<lbrakk> v \<rbrakk> ~ s
 i \<lbrakk> (c1  IMP  c2 )[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1
 i(x \<mapsto> s) \<lbrakk> c1  IMP  c2  \<rbrakk> ~ s2

goal (1 subgoal):
 1. (\<And>s21 s22.  i(x \<mapsto> s) \<lbrakk> c1 \<rbrakk> ~ s21  \<and>  i(x \<mapsto> s) \<lbrakk> c2 \<rbrakk> ~ s22  \<and> s2 = (s21 \<longrightarrow> s22) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
 i(x \<mapsto> s) \<lbrakk> c1 \<rbrakk> ~ s21  \<and>  i(x \<mapsto> s) \<lbrakk> c2 \<rbrakk> ~ s22  \<and> s2 = (s21 \<longrightarrow> s22)

goal (2 subgoals):
 1. \<And>x1 x2 s1 s2. \<lbrakk>\<And>s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> x1[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2; \<And>s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> x2[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x2 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2; i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> (x1  IMP  x2 )[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1  IMP  x2  \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2
 2. \<And>x1 x2 s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> (x1  ==  x2 )[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1  ==  x2  \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
s1 = (s11 \<longrightarrow> s12) \<and>  i \<lbrakk> c1[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s11  \<and>  i \<lbrakk> c2[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s12
 i(x \<mapsto> s) \<lbrakk> c1 \<rbrakk> ~ s21  \<and>  i(x \<mapsto> s) \<lbrakk> c2 \<rbrakk> ~ s22  \<and> s2 = (s21 \<longrightarrow> s22)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
s1 = (s11 \<longrightarrow> s12) \<and>  i \<lbrakk> c1[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s11  \<and>  i \<lbrakk> c2[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s12
 i(x \<mapsto> s) \<lbrakk> c1 \<rbrakk> ~ s21  \<and>  i(x \<mapsto> s) \<lbrakk> c2 \<rbrakk> ~ s22  \<and> s2 = (s21 \<longrightarrow> s22)

goal (1 subgoal):
 1. s1 = s2
[PROOF STEP]
using C_imp
[PROOF STATE]
proof (prove)
using this:
s1 = (s11 \<longrightarrow> s12) \<and>  i \<lbrakk> c1[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s11  \<and>  i \<lbrakk> c2[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s12
 i(x \<mapsto> s) \<lbrakk> c1 \<rbrakk> ~ s21  \<and>  i(x \<mapsto> s) \<lbrakk> c2 \<rbrakk> ~ s22  \<and> s2 = (s21 \<longrightarrow> s22)
\<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> c1[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ ?s1.0 ;  i(x \<mapsto> s) \<lbrakk> c1 \<rbrakk> ~ ?s2.0 \<rbrakk> \<Longrightarrow> ?s1.0 = ?s2.0
\<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> c2[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ ?s1.0 ;  i(x \<mapsto> s) \<lbrakk> c2 \<rbrakk> ~ ?s2.0 \<rbrakk> \<Longrightarrow> ?s1.0 = ?s2.0
i \<lbrakk> v \<rbrakk> ~ s
 i \<lbrakk> (c1  IMP  c2 )[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1
 i(x \<mapsto> s) \<lbrakk> c1  IMP  c2  \<rbrakk> ~ s2

goal (1 subgoal):
 1. s1 = s2
[PROOF STEP]
by (meson eval_c_elims)
[PROOF STATE]
proof (state)
this:
s1 = s2

goal (1 subgoal):
 1. \<And>x1 x2 s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> (x1  ==  x2 )[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1  ==  x2  \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x1 x2 s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> (x1  ==  x2 )[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1  ==  x2  \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2
[PROOF STEP]
case (C_eq e1 e2)
[PROOF STATE]
proof (state)
this:
i \<lbrakk> v \<rbrakk> ~ s
 i \<lbrakk> (e1  ==  e2 )[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1
 i(x \<mapsto> s) \<lbrakk> e1  ==  e2  \<rbrakk> ~ s2

goal (1 subgoal):
 1. \<And>x1 x2 s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> (x1  ==  x2 )[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1  ==  x2  \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2
[PROOF STEP]
hence *:"eval_c i (e1[x::=v]\<^sub>c\<^sub>e\<^sub>v == e2[x::=v]\<^sub>c\<^sub>e\<^sub>v) s1"
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> v \<rbrakk> ~ s
 i \<lbrakk> (e1  ==  e2 )[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1
 i(x \<mapsto> s) \<lbrakk> e1  ==  e2  \<rbrakk> ~ s2

goal (1 subgoal):
 1.  i \<lbrakk> e1[x::=v]\<^sub>c\<^sub>e\<^sub>v  ==  e2[x::=v]\<^sub>c\<^sub>e\<^sub>v  \<rbrakk> ~ s1
[PROOF STEP]
using subst_cv.simps
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> v \<rbrakk> ~ s
 i \<lbrakk> (e1  ==  e2 )[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1
 i(x \<mapsto> s) \<lbrakk> e1  ==  e2  \<rbrakk> ~ s2
(TRUE)[?x::=?v]\<^sub>c\<^sub>v = (TRUE)
(FALSE)[?x::=?v]\<^sub>c\<^sub>v = (FALSE)
(?c1.0  AND  ?c2.0 )[?x::=?v]\<^sub>c\<^sub>v = (?c1.0[?x::=?v]\<^sub>c\<^sub>v  AND  ?c2.0[?x::=?v]\<^sub>c\<^sub>v )
(?c1.0 OR ?c2.0 )[?x::=?v]\<^sub>c\<^sub>v = (?c1.0[?x::=?v]\<^sub>c\<^sub>v OR ?c2.0[?x::=?v]\<^sub>c\<^sub>v )
(?c1.0  IMP  ?c2.0 )[?x::=?v]\<^sub>c\<^sub>v = (?c1.0[?x::=?v]\<^sub>c\<^sub>v  IMP  ?c2.0[?x::=?v]\<^sub>c\<^sub>v )
(?e1.0  ==  ?e2.0 )[?x::=?v]\<^sub>c\<^sub>v = (?e1.0[?x::=?v]\<^sub>c\<^sub>e\<^sub>v  ==  ?e2.0[?x::=?v]\<^sub>c\<^sub>e\<^sub>v )
(\<not> ?c )[?x::=?v]\<^sub>c\<^sub>v = (\<not> ?c[?x::=?v]\<^sub>c\<^sub>v )

goal (1 subgoal):
 1.  i \<lbrakk> e1[x::=v]\<^sub>c\<^sub>e\<^sub>v  ==  e2[x::=v]\<^sub>c\<^sub>e\<^sub>v  \<rbrakk> ~ s1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
 i \<lbrakk> e1[x::=v]\<^sub>c\<^sub>e\<^sub>v  ==  e2[x::=v]\<^sub>c\<^sub>e\<^sub>v  \<rbrakk> ~ s1

goal (1 subgoal):
 1. \<And>x1 x2 s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> (x1  ==  x2 )[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1  ==  x2  \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
 i \<lbrakk> e1[x::=v]\<^sub>c\<^sub>e\<^sub>v  ==  e2[x::=v]\<^sub>c\<^sub>e\<^sub>v  \<rbrakk> ~ s1
[PROOF STEP]
obtain s11 and s12 where "(s1 = (s11 = s12)) \<and> eval_e i (e1[x::=v]\<^sub>c\<^sub>e\<^sub>v) s11 \<and> eval_e i (e2[x::=v]\<^sub>c\<^sub>e\<^sub>v) s12"
[PROOF STATE]
proof (prove)
using this:
 i \<lbrakk> e1[x::=v]\<^sub>c\<^sub>e\<^sub>v  ==  e2[x::=v]\<^sub>c\<^sub>e\<^sub>v  \<rbrakk> ~ s1

goal (1 subgoal):
 1. (\<And>s11 s12. s1 = (s11 = s12) \<and> i \<lbrakk> e1[x::=v]\<^sub>c\<^sub>e\<^sub>v \<rbrakk> ~ s11  \<and> i \<lbrakk> e2[x::=v]\<^sub>c\<^sub>e\<^sub>v \<rbrakk> ~ s12  \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using
      eval_c_elims(7)
[PROOF STATE]
proof (prove)
using this:
 i \<lbrakk> e1[x::=v]\<^sub>c\<^sub>e\<^sub>v  ==  e2[x::=v]\<^sub>c\<^sub>e\<^sub>v  \<rbrakk> ~ s1
\<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. (\<And>s11 s12. s1 = (s11 = s12) \<and> i \<lbrakk> e1[x::=v]\<^sub>c\<^sub>e\<^sub>v \<rbrakk> ~ s11  \<and> i \<lbrakk> e2[x::=v]\<^sub>c\<^sub>e\<^sub>v \<rbrakk> ~ s12  \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
s1 = (s11 = s12) \<and> i \<lbrakk> e1[x::=v]\<^sub>c\<^sub>e\<^sub>v \<rbrakk> ~ s11  \<and> i \<lbrakk> e2[x::=v]\<^sub>c\<^sub>e\<^sub>v \<rbrakk> ~ s12

goal (1 subgoal):
 1. \<And>x1 x2 s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> (x1  ==  x2 )[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1  ==  x2  \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
s1 = (s11 = s12) \<and> i \<lbrakk> e1[x::=v]\<^sub>c\<^sub>e\<^sub>v \<rbrakk> ~ s11  \<and> i \<lbrakk> e2[x::=v]\<^sub>c\<^sub>e\<^sub>v \<rbrakk> ~ s12

goal (1 subgoal):
 1. \<And>x1 x2 s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> (x1  ==  x2 )[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1  ==  x2  \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2
[PROOF STEP]
obtain   s21 and s22 where "eval_e  (i ( x \<mapsto> s)) e1 s21 \<and> eval_e  (i ( x \<mapsto> s)) e2 s22 \<and> (s2 = (s21 = s22))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>s21 s22. i(x \<mapsto> s) \<lbrakk> e1 \<rbrakk> ~ s21  \<and> i(x \<mapsto> s) \<lbrakk> e2 \<rbrakk> ~ s22  \<and> s2 = (s21 = s22) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using
      eval_c_elims(7) C_eq
[PROOF STATE]
proof (prove)
using this:
\<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
i \<lbrakk> v \<rbrakk> ~ s
 i \<lbrakk> (e1  ==  e2 )[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1
 i(x \<mapsto> s) \<lbrakk> e1  ==  e2  \<rbrakk> ~ s2

goal (1 subgoal):
 1. (\<And>s21 s22. i(x \<mapsto> s) \<lbrakk> e1 \<rbrakk> ~ s21  \<and> i(x \<mapsto> s) \<lbrakk> e2 \<rbrakk> ~ s22  \<and> s2 = (s21 = s22) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
i(x \<mapsto> s) \<lbrakk> e1 \<rbrakk> ~ s21  \<and> i(x \<mapsto> s) \<lbrakk> e2 \<rbrakk> ~ s22  \<and> s2 = (s21 = s22)

goal (1 subgoal):
 1. \<And>x1 x2 s1 s2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ;  i \<lbrakk> (x1  ==  x2 )[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1 ;  i(x \<mapsto> s) \<lbrakk> x1  ==  x2  \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> s1 = s2
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
s1 = (s11 = s12) \<and> i \<lbrakk> e1[x::=v]\<^sub>c\<^sub>e\<^sub>v \<rbrakk> ~ s11  \<and> i \<lbrakk> e2[x::=v]\<^sub>c\<^sub>e\<^sub>v \<rbrakk> ~ s12
i(x \<mapsto> s) \<lbrakk> e1 \<rbrakk> ~ s21  \<and> i(x \<mapsto> s) \<lbrakk> e2 \<rbrakk> ~ s22  \<and> s2 = (s21 = s22)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
s1 = (s11 = s12) \<and> i \<lbrakk> e1[x::=v]\<^sub>c\<^sub>e\<^sub>v \<rbrakk> ~ s11  \<and> i \<lbrakk> e2[x::=v]\<^sub>c\<^sub>e\<^sub>v \<rbrakk> ~ s12
i(x \<mapsto> s) \<lbrakk> e1 \<rbrakk> ~ s21  \<and> i(x \<mapsto> s) \<lbrakk> e2 \<rbrakk> ~ s22  \<and> s2 = (s21 = s22)

goal (1 subgoal):
 1. s1 = s2
[PROOF STEP]
using C_eq subst_e_eval_v
[PROOF STATE]
proof (prove)
using this:
s1 = (s11 = s12) \<and> i \<lbrakk> e1[x::=v]\<^sub>c\<^sub>e\<^sub>v \<rbrakk> ~ s11  \<and> i \<lbrakk> e2[x::=v]\<^sub>c\<^sub>e\<^sub>v \<rbrakk> ~ s12
i(x \<mapsto> s) \<lbrakk> e1 \<rbrakk> ~ s21  \<and> i(x \<mapsto> s) \<lbrakk> e2 \<rbrakk> ~ s22  \<and> s2 = (s21 = s22)
i \<lbrakk> v \<rbrakk> ~ s
 i \<lbrakk> (e1  ==  e2 )[x::=v]\<^sub>c\<^sub>v \<rbrakk> ~ s1
 i(x \<mapsto> s) \<lbrakk> e1  ==  e2  \<rbrakk> ~ s2
\<lbrakk>?i \<lbrakk> ?e' \<rbrakk> ~ ?s' ; ?e' = ?e[?y::=?v]\<^sub>c\<^sub>e\<^sub>v; ?i \<lbrakk> ?v \<rbrakk> ~ ?s \<rbrakk> \<Longrightarrow> ?i(?y \<mapsto> ?s) \<lbrakk> ?e \<rbrakk> ~ ?s'

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

goal:
No subgoals!
[PROOF STEP]
qed