[STATEMENT]
lemma symm_closure_of_preorder_is_trans:
  fixes Rel :: "('a \<times> 'a) set"
  assumes condA: "\<forall>a b c. (a, b) \<in> Rel \<and> (c, b) \<in> Rel \<and> (a, c) \<notin> Rel
                  \<longrightarrow> (b, a) \<in> Rel \<or> (b, c) \<in> Rel"
      and condB: "\<forall>a b c. (a, b) \<in> Rel \<and> (a, c) \<in> Rel \<and> (b, c) \<notin> Rel
                  \<longrightarrow> (b, a) \<in> Rel \<or> (c, a) \<in> Rel"
      and reflR: "refl Rel"
      and tranR: "trans Rel"
  shows "trans (symcl Rel)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trans (symcl Rel)
[PROOF STEP]
unfolding trans_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x y z. (x, y) \<in> symcl Rel \<longrightarrow> (y, z) \<in> symcl Rel \<longrightarrow> (x, z) \<in> symcl Rel
[PROOF STEP]
proof clarify
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y z. (x, y) \<in> symcl Rel \<and> (y, z) \<in> symcl Rel \<Longrightarrow> (x, z) \<in> symcl Rel
[PROOF STEP]
fix a b c
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y z. (x, y) \<in> symcl Rel \<and> (y, z) \<in> symcl Rel \<Longrightarrow> (x, z) \<in> symcl Rel
[PROOF STEP]
have "\<lbrakk>(a, b) \<in> Rel; (b, c) \<in> Rel\<rbrakk> \<Longrightarrow> (a, c) \<in> symcl Rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a, b) \<in> Rel \<and> (b, c) \<in> Rel \<Longrightarrow> (a, c) \<in> symcl Rel
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (a, b) \<in> Rel \<and> (b, c) \<in> Rel \<Longrightarrow> (a, c) \<in> symcl Rel
[PROOF STEP]
assume "(a, b) \<in> Rel" and "(b, c) \<in> Rel"
[PROOF STATE]
proof (state)
this:
(a, b) \<in> Rel
(b, c) \<in> Rel

goal (1 subgoal):
 1. (a, b) \<in> Rel \<and> (b, c) \<in> Rel \<Longrightarrow> (a, c) \<in> symcl Rel
[PROOF STEP]
with tranR
[PROOF STATE]
proof (chain)
picking this:
trans Rel
(a, b) \<in> Rel
(b, c) \<in> Rel
[PROOF STEP]
have "(a, c) \<in> Rel"
[PROOF STATE]
proof (prove)
using this:
trans Rel
(a, b) \<in> Rel
(b, c) \<in> Rel

goal (1 subgoal):
 1. (a, c) \<in> Rel
[PROOF STEP]
unfolding trans_def
[PROOF STATE]
proof (prove)
using this:
\<forall>x y z. (x, y) \<in> Rel \<longrightarrow> (y, z) \<in> Rel \<longrightarrow> (x, z) \<in> Rel
(a, b) \<in> Rel
(b, c) \<in> Rel

goal (1 subgoal):
 1. (a, c) \<in> Rel
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(a, c) \<in> Rel

goal (1 subgoal):
 1. (a, b) \<in> Rel \<and> (b, c) \<in> Rel \<Longrightarrow> (a, c) \<in> symcl Rel
[PROOF STEP]
thus "(a, c) \<in> symcl Rel"
[PROOF STATE]
proof (prove)
using this:
(a, c) \<in> Rel

goal (1 subgoal):
 1. (a, c) \<in> symcl Rel
[PROOF STEP]
by (simp add: symcl_def)
[PROOF STATE]
proof (state)
this:
(a, c) \<in> symcl Rel

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(a, b) \<in> Rel \<and> (b, c) \<in> Rel \<Longrightarrow> (a, c) \<in> symcl Rel

goal (1 subgoal):
 1. \<And>x y z. (x, y) \<in> symcl Rel \<and> (y, z) \<in> symcl Rel \<Longrightarrow> (x, z) \<in> symcl Rel
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(a, b) \<in> Rel \<and> (b, c) \<in> Rel \<Longrightarrow> (a, c) \<in> symcl Rel

goal (1 subgoal):
 1. \<And>x y z. (x, y) \<in> symcl Rel \<and> (y, z) \<in> symcl Rel \<Longrightarrow> (x, z) \<in> symcl Rel
[PROOF STEP]
have "\<lbrakk>(a, b) \<in> Rel; (c, b) \<in> Rel; (a, c) \<notin> Rel\<rbrakk> \<Longrightarrow> (a, c) \<in> symcl Rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a, b) \<in> Rel \<and> (c, b) \<in> Rel \<and> (a, c) \<notin> Rel \<Longrightarrow> (a, c) \<in> symcl Rel
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (a, b) \<in> Rel \<and> (c, b) \<in> Rel \<and> (a, c) \<notin> Rel \<Longrightarrow> (a, c) \<in> symcl Rel
[PROOF STEP]
assume A1: "(a, b) \<in> Rel" and A2: "(c, b) \<in> Rel" and "(a, c) \<notin> Rel"
[PROOF STATE]
proof (state)
this:
(a, b) \<in> Rel
(c, b) \<in> Rel
(a, c) \<notin> Rel

goal (1 subgoal):
 1. (a, b) \<in> Rel \<and> (c, b) \<in> Rel \<and> (a, c) \<notin> Rel \<Longrightarrow> (a, c) \<in> symcl Rel
[PROOF STEP]
with condA
[PROOF STATE]
proof (chain)
picking this:
\<forall>a b c. (a, b) \<in> Rel \<and> (c, b) \<in> Rel \<and> (a, c) \<notin> Rel \<longrightarrow> (b, a) \<in> Rel \<or> (b, c) \<in> Rel
(a, b) \<in> Rel
(c, b) \<in> Rel
(a, c) \<notin> Rel
[PROOF STEP]
have "(b, a) \<in> Rel \<or> (b, c) \<in> Rel"
[PROOF STATE]
proof (prove)
using this:
\<forall>a b c. (a, b) \<in> Rel \<and> (c, b) \<in> Rel \<and> (a, c) \<notin> Rel \<longrightarrow> (b, a) \<in> Rel \<or> (b, c) \<in> Rel
(a, b) \<in> Rel
(c, b) \<in> Rel
(a, c) \<notin> Rel

goal (1 subgoal):
 1. (b, a) \<in> Rel \<or> (b, c) \<in> Rel
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(b, a) \<in> Rel \<or> (b, c) \<in> Rel

goal (1 subgoal):
 1. (a, b) \<in> Rel \<and> (c, b) \<in> Rel \<and> (a, c) \<notin> Rel \<Longrightarrow> (a, c) \<in> symcl Rel
[PROOF STEP]
thus "(a, c) \<in> symcl Rel"
[PROOF STATE]
proof (prove)
using this:
(b, a) \<in> Rel \<or> (b, c) \<in> Rel

goal (1 subgoal):
 1. (a, c) \<in> symcl Rel
[PROOF STEP]
proof auto
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (b, a) \<in> Rel \<Longrightarrow> (a, c) \<in> symcl Rel
 2. (b, c) \<in> Rel \<Longrightarrow> (a, c) \<in> symcl Rel
[PROOF STEP]
assume "(b, a) \<in> Rel"
[PROOF STATE]
proof (state)
this:
(b, a) \<in> Rel

goal (2 subgoals):
 1. (b, a) \<in> Rel \<Longrightarrow> (a, c) \<in> symcl Rel
 2. (b, c) \<in> Rel \<Longrightarrow> (a, c) \<in> symcl Rel
[PROOF STEP]
with A2 tranR
[PROOF STATE]
proof (chain)
picking this:
(c, b) \<in> Rel
trans Rel
(b, a) \<in> Rel
[PROOF STEP]
have "(c, a) \<in> Rel"
[PROOF STATE]
proof (prove)
using this:
(c, b) \<in> Rel
trans Rel
(b, a) \<in> Rel

goal (1 subgoal):
 1. (c, a) \<in> Rel
[PROOF STEP]
unfolding trans_def
[PROOF STATE]
proof (prove)
using this:
(c, b) \<in> Rel
\<forall>x y z. (x, y) \<in> Rel \<longrightarrow> (y, z) \<in> Rel \<longrightarrow> (x, z) \<in> Rel
(b, a) \<in> Rel

goal (1 subgoal):
 1. (c, a) \<in> Rel
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(c, a) \<in> Rel

goal (2 subgoals):
 1. (b, a) \<in> Rel \<Longrightarrow> (a, c) \<in> symcl Rel
 2. (b, c) \<in> Rel \<Longrightarrow> (a, c) \<in> symcl Rel
[PROOF STEP]
thus "(a, c) \<in> symcl Rel"
[PROOF STATE]
proof (prove)
using this:
(c, a) \<in> Rel

goal (1 subgoal):
 1. (a, c) \<in> symcl Rel
[PROOF STEP]
by (simp add: symcl_def)
[PROOF STATE]
proof (state)
this:
(a, c) \<in> symcl Rel

goal (1 subgoal):
 1. (b, c) \<in> Rel \<Longrightarrow> (a, c) \<in> symcl Rel
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (b, c) \<in> Rel \<Longrightarrow> (a, c) \<in> symcl Rel
[PROOF STEP]
assume "(b, c) \<in> Rel"
[PROOF STATE]
proof (state)
this:
(b, c) \<in> Rel

goal (1 subgoal):
 1. (b, c) \<in> Rel \<Longrightarrow> (a, c) \<in> symcl Rel
[PROOF STEP]
with A1 tranR
[PROOF STATE]
proof (chain)
picking this:
(a, b) \<in> Rel
trans Rel
(b, c) \<in> Rel
[PROOF STEP]
have "(a, c) \<in> Rel"
[PROOF STATE]
proof (prove)
using this:
(a, b) \<in> Rel
trans Rel
(b, c) \<in> Rel

goal (1 subgoal):
 1. (a, c) \<in> Rel
[PROOF STEP]
unfolding trans_def
[PROOF STATE]
proof (prove)
using this:
(a, b) \<in> Rel
\<forall>x y z. (x, y) \<in> Rel \<longrightarrow> (y, z) \<in> Rel \<longrightarrow> (x, z) \<in> Rel
(b, c) \<in> Rel

goal (1 subgoal):
 1. (a, c) \<in> Rel
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(a, c) \<in> Rel

goal (1 subgoal):
 1. (b, c) \<in> Rel \<Longrightarrow> (a, c) \<in> symcl Rel
[PROOF STEP]
thus "(a, c) \<in> symcl Rel"
[PROOF STATE]
proof (prove)
using this:
(a, c) \<in> Rel

goal (1 subgoal):
 1. (a, c) \<in> symcl Rel
[PROOF STEP]
by (simp add: symcl_def)
[PROOF STATE]
proof (state)
this:
(a, c) \<in> symcl Rel

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(a, c) \<in> symcl Rel

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(a, b) \<in> Rel \<and> (c, b) \<in> Rel \<and> (a, c) \<notin> Rel \<Longrightarrow> (a, c) \<in> symcl Rel

goal (1 subgoal):
 1. \<And>x y z. (x, y) \<in> symcl Rel \<and> (y, z) \<in> symcl Rel \<Longrightarrow> (x, z) \<in> symcl Rel
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(a, b) \<in> Rel \<and> (c, b) \<in> Rel \<and> (a, c) \<notin> Rel \<Longrightarrow> (a, c) \<in> symcl Rel

goal (1 subgoal):
 1. \<And>x y z. (x, y) \<in> symcl Rel \<and> (y, z) \<in> symcl Rel \<Longrightarrow> (x, z) \<in> symcl Rel
[PROOF STEP]
have "\<lbrakk>(b, a) \<in> Rel; (b, c) \<in> Rel; (a, c) \<notin> Rel\<rbrakk> \<Longrightarrow> (a, c) \<in> symcl Rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (b, a) \<in> Rel \<and> (b, c) \<in> Rel \<and> (a, c) \<notin> Rel \<Longrightarrow> (a, c) \<in> symcl Rel
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (b, a) \<in> Rel \<and> (b, c) \<in> Rel \<and> (a, c) \<notin> Rel \<Longrightarrow> (a, c) \<in> symcl Rel
[PROOF STEP]
assume B1: "(b, a) \<in> Rel" and B2: "(b, c) \<in> Rel" and "(a, c) \<notin> Rel"
[PROOF STATE]
proof (state)
this:
(b, a) \<in> Rel
(b, c) \<in> Rel
(a, c) \<notin> Rel

goal (1 subgoal):
 1. (b, a) \<in> Rel \<and> (b, c) \<in> Rel \<and> (a, c) \<notin> Rel \<Longrightarrow> (a, c) \<in> symcl Rel
[PROOF STEP]
with condB
[PROOF STATE]
proof (chain)
picking this:
\<forall>a b c. (a, b) \<in> Rel \<and> (a, c) \<in> Rel \<and> (b, c) \<notin> Rel \<longrightarrow> (b, a) \<in> Rel \<or> (c, a) \<in> Rel
(b, a) \<in> Rel
(b, c) \<in> Rel
(a, c) \<notin> Rel
[PROOF STEP]
have "(a, b) \<in> Rel \<or> (c, b) \<in> Rel"
[PROOF STATE]
proof (prove)
using this:
\<forall>a b c. (a, b) \<in> Rel \<and> (a, c) \<in> Rel \<and> (b, c) \<notin> Rel \<longrightarrow> (b, a) \<in> Rel \<or> (c, a) \<in> Rel
(b, a) \<in> Rel
(b, c) \<in> Rel
(a, c) \<notin> Rel

goal (1 subgoal):
 1. (a, b) \<in> Rel \<or> (c, b) \<in> Rel
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(a, b) \<in> Rel \<or> (c, b) \<in> Rel

goal (1 subgoal):
 1. (b, a) \<in> Rel \<and> (b, c) \<in> Rel \<and> (a, c) \<notin> Rel \<Longrightarrow> (a, c) \<in> symcl Rel
[PROOF STEP]
thus "(a, c) \<in> symcl Rel"
[PROOF STATE]
proof (prove)
using this:
(a, b) \<in> Rel \<or> (c, b) \<in> Rel

goal (1 subgoal):
 1. (a, c) \<in> symcl Rel
[PROOF STEP]
proof auto
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (a, b) \<in> Rel \<Longrightarrow> (a, c) \<in> symcl Rel
 2. (c, b) \<in> Rel \<Longrightarrow> (a, c) \<in> symcl Rel
[PROOF STEP]
assume "(a, b) \<in> Rel"
[PROOF STATE]
proof (state)
this:
(a, b) \<in> Rel

goal (2 subgoals):
 1. (a, b) \<in> Rel \<Longrightarrow> (a, c) \<in> symcl Rel
 2. (c, b) \<in> Rel \<Longrightarrow> (a, c) \<in> symcl Rel
[PROOF STEP]
with B2 tranR
[PROOF STATE]
proof (chain)
picking this:
(b, c) \<in> Rel
trans Rel
(a, b) \<in> Rel
[PROOF STEP]
have "(a, c) \<in> Rel"
[PROOF STATE]
proof (prove)
using this:
(b, c) \<in> Rel
trans Rel
(a, b) \<in> Rel

goal (1 subgoal):
 1. (a, c) \<in> Rel
[PROOF STEP]
unfolding trans_def
[PROOF STATE]
proof (prove)
using this:
(b, c) \<in> Rel
\<forall>x y z. (x, y) \<in> Rel \<longrightarrow> (y, z) \<in> Rel \<longrightarrow> (x, z) \<in> Rel
(a, b) \<in> Rel

goal (1 subgoal):
 1. (a, c) \<in> Rel
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(a, c) \<in> Rel

goal (2 subgoals):
 1. (a, b) \<in> Rel \<Longrightarrow> (a, c) \<in> symcl Rel
 2. (c, b) \<in> Rel \<Longrightarrow> (a, c) \<in> symcl Rel
[PROOF STEP]
thus "(a, c) \<in> symcl Rel"
[PROOF STATE]
proof (prove)
using this:
(a, c) \<in> Rel

goal (1 subgoal):
 1. (a, c) \<in> symcl Rel
[PROOF STEP]
by (simp add: symcl_def)
[PROOF STATE]
proof (state)
this:
(a, c) \<in> symcl Rel

goal (1 subgoal):
 1. (c, b) \<in> Rel \<Longrightarrow> (a, c) \<in> symcl Rel
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (c, b) \<in> Rel \<Longrightarrow> (a, c) \<in> symcl Rel
[PROOF STEP]
assume "(c, b) \<in> Rel"
[PROOF STATE]
proof (state)
this:
(c, b) \<in> Rel

goal (1 subgoal):
 1. (c, b) \<in> Rel \<Longrightarrow> (a, c) \<in> symcl Rel
[PROOF STEP]
with B1 tranR
[PROOF STATE]
proof (chain)
picking this:
(b, a) \<in> Rel
trans Rel
(c, b) \<in> Rel
[PROOF STEP]
have "(c, a) \<in> Rel"
[PROOF STATE]
proof (prove)
using this:
(b, a) \<in> Rel
trans Rel
(c, b) \<in> Rel

goal (1 subgoal):
 1. (c, a) \<in> Rel
[PROOF STEP]
unfolding trans_def
[PROOF STATE]
proof (prove)
using this:
(b, a) \<in> Rel
\<forall>x y z. (x, y) \<in> Rel \<longrightarrow> (y, z) \<in> Rel \<longrightarrow> (x, z) \<in> Rel
(c, b) \<in> Rel

goal (1 subgoal):
 1. (c, a) \<in> Rel
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(c, a) \<in> Rel

goal (1 subgoal):
 1. (c, b) \<in> Rel \<Longrightarrow> (a, c) \<in> symcl Rel
[PROOF STEP]
thus "(a, c) \<in> symcl Rel"
[PROOF STATE]
proof (prove)
using this:
(c, a) \<in> Rel

goal (1 subgoal):
 1. (a, c) \<in> symcl Rel
[PROOF STEP]
by (simp add: symcl_def)
[PROOF STATE]
proof (state)
this:
(a, c) \<in> symcl Rel

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(a, c) \<in> symcl Rel

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(b, a) \<in> Rel \<and> (b, c) \<in> Rel \<and> (a, c) \<notin> Rel \<Longrightarrow> (a, c) \<in> symcl Rel

goal (1 subgoal):
 1. \<And>x y z. (x, y) \<in> symcl Rel \<and> (y, z) \<in> symcl Rel \<Longrightarrow> (x, z) \<in> symcl Rel
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(b, a) \<in> Rel \<and> (b, c) \<in> Rel \<and> (a, c) \<notin> Rel \<Longrightarrow> (a, c) \<in> symcl Rel

goal (1 subgoal):
 1. \<And>x y z. (x, y) \<in> symcl Rel \<and> (y, z) \<in> symcl Rel \<Longrightarrow> (x, z) \<in> symcl Rel
[PROOF STEP]
have "\<lbrakk>(b, a) \<in> Rel; (c, b) \<in> Rel\<rbrakk> \<Longrightarrow> (a, c) \<in> symcl Rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (b, a) \<in> Rel \<and> (c, b) \<in> Rel \<Longrightarrow> (a, c) \<in> symcl Rel
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (b, a) \<in> Rel \<and> (c, b) \<in> Rel \<Longrightarrow> (a, c) \<in> symcl Rel
[PROOF STEP]
assume "(c, b) \<in> Rel" and "(b, a) \<in> Rel"
[PROOF STATE]
proof (state)
this:
(c, b) \<in> Rel
(b, a) \<in> Rel

goal (1 subgoal):
 1. (b, a) \<in> Rel \<and> (c, b) \<in> Rel \<Longrightarrow> (a, c) \<in> symcl Rel
[PROOF STEP]
with tranR
[PROOF STATE]
proof (chain)
picking this:
trans Rel
(c, b) \<in> Rel
(b, a) \<in> Rel
[PROOF STEP]
have "(c, a) \<in> Rel"
[PROOF STATE]
proof (prove)
using this:
trans Rel
(c, b) \<in> Rel
(b, a) \<in> Rel

goal (1 subgoal):
 1. (c, a) \<in> Rel
[PROOF STEP]
unfolding trans_def
[PROOF STATE]
proof (prove)
using this:
\<forall>x y z. (x, y) \<in> Rel \<longrightarrow> (y, z) \<in> Rel \<longrightarrow> (x, z) \<in> Rel
(c, b) \<in> Rel
(b, a) \<in> Rel

goal (1 subgoal):
 1. (c, a) \<in> Rel
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(c, a) \<in> Rel

goal (1 subgoal):
 1. (b, a) \<in> Rel \<and> (c, b) \<in> Rel \<Longrightarrow> (a, c) \<in> symcl Rel
[PROOF STEP]
thus "(a, c) \<in> symcl Rel"
[PROOF STATE]
proof (prove)
using this:
(c, a) \<in> Rel

goal (1 subgoal):
 1. (a, c) \<in> symcl Rel
[PROOF STEP]
by (simp add: symcl_def)
[PROOF STATE]
proof (state)
this:
(a, c) \<in> symcl Rel

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(b, a) \<in> Rel \<and> (c, b) \<in> Rel \<Longrightarrow> (a, c) \<in> symcl Rel

goal (1 subgoal):
 1. \<And>x y z. (x, y) \<in> symcl Rel \<and> (y, z) \<in> symcl Rel \<Longrightarrow> (x, z) \<in> symcl Rel
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(b, a) \<in> Rel \<and> (c, b) \<in> Rel \<Longrightarrow> (a, c) \<in> symcl Rel

goal (1 subgoal):
 1. \<And>x y z. (x, y) \<in> symcl Rel \<and> (y, z) \<in> symcl Rel \<Longrightarrow> (x, z) \<in> symcl Rel
[PROOF STEP]
assume "(a, b) \<in> symcl Rel" and "(b, c) \<in> symcl Rel"
[PROOF STATE]
proof (state)
this:
(a, b) \<in> symcl Rel
(b, c) \<in> symcl Rel

goal (1 subgoal):
 1. \<And>x y z. (x, y) \<in> symcl Rel \<and> (y, z) \<in> symcl Rel \<Longrightarrow> (x, z) \<in> symcl Rel
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(a, b) \<in> Rel \<and> (b, c) \<in> Rel \<Longrightarrow> (a, c) \<in> symcl Rel
(a, b) \<in> Rel \<and> (c, b) \<in> Rel \<and> (a, c) \<notin> Rel \<Longrightarrow> (a, c) \<in> symcl Rel
(b, a) \<in> Rel \<and> (b, c) \<in> Rel \<and> (a, c) \<notin> Rel \<Longrightarrow> (a, c) \<in> symcl Rel
(b, a) \<in> Rel \<and> (c, b) \<in> Rel \<Longrightarrow> (a, c) \<in> symcl Rel
(a, b) \<in> symcl Rel
(b, c) \<in> symcl Rel
[PROOF STEP]
show "(a, c) \<in> symcl Rel"
[PROOF STATE]
proof (prove)
using this:
(a, b) \<in> Rel \<and> (b, c) \<in> Rel \<Longrightarrow> (a, c) \<in> symcl Rel
(a, b) \<in> Rel \<and> (c, b) \<in> Rel \<and> (a, c) \<notin> Rel \<Longrightarrow> (a, c) \<in> symcl Rel
(b, a) \<in> Rel \<and> (b, c) \<in> Rel \<and> (a, c) \<notin> Rel \<Longrightarrow> (a, c) \<in> symcl Rel
(b, a) \<in> Rel \<and> (c, b) \<in> Rel \<Longrightarrow> (a, c) \<in> symcl Rel
(a, b) \<in> symcl Rel
(b, c) \<in> symcl Rel

goal (1 subgoal):
 1. (a, c) \<in> symcl Rel
[PROOF STEP]
by (auto simp add: symcl_def)
[PROOF STATE]
proof (state)
this:
(a, c) \<in> symcl Rel

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma below_monic_ValF [iff]:
  "below_monic_cfun ValF"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. below_monic_cfun ValF
[PROOF STEP]
by (rule below_monicI) simp


[STATEMENT]
lemma sum_case_non [simp]: "\<not> is_sum a \<Longrightarrow> sum_case f g a = undefined"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> is_sum a \<Longrightarrow> sum_case f g a = undefined
[PROOF STEP]
by (simp add: sum_case_def is_sum_def)


[STATEMENT]
lemma Card_ord_of_nat [simp]: "Card (ord_of_nat n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Card (ord_of_nat n)
[PROOF STEP]
by (simp add: \<omega>_def nat_into_Card)


[STATEMENT]
lemma ordinal_cases:
assumes zero: "a = 0 \<Longrightarrow> P"
    and suc:  "\<And>x. a = oSuc x \<Longrightarrow> P"
    and lim:  "\<And>f. \<lbrakk>strict_mono f; a = oLimit f\<rbrakk> \<Longrightarrow> P"
shows "P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P
[PROOF STEP]
apply (subgoal_tac "\<forall>x. a = x \<longrightarrow> P", force)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x. a = x \<longrightarrow> P
[PROOF STEP]
apply (rule allI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. a = x \<longrightarrow> P
[PROOF STEP]
apply (rule_tac a=x in oLimit_induct)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. a = 0 \<longrightarrow> P
 2. \<And>x xa. a = xa \<longrightarrow> P \<Longrightarrow> a = oSuc xa \<longrightarrow> P
 3. \<And>x f. \<lbrakk>OrdinalInduct.strict_mono f; \<forall>n. a = f n \<longrightarrow> P\<rbrakk> \<Longrightarrow> a = oLimit f \<longrightarrow> P
[PROOF STEP]
apply (rule impI, erule zero)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x xa. a = xa \<longrightarrow> P \<Longrightarrow> a = oSuc xa \<longrightarrow> P
 2. \<And>x f. \<lbrakk>OrdinalInduct.strict_mono f; \<forall>n. a = f n \<longrightarrow> P\<rbrakk> \<Longrightarrow> a = oLimit f \<longrightarrow> P
[PROOF STEP]
apply (rule impI, erule suc)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x f. \<lbrakk>OrdinalInduct.strict_mono f; \<forall>n. a = f n \<longrightarrow> P\<rbrakk> \<Longrightarrow> a = oLimit f \<longrightarrow> P
[PROOF STEP]
apply (rule impI, erule lim, assumption)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma eq_subst_scheme_list_eq_free:
  "\<lbrakk> $S1 (A::type_scheme list) = $S2 A;  n:(free_tv A) \<rbrakk> \<Longrightarrow> S1 n = S2 n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>$ S1 A = $ S2 A; n \<in> free_tv A\<rbrakk> \<Longrightarrow> S1 n = S2 n
[PROOF STEP]
proof (induct A)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>$ S1 [] = $ S2 []; n \<in> free_tv []\<rbrakk> \<Longrightarrow> S1 n = S2 n
 2. \<And>a A. \<lbrakk>\<lbrakk>$ S1 A = $ S2 A; n \<in> free_tv A\<rbrakk> \<Longrightarrow> S1 n = S2 n; $ S1 (a # A) = $ S2 (a # A); n \<in> free_tv (a # A)\<rbrakk> \<Longrightarrow> S1 n = S2 n
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
$ S1 [] = $ S2 []
n \<in> free_tv []

goal (2 subgoals):
 1. \<lbrakk>$ S1 [] = $ S2 []; n \<in> free_tv []\<rbrakk> \<Longrightarrow> S1 n = S2 n
 2. \<And>a A. \<lbrakk>\<lbrakk>$ S1 A = $ S2 A; n \<in> free_tv A\<rbrakk> \<Longrightarrow> S1 n = S2 n; $ S1 (a # A) = $ S2 (a # A); n \<in> free_tv (a # A)\<rbrakk> \<Longrightarrow> S1 n = S2 n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
$ S1 [] = $ S2 []
n \<in> free_tv []
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
$ S1 [] = $ S2 []
n \<in> free_tv []

goal (1 subgoal):
 1. S1 n = S2 n
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
S1 n = S2 n

goal (1 subgoal):
 1. \<And>a A. \<lbrakk>\<lbrakk>$ S1 A = $ S2 A; n \<in> free_tv A\<rbrakk> \<Longrightarrow> S1 n = S2 n; $ S1 (a # A) = $ S2 (a # A); n \<in> free_tv (a # A)\<rbrakk> \<Longrightarrow> S1 n = S2 n
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a A. \<lbrakk>\<lbrakk>$ S1 A = $ S2 A; n \<in> free_tv A\<rbrakk> \<Longrightarrow> S1 n = S2 n; $ S1 (a # A) = $ S2 (a # A); n \<in> free_tv (a # A)\<rbrakk> \<Longrightarrow> S1 n = S2 n
[PROOF STEP]
case Cons
[PROOF STATE]
proof (state)
this:
\<lbrakk>$ S1 A_ = $ S2 A_; n \<in> free_tv A_\<rbrakk> \<Longrightarrow> S1 n = S2 n
$ S1 (a_ # A_) = $ S2 (a_ # A_)
n \<in> free_tv (a_ # A_)

goal (1 subgoal):
 1. \<And>a A. \<lbrakk>\<lbrakk>$ S1 A = $ S2 A; n \<in> free_tv A\<rbrakk> \<Longrightarrow> S1 n = S2 n; $ S1 (a # A) = $ S2 (a # A); n \<in> free_tv (a # A)\<rbrakk> \<Longrightarrow> S1 n = S2 n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>$ S1 A_ = $ S2 A_; n \<in> free_tv A_\<rbrakk> \<Longrightarrow> S1 n = S2 n
$ S1 (a_ # A_) = $ S2 (a_ # A_)
n \<in> free_tv (a_ # A_)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>$ S1 A_ = $ S2 A_; n \<in> free_tv A_\<rbrakk> \<Longrightarrow> S1 n = S2 n
$ S1 (a_ # A_) = $ S2 (a_ # A_)
n \<in> free_tv (a_ # A_)

goal (1 subgoal):
 1. S1 n = S2 n
[PROOF STEP]
by (fastforce intro: eq_subst_type_scheme_eq_free)
[PROOF STATE]
proof (state)
this:
S1 n = S2 n

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mgu_new:
  "[|mgu t1 t2 = Some u; new_tv n t1; new_tv n t2|] ==> new_tv n u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>mgu t1 t2 = Some u; new_tv n t1; new_tv n t2\<rbrakk> \<Longrightarrow> new_tv n u
[PROOF STEP]
by (meson UnE mgu_free new_tv_def subsetD)


[STATEMENT]
lemma PO_m1_inv0_fin_trans [iff]:
  "{m1_inv0_fin} trans m1 {> m1_inv0_fin}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {m1_inv0_fin} TS.trans m1 {> m1_inv0_fin}
[PROOF STEP]
by (auto simp add: PO_hoare_defs m1_defs intro!: m1_inv0_finI)


[STATEMENT]
lemma (in PolynRg) s_cf_pol_coeff:"p \<in> carrier R \<Longrightarrow>
                         pol_coeff S (s_cf R S X p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<in> carrier R \<Longrightarrow> pol_coeff S (s_cf R S X p)
[PROOF STEP]
apply (simp add:s_cf_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<in> carrier R \<Longrightarrow> (p = \<zero> \<longrightarrow> pol_coeff S (0, \<lambda>j. \<zero>\<^bsub>S\<^esub>)) \<and> (p \<noteq> \<zero> \<longrightarrow> pol_coeff S (SOME c. pol_coeff S c \<and> p = polyn_expr R X (fst c) c \<and> snd c (fst c) \<noteq> \<zero>\<^bsub>S\<^esub>))
[PROOF STEP]
apply (case_tac "p = \<zero>\<^bsub>R\<^esub>", simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<zero> \<in> carrier R; p = \<zero>\<rbrakk> \<Longrightarrow> pol_coeff S (0, \<lambda>j. \<zero>\<^bsub>S\<^esub>)
 2. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>\<rbrakk> \<Longrightarrow> (p = \<zero> \<longrightarrow> pol_coeff S (0, \<lambda>j. \<zero>\<^bsub>S\<^esub>)) \<and> (p \<noteq> \<zero> \<longrightarrow> pol_coeff S (SOME c. pol_coeff S c \<and> p = polyn_expr R X (fst c) c \<and> snd c (fst c) \<noteq> \<zero>\<^bsub>S\<^esub>))
[PROOF STEP]
apply (cut_tac subring, frule subring_Ring,
             simp add:pol_coeff_def Ring.ring_zero)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>\<rbrakk> \<Longrightarrow> (p = \<zero> \<longrightarrow> pol_coeff S (0, \<lambda>j. \<zero>\<^bsub>S\<^esub>)) \<and> (p \<noteq> \<zero> \<longrightarrow> pol_coeff S (SOME c. pol_coeff S c \<and> p = polyn_expr R X (fst c) c \<and> snd c (fst c) \<noteq> \<zero>\<^bsub>S\<^esub>))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>\<rbrakk> \<Longrightarrow> pol_coeff S (SOME c. pol_coeff S c \<and> p = polyn_expr R X (fst c) c \<and> snd c (fst c) \<noteq> \<zero>\<^bsub>S\<^esub>)
[PROOF STEP]
apply (rule someI2_ex)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>\<rbrakk> \<Longrightarrow> \<exists>a. pol_coeff S a \<and> p = polyn_expr R X (fst a) a \<and> snd a (fst a) \<noteq> \<zero>\<^bsub>S\<^esub>
 2. \<And>c. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S c \<and> p = polyn_expr R X (fst c) c \<and> snd c (fst c) \<noteq> \<zero>\<^bsub>S\<^esub>\<rbrakk> \<Longrightarrow> pol_coeff S c
[PROOF STEP]
apply (frule ex_polyn_expr[of p], erule exE, erule conjE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>c. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S c; p = polyn_expr R X (fst c) c\<rbrakk> \<Longrightarrow> \<exists>a. pol_coeff S a \<and> p = polyn_expr R X (fst a) a \<and> snd a (fst a) \<noteq> \<zero>\<^bsub>S\<^esub>
 2. \<And>c. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S c \<and> p = polyn_expr R X (fst c) c \<and> snd c (fst c) \<noteq> \<zero>\<^bsub>S\<^esub>\<rbrakk> \<Longrightarrow> pol_coeff S c
[PROOF STEP]
apply (frule_tac c = c in coeff_max_bddTr)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>c. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S c; p = polyn_expr R X (fst c) c; c_max S c \<le> fst c\<rbrakk> \<Longrightarrow> \<exists>a. pol_coeff S a \<and> p = polyn_expr R X (fst a) a \<and> snd a (fst a) \<noteq> \<zero>\<^bsub>S\<^esub>
 2. \<And>c. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S c \<and> p = polyn_expr R X (fst c) c \<and> snd c (fst c) \<noteq> \<zero>\<^bsub>S\<^esub>\<rbrakk> \<Longrightarrow> pol_coeff S c
[PROOF STEP]
apply (frule_tac c = c and n = "c_max S c" in pol_coeff_le, assumption)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>c. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S c; p = polyn_expr R X (fst c) c; c_max S c \<le> fst c; pol_coeff S (c_max S c, snd c)\<rbrakk> \<Longrightarrow> \<exists>a. pol_coeff S a \<and> p = polyn_expr R X (fst a) a \<and> snd a (fst a) \<noteq> \<zero>\<^bsub>S\<^esub>
 2. \<And>c. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S c \<and> p = polyn_expr R X (fst c) c \<and> snd c (fst c) \<noteq> \<zero>\<^bsub>S\<^esub>\<rbrakk> \<Longrightarrow> pol_coeff S c
[PROOF STEP]
apply (subgoal_tac "p = polyn_expr R X (fst (c_max S c, snd c))
                                                  (c_max S c, snd c) \<and>
                     snd (c_max S c, snd c) (fst (c_max S c, snd c)) \<noteq> \<zero>\<^bsub>S\<^esub>",
        blast)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>c. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S c; p = polyn_expr R X (fst c) c; c_max S c \<le> fst c; pol_coeff S (c_max S c, snd c)\<rbrakk> \<Longrightarrow> p = polyn_expr R X (fst (c_max S c, snd c)) (c_max S c, snd c) \<and> snd (c_max S c, snd c) (fst (c_max S c, snd c)) \<noteq> \<zero>\<^bsub>S\<^esub>
 2. \<And>c. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S c \<and> p = polyn_expr R X (fst c) c \<and> snd c (fst c) \<noteq> \<zero>\<^bsub>S\<^esub>\<rbrakk> \<Longrightarrow> pol_coeff S c
[PROOF STEP]
apply (rule conjI, simp)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>c. \<lbrakk>polyn_expr R X (fst c) c \<in> carrier R; polyn_expr R X (fst c) c \<noteq> \<zero>; pol_coeff S c; p = polyn_expr R X (fst c) c; c_max S c \<le> fst c; pol_coeff S (c_max S c, snd c)\<rbrakk> \<Longrightarrow> polyn_expr R X (fst c) c = polyn_expr R X (c_max S c) (c_max S c, snd c)
 2. \<And>c. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S c; p = polyn_expr R X (fst c) c; c_max S c \<le> fst c; pol_coeff S (c_max S c, snd c)\<rbrakk> \<Longrightarrow> snd (c_max S c, snd c) (fst (c_max S c, snd c)) \<noteq> \<zero>\<^bsub>S\<^esub>
 3. \<And>c. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S c \<and> p = polyn_expr R X (fst c) c \<and> snd c (fst c) \<noteq> \<zero>\<^bsub>S\<^esub>\<rbrakk> \<Longrightarrow> pol_coeff S c
[PROOF STEP]
apply (subst polyn_expr_short[THEN sym], assumption+)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>c. \<lbrakk>polyn_expr R X (fst c) c \<in> carrier R; polyn_expr R X (fst c) c \<noteq> \<zero>; pol_coeff S c; p = polyn_expr R X (fst c) c; c_max S c \<le> fst c; pol_coeff S (c_max S c, snd c)\<rbrakk> \<Longrightarrow> polyn_expr R X (fst c) c = polyn_expr R X (c_max S c) c
 2. \<And>c. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S c; p = polyn_expr R X (fst c) c; c_max S c \<le> fst c; pol_coeff S (c_max S c, snd c)\<rbrakk> \<Longrightarrow> snd (c_max S c, snd c) (fst (c_max S c, snd c)) \<noteq> \<zero>\<^bsub>S\<^esub>
 3. \<And>c. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S c \<and> p = polyn_expr R X (fst c) c \<and> snd c (fst c) \<noteq> \<zero>\<^bsub>S\<^esub>\<rbrakk> \<Longrightarrow> pol_coeff S c
[PROOF STEP]
apply (simp add:polyn_c_max)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>c. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S c; p = polyn_expr R X (fst c) c; c_max S c \<le> fst c; pol_coeff S (c_max S c, snd c)\<rbrakk> \<Longrightarrow> snd (c_max S c, snd c) (fst (c_max S c, snd c)) \<noteq> \<zero>\<^bsub>S\<^esub>
 2. \<And>c. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S c \<and> p = polyn_expr R X (fst c) c \<and> snd c (fst c) \<noteq> \<zero>\<^bsub>S\<^esub>\<rbrakk> \<Longrightarrow> pol_coeff S c
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>c. \<lbrakk>polyn_expr R X (fst c) c \<in> carrier R; polyn_expr R X (fst c) c \<noteq> \<zero>; pol_coeff S c; p = polyn_expr R X (fst c) c; c_max S c \<le> fst c; pol_coeff S (c_max S c, snd c)\<rbrakk> \<Longrightarrow> snd c (c_max S c) \<noteq> \<zero>\<^bsub>S\<^esub>
 2. \<And>c. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S c \<and> p = polyn_expr R X (fst c) c \<and> snd c (fst c) \<noteq> \<zero>\<^bsub>S\<^esub>\<rbrakk> \<Longrightarrow> pol_coeff S c
[PROOF STEP]
apply (rule coeff_max_nonzeroTr, assumption)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>c. \<lbrakk>polyn_expr R X (fst c) c \<in> carrier R; polyn_expr R X (fst c) c \<noteq> \<zero>; pol_coeff S c; p = polyn_expr R X (fst c) c; c_max S c \<le> fst c; pol_coeff S (c_max S c, snd c)\<rbrakk> \<Longrightarrow> \<exists>j\<le>fst c. snd c j \<noteq> \<zero>\<^bsub>S\<^esub>
 2. \<And>c. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S c \<and> p = polyn_expr R X (fst c) c \<and> snd c (fst c) \<noteq> \<zero>\<^bsub>S\<^esub>\<rbrakk> \<Longrightarrow> pol_coeff S c
[PROOF STEP]
apply (simp add:coeff_0_pol_0[THEN sym])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>c. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S c \<and> p = polyn_expr R X (fst c) c \<and> snd c (fst c) \<noteq> \<zero>\<^bsub>S\<^esub>\<rbrakk> \<Longrightarrow> pol_coeff S c
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma setdiff_diff_insert: "A-B-C=D-E-F \<Longrightarrow> insert m (A-B-C) = insert m (D-E-F)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A - B - C = D - E - F \<Longrightarrow> insert m (A - B - C) = insert m (D - E - F)
[PROOF STEP]
by simp


[STATEMENT]
lemma sum_reorder_triple: "(\<Sum> l \<in> A . (\<Sum> i \<in> B . (\<Sum> j \<in> C . g l i j))) =
  (\<Sum> i \<in> B . (\<Sum> j \<in> C . (\<Sum> l \<in> A . g l i j)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>l\<in>A. \<Sum>i\<in>B. sum (g l i) C) = (\<Sum>i\<in>B. \<Sum>j\<in>C. \<Sum>l\<in>A. g l i j)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<Sum>l\<in>A. \<Sum>i\<in>B. sum (g l i) C) = (\<Sum>i\<in>B. \<Sum>j\<in>C. \<Sum>l\<in>A. g l i j)
[PROOF STEP]
have "(\<Sum> l \<in> A . (\<Sum> i \<in> B . (\<Sum> j \<in> C . g l i j))) = (\<Sum>i \<in> B . (\<Sum> l \<in> A  . (\<Sum> j \<in> C . g l i j)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>l\<in>A. \<Sum>i\<in>B. sum (g l i) C) = (\<Sum>i\<in>B. \<Sum>l\<in>A. sum (g l i) C)
[PROOF STEP]
using sum.swap[of "(\<lambda> l i . (\<Sum> j \<in> C . g l i j))" "B" "A"]
[PROOF STATE]
proof (prove)
using this:
(\<Sum>i\<in>A. \<Sum>ia\<in>B. sum (g i ia) C) = (\<Sum>j\<in>B. \<Sum>i\<in>A. sum (g i j) C)

goal (1 subgoal):
 1. (\<Sum>l\<in>A. \<Sum>i\<in>B. sum (g l i) C) = (\<Sum>i\<in>B. \<Sum>l\<in>A. sum (g l i) C)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<Sum>l\<in>A. \<Sum>i\<in>B. sum (g l i) C) = (\<Sum>i\<in>B. \<Sum>l\<in>A. sum (g l i) C)

goal (1 subgoal):
 1. (\<Sum>l\<in>A. \<Sum>i\<in>B. sum (g l i) C) = (\<Sum>i\<in>B. \<Sum>j\<in>C. \<Sum>l\<in>A. g l i j)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>l\<in>A. \<Sum>i\<in>B. sum (g l i) C) = (\<Sum>i\<in>B. \<Sum>l\<in>A. sum (g l i) C)

goal (1 subgoal):
 1. (\<Sum>l\<in>A. \<Sum>i\<in>B. sum (g l i) C) = (\<Sum>i\<in>B. \<Sum>j\<in>C. \<Sum>l\<in>A. g l i j)
[PROOF STEP]
have "...  = (\<Sum>i \<in> B . (\<Sum> j \<in> C . (\<Sum>l \<in> A . g l i j)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i\<in>B. \<Sum>l\<in>A. sum (g l i) C) = (\<Sum>i\<in>B. \<Sum>j\<in>C. \<Sum>l\<in>A. g l i j)
[PROOF STEP]
using sum.swap
[PROOF STATE]
proof (prove)
using this:
(\<Sum>i\<in>?A. sum (?g i) ?B) = (\<Sum>j\<in>?B. \<Sum>i\<in>?A. ?g i j)

goal (1 subgoal):
 1. (\<Sum>i\<in>B. \<Sum>l\<in>A. sum (g l i) C) = (\<Sum>i\<in>B. \<Sum>j\<in>C. \<Sum>l\<in>A. g l i j)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
(\<Sum>i\<in>B. \<Sum>l\<in>A. sum (g l i) C) = (\<Sum>i\<in>B. \<Sum>j\<in>C. \<Sum>l\<in>A. g l i j)

goal (1 subgoal):
 1. (\<Sum>l\<in>A. \<Sum>i\<in>B. sum (g l i) C) = (\<Sum>i\<in>B. \<Sum>j\<in>C. \<Sum>l\<in>A. g l i j)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<Sum>l\<in>A. \<Sum>i\<in>B. sum (g l i) C) = (\<Sum>i\<in>B. \<Sum>j\<in>C. \<Sum>l\<in>A. g l i j)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<Sum>l\<in>A. \<Sum>i\<in>B. sum (g l i) C) = (\<Sum>i\<in>B. \<Sum>j\<in>C. \<Sum>l\<in>A. g l i j)

goal (1 subgoal):
 1. (\<Sum>l\<in>A. \<Sum>i\<in>B. sum (g l i) C) = (\<Sum>i\<in>B. \<Sum>j\<in>C. \<Sum>l\<in>A. g l i j)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<Sum>l\<in>A. \<Sum>i\<in>B. sum (g l i) C) = (\<Sum>i\<in>B. \<Sum>j\<in>C. \<Sum>l\<in>A. g l i j)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma a_meet_d: "a \<sqinter> (d_aux a b c) = (a \<sqinter> b) \<squnion> (c \<sqinter> a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<sqinter> d_aux a b c = a \<sqinter> b \<squnion> c \<sqinter> a
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a \<sqinter> d_aux a b c = a \<sqinter> b \<squnion> c \<sqinter> a
[PROOF STEP]
have "a \<sqinter> (d_aux a b c) = a \<sqinter> ((a \<sqinter> b) \<squnion> (b \<sqinter> c) \<squnion> (c \<sqinter> a))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<sqinter> d_aux a b c = a \<sqinter> (a \<sqinter> b \<squnion> b \<sqinter> c \<squnion> c \<sqinter> a)
[PROOF STEP]
by (simp add: d_aux_def)
[PROOF STATE]
proof (state)
this:
a \<sqinter> d_aux a b c = a \<sqinter> (a \<sqinter> b \<squnion> b \<sqinter> c \<squnion> c \<sqinter> a)

goal (1 subgoal):
 1. a \<sqinter> d_aux a b c = a \<sqinter> b \<squnion> c \<sqinter> a
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
a \<sqinter> d_aux a b c = a \<sqinter> (a \<sqinter> b \<squnion> b \<sqinter> c \<squnion> c \<sqinter> a)

goal (1 subgoal):
 1. a \<sqinter> d_aux a b c = a \<sqinter> b \<squnion> c \<sqinter> a
[PROOF STEP]
have "... = a \<sqinter> (a \<sqinter> b \<squnion> c \<sqinter> a \<squnion> b \<sqinter> c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<sqinter> (a \<sqinter> b \<squnion> b \<sqinter> c \<squnion> c \<sqinter> a) = a \<sqinter> (a \<sqinter> b \<squnion> c \<sqinter> a \<squnion> b \<sqinter> c)
[PROOF STEP]
by (simp add: sup_assoc, simp add: sup_commute)
[PROOF STATE]
proof (state)
this:
a \<sqinter> (a \<sqinter> b \<squnion> b \<sqinter> c \<squnion> c \<sqinter> a) = a \<sqinter> (a \<sqinter> b \<squnion> c \<sqinter> a \<squnion> b \<sqinter> c)

goal (1 subgoal):
 1. a \<sqinter> d_aux a b c = a \<sqinter> b \<squnion> c \<sqinter> a
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
a \<sqinter> (a \<sqinter> b \<squnion> b \<sqinter> c \<squnion> c \<sqinter> a) = a \<sqinter> (a \<sqinter> b \<squnion> c \<sqinter> a \<squnion> b \<sqinter> c)

goal (1 subgoal):
 1. a \<sqinter> d_aux a b c = a \<sqinter> b \<squnion> c \<sqinter> a
[PROOF STEP]
have "... = (a \<sqinter> b \<squnion> c \<sqinter> a) \<squnion> (a \<sqinter> (b \<sqinter> c))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<sqinter> (a \<sqinter> b \<squnion> c \<sqinter> a \<squnion> b \<sqinter> c) = a \<sqinter> b \<squnion> c \<sqinter> a \<squnion> a \<sqinter> (b \<sqinter> c)
[PROOF STEP]
by (simp add: modular)
[PROOF STATE]
proof (state)
this:
a \<sqinter> (a \<sqinter> b \<squnion> c \<sqinter> a \<squnion> b \<sqinter> c) = a \<sqinter> b \<squnion> c \<sqinter> a \<squnion> a \<sqinter> (b \<sqinter> c)

goal (1 subgoal):
 1. a \<sqinter> d_aux a b c = a \<sqinter> b \<squnion> c \<sqinter> a
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
a \<sqinter> (a \<sqinter> b \<squnion> c \<sqinter> a \<squnion> b \<sqinter> c) = a \<sqinter> b \<squnion> c \<sqinter> a \<squnion> a \<sqinter> (b \<sqinter> c)

goal (1 subgoal):
 1. a \<sqinter> d_aux a b c = a \<sqinter> b \<squnion> c \<sqinter> a
[PROOF STEP]
have "... = (a \<sqinter> b) \<squnion> (c \<sqinter> a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<sqinter> b \<squnion> c \<sqinter> a \<squnion> a \<sqinter> (b \<sqinter> c) = a \<sqinter> b \<squnion> c \<sqinter> a
[PROOF STEP]
by (rule order.antisym, simp_all, rule_tac y = "a \<sqinter> b" in order_trans, simp_all)
[PROOF STATE]
proof (state)
this:
a \<sqinter> b \<squnion> c \<sqinter> a \<squnion> a \<sqinter> (b \<sqinter> c) = a \<sqinter> b \<squnion> c \<sqinter> a

goal (1 subgoal):
 1. a \<sqinter> d_aux a b c = a \<sqinter> b \<squnion> c \<sqinter> a
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
a \<sqinter> d_aux a b c = a \<sqinter> b \<squnion> c \<sqinter> a
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
a \<sqinter> d_aux a b c = a \<sqinter> b \<squnion> c \<sqinter> a

goal (1 subgoal):
 1. a \<sqinter> d_aux a b c = a \<sqinter> b \<squnion> c \<sqinter> a
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
a \<sqinter> d_aux a b c = a \<sqinter> b \<squnion> c \<sqinter> a

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma arith_prog_Suc_0_right [simp]: "arith_prog a (Suc 0) = UNIV"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. arith_prog a (Suc 0) = UNIV
[PROOF STEP]
by (auto simp: arith_prog_def)


[STATEMENT]
lemma arith_prog_dvd_mono: "b dvd b' \<Longrightarrow> arith_prog a b' \<subseteq> arith_prog a b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b dvd b' \<Longrightarrow> arith_prog a b' \<subseteq> arith_prog a b
[PROOF STEP]
by (auto simp: arith_prog_def cong_dvd_modulus)


[STATEMENT]
lemma relevant_vars_subl:
  assumes "\<forall>x \<in> vars\<^sub>l l. \<sigma>\<^sub>1 x = \<sigma>\<^sub>2 x "
  shows "l \<cdot>\<^sub>l \<sigma>\<^sub>1 = l \<cdot>\<^sub>l \<sigma>\<^sub>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l \<cdot>\<^sub>l \<sigma>\<^sub>1 = l \<cdot>\<^sub>l \<sigma>\<^sub>2
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>vars\<^sub>l l. \<sigma>\<^sub>1 x = \<sigma>\<^sub>2 x

goal (1 subgoal):
 1. l \<cdot>\<^sub>l \<sigma>\<^sub>1 = l \<cdot>\<^sub>l \<sigma>\<^sub>2
[PROOF STEP]
proof (induction l)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x1 x2. \<forall>x\<in>vars\<^sub>l (Pos x1 x2). \<sigma>\<^sub>1 x = \<sigma>\<^sub>2 x \<Longrightarrow> Pos x1 x2 \<cdot>\<^sub>l \<sigma>\<^sub>1 = Pos x1 x2 \<cdot>\<^sub>l \<sigma>\<^sub>2
 2. \<And>x1 x2. \<forall>x\<in>vars\<^sub>l (Neg x1 x2). \<sigma>\<^sub>1 x = \<sigma>\<^sub>2 x \<Longrightarrow> Neg x1 x2 \<cdot>\<^sub>l \<sigma>\<^sub>1 = Neg x1 x2 \<cdot>\<^sub>l \<sigma>\<^sub>2
[PROOF STEP]
case (Pos p ts)
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>vars\<^sub>l (Pos p ts). \<sigma>\<^sub>1 x = \<sigma>\<^sub>2 x

goal (2 subgoals):
 1. \<And>x1 x2. \<forall>x\<in>vars\<^sub>l (Pos x1 x2). \<sigma>\<^sub>1 x = \<sigma>\<^sub>2 x \<Longrightarrow> Pos x1 x2 \<cdot>\<^sub>l \<sigma>\<^sub>1 = Pos x1 x2 \<cdot>\<^sub>l \<sigma>\<^sub>2
 2. \<And>x1 x2. \<forall>x\<in>vars\<^sub>l (Neg x1 x2). \<sigma>\<^sub>1 x = \<sigma>\<^sub>2 x \<Longrightarrow> Neg x1 x2 \<cdot>\<^sub>l \<sigma>\<^sub>1 = Neg x1 x2 \<cdot>\<^sub>l \<sigma>\<^sub>2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>x\<in>vars\<^sub>l (Pos p ts). \<sigma>\<^sub>1 x = \<sigma>\<^sub>2 x
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>vars\<^sub>l (Pos p ts). \<sigma>\<^sub>1 x = \<sigma>\<^sub>2 x

goal (1 subgoal):
 1. Pos p ts \<cdot>\<^sub>l \<sigma>\<^sub>1 = Pos p ts \<cdot>\<^sub>l \<sigma>\<^sub>2
[PROOF STEP]
using relevant_vars_subts
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>vars\<^sub>l (Pos p ts). \<sigma>\<^sub>1 x = \<sigma>\<^sub>2 x
\<forall>x\<in>vars\<^sub>t\<^sub>s ?ts. ?\<sigma>\<^sub>1 x = ?\<sigma>\<^sub>2 x \<Longrightarrow> ?ts \<cdot>\<^sub>t\<^sub>s ?\<sigma>\<^sub>1 = ?ts \<cdot>\<^sub>t\<^sub>s ?\<sigma>\<^sub>2

goal (1 subgoal):
 1. Pos p ts \<cdot>\<^sub>l \<sigma>\<^sub>1 = Pos p ts \<cdot>\<^sub>l \<sigma>\<^sub>2
[PROOF STEP]
unfolding vars\<^sub>l_def
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>vars\<^sub>t\<^sub>s (get_terms (Pos p ts)). \<sigma>\<^sub>1 x = \<sigma>\<^sub>2 x
\<forall>x\<in>vars\<^sub>t\<^sub>s ?ts. ?\<sigma>\<^sub>1 x = ?\<sigma>\<^sub>2 x \<Longrightarrow> ?ts \<cdot>\<^sub>t\<^sub>s ?\<sigma>\<^sub>1 = ?ts \<cdot>\<^sub>t\<^sub>s ?\<sigma>\<^sub>2

goal (1 subgoal):
 1. Pos p ts \<cdot>\<^sub>l \<sigma>\<^sub>1 = Pos p ts \<cdot>\<^sub>l \<sigma>\<^sub>2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Pos p ts \<cdot>\<^sub>l \<sigma>\<^sub>1 = Pos p ts \<cdot>\<^sub>l \<sigma>\<^sub>2

goal (1 subgoal):
 1. \<And>x1 x2. \<forall>x\<in>vars\<^sub>l (Neg x1 x2). \<sigma>\<^sub>1 x = \<sigma>\<^sub>2 x \<Longrightarrow> Neg x1 x2 \<cdot>\<^sub>l \<sigma>\<^sub>1 = Neg x1 x2 \<cdot>\<^sub>l \<sigma>\<^sub>2
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x1 x2. \<forall>x\<in>vars\<^sub>l (Neg x1 x2). \<sigma>\<^sub>1 x = \<sigma>\<^sub>2 x \<Longrightarrow> Neg x1 x2 \<cdot>\<^sub>l \<sigma>\<^sub>1 = Neg x1 x2 \<cdot>\<^sub>l \<sigma>\<^sub>2
[PROOF STEP]
case (Neg p ts)
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>vars\<^sub>l (Neg p ts). \<sigma>\<^sub>1 x = \<sigma>\<^sub>2 x

goal (1 subgoal):
 1. \<And>x1 x2. \<forall>x\<in>vars\<^sub>l (Neg x1 x2). \<sigma>\<^sub>1 x = \<sigma>\<^sub>2 x \<Longrightarrow> Neg x1 x2 \<cdot>\<^sub>l \<sigma>\<^sub>1 = Neg x1 x2 \<cdot>\<^sub>l \<sigma>\<^sub>2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>x\<in>vars\<^sub>l (Neg p ts). \<sigma>\<^sub>1 x = \<sigma>\<^sub>2 x
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>vars\<^sub>l (Neg p ts). \<sigma>\<^sub>1 x = \<sigma>\<^sub>2 x

goal (1 subgoal):
 1. Neg p ts \<cdot>\<^sub>l \<sigma>\<^sub>1 = Neg p ts \<cdot>\<^sub>l \<sigma>\<^sub>2
[PROOF STEP]
using relevant_vars_subts
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>vars\<^sub>l (Neg p ts). \<sigma>\<^sub>1 x = \<sigma>\<^sub>2 x
\<forall>x\<in>vars\<^sub>t\<^sub>s ?ts. ?\<sigma>\<^sub>1 x = ?\<sigma>\<^sub>2 x \<Longrightarrow> ?ts \<cdot>\<^sub>t\<^sub>s ?\<sigma>\<^sub>1 = ?ts \<cdot>\<^sub>t\<^sub>s ?\<sigma>\<^sub>2

goal (1 subgoal):
 1. Neg p ts \<cdot>\<^sub>l \<sigma>\<^sub>1 = Neg p ts \<cdot>\<^sub>l \<sigma>\<^sub>2
[PROOF STEP]
unfolding vars\<^sub>l_def
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>vars\<^sub>t\<^sub>s (get_terms (Neg p ts)). \<sigma>\<^sub>1 x = \<sigma>\<^sub>2 x
\<forall>x\<in>vars\<^sub>t\<^sub>s ?ts. ?\<sigma>\<^sub>1 x = ?\<sigma>\<^sub>2 x \<Longrightarrow> ?ts \<cdot>\<^sub>t\<^sub>s ?\<sigma>\<^sub>1 = ?ts \<cdot>\<^sub>t\<^sub>s ?\<sigma>\<^sub>2

goal (1 subgoal):
 1. Neg p ts \<cdot>\<^sub>l \<sigma>\<^sub>1 = Neg p ts \<cdot>\<^sub>l \<sigma>\<^sub>2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Neg p ts \<cdot>\<^sub>l \<sigma>\<^sub>1 = Neg p ts \<cdot>\<^sub>l \<sigma>\<^sub>2

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma foldr_cong_plus: (* a more elaborate version of foldr_cong. Using f'=id, g'=id and s = set lst would give foldr_cong exactly. *)
  assumes f_is_g : "\<And> a b c. b \<in> s \<Longrightarrow> f' a = f b (f' c) \<Longrightarrow> g' a = g b (g' c)" (* main assumption *)
      and f'_inj : "\<And> a b. f' a = f' b \<Longrightarrow> a = b"
      and f_bit_sur : "\<And> a b c. f' a = f b c \<Longrightarrow> \<exists> c'. c = f' c'" (* should be provable by cases c *)
      and lst_in_s : "set lst \<subseteq> s" (* formulated like this to make induction easier *)
  shows "f' a = foldr f lst (f' b) \<Longrightarrow> g' a = foldr g lst (g' b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f' a = foldr f lst (f' b) \<Longrightarrow> g' a = foldr g lst (g' b)
[PROOF STEP]
using lst_in_s
[PROOF STATE]
proof (prove)
using this:
set lst \<subseteq> s

goal (1 subgoal):
 1. f' a = foldr f lst (f' b) \<Longrightarrow> g' a = foldr g lst (g' b)
[PROOF STEP]
proof (induct lst arbitrary: a)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>f' a = foldr f [] (f' b); set [] \<subseteq> s\<rbrakk> \<Longrightarrow> g' a = foldr g [] (g' b)
 2. \<And>a lst aa. \<lbrakk>\<And>a. \<lbrakk>f' a = foldr f lst (f' b); set lst \<subseteq> s\<rbrakk> \<Longrightarrow> g' a = foldr g lst (g' b); f' aa = foldr f (a # lst) (f' b); set (a # lst) \<subseteq> s\<rbrakk> \<Longrightarrow> g' aa = foldr g (a # lst) (g' b)
[PROOF STEP]
case (Cons x xs)
[PROOF STATE]
proof (state)
this:
\<lbrakk>f' ?a = foldr f xs (f' b); set xs \<subseteq> s\<rbrakk> \<Longrightarrow> g' ?a = foldr g xs (g' b)
f' a = foldr f (x # xs) (f' b)
set (x # xs) \<subseteq> s

goal (2 subgoals):
 1. \<And>a. \<lbrakk>f' a = foldr f [] (f' b); set [] \<subseteq> s\<rbrakk> \<Longrightarrow> g' a = foldr g [] (g' b)
 2. \<And>a lst aa. \<lbrakk>\<And>a. \<lbrakk>f' a = foldr f lst (f' b); set lst \<subseteq> s\<rbrakk> \<Longrightarrow> g' a = foldr g lst (g' b); f' aa = foldr f (a # lst) (f' b); set (a # lst) \<subseteq> s\<rbrakk> \<Longrightarrow> g' aa = foldr g (a # lst) (g' b)
[PROOF STEP]
have prems: "f' a = (f x \<circ> foldr f xs) (f' b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f' a = (f x \<circ> foldr f xs) (f' b)
[PROOF STEP]
using Cons.prems
[PROOF STATE]
proof (prove)
using this:
f' a = foldr f (x # xs) (f' b)
set (x # xs) \<subseteq> s

goal (1 subgoal):
 1. f' a = (f x \<circ> foldr f xs) (f' b)
[PROOF STEP]
unfolding foldr_Cons
[PROOF STATE]
proof (prove)
using this:
f' a = (f x \<circ> foldr f xs) (f' b)
set (x # xs) \<subseteq> s

goal (1 subgoal):
 1. f' a = (f x \<circ> foldr f xs) (f' b)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f' a = (f x \<circ> foldr f xs) (f' b)

goal (2 subgoals):
 1. \<And>a. \<lbrakk>f' a = foldr f [] (f' b); set [] \<subseteq> s\<rbrakk> \<Longrightarrow> g' a = foldr g [] (g' b)
 2. \<And>a lst aa. \<lbrakk>\<And>a. \<lbrakk>f' a = foldr f lst (f' b); set lst \<subseteq> s\<rbrakk> \<Longrightarrow> g' a = foldr g lst (g' b); f' aa = foldr f (a # lst) (f' b); set (a # lst) \<subseteq> s\<rbrakk> \<Longrightarrow> g' aa = foldr g (a # lst) (g' b)
[PROOF STEP]
hence "\<exists> c'. f' c' = foldr f xs (f' b)"
[PROOF STATE]
proof (prove)
using this:
f' a = (f x \<circ> foldr f xs) (f' b)

goal (1 subgoal):
 1. \<exists>c'. f' c' = foldr f xs (f' b)
[PROOF STEP]
using f_bit_sur
[PROOF STATE]
proof (prove)
using this:
f' a = (f x \<circ> foldr f xs) (f' b)
f' ?a = f ?b ?c \<Longrightarrow> \<exists>c'. ?c = f' c'

goal (1 subgoal):
 1. \<exists>c'. f' c' = foldr f xs (f' b)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<exists>c'. f' c' = foldr f xs (f' b)

goal (2 subgoals):
 1. \<And>a. \<lbrakk>f' a = foldr f [] (f' b); set [] \<subseteq> s\<rbrakk> \<Longrightarrow> g' a = foldr g [] (g' b)
 2. \<And>a lst aa. \<lbrakk>\<And>a. \<lbrakk>f' a = foldr f lst (f' b); set lst \<subseteq> s\<rbrakk> \<Longrightarrow> g' a = foldr g lst (g' b); f' aa = foldr f (a # lst) (f' b); set (a # lst) \<subseteq> s\<rbrakk> \<Longrightarrow> g' aa = foldr g (a # lst) (g' b)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>c'. f' c' = foldr f xs (f' b)
[PROOF STEP]
obtain c' where c'_def: "f' c' = foldr f xs (f' b)"
[PROOF STATE]
proof (prove)
using this:
\<exists>c'. f' c' = foldr f xs (f' b)

goal (1 subgoal):
 1. (\<And>c'. f' c' = foldr f xs (f' b) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
f' c' = foldr f xs (f' b)

goal (2 subgoals):
 1. \<And>a. \<lbrakk>f' a = foldr f [] (f' b); set [] \<subseteq> s\<rbrakk> \<Longrightarrow> g' a = foldr g [] (g' b)
 2. \<And>a lst aa. \<lbrakk>\<And>a. \<lbrakk>f' a = foldr f lst (f' b); set lst \<subseteq> s\<rbrakk> \<Longrightarrow> g' a = foldr g lst (g' b); f' aa = foldr f (a # lst) (f' b); set (a # lst) \<subseteq> s\<rbrakk> \<Longrightarrow> g' aa = foldr g (a # lst) (g' b)
[PROOF STEP]
hence "f' a = f x (f' c')"
[PROOF STATE]
proof (prove)
using this:
f' c' = foldr f xs (f' b)

goal (1 subgoal):
 1. f' a = f x (f' c')
[PROOF STEP]
using prems
[PROOF STATE]
proof (prove)
using this:
f' c' = foldr f xs (f' b)
f' a = (f x \<circ> foldr f xs) (f' b)

goal (1 subgoal):
 1. f' a = f x (f' c')
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
f' a = f x (f' c')

goal (2 subgoals):
 1. \<And>a. \<lbrakk>f' a = foldr f [] (f' b); set [] \<subseteq> s\<rbrakk> \<Longrightarrow> g' a = foldr g [] (g' b)
 2. \<And>a lst aa. \<lbrakk>\<And>a. \<lbrakk>f' a = foldr f lst (f' b); set lst \<subseteq> s\<rbrakk> \<Longrightarrow> g' a = foldr g lst (g' b); f' aa = foldr f (a # lst) (f' b); set (a # lst) \<subseteq> s\<rbrakk> \<Longrightarrow> g' aa = foldr g (a # lst) (g' b)
[PROOF STEP]
hence "g' a = g x (g' c')"
[PROOF STATE]
proof (prove)
using this:
f' a = f x (f' c')

goal (1 subgoal):
 1. g' a = g x (g' c')
[PROOF STEP]
using f_is_g Cons.prems(2)
[PROOF STATE]
proof (prove)
using this:
f' a = f x (f' c')
\<lbrakk>?b \<in> s; f' ?a = f ?b (f' ?c)\<rbrakk> \<Longrightarrow> g' ?a = g ?b (g' ?c)
set (x # xs) \<subseteq> s

goal (1 subgoal):
 1. g' a = g x (g' c')
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
g' a = g x (g' c')

goal (2 subgoals):
 1. \<And>a. \<lbrakk>f' a = foldr f [] (f' b); set [] \<subseteq> s\<rbrakk> \<Longrightarrow> g' a = foldr g [] (g' b)
 2. \<And>a lst aa. \<lbrakk>\<And>a. \<lbrakk>f' a = foldr f lst (f' b); set lst \<subseteq> s\<rbrakk> \<Longrightarrow> g' a = foldr g lst (g' b); f' aa = foldr f (a # lst) (f' b); set (a # lst) \<subseteq> s\<rbrakk> \<Longrightarrow> g' aa = foldr g (a # lst) (g' b)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
g' a = g x (g' c')

goal (2 subgoals):
 1. \<And>a. \<lbrakk>f' a = foldr f [] (f' b); set [] \<subseteq> s\<rbrakk> \<Longrightarrow> g' a = foldr g [] (g' b)
 2. \<And>a lst aa. \<lbrakk>\<And>a. \<lbrakk>f' a = foldr f lst (f' b); set lst \<subseteq> s\<rbrakk> \<Longrightarrow> g' a = foldr g lst (g' b); f' aa = foldr f (a # lst) (f' b); set (a # lst) \<subseteq> s\<rbrakk> \<Longrightarrow> g' aa = foldr g (a # lst) (g' b)
[PROOF STEP]
have "g' c' = foldr g xs (g' b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g' c' = foldr g xs (g' b)
[PROOF STEP]
using Cons.hyps[of c'] c'_def Cons.prems(2)
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>f' c' = foldr f xs (f' b); set xs \<subseteq> s\<rbrakk> \<Longrightarrow> g' c' = foldr g xs (g' b)
f' c' = foldr f xs (f' b)
set (x # xs) \<subseteq> s

goal (1 subgoal):
 1. g' c' = foldr g xs (g' b)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
g' c' = foldr g xs (g' b)

goal (2 subgoals):
 1. \<And>a. \<lbrakk>f' a = foldr f [] (f' b); set [] \<subseteq> s\<rbrakk> \<Longrightarrow> g' a = foldr g [] (g' b)
 2. \<And>a lst aa. \<lbrakk>\<And>a. \<lbrakk>f' a = foldr f lst (f' b); set lst \<subseteq> s\<rbrakk> \<Longrightarrow> g' a = foldr g lst (g' b); f' aa = foldr f (a # lst) (f' b); set (a # lst) \<subseteq> s\<rbrakk> \<Longrightarrow> g' aa = foldr g (a # lst) (g' b)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
g' a = g x (foldr g xs (g' b))
[PROOF STEP]
have "g' a = (g x \<circ> foldr g xs) (g' b)"
[PROOF STATE]
proof (prove)
using this:
g' a = g x (foldr g xs (g' b))

goal (1 subgoal):
 1. g' a = (g x \<circ> foldr g xs) (g' b)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
g' a = (g x \<circ> foldr g xs) (g' b)

goal (2 subgoals):
 1. \<And>a. \<lbrakk>f' a = foldr f [] (f' b); set [] \<subseteq> s\<rbrakk> \<Longrightarrow> g' a = foldr g [] (g' b)
 2. \<And>a lst aa. \<lbrakk>\<And>a. \<lbrakk>f' a = foldr f lst (f' b); set lst \<subseteq> s\<rbrakk> \<Longrightarrow> g' a = foldr g lst (g' b); f' aa = foldr f (a # lst) (f' b); set (a # lst) \<subseteq> s\<rbrakk> \<Longrightarrow> g' aa = foldr g (a # lst) (g' b)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
g' a = (g x \<circ> foldr g xs) (g' b)

goal (1 subgoal):
 1. g' a = foldr g (x # xs) (g' b)
[PROOF STEP]
using foldr_Cons
[PROOF STATE]
proof (prove)
using this:
g' a = (g x \<circ> foldr g xs) (g' b)
foldr ?f (?x # ?xs) = ?f ?x \<circ> foldr ?f ?xs

goal (1 subgoal):
 1. g' a = foldr g (x # xs) (g' b)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
g' a = foldr g (x # xs) (g' b)

goal (1 subgoal):
 1. \<And>a. \<lbrakk>f' a = foldr f [] (f' b); set [] \<subseteq> s\<rbrakk> \<Longrightarrow> g' a = foldr g [] (g' b)
[PROOF STEP]
qed (insert f'_inj, auto)


[STATEMENT]
lemma eqButUID_step_\<phi>_imp:
assumes ss1: "eqButUID s s1"
and rs: "reach s" and rs1: "reach s1"
and step: "step s a = (ou,s')" and step1: "step s1 a = (ou1,s1')"
and a: "a \<noteq> Cact (cFriend UID1 (pass s UID1) UID2) \<and> a \<noteq> Cact (cFriend UID2 (pass s UID2) UID1) \<and>
        a \<noteq> Dact (dFriend UID1 (pass s UID1) UID2) \<and> a \<noteq> Dact (dFriend UID2 (pass s UID2) UID1)"
and \<phi>: "\<phi> (Trans s a ou s')"
shows "\<phi> (Trans s1 a ou1 s1')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi> (Trans s1 a ou1 s1')
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<phi> (Trans s1 a ou1 s1')
[PROOF STEP]
have "eqButUID s' s1'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eqButUID s' s1'
[PROOF STEP]
using eqButUID_step[OF ss1 step step1 rs rs1]
[PROOF STATE]
proof (prove)
using this:
eqButUID s' s1'

goal (1 subgoal):
 1. eqButUID s' s1'
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
eqButUID s' s1'

goal (1 subgoal):
 1. \<phi> (Trans s1 a ou1 s1')
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
eqButUID s' s1'
[PROOF STEP]
have "open s = open s1" and "open s' = open s1'"
        and "openByA s = openByA s1" and "openByA s' = openByA s1'"
        and "openByF s = openByF s1" and "openByF s' = openByF s1'"
[PROOF STATE]
proof (prove)
using this:
eqButUID s' s1'

goal (1 subgoal):
 1. (open s = open s1 &&& open s' = open s1' &&& openByA s = openByA s1) &&& openByA s' = openByA s1' &&& openByF s = openByF s1 &&& openByF s' = openByF s1'
[PROOF STEP]
using ss1
[PROOF STATE]
proof (prove)
using this:
eqButUID s' s1'
eqButUID s s1

goal (1 subgoal):
 1. (open s = open s1 &&& open s' = open s1' &&& openByA s = openByA s1) &&& openByA s' = openByA s1' &&& openByF s = openByF s1 &&& openByF s' = openByF s1'
[PROOF STEP]
by (auto simp: eqButUID_open_eq eqButUID_openByA_eq eqButUID_openByF_eq)
[PROOF STATE]
proof (state)
this:
open s = open s1
open s' = open s1'
openByA s = openByA s1
openByA s' = openByA s1'
openByF s = openByF s1
openByF s' = openByF s1'

goal (1 subgoal):
 1. \<phi> (Trans s1 a ou1 s1')
[PROOF STEP]
with \<phi> a step step1
[PROOF STATE]
proof (chain)
picking this:
\<phi> (Trans s a ou s')
a \<noteq> Cact (cFriend UID1 (pass s UID1) UID2) \<and> a \<noteq> Cact (cFriend UID2 (pass s UID2) UID1) \<and> a \<noteq> Dact (dFriend UID1 (pass s UID1) UID2) \<and> a \<noteq> Dact (dFriend UID2 (pass s UID2) UID1)
step s a = (ou, s')
step s1 a = (ou1, s1')
open s = open s1
open s' = open s1'
openByA s = openByA s1
openByA s' = openByA s1'
openByF s = openByF s1
openByF s' = openByF s1'
[PROOF STEP]
show "\<phi> (Trans s1 a ou1 s1')"
[PROOF STATE]
proof (prove)
using this:
\<phi> (Trans s a ou s')
a \<noteq> Cact (cFriend UID1 (pass s UID1) UID2) \<and> a \<noteq> Cact (cFriend UID2 (pass s UID2) UID1) \<and> a \<noteq> Dact (dFriend UID1 (pass s UID1) UID2) \<and> a \<noteq> Dact (dFriend UID2 (pass s UID2) UID1)
step s a = (ou, s')
step s1 a = (ou1, s1')
open s = open s1
open s' = open s1'
openByA s = openByA s1
openByA s' = openByA s1'
openByF s = openByF s1
openByF s' = openByF s1'

goal (1 subgoal):
 1. \<phi> (Trans s1 a ou1 s1')
[PROOF STEP]
using UID1_UID2_UIDs
[PROOF STATE]
proof (prove)
using this:
\<phi> (Trans s a ou s')
a \<noteq> Cact (cFriend UID1 (pass s UID1) UID2) \<and> a \<noteq> Cact (cFriend UID2 (pass s UID2) UID1) \<and> a \<noteq> Dact (dFriend UID1 (pass s UID1) UID2) \<and> a \<noteq> Dact (dFriend UID2 (pass s UID2) UID1)
step s a = (ou, s')
step s1 a = (ou1, s1')
open s = open s1
open s' = open s1'
openByA s = openByA s1
openByA s' = openByA s1'
openByF s = openByF s1
openByF s' = openByF s1'
{UID1, UID2} \<inter> UIDs = {}

goal (1 subgoal):
 1. \<phi> (Trans s1 a ou1 s1')
[PROOF STEP]
by (elim \<phi>.elims) (auto simp: c_defs d_defs)
[PROOF STATE]
proof (state)
this:
\<phi> (Trans s1 a ou1 s1')

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma inst_cswitch_consistency:
  assumes "rvpeq u s t"
  shows "rvpeq u (rcswitch n s) (rcswitch n t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rvpeq u (rcswitch n s) (rcswitch n t)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. rvpeq u (rcswitch n s) (rcswitch n t)
[PROOF STEP]
have 1: "vpeq (partition u) (\<down>s) \<down>(rcswitch n s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vpeq (Step.partition u) \<down> s \<down> rcswitch n s
[PROOF STEP]
using rstate_invariant cswitch_consistency_and_respect cswitch_preserves_invariants
[PROOF STATE]
proof (prove)
using this:
atomic_step_invariant \<down> ?s
atomic_step_invariant ?s \<Longrightarrow> vpeq ?u ?s (?s\<lparr>current := ?new_current\<rparr>)
atomic_step_invariant ?s \<Longrightarrow> atomic_step_invariant (?s\<lparr>current := ?new_current\<rparr>)

goal (1 subgoal):
 1. vpeq (Step.partition u) \<down> s \<down> rcswitch n s
[PROOF STEP]
unfolding rcswitch_def
[PROOF STATE]
proof (prove)
using this:
atomic_step_invariant \<down> ?s
atomic_step_invariant ?s \<Longrightarrow> vpeq ?u ?s (?s\<lparr>current := ?new_current\<rparr>)
atomic_step_invariant ?s \<Longrightarrow> atomic_step_invariant (?s\<lparr>current := ?new_current\<rparr>)

goal (1 subgoal):
 1. vpeq (Step.partition u) \<down> s \<down> \<up> \<down> s\<lparr>current := Eps rinvariant\<rparr>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vpeq (Step.partition u) \<down> s \<down> rcswitch n s

goal (1 subgoal):
 1. rvpeq u (rcswitch n s) (rcswitch n t)
[PROOF STEP]
have 2: "vpeq (partition u) (\<down>t) \<down>(rcswitch n t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vpeq (Step.partition u) \<down> t \<down> rcswitch n t
[PROOF STEP]
using rstate_invariant cswitch_consistency_and_respect cswitch_preserves_invariants
[PROOF STATE]
proof (prove)
using this:
atomic_step_invariant \<down> ?s
atomic_step_invariant ?s \<Longrightarrow> vpeq ?u ?s (?s\<lparr>current := ?new_current\<rparr>)
atomic_step_invariant ?s \<Longrightarrow> atomic_step_invariant (?s\<lparr>current := ?new_current\<rparr>)

goal (1 subgoal):
 1. vpeq (Step.partition u) \<down> t \<down> rcswitch n t
[PROOF STEP]
unfolding rcswitch_def
[PROOF STATE]
proof (prove)
using this:
atomic_step_invariant \<down> ?s
atomic_step_invariant ?s \<Longrightarrow> vpeq ?u ?s (?s\<lparr>current := ?new_current\<rparr>)
atomic_step_invariant ?s \<Longrightarrow> atomic_step_invariant (?s\<lparr>current := ?new_current\<rparr>)

goal (1 subgoal):
 1. vpeq (Step.partition u) \<down> t \<down> \<up> \<down> t\<lparr>current := Eps rinvariant\<rparr>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vpeq (Step.partition u) \<down> t \<down> rcswitch n t

goal (1 subgoal):
 1. rvpeq u (rcswitch n s) (rcswitch n t)
[PROOF STEP]
from 1 2 assms
[PROOF STATE]
proof (chain)
picking this:
vpeq (Step.partition u) \<down> s \<down> rcswitch n s
vpeq (Step.partition u) \<down> t \<down> rcswitch n t
rvpeq u s t
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
vpeq (Step.partition u) \<down> s \<down> rcswitch n s
vpeq (Step.partition u) \<down> t \<down> rcswitch n t
rvpeq u s t

goal (1 subgoal):
 1. rvpeq u (rcswitch n s) (rcswitch n t)
[PROOF STEP]
unfolding rvpeq_def
[PROOF STATE]
proof (prove)
using this:
vpeq (Step.partition u) \<down> s \<down> rcswitch n s
vpeq (Step.partition u) \<down> t \<down> rcswitch n t
vpeq (Step.partition u) \<down> s \<down> t

goal (1 subgoal):
 1. vpeq (Step.partition u) \<down> rcswitch n s \<down> rcswitch n t
[PROOF STEP]
using vpeq_rel
[PROOF STATE]
proof (prove)
using this:
vpeq (Step.partition u) \<down> s \<down> rcswitch n s
vpeq (Step.partition u) \<down> t \<down> rcswitch n t
vpeq (Step.partition u) \<down> s \<down> t
vpeq ?u ?s ?s
vpeq ?u ?s ?t \<Longrightarrow> vpeq ?u ?t ?s
\<lbrakk>vpeq ?u ?s1.0 ?s2.0; vpeq ?u ?s2.0 ?s3.0\<rbrakk> \<Longrightarrow> vpeq ?u ?s1.0 ?s3.0

goal (1 subgoal):
 1. vpeq (Step.partition u) \<down> rcswitch n s \<down> rcswitch n t
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
rvpeq u (rcswitch n s) (rcswitch n t)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma pos_literal_in_imp_true_cls[intro]: "Pos A \<in># C \<Longrightarrow> A \<in> I \<Longrightarrow> I \<Turnstile> C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Pos A \<in># C; A \<in> I\<rbrakk> \<Longrightarrow> I \<Turnstile> C
[PROOF STEP]
using true_cls_def
[PROOF STATE]
proof (prove)
using this:
(?I \<Turnstile> ?C) = (\<exists>L\<in>#?C. ?I \<Turnstile>l L)

goal (1 subgoal):
 1. \<lbrakk>Pos A \<in># C; A \<in> I\<rbrakk> \<Longrightarrow> I \<Turnstile> C
[PROOF STEP]
by blast


[STATEMENT]
lemma wf_indexlt_rel: "wf indexlt_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf indexlt_rel
[PROOF STEP]
using indexlt_rel_def pair_less_def
[PROOF STATE]
proof (prove)
using this:
indexlt_rel = less_than <*lex*> less_than
pair_less = less_than <*lex*> less_than

goal (1 subgoal):
 1. wf indexlt_rel
[PROOF STEP]
by auto


[STATEMENT]
lemma OclAnd15[simp]: "(true and null) = null"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (true and null) = null
[PROOF STEP]
by(rule ext,simp add: OclAnd_def null_def invalid_def true_def false_def bot_option_def
                        null_fun_def null_option_def)


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

goal (1 subgoal):
 1. s = s'
[PROOF STEP]
proof(nominal_induct v arbitrary: s s' rule:v.strong_induct)
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>x s s'. \<lbrakk>i \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ s ; i \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 2. \<And>x s s'. \<lbrakk>i \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ s ; i \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 3. \<And>x1a x2a s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x1a \<rbrakk> ~ s ; i \<lbrakk> x1a \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; \<And>s s'. \<lbrakk>i \<lbrakk> x2a \<rbrakk> ~ s ; i \<lbrakk> x2a \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> [ x1a , x2a ]\<^sup>v \<rbrakk> ~ s ; i \<lbrakk> [ x1a , x2a ]\<^sup>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 4. \<And>x1a x2a x3 s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x3 \<rbrakk> ~ s ; i \<lbrakk> x3 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s ; i \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 5. \<And>x1a x2a x3 x4 s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x4 \<rbrakk> ~ s ; i \<lbrakk> x4 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s ; i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
[PROOF STEP]
case (V_lit x)
[PROOF STATE]
proof (state)
this:
i \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ s
i \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ s'

goal (5 subgoals):
 1. \<And>x s s'. \<lbrakk>i \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ s ; i \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 2. \<And>x s s'. \<lbrakk>i \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ s ; i \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 3. \<And>x1a x2a s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x1a \<rbrakk> ~ s ; i \<lbrakk> x1a \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; \<And>s s'. \<lbrakk>i \<lbrakk> x2a \<rbrakk> ~ s ; i \<lbrakk> x2a \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> [ x1a , x2a ]\<^sup>v \<rbrakk> ~ s ; i \<lbrakk> [ x1a , x2a ]\<^sup>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 4. \<And>x1a x2a x3 s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x3 \<rbrakk> ~ s ; i \<lbrakk> x3 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s ; i \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 5. \<And>x1a x2a x3 x4 s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x4 \<rbrakk> ~ s ; i \<lbrakk> x4 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s ; i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ s
i \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ s'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ s
i \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ s'

goal (1 subgoal):
 1. s = s'
[PROOF STEP]
using eval_v_elims eval_l.simps
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ s
i \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ s'
\<lbrakk>?i \<lbrakk> [ ?l ]\<^sup>v \<rbrakk> ~ ?s ; ?s = \<lbrakk> ?l \<rbrakk>  \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> [ ?x ]\<^sup>v \<rbrakk> ~ ?s ; Some ?s = ?i ?x \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> [ ?v1.0 , ?v2.0 ]\<^sup>v \<rbrakk> ~ ?s ; \<And>s1 s2. \<lbrakk>?s = SPair s1 s2; ?i \<lbrakk> ?v1.0 \<rbrakk> ~ s1 ; ?i \<lbrakk> ?v2.0 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> V_cons ?tyid ?dc ?v \<rbrakk> ~ ?s ; \<And>s. \<lbrakk>?s = SCons ?tyid ?dc s; ?i \<lbrakk> ?v \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> V_consp ?tyid ?dc ?b ?v \<rbrakk> ~ ?s ; \<And>s. \<lbrakk>?s = SConsp ?tyid ?dc ?b s; ?i \<lbrakk> ?v \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk> L_true \<rbrakk>  = SBool True
\<lbrakk> L_false \<rbrakk>  = SBool False
\<lbrakk> L_num ?n \<rbrakk>  = SNum ?n
\<lbrakk> L_unit \<rbrakk>  = SUnit
\<lbrakk> L_bitvec ?n \<rbrakk>  = SBitvec ?n

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

goal (4 subgoals):
 1. \<And>x s s'. \<lbrakk>i \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ s ; i \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 2. \<And>x1a x2a s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x1a \<rbrakk> ~ s ; i \<lbrakk> x1a \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; \<And>s s'. \<lbrakk>i \<lbrakk> x2a \<rbrakk> ~ s ; i \<lbrakk> x2a \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> [ x1a , x2a ]\<^sup>v \<rbrakk> ~ s ; i \<lbrakk> [ x1a , x2a ]\<^sup>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 3. \<And>x1a x2a x3 s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x3 \<rbrakk> ~ s ; i \<lbrakk> x3 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s ; i \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 4. \<And>x1a x2a x3 x4 s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x4 \<rbrakk> ~ s ; i \<lbrakk> x4 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s ; i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>x s s'. \<lbrakk>i \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ s ; i \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 2. \<And>x1a x2a s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x1a \<rbrakk> ~ s ; i \<lbrakk> x1a \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; \<And>s s'. \<lbrakk>i \<lbrakk> x2a \<rbrakk> ~ s ; i \<lbrakk> x2a \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> [ x1a , x2a ]\<^sup>v \<rbrakk> ~ s ; i \<lbrakk> [ x1a , x2a ]\<^sup>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 3. \<And>x1a x2a x3 s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x3 \<rbrakk> ~ s ; i \<lbrakk> x3 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s ; i \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 4. \<And>x1a x2a x3 x4 s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x4 \<rbrakk> ~ s ; i \<lbrakk> x4 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s ; i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
[PROOF STEP]
case (V_var x)
[PROOF STATE]
proof (state)
this:
i \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ s
i \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ s'

goal (4 subgoals):
 1. \<And>x s s'. \<lbrakk>i \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ s ; i \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 2. \<And>x1a x2a s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x1a \<rbrakk> ~ s ; i \<lbrakk> x1a \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; \<And>s s'. \<lbrakk>i \<lbrakk> x2a \<rbrakk> ~ s ; i \<lbrakk> x2a \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> [ x1a , x2a ]\<^sup>v \<rbrakk> ~ s ; i \<lbrakk> [ x1a , x2a ]\<^sup>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 3. \<And>x1a x2a x3 s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x3 \<rbrakk> ~ s ; i \<lbrakk> x3 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s ; i \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 4. \<And>x1a x2a x3 x4 s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x4 \<rbrakk> ~ s ; i \<lbrakk> x4 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s ; i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ s
i \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ s'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ s
i \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ s'

goal (1 subgoal):
 1. s = s'
[PROOF STEP]
using eval_v_elims
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ s
i \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ s'
\<lbrakk>?i \<lbrakk> [ ?l ]\<^sup>v \<rbrakk> ~ ?s ; ?s = \<lbrakk> ?l \<rbrakk>  \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> [ ?x ]\<^sup>v \<rbrakk> ~ ?s ; Some ?s = ?i ?x \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> [ ?v1.0 , ?v2.0 ]\<^sup>v \<rbrakk> ~ ?s ; \<And>s1 s2. \<lbrakk>?s = SPair s1 s2; ?i \<lbrakk> ?v1.0 \<rbrakk> ~ s1 ; ?i \<lbrakk> ?v2.0 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> V_cons ?tyid ?dc ?v \<rbrakk> ~ ?s ; \<And>s. \<lbrakk>?s = SCons ?tyid ?dc s; ?i \<lbrakk> ?v \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> V_consp ?tyid ?dc ?b ?v \<rbrakk> ~ ?s ; \<And>s. \<lbrakk>?s = SConsp ?tyid ?dc ?b s; ?i \<lbrakk> ?v \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

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

goal (3 subgoals):
 1. \<And>x1a x2a s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x1a \<rbrakk> ~ s ; i \<lbrakk> x1a \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; \<And>s s'. \<lbrakk>i \<lbrakk> x2a \<rbrakk> ~ s ; i \<lbrakk> x2a \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> [ x1a , x2a ]\<^sup>v \<rbrakk> ~ s ; i \<lbrakk> [ x1a , x2a ]\<^sup>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 2. \<And>x1a x2a x3 s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x3 \<rbrakk> ~ s ; i \<lbrakk> x3 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s ; i \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 3. \<And>x1a x2a x3 x4 s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x4 \<rbrakk> ~ s ; i \<lbrakk> x4 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s ; i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x1a x2a s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x1a \<rbrakk> ~ s ; i \<lbrakk> x1a \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; \<And>s s'. \<lbrakk>i \<lbrakk> x2a \<rbrakk> ~ s ; i \<lbrakk> x2a \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> [ x1a , x2a ]\<^sup>v \<rbrakk> ~ s ; i \<lbrakk> [ x1a , x2a ]\<^sup>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 2. \<And>x1a x2a x3 s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x3 \<rbrakk> ~ s ; i \<lbrakk> x3 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s ; i \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 3. \<And>x1a x2a x3 x4 s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x4 \<rbrakk> ~ s ; i \<lbrakk> x4 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s ; i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
[PROOF STEP]
case (V_pair v1 v2)
[PROOF STATE]
proof (state)
this:
\<lbrakk>i \<lbrakk> v1 \<rbrakk> ~ ?s ; i \<lbrakk> v1 \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> ?s = ?s'
\<lbrakk>i \<lbrakk> v2 \<rbrakk> ~ ?s ; i \<lbrakk> v2 \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> ?s = ?s'
i \<lbrakk> [ v1 , v2 ]\<^sup>v \<rbrakk> ~ s
i \<lbrakk> [ v1 , v2 ]\<^sup>v \<rbrakk> ~ s'

goal (3 subgoals):
 1. \<And>x1a x2a s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x1a \<rbrakk> ~ s ; i \<lbrakk> x1a \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; \<And>s s'. \<lbrakk>i \<lbrakk> x2a \<rbrakk> ~ s ; i \<lbrakk> x2a \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> [ x1a , x2a ]\<^sup>v \<rbrakk> ~ s ; i \<lbrakk> [ x1a , x2a ]\<^sup>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 2. \<And>x1a x2a x3 s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x3 \<rbrakk> ~ s ; i \<lbrakk> x3 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s ; i \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 3. \<And>x1a x2a x3 x4 s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x4 \<rbrakk> ~ s ; i \<lbrakk> x4 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s ; i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
[PROOF STEP]
obtain s1 and s2 where s:"i \<lbrakk> v1 \<rbrakk> ~ s1  \<and> i \<lbrakk> v2 \<rbrakk> ~ s2 \<and> s = SPair s1 s2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>s1 s2. i \<lbrakk> v1 \<rbrakk> ~ s1  \<and> i \<lbrakk> v2 \<rbrakk> ~ s2  \<and> s = SPair s1 s2 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using eval_v_elims V_pair
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?i \<lbrakk> [ ?l ]\<^sup>v \<rbrakk> ~ ?s ; ?s = \<lbrakk> ?l \<rbrakk>  \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> [ ?x ]\<^sup>v \<rbrakk> ~ ?s ; Some ?s = ?i ?x \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> [ ?v1.0 , ?v2.0 ]\<^sup>v \<rbrakk> ~ ?s ; \<And>s1 s2. \<lbrakk>?s = SPair s1 s2; ?i \<lbrakk> ?v1.0 \<rbrakk> ~ s1 ; ?i \<lbrakk> ?v2.0 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> V_cons ?tyid ?dc ?v \<rbrakk> ~ ?s ; \<And>s. \<lbrakk>?s = SCons ?tyid ?dc s; ?i \<lbrakk> ?v \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> V_consp ?tyid ?dc ?b ?v \<rbrakk> ~ ?s ; \<And>s. \<lbrakk>?s = SConsp ?tyid ?dc ?b s; ?i \<lbrakk> ?v \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>i \<lbrakk> v1 \<rbrakk> ~ ?s ; i \<lbrakk> v1 \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> ?s = ?s'
\<lbrakk>i \<lbrakk> v2 \<rbrakk> ~ ?s ; i \<lbrakk> v2 \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> ?s = ?s'
i \<lbrakk> [ v1 , v2 ]\<^sup>v \<rbrakk> ~ s
i \<lbrakk> [ v1 , v2 ]\<^sup>v \<rbrakk> ~ s'

goal (1 subgoal):
 1. (\<And>s1 s2. i \<lbrakk> v1 \<rbrakk> ~ s1  \<and> i \<lbrakk> v2 \<rbrakk> ~ s2  \<and> s = SPair s1 s2 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
i \<lbrakk> v1 \<rbrakk> ~ s1  \<and> i \<lbrakk> v2 \<rbrakk> ~ s2  \<and> s = SPair s1 s2

goal (3 subgoals):
 1. \<And>x1a x2a s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x1a \<rbrakk> ~ s ; i \<lbrakk> x1a \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; \<And>s s'. \<lbrakk>i \<lbrakk> x2a \<rbrakk> ~ s ; i \<lbrakk> x2a \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> [ x1a , x2a ]\<^sup>v \<rbrakk> ~ s ; i \<lbrakk> [ x1a , x2a ]\<^sup>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 2. \<And>x1a x2a x3 s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x3 \<rbrakk> ~ s ; i \<lbrakk> x3 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s ; i \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 3. \<And>x1a x2a x3 x4 s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x4 \<rbrakk> ~ s ; i \<lbrakk> x4 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s ; i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
[PROOF STEP]
obtain s1' and s2' where s':"i \<lbrakk> v1 \<rbrakk> ~ s1'  \<and> i \<lbrakk> v2 \<rbrakk> ~ s2' \<and> s' = SPair s1' s2'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>s1' s2'. i \<lbrakk> v1 \<rbrakk> ~ s1'  \<and> i \<lbrakk> v2 \<rbrakk> ~ s2'  \<and> s' = SPair s1' s2' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using eval_v_elims V_pair
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?i \<lbrakk> [ ?l ]\<^sup>v \<rbrakk> ~ ?s ; ?s = \<lbrakk> ?l \<rbrakk>  \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> [ ?x ]\<^sup>v \<rbrakk> ~ ?s ; Some ?s = ?i ?x \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> [ ?v1.0 , ?v2.0 ]\<^sup>v \<rbrakk> ~ ?s ; \<And>s1 s2. \<lbrakk>?s = SPair s1 s2; ?i \<lbrakk> ?v1.0 \<rbrakk> ~ s1 ; ?i \<lbrakk> ?v2.0 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> V_cons ?tyid ?dc ?v \<rbrakk> ~ ?s ; \<And>s. \<lbrakk>?s = SCons ?tyid ?dc s; ?i \<lbrakk> ?v \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> V_consp ?tyid ?dc ?b ?v \<rbrakk> ~ ?s ; \<And>s. \<lbrakk>?s = SConsp ?tyid ?dc ?b s; ?i \<lbrakk> ?v \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>i \<lbrakk> v1 \<rbrakk> ~ ?s ; i \<lbrakk> v1 \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> ?s = ?s'
\<lbrakk>i \<lbrakk> v2 \<rbrakk> ~ ?s ; i \<lbrakk> v2 \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> ?s = ?s'
i \<lbrakk> [ v1 , v2 ]\<^sup>v \<rbrakk> ~ s
i \<lbrakk> [ v1 , v2 ]\<^sup>v \<rbrakk> ~ s'

goal (1 subgoal):
 1. (\<And>s1' s2'. i \<lbrakk> v1 \<rbrakk> ~ s1'  \<and> i \<lbrakk> v2 \<rbrakk> ~ s2'  \<and> s' = SPair s1' s2' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
i \<lbrakk> v1 \<rbrakk> ~ s1'  \<and> i \<lbrakk> v2 \<rbrakk> ~ s2'  \<and> s' = SPair s1' s2'

goal (3 subgoals):
 1. \<And>x1a x2a s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x1a \<rbrakk> ~ s ; i \<lbrakk> x1a \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; \<And>s s'. \<lbrakk>i \<lbrakk> x2a \<rbrakk> ~ s ; i \<lbrakk> x2a \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> [ x1a , x2a ]\<^sup>v \<rbrakk> ~ s ; i \<lbrakk> [ x1a , x2a ]\<^sup>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 2. \<And>x1a x2a x3 s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x3 \<rbrakk> ~ s ; i \<lbrakk> x3 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s ; i \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 3. \<And>x1a x2a x3 x4 s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x4 \<rbrakk> ~ s ; i \<lbrakk> x4 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s ; i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i \<lbrakk> v1 \<rbrakk> ~ s1'  \<and> i \<lbrakk> v2 \<rbrakk> ~ s2'  \<and> s' = SPair s1' s2'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> v1 \<rbrakk> ~ s1'  \<and> i \<lbrakk> v2 \<rbrakk> ~ s2'  \<and> s' = SPair s1' s2'

goal (1 subgoal):
 1. s = s'
[PROOF STEP]
using eval_v_elims
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> v1 \<rbrakk> ~ s1'  \<and> i \<lbrakk> v2 \<rbrakk> ~ s2'  \<and> s' = SPair s1' s2'
\<lbrakk>?i \<lbrakk> [ ?l ]\<^sup>v \<rbrakk> ~ ?s ; ?s = \<lbrakk> ?l \<rbrakk>  \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> [ ?x ]\<^sup>v \<rbrakk> ~ ?s ; Some ?s = ?i ?x \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> [ ?v1.0 , ?v2.0 ]\<^sup>v \<rbrakk> ~ ?s ; \<And>s1 s2. \<lbrakk>?s = SPair s1 s2; ?i \<lbrakk> ?v1.0 \<rbrakk> ~ s1 ; ?i \<lbrakk> ?v2.0 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> V_cons ?tyid ?dc ?v \<rbrakk> ~ ?s ; \<And>s. \<lbrakk>?s = SCons ?tyid ?dc s; ?i \<lbrakk> ?v \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> V_consp ?tyid ?dc ?b ?v \<rbrakk> ~ ?s ; \<And>s. \<lbrakk>?s = SConsp ?tyid ?dc ?b s; ?i \<lbrakk> ?v \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

goal (1 subgoal):
 1. s = s'
[PROOF STEP]
using V_pair s s'
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> v1 \<rbrakk> ~ s1'  \<and> i \<lbrakk> v2 \<rbrakk> ~ s2'  \<and> s' = SPair s1' s2'
\<lbrakk>?i \<lbrakk> [ ?l ]\<^sup>v \<rbrakk> ~ ?s ; ?s = \<lbrakk> ?l \<rbrakk>  \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> [ ?x ]\<^sup>v \<rbrakk> ~ ?s ; Some ?s = ?i ?x \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> [ ?v1.0 , ?v2.0 ]\<^sup>v \<rbrakk> ~ ?s ; \<And>s1 s2. \<lbrakk>?s = SPair s1 s2; ?i \<lbrakk> ?v1.0 \<rbrakk> ~ s1 ; ?i \<lbrakk> ?v2.0 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> V_cons ?tyid ?dc ?v \<rbrakk> ~ ?s ; \<And>s. \<lbrakk>?s = SCons ?tyid ?dc s; ?i \<lbrakk> ?v \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> V_consp ?tyid ?dc ?b ?v \<rbrakk> ~ ?s ; \<And>s. \<lbrakk>?s = SConsp ?tyid ?dc ?b s; ?i \<lbrakk> ?v \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>i \<lbrakk> v1 \<rbrakk> ~ ?s ; i \<lbrakk> v1 \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> ?s = ?s'
\<lbrakk>i \<lbrakk> v2 \<rbrakk> ~ ?s ; i \<lbrakk> v2 \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> ?s = ?s'
i \<lbrakk> [ v1 , v2 ]\<^sup>v \<rbrakk> ~ s
i \<lbrakk> [ v1 , v2 ]\<^sup>v \<rbrakk> ~ s'
i \<lbrakk> v1 \<rbrakk> ~ s1  \<and> i \<lbrakk> v2 \<rbrakk> ~ s2  \<and> s = SPair s1 s2
i \<lbrakk> v1 \<rbrakk> ~ s1'  \<and> i \<lbrakk> v2 \<rbrakk> ~ s2'  \<and> s' = SPair s1' s2'

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

goal (2 subgoals):
 1. \<And>x1a x2a x3 s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x3 \<rbrakk> ~ s ; i \<lbrakk> x3 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s ; i \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 2. \<And>x1a x2a x3 x4 s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x4 \<rbrakk> ~ s ; i \<lbrakk> x4 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s ; i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x1a x2a x3 s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x3 \<rbrakk> ~ s ; i \<lbrakk> x3 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s ; i \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 2. \<And>x1a x2a x3 x4 s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x4 \<rbrakk> ~ s ; i \<lbrakk> x4 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s ; i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
[PROOF STEP]
case (V_cons tyid dc v1)
[PROOF STATE]
proof (state)
this:
\<lbrakk>i \<lbrakk> v1 \<rbrakk> ~ ?s ; i \<lbrakk> v1 \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> ?s = ?s'
i \<lbrakk> V_cons tyid dc v1 \<rbrakk> ~ s
i \<lbrakk> V_cons tyid dc v1 \<rbrakk> ~ s'

goal (2 subgoals):
 1. \<And>x1a x2a x3 s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x3 \<rbrakk> ~ s ; i \<lbrakk> x3 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s ; i \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 2. \<And>x1a x2a x3 x4 s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x4 \<rbrakk> ~ s ; i \<lbrakk> x4 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s ; i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
[PROOF STEP]
obtain sv1 where 1:"i \<lbrakk> v1 \<rbrakk> ~ sv1 \<and> s = SCons tyid dc sv1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>sv1. i \<lbrakk> v1 \<rbrakk> ~ sv1  \<and> s = SCons tyid dc sv1 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using eval_v_elims V_cons
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?i \<lbrakk> [ ?l ]\<^sup>v \<rbrakk> ~ ?s ; ?s = \<lbrakk> ?l \<rbrakk>  \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> [ ?x ]\<^sup>v \<rbrakk> ~ ?s ; Some ?s = ?i ?x \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> [ ?v1.0 , ?v2.0 ]\<^sup>v \<rbrakk> ~ ?s ; \<And>s1 s2. \<lbrakk>?s = SPair s1 s2; ?i \<lbrakk> ?v1.0 \<rbrakk> ~ s1 ; ?i \<lbrakk> ?v2.0 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> V_cons ?tyid ?dc ?v \<rbrakk> ~ ?s ; \<And>s. \<lbrakk>?s = SCons ?tyid ?dc s; ?i \<lbrakk> ?v \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> V_consp ?tyid ?dc ?b ?v \<rbrakk> ~ ?s ; \<And>s. \<lbrakk>?s = SConsp ?tyid ?dc ?b s; ?i \<lbrakk> ?v \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>i \<lbrakk> v1 \<rbrakk> ~ ?s ; i \<lbrakk> v1 \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> ?s = ?s'
i \<lbrakk> V_cons tyid dc v1 \<rbrakk> ~ s
i \<lbrakk> V_cons tyid dc v1 \<rbrakk> ~ s'

goal (1 subgoal):
 1. (\<And>sv1. i \<lbrakk> v1 \<rbrakk> ~ sv1  \<and> s = SCons tyid dc sv1 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
i \<lbrakk> v1 \<rbrakk> ~ sv1  \<and> s = SCons tyid dc sv1

goal (2 subgoals):
 1. \<And>x1a x2a x3 s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x3 \<rbrakk> ~ s ; i \<lbrakk> x3 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s ; i \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 2. \<And>x1a x2a x3 x4 s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x4 \<rbrakk> ~ s ; i \<lbrakk> x4 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s ; i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
i \<lbrakk> v1 \<rbrakk> ~ sv1  \<and> s = SCons tyid dc sv1

goal (2 subgoals):
 1. \<And>x1a x2a x3 s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x3 \<rbrakk> ~ s ; i \<lbrakk> x3 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s ; i \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 2. \<And>x1a x2a x3 x4 s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x4 \<rbrakk> ~ s ; i \<lbrakk> x4 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s ; i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
[PROOF STEP]
obtain sv2 where 2:"i \<lbrakk> v1 \<rbrakk> ~ sv2 \<and> s' = SCons tyid dc sv2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>sv2. i \<lbrakk> v1 \<rbrakk> ~ sv2  \<and> s' = SCons tyid dc sv2 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using eval_v_elims V_cons
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?i \<lbrakk> [ ?l ]\<^sup>v \<rbrakk> ~ ?s ; ?s = \<lbrakk> ?l \<rbrakk>  \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> [ ?x ]\<^sup>v \<rbrakk> ~ ?s ; Some ?s = ?i ?x \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> [ ?v1.0 , ?v2.0 ]\<^sup>v \<rbrakk> ~ ?s ; \<And>s1 s2. \<lbrakk>?s = SPair s1 s2; ?i \<lbrakk> ?v1.0 \<rbrakk> ~ s1 ; ?i \<lbrakk> ?v2.0 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> V_cons ?tyid ?dc ?v \<rbrakk> ~ ?s ; \<And>s. \<lbrakk>?s = SCons ?tyid ?dc s; ?i \<lbrakk> ?v \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> V_consp ?tyid ?dc ?b ?v \<rbrakk> ~ ?s ; \<And>s. \<lbrakk>?s = SConsp ?tyid ?dc ?b s; ?i \<lbrakk> ?v \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>i \<lbrakk> v1 \<rbrakk> ~ ?s ; i \<lbrakk> v1 \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> ?s = ?s'
i \<lbrakk> V_cons tyid dc v1 \<rbrakk> ~ s
i \<lbrakk> V_cons tyid dc v1 \<rbrakk> ~ s'

goal (1 subgoal):
 1. (\<And>sv2. i \<lbrakk> v1 \<rbrakk> ~ sv2  \<and> s' = SCons tyid dc sv2 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
i \<lbrakk> v1 \<rbrakk> ~ sv2  \<and> s' = SCons tyid dc sv2

goal (2 subgoals):
 1. \<And>x1a x2a x3 s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x3 \<rbrakk> ~ s ; i \<lbrakk> x3 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s ; i \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 2. \<And>x1a x2a x3 x4 s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x4 \<rbrakk> ~ s ; i \<lbrakk> x4 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s ; i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
i \<lbrakk> v1 \<rbrakk> ~ sv1  \<and> s = SCons tyid dc sv1
i \<lbrakk> v1 \<rbrakk> ~ sv2  \<and> s' = SCons tyid dc sv2
[PROOF STEP]
have "sv1 = sv2"
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> v1 \<rbrakk> ~ sv1  \<and> s = SCons tyid dc sv1
i \<lbrakk> v1 \<rbrakk> ~ sv2  \<and> s' = SCons tyid dc sv2

goal (1 subgoal):
 1. sv1 = sv2
[PROOF STEP]
using V_cons
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> v1 \<rbrakk> ~ sv1  \<and> s = SCons tyid dc sv1
i \<lbrakk> v1 \<rbrakk> ~ sv2  \<and> s' = SCons tyid dc sv2
\<lbrakk>i \<lbrakk> v1 \<rbrakk> ~ ?s ; i \<lbrakk> v1 \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> ?s = ?s'
i \<lbrakk> V_cons tyid dc v1 \<rbrakk> ~ s
i \<lbrakk> V_cons tyid dc v1 \<rbrakk> ~ s'

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

goal (2 subgoals):
 1. \<And>x1a x2a x3 s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x3 \<rbrakk> ~ s ; i \<lbrakk> x3 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s ; i \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
 2. \<And>x1a x2a x3 x4 s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x4 \<rbrakk> ~ s ; i \<lbrakk> x4 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s ; i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
sv1 = sv2
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
sv1 = sv2

goal (1 subgoal):
 1. s = s'
[PROOF STEP]
using 1 2
[PROOF STATE]
proof (prove)
using this:
sv1 = sv2
i \<lbrakk> v1 \<rbrakk> ~ sv1  \<and> s = SCons tyid dc sv1
i \<lbrakk> v1 \<rbrakk> ~ sv2  \<and> s' = SCons tyid dc sv2

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

goal (1 subgoal):
 1. \<And>x1a x2a x3 x4 s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x4 \<rbrakk> ~ s ; i \<lbrakk> x4 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s ; i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x1a x2a x3 x4 s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x4 \<rbrakk> ~ s ; i \<lbrakk> x4 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s ; i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
[PROOF STEP]
case (V_consp tyid dc b v1)
[PROOF STATE]
proof (state)
this:
\<lbrakk>i \<lbrakk> v1 \<rbrakk> ~ ?s ; i \<lbrakk> v1 \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> ?s = ?s'
i \<lbrakk> V_consp tyid dc b v1 \<rbrakk> ~ s
i \<lbrakk> V_consp tyid dc b v1 \<rbrakk> ~ s'

goal (1 subgoal):
 1. \<And>x1a x2a x3 x4 s s'. \<lbrakk>\<And>s s'. \<lbrakk>i \<lbrakk> x4 \<rbrakk> ~ s ; i \<lbrakk> x4 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'; i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s ; i \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> s = s'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>i \<lbrakk> v1 \<rbrakk> ~ ?s ; i \<lbrakk> v1 \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> ?s = ?s'
i \<lbrakk> V_consp tyid dc b v1 \<rbrakk> ~ s
i \<lbrakk> V_consp tyid dc b v1 \<rbrakk> ~ s'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>i \<lbrakk> v1 \<rbrakk> ~ ?s ; i \<lbrakk> v1 \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> ?s = ?s'
i \<lbrakk> V_consp tyid dc b v1 \<rbrakk> ~ s
i \<lbrakk> V_consp tyid dc b v1 \<rbrakk> ~ s'

goal (1 subgoal):
 1. s = s'
[PROOF STEP]
using eval_v_elims
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>i \<lbrakk> v1 \<rbrakk> ~ ?s ; i \<lbrakk> v1 \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> ?s = ?s'
i \<lbrakk> V_consp tyid dc b v1 \<rbrakk> ~ s
i \<lbrakk> V_consp tyid dc b v1 \<rbrakk> ~ s'
\<lbrakk>?i \<lbrakk> [ ?l ]\<^sup>v \<rbrakk> ~ ?s ; ?s = \<lbrakk> ?l \<rbrakk>  \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> [ ?x ]\<^sup>v \<rbrakk> ~ ?s ; Some ?s = ?i ?x \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> [ ?v1.0 , ?v2.0 ]\<^sup>v \<rbrakk> ~ ?s ; \<And>s1 s2. \<lbrakk>?s = SPair s1 s2; ?i \<lbrakk> ?v1.0 \<rbrakk> ~ s1 ; ?i \<lbrakk> ?v2.0 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> V_cons ?tyid ?dc ?v \<rbrakk> ~ ?s ; \<And>s. \<lbrakk>?s = SCons ?tyid ?dc s; ?i \<lbrakk> ?v \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> V_consp ?tyid ?dc ?b ?v \<rbrakk> ~ ?s ; \<And>s. \<lbrakk>?s = SConsp ?tyid ?dc ?b s; ?i \<lbrakk> ?v \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

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

goal:
No subgoals!
[PROOF STEP]
qed