[STATEMENT]
lemma ce_rel_lm_2 [simp]: "ce_rel_to_set (ce_set_to_rel A) = A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ce_rel_to_set (ce_set_to_rel A) = A
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ce_rel_to_set (ce_set_to_rel A) \<subseteq> A
 2. A \<subseteq> ce_rel_to_set (ce_set_to_rel A)
[PROOF STEP]
show "ce_rel_to_set (ce_set_to_rel A) \<subseteq> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ce_rel_to_set (ce_set_to_rel A) \<subseteq> A
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> ce_rel_to_set (ce_set_to_rel A) \<Longrightarrow> x \<in> A
[PROOF STEP]
fix z
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> ce_rel_to_set (ce_set_to_rel A) \<Longrightarrow> x \<in> A
[PROOF STEP]
show "z \<in> ce_rel_to_set (ce_set_to_rel A) \<Longrightarrow> z \<in> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. z \<in> ce_rel_to_set (ce_set_to_rel A) \<Longrightarrow> z \<in> A
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. z \<in> ce_rel_to_set (ce_set_to_rel A) \<Longrightarrow> z \<in> A
[PROOF STEP]
assume A: "z \<in> ce_rel_to_set (ce_set_to_rel A)"
[PROOF STATE]
proof (state)
this:
z \<in> ce_rel_to_set (ce_set_to_rel A)

goal (1 subgoal):
 1. z \<in> ce_rel_to_set (ce_set_to_rel A) \<Longrightarrow> z \<in> A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
z \<in> ce_rel_to_set (ce_set_to_rel A)
[PROOF STEP]
obtain x y where L1: "z = c_pair x y" and L2: "(x,y) \<in> ce_set_to_rel A"
[PROOF STATE]
proof (prove)
using this:
z \<in> ce_rel_to_set (ce_set_to_rel A)

goal (1 subgoal):
 1. (\<And>x y. \<lbrakk>z = c_pair x y; (x, y) \<in> ce_set_to_rel A\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding ce_rel_to_set_def
[PROOF STATE]
proof (prove)
using this:
z \<in> {c_pair x y |x y. (x, y) \<in> ce_set_to_rel A}

goal (1 subgoal):
 1. (\<And>x y. \<lbrakk>z = c_pair x y; (x, y) \<in> ce_set_to_rel A\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
z = c_pair x y
(x, y) \<in> ce_set_to_rel A

goal (1 subgoal):
 1. z \<in> ce_rel_to_set (ce_set_to_rel A) \<Longrightarrow> z \<in> A
[PROOF STEP]
from L2
[PROOF STATE]
proof (chain)
picking this:
(x, y) \<in> ce_set_to_rel A
[PROOF STEP]
obtain u where L3: "(x,y) = (c_fst u, c_snd u)" and L4: "u \<in> A"
[PROOF STATE]
proof (prove)
using this:
(x, y) \<in> ce_set_to_rel A

goal (1 subgoal):
 1. (\<And>u. \<lbrakk>(x, y) = (c_fst u, c_snd u); u \<in> A\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding ce_set_to_rel_def
[PROOF STATE]
proof (prove)
using this:
(x, y) \<in> {(c_fst x, c_snd x) |x. x \<in> A}

goal (1 subgoal):
 1. (\<And>u. \<lbrakk>(x, y) = (c_fst u, c_snd u); u \<in> A\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(x, y) = (c_fst u, c_snd u)
u \<in> A

goal (1 subgoal):
 1. z \<in> ce_rel_to_set (ce_set_to_rel A) \<Longrightarrow> z \<in> A
[PROOF STEP]
from L3 L1
[PROOF STATE]
proof (chain)
picking this:
(x, y) = (c_fst u, c_snd u)
z = c_pair x y
[PROOF STEP]
have L5: "z = u"
[PROOF STATE]
proof (prove)
using this:
(x, y) = (c_fst u, c_snd u)
z = c_pair x y

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

goal (1 subgoal):
 1. z \<in> ce_rel_to_set (ce_set_to_rel A) \<Longrightarrow> z \<in> A
[PROOF STEP]
with L4
[PROOF STATE]
proof (chain)
picking this:
u \<in> A
z = u
[PROOF STEP]
show "z \<in> A"
[PROOF STATE]
proof (prove)
using this:
u \<in> A
z = u

goal (1 subgoal):
 1. z \<in> A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
z \<in> A

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
z \<in> ce_rel_to_set (ce_set_to_rel A) \<Longrightarrow> z \<in> A

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
ce_rel_to_set (ce_set_to_rel A) \<subseteq> A

goal (1 subgoal):
 1. A \<subseteq> ce_rel_to_set (ce_set_to_rel A)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. A \<subseteq> ce_rel_to_set (ce_set_to_rel A)
[PROOF STEP]
show "A \<subseteq> ce_rel_to_set (ce_set_to_rel A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<subseteq> ce_rel_to_set (ce_set_to_rel A)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> A \<Longrightarrow> x \<in> ce_rel_to_set (ce_set_to_rel A)
[PROOF STEP]
fix z
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> A \<Longrightarrow> x \<in> ce_rel_to_set (ce_set_to_rel A)
[PROOF STEP]
show "z \<in> A \<Longrightarrow> z \<in> ce_rel_to_set (ce_set_to_rel A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. z \<in> A \<Longrightarrow> z \<in> ce_rel_to_set (ce_set_to_rel A)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. z \<in> A \<Longrightarrow> z \<in> ce_rel_to_set (ce_set_to_rel A)
[PROOF STEP]
assume A: "z \<in> A"
[PROOF STATE]
proof (state)
this:
z \<in> A

goal (1 subgoal):
 1. z \<in> A \<Longrightarrow> z \<in> ce_rel_to_set (ce_set_to_rel A)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
z \<in> A
[PROOF STEP]
have L1: "(c_fst z, c_snd z) \<in> ce_set_to_rel A"
[PROOF STATE]
proof (prove)
using this:
z \<in> A

goal (1 subgoal):
 1. (c_fst z, c_snd z) \<in> ce_set_to_rel A
[PROOF STEP]
by (unfold ce_set_to_rel_def, auto)
[PROOF STATE]
proof (state)
this:
(c_fst z, c_snd z) \<in> ce_set_to_rel A

goal (1 subgoal):
 1. z \<in> A \<Longrightarrow> z \<in> ce_rel_to_set (ce_set_to_rel A)
[PROOF STEP]
define x where "x = c_fst z"
[PROOF STATE]
proof (state)
this:
x = c_fst z

goal (1 subgoal):
 1. z \<in> A \<Longrightarrow> z \<in> ce_rel_to_set (ce_set_to_rel A)
[PROOF STEP]
define y where "y = c_snd z"
[PROOF STATE]
proof (state)
this:
y = c_snd z

goal (1 subgoal):
 1. z \<in> A \<Longrightarrow> z \<in> ce_rel_to_set (ce_set_to_rel A)
[PROOF STEP]
from L1 x_def y_def
[PROOF STATE]
proof (chain)
picking this:
(c_fst z, c_snd z) \<in> ce_set_to_rel A
x = c_fst z
y = c_snd z
[PROOF STEP]
have L2: "(x,y) \<in> ce_set_to_rel A"
[PROOF STATE]
proof (prove)
using this:
(c_fst z, c_snd z) \<in> ce_set_to_rel A
x = c_fst z
y = c_snd z

goal (1 subgoal):
 1. (x, y) \<in> ce_set_to_rel A
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(x, y) \<in> ce_set_to_rel A

goal (1 subgoal):
 1. z \<in> A \<Longrightarrow> z \<in> ce_rel_to_set (ce_set_to_rel A)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(x, y) \<in> ce_set_to_rel A
[PROOF STEP]
have L3: "c_pair x y \<in> ce_rel_to_set (ce_set_to_rel A)"
[PROOF STATE]
proof (prove)
using this:
(x, y) \<in> ce_set_to_rel A

goal (1 subgoal):
 1. c_pair x y \<in> ce_rel_to_set (ce_set_to_rel A)
[PROOF STEP]
by (unfold ce_rel_to_set_def, auto)
[PROOF STATE]
proof (state)
this:
c_pair x y \<in> ce_rel_to_set (ce_set_to_rel A)

goal (1 subgoal):
 1. z \<in> A \<Longrightarrow> z \<in> ce_rel_to_set (ce_set_to_rel A)
[PROOF STEP]
with x_def y_def
[PROOF STATE]
proof (chain)
picking this:
x = c_fst z
y = c_snd z
c_pair x y \<in> ce_rel_to_set (ce_set_to_rel A)
[PROOF STEP]
show "z \<in> ce_rel_to_set (ce_set_to_rel A)"
[PROOF STATE]
proof (prove)
using this:
x = c_fst z
y = c_snd z
c_pair x y \<in> ce_rel_to_set (ce_set_to_rel A)

goal (1 subgoal):
 1. z \<in> ce_rel_to_set (ce_set_to_rel A)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
z \<in> ce_rel_to_set (ce_set_to_rel A)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
z \<in> A \<Longrightarrow> z \<in> ce_rel_to_set (ce_set_to_rel A)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
A \<subseteq> ce_rel_to_set (ce_set_to_rel A)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ce_rels_def1: "ce_rels = { ce_set_to_rel A | A. A \<in> ce_sets}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ce_rels = {ce_set_to_rel A |A. A \<in> ce_sets}
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ce_rels \<subseteq> {ce_set_to_rel A |A. A \<in> ce_sets}
 2. {ce_set_to_rel A |A. A \<in> ce_sets} \<subseteq> ce_rels
[PROOF STEP]
show "ce_rels \<subseteq> {ce_set_to_rel A |A. A \<in> ce_sets}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ce_rels \<subseteq> {ce_set_to_rel A |A. A \<in> ce_sets}
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> ce_rels \<Longrightarrow> x \<in> {ce_set_to_rel A |A. A \<in> ce_sets}
[PROOF STEP]
fix r
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> ce_rels \<Longrightarrow> x \<in> {ce_set_to_rel A |A. A \<in> ce_sets}
[PROOF STEP]
show " r \<in> ce_rels \<Longrightarrow> r \<in> {ce_set_to_rel A |A. A \<in> ce_sets}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r \<in> ce_rels \<Longrightarrow> r \<in> {ce_set_to_rel A |A. A \<in> ce_sets}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. r \<in> ce_rels \<Longrightarrow> r \<in> {ce_set_to_rel A |A. A \<in> ce_sets}
[PROOF STEP]
assume A: "r \<in> ce_rels"
[PROOF STATE]
proof (state)
this:
r \<in> ce_rels

goal (1 subgoal):
 1. r \<in> ce_rels \<Longrightarrow> r \<in> {ce_set_to_rel A |A. A \<in> ce_sets}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
r \<in> ce_rels
[PROOF STEP]
have L1: "ce_rel_to_set r \<in> ce_sets"
[PROOF STATE]
proof (prove)
using this:
r \<in> ce_rels

goal (1 subgoal):
 1. ce_rel_to_set r \<in> ce_sets
[PROOF STEP]
by (unfold ce_rels_def, auto)
[PROOF STATE]
proof (state)
this:
ce_rel_to_set r \<in> ce_sets

goal (1 subgoal):
 1. r \<in> ce_rels \<Longrightarrow> r \<in> {ce_set_to_rel A |A. A \<in> ce_sets}
[PROOF STEP]
define A where "A = ce_rel_to_set r"
[PROOF STATE]
proof (state)
this:
A = ce_rel_to_set r

goal (1 subgoal):
 1. r \<in> ce_rels \<Longrightarrow> r \<in> {ce_set_to_rel A |A. A \<in> ce_sets}
[PROOF STEP]
from A_def L1
[PROOF STATE]
proof (chain)
picking this:
A = ce_rel_to_set r
ce_rel_to_set r \<in> ce_sets
[PROOF STEP]
have L2: "A \<in> ce_sets"
[PROOF STATE]
proof (prove)
using this:
A = ce_rel_to_set r
ce_rel_to_set r \<in> ce_sets

goal (1 subgoal):
 1. A \<in> ce_sets
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
A \<in> ce_sets

goal (1 subgoal):
 1. r \<in> ce_rels \<Longrightarrow> r \<in> {ce_set_to_rel A |A. A \<in> ce_sets}
[PROOF STEP]
from A_def
[PROOF STATE]
proof (chain)
picking this:
A = ce_rel_to_set r
[PROOF STEP]
have L3: "ce_set_to_rel A = r"
[PROOF STATE]
proof (prove)
using this:
A = ce_rel_to_set r

goal (1 subgoal):
 1. ce_set_to_rel A = r
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
ce_set_to_rel A = r

goal (1 subgoal):
 1. r \<in> ce_rels \<Longrightarrow> r \<in> {ce_set_to_rel A |A. A \<in> ce_sets}
[PROOF STEP]
with L2
[PROOF STATE]
proof (chain)
picking this:
A \<in> ce_sets
ce_set_to_rel A = r
[PROOF STEP]
show "r \<in> {ce_set_to_rel A |A. A \<in> ce_sets}"
[PROOF STATE]
proof (prove)
using this:
A \<in> ce_sets
ce_set_to_rel A = r

goal (1 subgoal):
 1. r \<in> {ce_set_to_rel A |A. A \<in> ce_sets}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
r \<in> {ce_set_to_rel A |A. A \<in> ce_sets}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
r \<in> ce_rels \<Longrightarrow> r \<in> {ce_set_to_rel A |A. A \<in> ce_sets}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
ce_rels \<subseteq> {ce_set_to_rel A |A. A \<in> ce_sets}

goal (1 subgoal):
 1. {ce_set_to_rel A |A. A \<in> ce_sets} \<subseteq> ce_rels
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. {ce_set_to_rel A |A. A \<in> ce_sets} \<subseteq> ce_rels
[PROOF STEP]
show "{ce_set_to_rel A |A. A \<in> ce_sets} \<subseteq> ce_rels"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {ce_set_to_rel A |A. A \<in> ce_sets} \<subseteq> ce_rels
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> {ce_set_to_rel A |A. A \<in> ce_sets} \<Longrightarrow> x \<in> ce_rels
[PROOF STEP]
fix r
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> {ce_set_to_rel A |A. A \<in> ce_sets} \<Longrightarrow> x \<in> ce_rels
[PROOF STEP]
show "r \<in> {ce_set_to_rel A |A. A \<in> ce_sets} \<Longrightarrow> r \<in> ce_rels"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r \<in> {ce_set_to_rel A |A. A \<in> ce_sets} \<Longrightarrow> r \<in> ce_rels
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. r \<in> {ce_set_to_rel A |A. A \<in> ce_sets} \<Longrightarrow> r \<in> ce_rels
[PROOF STEP]
assume A: "r \<in> {ce_set_to_rel A |A. A \<in> ce_sets}"
[PROOF STATE]
proof (state)
this:
r \<in> {ce_set_to_rel A |A. A \<in> ce_sets}

goal (1 subgoal):
 1. r \<in> {ce_set_to_rel A |A. A \<in> ce_sets} \<Longrightarrow> r \<in> ce_rels
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
r \<in> {ce_set_to_rel A |A. A \<in> ce_sets}
[PROOF STEP]
obtain A where L1: "r = ce_set_to_rel A" and L2: "A \<in> ce_sets"
[PROOF STATE]
proof (prove)
using this:
r \<in> {ce_set_to_rel A |A. A \<in> ce_sets}

goal (1 subgoal):
 1. (\<And>A. \<lbrakk>r = ce_set_to_rel A; A \<in> ce_sets\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
r = ce_set_to_rel A
A \<in> ce_sets

goal (1 subgoal):
 1. r \<in> {ce_set_to_rel A |A. A \<in> ce_sets} \<Longrightarrow> r \<in> ce_rels
[PROOF STEP]
from L1
[PROOF STATE]
proof (chain)
picking this:
r = ce_set_to_rel A
[PROOF STEP]
have "ce_rel_to_set r = A"
[PROOF STATE]
proof (prove)
using this:
r = ce_set_to_rel A

goal (1 subgoal):
 1. ce_rel_to_set r = A
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
ce_rel_to_set r = A

goal (1 subgoal):
 1. r \<in> {ce_set_to_rel A |A. A \<in> ce_sets} \<Longrightarrow> r \<in> ce_rels
[PROOF STEP]
with L2
[PROOF STATE]
proof (chain)
picking this:
A \<in> ce_sets
ce_rel_to_set r = A
[PROOF STEP]
show "r \<in> ce_rels"
[PROOF STATE]
proof (prove)
using this:
A \<in> ce_sets
ce_rel_to_set r = A

goal (1 subgoal):
 1. r \<in> ce_rels
[PROOF STEP]
unfolding ce_rels_def
[PROOF STATE]
proof (prove)
using this:
A \<in> ce_sets
ce_rel_to_set r = A

goal (1 subgoal):
 1. r \<in> {R |R. ce_rel_to_set R \<in> ce_sets}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
r \<in> ce_rels

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
r \<in> {ce_set_to_rel A |A. A \<in> ce_sets} \<Longrightarrow> r \<in> ce_rels

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
{ce_set_to_rel A |A. A \<in> ce_sets} \<subseteq> ce_rels

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ce_rel_to_set_inj: "inj ce_rel_to_set"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj ce_rel_to_set
[PROOF STEP]
proof (rule inj_on_inverseI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> UNIV \<Longrightarrow> ?g (ce_rel_to_set x) = x
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> UNIV \<Longrightarrow> ?g (ce_rel_to_set x) = x
[PROOF STEP]
assume A: "(x::(nat\<times>nat) set) \<in> UNIV"
[PROOF STATE]
proof (state)
this:
x \<in> UNIV

goal (1 subgoal):
 1. \<And>x. x \<in> UNIV \<Longrightarrow> ?g (ce_rel_to_set x) = x
[PROOF STEP]
show "ce_set_to_rel (ce_rel_to_set x) = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ce_set_to_rel (ce_rel_to_set x) = x
[PROOF STEP]
by (rule ce_rel_lm_1)
[PROOF STATE]
proof (state)
this:
ce_set_to_rel (ce_rel_to_set x) = x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ce_rel_to_set_srj: "surj ce_rel_to_set"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. surj ce_rel_to_set
[PROOF STEP]
proof (rule surjI [where ?f=ce_set_to_rel])
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. ce_rel_to_set (ce_set_to_rel x) = x
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. ce_rel_to_set (ce_set_to_rel x) = x
[PROOF STEP]
show "ce_rel_to_set (ce_set_to_rel x) = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ce_rel_to_set (ce_set_to_rel x) = x
[PROOF STEP]
by (rule ce_rel_lm_2)
[PROOF STATE]
proof (state)
this:
ce_rel_to_set (ce_set_to_rel x) = x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ce_rel_to_set_bij: "bij ce_rel_to_set"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bij ce_rel_to_set
[PROOF STEP]
proof (rule bijI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. inj ce_rel_to_set
 2. surj ce_rel_to_set
[PROOF STEP]
show "inj ce_rel_to_set"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj ce_rel_to_set
[PROOF STEP]
by (rule ce_rel_to_set_inj)
[PROOF STATE]
proof (state)
this:
inj ce_rel_to_set

goal (1 subgoal):
 1. surj ce_rel_to_set
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. surj ce_rel_to_set
[PROOF STEP]
show "surj ce_rel_to_set"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. surj ce_rel_to_set
[PROOF STEP]
by (rule ce_rel_to_set_srj)
[PROOF STATE]
proof (state)
this:
surj ce_rel_to_set

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ce_set_to_rel_inj: "inj ce_set_to_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj ce_set_to_rel
[PROOF STEP]
proof (rule inj_on_inverseI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> UNIV \<Longrightarrow> ?g (ce_set_to_rel x) = x
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> UNIV \<Longrightarrow> ?g (ce_set_to_rel x) = x
[PROOF STEP]
assume A: "(x::nat set) \<in> UNIV"
[PROOF STATE]
proof (state)
this:
x \<in> UNIV

goal (1 subgoal):
 1. \<And>x. x \<in> UNIV \<Longrightarrow> ?g (ce_set_to_rel x) = x
[PROOF STEP]
show "ce_rel_to_set (ce_set_to_rel x) = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ce_rel_to_set (ce_set_to_rel x) = x
[PROOF STEP]
by (rule ce_rel_lm_2)
[PROOF STATE]
proof (state)
this:
ce_rel_to_set (ce_set_to_rel x) = x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ce_set_to_rel_srj: "surj ce_set_to_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. surj ce_set_to_rel
[PROOF STEP]
proof (rule surjI [where ?f=ce_rel_to_set])
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. ce_set_to_rel (ce_rel_to_set x) = x
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. ce_set_to_rel (ce_rel_to_set x) = x
[PROOF STEP]
show "ce_set_to_rel (ce_rel_to_set x) = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ce_set_to_rel (ce_rel_to_set x) = x
[PROOF STEP]
by (rule ce_rel_lm_1)
[PROOF STATE]
proof (state)
this:
ce_set_to_rel (ce_rel_to_set x) = x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ce_set_to_rel_bij: "bij ce_set_to_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bij ce_set_to_rel
[PROOF STEP]
proof (rule bijI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. inj ce_set_to_rel
 2. surj ce_set_to_rel
[PROOF STEP]
show "inj ce_set_to_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj ce_set_to_rel
[PROOF STEP]
by (rule ce_set_to_rel_inj)
[PROOF STATE]
proof (state)
this:
inj ce_set_to_rel

goal (1 subgoal):
 1. surj ce_set_to_rel
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. surj ce_set_to_rel
[PROOF STEP]
show "surj ce_set_to_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. surj ce_set_to_rel
[PROOF STEP]
by (rule ce_set_to_rel_srj)
[PROOF STATE]
proof (state)
this:
surj ce_set_to_rel

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ce_rel_lm_3: "A \<in> ce_sets \<Longrightarrow> ce_set_to_rel A \<in> ce_rels"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<in> ce_sets \<Longrightarrow> ce_set_to_rel A \<in> ce_rels
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. A \<in> ce_sets \<Longrightarrow> ce_set_to_rel A \<in> ce_rels
[PROOF STEP]
assume A: "A \<in> ce_sets"
[PROOF STATE]
proof (state)
this:
A \<in> ce_sets

goal (1 subgoal):
 1. A \<in> ce_sets \<Longrightarrow> ce_set_to_rel A \<in> ce_rels
[PROOF STEP]
from A ce_rels_def1
[PROOF STATE]
proof (chain)
picking this:
A \<in> ce_sets
ce_rels = {ce_set_to_rel A |A. A \<in> ce_sets}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
A \<in> ce_sets
ce_rels = {ce_set_to_rel A |A. A \<in> ce_sets}

goal (1 subgoal):
 1. ce_set_to_rel A \<in> ce_rels
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ce_set_to_rel A \<in> ce_rels

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ce_rel_lm_4: "ce_set_to_rel A \<in> ce_rels \<Longrightarrow> A \<in> ce_sets"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ce_set_to_rel A \<in> ce_rels \<Longrightarrow> A \<in> ce_sets
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ce_set_to_rel A \<in> ce_rels \<Longrightarrow> A \<in> ce_sets
[PROOF STEP]
assume A: "ce_set_to_rel A \<in> ce_rels"
[PROOF STATE]
proof (state)
this:
ce_set_to_rel A \<in> ce_rels

goal (1 subgoal):
 1. ce_set_to_rel A \<in> ce_rels \<Longrightarrow> A \<in> ce_sets
[PROOF STEP]
from A
[PROOF STATE]
proof (chain)
picking this:
ce_set_to_rel A \<in> ce_rels
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
ce_set_to_rel A \<in> ce_rels

goal (1 subgoal):
 1. A \<in> ce_sets
[PROOF STEP]
by (unfold ce_rels_def, auto)
[PROOF STATE]
proof (state)
this:
A \<in> ce_sets

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ce_rel_lm_5: "(A \<in> ce_sets) = (ce_set_to_rel A \<in> ce_rels)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (A \<in> ce_sets) = (ce_set_to_rel A \<in> ce_rels)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. A \<in> ce_sets \<Longrightarrow> ce_set_to_rel A \<in> ce_rels
 2. ce_set_to_rel A \<in> ce_rels \<Longrightarrow> A \<in> ce_sets
[PROOF STEP]
assume "A \<in> ce_sets"
[PROOF STATE]
proof (state)
this:
A \<in> ce_sets

goal (2 subgoals):
 1. A \<in> ce_sets \<Longrightarrow> ce_set_to_rel A \<in> ce_rels
 2. ce_set_to_rel A \<in> ce_rels \<Longrightarrow> A \<in> ce_sets
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
A \<in> ce_sets
[PROOF STEP]
show "ce_set_to_rel A \<in> ce_rels"
[PROOF STATE]
proof (prove)
using this:
A \<in> ce_sets

goal (1 subgoal):
 1. ce_set_to_rel A \<in> ce_rels
[PROOF STEP]
by (rule ce_rel_lm_3)
[PROOF STATE]
proof (state)
this:
ce_set_to_rel A \<in> ce_rels

goal (1 subgoal):
 1. ce_set_to_rel A \<in> ce_rels \<Longrightarrow> A \<in> ce_sets
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ce_set_to_rel A \<in> ce_rels \<Longrightarrow> A \<in> ce_sets
[PROOF STEP]
assume "ce_set_to_rel A \<in> ce_rels"
[PROOF STATE]
proof (state)
this:
ce_set_to_rel A \<in> ce_rels

goal (1 subgoal):
 1. ce_set_to_rel A \<in> ce_rels \<Longrightarrow> A \<in> ce_sets
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ce_set_to_rel A \<in> ce_rels
[PROOF STEP]
show "A \<in> ce_sets"
[PROOF STATE]
proof (prove)
using this:
ce_set_to_rel A \<in> ce_rels

goal (1 subgoal):
 1. A \<in> ce_sets
[PROOF STEP]
by (rule ce_rel_lm_4)
[PROOF STATE]
proof (state)
this:
A \<in> ce_sets

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ce_rel_lm_6: "r \<in> ce_rels \<Longrightarrow> ce_rel_to_set r \<in> ce_sets"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r \<in> ce_rels \<Longrightarrow> ce_rel_to_set r \<in> ce_sets
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. r \<in> ce_rels \<Longrightarrow> ce_rel_to_set r \<in> ce_sets
[PROOF STEP]
assume A: "r \<in> ce_rels"
[PROOF STATE]
proof (state)
this:
r \<in> ce_rels

goal (1 subgoal):
 1. r \<in> ce_rels \<Longrightarrow> ce_rel_to_set r \<in> ce_sets
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
r \<in> ce_rels
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
r \<in> ce_rels

goal (1 subgoal):
 1. ce_rel_to_set r \<in> ce_sets
[PROOF STEP]
by (unfold ce_rels_def, auto)
[PROOF STATE]
proof (state)
this:
ce_rel_to_set r \<in> ce_sets

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ce_rel_lm_7: "ce_rel_to_set r \<in> ce_sets \<Longrightarrow> r \<in> ce_rels"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ce_rel_to_set r \<in> ce_sets \<Longrightarrow> r \<in> ce_rels
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ce_rel_to_set r \<in> ce_sets \<Longrightarrow> r \<in> ce_rels
[PROOF STEP]
assume "ce_rel_to_set r \<in> ce_sets"
[PROOF STATE]
proof (state)
this:
ce_rel_to_set r \<in> ce_sets

goal (1 subgoal):
 1. ce_rel_to_set r \<in> ce_sets \<Longrightarrow> r \<in> ce_rels
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ce_rel_to_set r \<in> ce_sets
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
ce_rel_to_set r \<in> ce_sets

goal (1 subgoal):
 1. r \<in> ce_rels
[PROOF STEP]
by (unfold ce_rels_def, auto)
[PROOF STATE]
proof (state)
this:
r \<in> ce_rels

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ce_rel_lm_8: "(r \<in> ce_rels) = (ce_rel_to_set r \<in> ce_sets)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (r \<in> ce_rels) = (ce_rel_to_set r \<in> ce_sets)
[PROOF STEP]
by (unfold ce_rels_def, auto)


[STATEMENT]
lemma ce_rel_lm_9: "(x,y) \<in> r \<Longrightarrow> c_pair x y \<in> ce_rel_to_set r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x, y) \<in> r \<Longrightarrow> c_pair x y \<in> ce_rel_to_set r
[PROOF STEP]
by (unfold ce_rel_to_set_def, auto)


[STATEMENT]
lemma ce_rel_lm_10: "x \<in> A \<Longrightarrow> (c_fst x, c_snd x) \<in> ce_set_to_rel A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> A \<Longrightarrow> (c_fst x, c_snd x) \<in> ce_set_to_rel A
[PROOF STEP]
by (unfold ce_set_to_rel_def, auto)


[STATEMENT]
lemma ce_rel_lm_11: "c_pair x y \<in> ce_rel_to_set r \<Longrightarrow> (x,y) \<in> r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c_pair x y \<in> ce_rel_to_set r \<Longrightarrow> (x, y) \<in> r
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. c_pair x y \<in> ce_rel_to_set r \<Longrightarrow> (x, y) \<in> r
[PROOF STEP]
assume A: "c_pair x y \<in> ce_rel_to_set r"
[PROOF STATE]
proof (state)
this:
c_pair x y \<in> ce_rel_to_set r

goal (1 subgoal):
 1. c_pair x y \<in> ce_rel_to_set r \<Longrightarrow> (x, y) \<in> r
[PROOF STEP]
let ?z = "c_pair x y"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. c_pair x y \<in> ce_rel_to_set r \<Longrightarrow> (x, y) \<in> r
[PROOF STEP]
from A
[PROOF STATE]
proof (chain)
picking this:
c_pair x y \<in> ce_rel_to_set r
[PROOF STEP]
have "(c_fst ?z, c_snd ?z) \<in> ce_set_to_rel (ce_rel_to_set r)"
[PROOF STATE]
proof (prove)
using this:
c_pair x y \<in> ce_rel_to_set r

goal (1 subgoal):
 1. (c_fst (c_pair x y), c_snd (c_pair x y)) \<in> ce_set_to_rel (ce_rel_to_set r)
[PROOF STEP]
by (rule ce_rel_lm_10)
[PROOF STATE]
proof (state)
this:
(c_fst (c_pair x y), c_snd (c_pair x y)) \<in> ce_set_to_rel (ce_rel_to_set r)

goal (1 subgoal):
 1. c_pair x y \<in> ce_rel_to_set r \<Longrightarrow> (x, y) \<in> r
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(c_fst (c_pair x y), c_snd (c_pair x y)) \<in> ce_set_to_rel (ce_rel_to_set r)
[PROOF STEP]
show "(x,y) \<in> r"
[PROOF STATE]
proof (prove)
using this:
(c_fst (c_pair x y), c_snd (c_pair x y)) \<in> ce_set_to_rel (ce_rel_to_set r)

goal (1 subgoal):
 1. (x, y) \<in> r
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(x, y) \<in> r

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ce_rel_lm_12: "(c_pair x y \<in> ce_rel_to_set r) = ((x,y) \<in> r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (c_pair x y \<in> ce_rel_to_set r) = ((x, y) \<in> r)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. c_pair x y \<in> ce_rel_to_set r \<Longrightarrow> (x, y) \<in> r
 2. (x, y) \<in> r \<Longrightarrow> c_pair x y \<in> ce_rel_to_set r
[PROOF STEP]
assume "c_pair x y \<in> ce_rel_to_set r"
[PROOF STATE]
proof (state)
this:
c_pair x y \<in> ce_rel_to_set r

goal (2 subgoals):
 1. c_pair x y \<in> ce_rel_to_set r \<Longrightarrow> (x, y) \<in> r
 2. (x, y) \<in> r \<Longrightarrow> c_pair x y \<in> ce_rel_to_set r
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
c_pair x y \<in> ce_rel_to_set r
[PROOF STEP]
show "(x, y) \<in> r"
[PROOF STATE]
proof (prove)
using this:
c_pair x y \<in> ce_rel_to_set r

goal (1 subgoal):
 1. (x, y) \<in> r
[PROOF STEP]
by (rule ce_rel_lm_11)
[PROOF STATE]
proof (state)
this:
(x, y) \<in> r

goal (1 subgoal):
 1. (x, y) \<in> r \<Longrightarrow> c_pair x y \<in> ce_rel_to_set r
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (x, y) \<in> r \<Longrightarrow> c_pair x y \<in> ce_rel_to_set r
[PROOF STEP]
assume "(x, y) \<in> r"
[PROOF STATE]
proof (state)
this:
(x, y) \<in> r

goal (1 subgoal):
 1. (x, y) \<in> r \<Longrightarrow> c_pair x y \<in> ce_rel_to_set r
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(x, y) \<in> r
[PROOF STEP]
show "c_pair x y \<in> ce_rel_to_set r"
[PROOF STATE]
proof (prove)
using this:
(x, y) \<in> r

goal (1 subgoal):
 1. c_pair x y \<in> ce_rel_to_set r
[PROOF STEP]
by (rule ce_rel_lm_9)
[PROOF STATE]
proof (state)
this:
c_pair x y \<in> ce_rel_to_set r

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ce_rel_lm_13: "(x,y) \<in> ce_set_to_rel A \<Longrightarrow> c_pair x y \<in> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x, y) \<in> ce_set_to_rel A \<Longrightarrow> c_pair x y \<in> A
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (x, y) \<in> ce_set_to_rel A \<Longrightarrow> c_pair x y \<in> A
[PROOF STEP]
assume "(x,y) \<in> ce_set_to_rel A"
[PROOF STATE]
proof (state)
this:
(x, y) \<in> ce_set_to_rel A

goal (1 subgoal):
 1. (x, y) \<in> ce_set_to_rel A \<Longrightarrow> c_pair x y \<in> A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(x, y) \<in> ce_set_to_rel A
[PROOF STEP]
have "c_pair x y \<in> ce_rel_to_set (ce_set_to_rel A)"
[PROOF STATE]
proof (prove)
using this:
(x, y) \<in> ce_set_to_rel A

goal (1 subgoal):
 1. c_pair x y \<in> ce_rel_to_set (ce_set_to_rel A)
[PROOF STEP]
by (rule ce_rel_lm_9)
[PROOF STATE]
proof (state)
this:
c_pair x y \<in> ce_rel_to_set (ce_set_to_rel A)

goal (1 subgoal):
 1. (x, y) \<in> ce_set_to_rel A \<Longrightarrow> c_pair x y \<in> A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
c_pair x y \<in> ce_rel_to_set (ce_set_to_rel A)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
c_pair x y \<in> ce_rel_to_set (ce_set_to_rel A)

goal (1 subgoal):
 1. c_pair x y \<in> A
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
c_pair x y \<in> A

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ce_rel_lm_14: "c_pair x y \<in> A \<Longrightarrow> (x,y) \<in> ce_set_to_rel A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c_pair x y \<in> A \<Longrightarrow> (x, y) \<in> ce_set_to_rel A
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. c_pair x y \<in> A \<Longrightarrow> (x, y) \<in> ce_set_to_rel A
[PROOF STEP]
assume "c_pair x y \<in> A"
[PROOF STATE]
proof (state)
this:
c_pair x y \<in> A

goal (1 subgoal):
 1. c_pair x y \<in> A \<Longrightarrow> (x, y) \<in> ce_set_to_rel A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
c_pair x y \<in> A
[PROOF STEP]
have "c_pair x y \<in> ce_rel_to_set (ce_set_to_rel A)"
[PROOF STATE]
proof (prove)
using this:
c_pair x y \<in> A

goal (1 subgoal):
 1. c_pair x y \<in> ce_rel_to_set (ce_set_to_rel A)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
c_pair x y \<in> ce_rel_to_set (ce_set_to_rel A)

goal (1 subgoal):
 1. c_pair x y \<in> A \<Longrightarrow> (x, y) \<in> ce_set_to_rel A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
c_pair x y \<in> ce_rel_to_set (ce_set_to_rel A)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
c_pair x y \<in> ce_rel_to_set (ce_set_to_rel A)

goal (1 subgoal):
 1. (x, y) \<in> ce_set_to_rel A
[PROOF STEP]
by (rule ce_rel_lm_11)
[PROOF STATE]
proof (state)
this:
(x, y) \<in> ce_set_to_rel A

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ce_rel_lm_15: "((x,y) \<in> ce_set_to_rel A) = (c_pair x y \<in> A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((x, y) \<in> ce_set_to_rel A) = (c_pair x y \<in> A)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (x, y) \<in> ce_set_to_rel A \<Longrightarrow> c_pair x y \<in> A
 2. c_pair x y \<in> A \<Longrightarrow> (x, y) \<in> ce_set_to_rel A
[PROOF STEP]
assume "(x, y) \<in> ce_set_to_rel A"
[PROOF STATE]
proof (state)
this:
(x, y) \<in> ce_set_to_rel A

goal (2 subgoals):
 1. (x, y) \<in> ce_set_to_rel A \<Longrightarrow> c_pair x y \<in> A
 2. c_pair x y \<in> A \<Longrightarrow> (x, y) \<in> ce_set_to_rel A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(x, y) \<in> ce_set_to_rel A
[PROOF STEP]
show "c_pair x y \<in> A"
[PROOF STATE]
proof (prove)
using this:
(x, y) \<in> ce_set_to_rel A

goal (1 subgoal):
 1. c_pair x y \<in> A
[PROOF STEP]
by (rule ce_rel_lm_13)
[PROOF STATE]
proof (state)
this:
c_pair x y \<in> A

goal (1 subgoal):
 1. c_pair x y \<in> A \<Longrightarrow> (x, y) \<in> ce_set_to_rel A
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. c_pair x y \<in> A \<Longrightarrow> (x, y) \<in> ce_set_to_rel A
[PROOF STEP]
assume "c_pair x y \<in> A"
[PROOF STATE]
proof (state)
this:
c_pair x y \<in> A

goal (1 subgoal):
 1. c_pair x y \<in> A \<Longrightarrow> (x, y) \<in> ce_set_to_rel A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
c_pair x y \<in> A
[PROOF STEP]
show "(x, y) \<in> ce_set_to_rel A"
[PROOF STATE]
proof (prove)
using this:
c_pair x y \<in> A

goal (1 subgoal):
 1. (x, y) \<in> ce_set_to_rel A
[PROOF STEP]
by (rule ce_rel_lm_14)
[PROOF STATE]
proof (state)
this:
(x, y) \<in> ce_set_to_rel A

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ce_rel_lm_16: "x \<in> ce_rel_to_set r \<Longrightarrow> (c_fst x, c_snd x) \<in> r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> ce_rel_to_set r \<Longrightarrow> (c_fst x, c_snd x) \<in> r
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<in> ce_rel_to_set r \<Longrightarrow> (c_fst x, c_snd x) \<in> r
[PROOF STEP]
assume "x \<in> ce_rel_to_set r"
[PROOF STATE]
proof (state)
this:
x \<in> ce_rel_to_set r

goal (1 subgoal):
 1. x \<in> ce_rel_to_set r \<Longrightarrow> (c_fst x, c_snd x) \<in> r
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> ce_rel_to_set r
[PROOF STEP]
have "(c_fst x, c_snd x) \<in> ce_set_to_rel (ce_rel_to_set r)"
[PROOF STATE]
proof (prove)
using this:
x \<in> ce_rel_to_set r

goal (1 subgoal):
 1. (c_fst x, c_snd x) \<in> ce_set_to_rel (ce_rel_to_set r)
[PROOF STEP]
by (rule ce_rel_lm_10)
[PROOF STATE]
proof (state)
this:
(c_fst x, c_snd x) \<in> ce_set_to_rel (ce_rel_to_set r)

goal (1 subgoal):
 1. x \<in> ce_rel_to_set r \<Longrightarrow> (c_fst x, c_snd x) \<in> r
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(c_fst x, c_snd x) \<in> ce_set_to_rel (ce_rel_to_set r)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(c_fst x, c_snd x) \<in> ce_set_to_rel (ce_rel_to_set r)

goal (1 subgoal):
 1. (c_fst x, c_snd x) \<in> r
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(c_fst x, c_snd x) \<in> r

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ce_rel_lm_17: "(c_fst x, c_snd x) \<in> ce_set_to_rel A \<Longrightarrow> x \<in> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (c_fst x, c_snd x) \<in> ce_set_to_rel A \<Longrightarrow> x \<in> A
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (c_fst x, c_snd x) \<in> ce_set_to_rel A \<Longrightarrow> x \<in> A
[PROOF STEP]
assume "(c_fst x, c_snd x) \<in> ce_set_to_rel A"
[PROOF STATE]
proof (state)
this:
(c_fst x, c_snd x) \<in> ce_set_to_rel A

goal (1 subgoal):
 1. (c_fst x, c_snd x) \<in> ce_set_to_rel A \<Longrightarrow> x \<in> A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(c_fst x, c_snd x) \<in> ce_set_to_rel A
[PROOF STEP]
have "c_pair (c_fst x) (c_snd x) \<in> A"
[PROOF STATE]
proof (prove)
using this:
(c_fst x, c_snd x) \<in> ce_set_to_rel A

goal (1 subgoal):
 1. c_pair (c_fst x) (c_snd x) \<in> A
[PROOF STEP]
by (rule ce_rel_lm_13)
[PROOF STATE]
proof (state)
this:
c_pair (c_fst x) (c_snd x) \<in> A

goal (1 subgoal):
 1. (c_fst x, c_snd x) \<in> ce_set_to_rel A \<Longrightarrow> x \<in> A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
c_pair (c_fst x) (c_snd x) \<in> A
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
c_pair (c_fst x) (c_snd x) \<in> A

goal (1 subgoal):
 1. x \<in> A
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x \<in> A

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ce_rel_lm_18: "((c_fst x, c_snd x) \<in> ce_set_to_rel A) = (x \<in> A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((c_fst x, c_snd x) \<in> ce_set_to_rel A) = (x \<in> A)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (c_fst x, c_snd x) \<in> ce_set_to_rel A \<Longrightarrow> x \<in> A
 2. x \<in> A \<Longrightarrow> (c_fst x, c_snd x) \<in> ce_set_to_rel A
[PROOF STEP]
assume "(c_fst x, c_snd x) \<in> ce_set_to_rel A"
[PROOF STATE]
proof (state)
this:
(c_fst x, c_snd x) \<in> ce_set_to_rel A

goal (2 subgoals):
 1. (c_fst x, c_snd x) \<in> ce_set_to_rel A \<Longrightarrow> x \<in> A
 2. x \<in> A \<Longrightarrow> (c_fst x, c_snd x) \<in> ce_set_to_rel A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(c_fst x, c_snd x) \<in> ce_set_to_rel A
[PROOF STEP]
show "x \<in> A"
[PROOF STATE]
proof (prove)
using this:
(c_fst x, c_snd x) \<in> ce_set_to_rel A

goal (1 subgoal):
 1. x \<in> A
[PROOF STEP]
by (rule ce_rel_lm_17)
[PROOF STATE]
proof (state)
this:
x \<in> A

goal (1 subgoal):
 1. x \<in> A \<Longrightarrow> (c_fst x, c_snd x) \<in> ce_set_to_rel A
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<in> A \<Longrightarrow> (c_fst x, c_snd x) \<in> ce_set_to_rel A
[PROOF STEP]
assume "x \<in> A"
[PROOF STATE]
proof (state)
this:
x \<in> A

goal (1 subgoal):
 1. x \<in> A \<Longrightarrow> (c_fst x, c_snd x) \<in> ce_set_to_rel A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> A
[PROOF STEP]
show "(c_fst x, c_snd x) \<in> ce_set_to_rel A"
[PROOF STATE]
proof (prove)
using this:
x \<in> A

goal (1 subgoal):
 1. (c_fst x, c_snd x) \<in> ce_set_to_rel A
[PROOF STEP]
by (rule ce_rel_lm_10)
[PROOF STATE]
proof (state)
this:
(c_fst x, c_snd x) \<in> ce_set_to_rel A

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ce_rel_lm_19: "(c_fst x, c_snd x) \<in> r \<Longrightarrow> x \<in> ce_rel_to_set r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (c_fst x, c_snd x) \<in> r \<Longrightarrow> x \<in> ce_rel_to_set r
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (c_fst x, c_snd x) \<in> r \<Longrightarrow> x \<in> ce_rel_to_set r
[PROOF STEP]
assume "(c_fst x, c_snd x) \<in> r"
[PROOF STATE]
proof (state)
this:
(c_fst x, c_snd x) \<in> r

goal (1 subgoal):
 1. (c_fst x, c_snd x) \<in> r \<Longrightarrow> x \<in> ce_rel_to_set r
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(c_fst x, c_snd x) \<in> r
[PROOF STEP]
have "(c_fst x, c_snd x) \<in> ce_set_to_rel (ce_rel_to_set r)"
[PROOF STATE]
proof (prove)
using this:
(c_fst x, c_snd x) \<in> r

goal (1 subgoal):
 1. (c_fst x, c_snd x) \<in> ce_set_to_rel (ce_rel_to_set r)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(c_fst x, c_snd x) \<in> ce_set_to_rel (ce_rel_to_set r)

goal (1 subgoal):
 1. (c_fst x, c_snd x) \<in> r \<Longrightarrow> x \<in> ce_rel_to_set r
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(c_fst x, c_snd x) \<in> ce_set_to_rel (ce_rel_to_set r)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(c_fst x, c_snd x) \<in> ce_set_to_rel (ce_rel_to_set r)

goal (1 subgoal):
 1. x \<in> ce_rel_to_set r
[PROOF STEP]
by (rule ce_rel_lm_17)
[PROOF STATE]
proof (state)
this:
x \<in> ce_rel_to_set r

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ce_rel_lm_20: "((c_fst x, c_snd x) \<in> r) = (x \<in> ce_rel_to_set r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((c_fst x, c_snd x) \<in> r) = (x \<in> ce_rel_to_set r)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (c_fst x, c_snd x) \<in> r \<Longrightarrow> x \<in> ce_rel_to_set r
 2. x \<in> ce_rel_to_set r \<Longrightarrow> (c_fst x, c_snd x) \<in> r
[PROOF STEP]
assume "(c_fst x, c_snd x) \<in> r"
[PROOF STATE]
proof (state)
this:
(c_fst x, c_snd x) \<in> r

goal (2 subgoals):
 1. (c_fst x, c_snd x) \<in> r \<Longrightarrow> x \<in> ce_rel_to_set r
 2. x \<in> ce_rel_to_set r \<Longrightarrow> (c_fst x, c_snd x) \<in> r
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(c_fst x, c_snd x) \<in> r
[PROOF STEP]
show "x \<in> ce_rel_to_set r"
[PROOF STATE]
proof (prove)
using this:
(c_fst x, c_snd x) \<in> r

goal (1 subgoal):
 1. x \<in> ce_rel_to_set r
[PROOF STEP]
by (rule ce_rel_lm_19)
[PROOF STATE]
proof (state)
this:
x \<in> ce_rel_to_set r

goal (1 subgoal):
 1. x \<in> ce_rel_to_set r \<Longrightarrow> (c_fst x, c_snd x) \<in> r
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<in> ce_rel_to_set r \<Longrightarrow> (c_fst x, c_snd x) \<in> r
[PROOF STEP]
assume "x \<in> ce_rel_to_set r"
[PROOF STATE]
proof (state)
this:
x \<in> ce_rel_to_set r

goal (1 subgoal):
 1. x \<in> ce_rel_to_set r \<Longrightarrow> (c_fst x, c_snd x) \<in> r
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> ce_rel_to_set r
[PROOF STEP]
show "(c_fst x, c_snd x) \<in> r"
[PROOF STATE]
proof (prove)
using this:
x \<in> ce_rel_to_set r

goal (1 subgoal):
 1. (c_fst x, c_snd x) \<in> r
[PROOF STEP]
by (rule ce_rel_lm_16)
[PROOF STATE]
proof (state)
this:
(c_fst x, c_snd x) \<in> r

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ce_rel_lm_21: "r \<in> ce_rels \<Longrightarrow> \<exists> p \<in> PrimRec3. \<forall> x y. ((x,y) \<in> r) = (\<exists> u. p x y u = 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r \<in> ce_rels \<Longrightarrow> \<exists>p\<in>PrimRec3. \<forall>x y. ((x, y) \<in> r) = (\<exists>u. p x y u = 0)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. r \<in> ce_rels \<Longrightarrow> \<exists>p\<in>PrimRec3. \<forall>x y. ((x, y) \<in> r) = (\<exists>u. p x y u = 0)
[PROOF STEP]
assume r_ce: "r \<in> ce_rels"
[PROOF STATE]
proof (state)
this:
r \<in> ce_rels

goal (1 subgoal):
 1. r \<in> ce_rels \<Longrightarrow> \<exists>p\<in>PrimRec3. \<forall>x y. ((x, y) \<in> r) = (\<exists>u. p x y u = 0)
[PROOF STEP]
define A where "A = ce_rel_to_set r"
[PROOF STATE]
proof (state)
this:
A = ce_rel_to_set r

goal (1 subgoal):
 1. r \<in> ce_rels \<Longrightarrow> \<exists>p\<in>PrimRec3. \<forall>x y. ((x, y) \<in> r) = (\<exists>u. p x y u = 0)
[PROOF STEP]
from r_ce
[PROOF STATE]
proof (chain)
picking this:
r \<in> ce_rels
[PROOF STEP]
have A_ce: "A \<in> ce_sets"
[PROOF STATE]
proof (prove)
using this:
r \<in> ce_rels

goal (1 subgoal):
 1. A \<in> ce_sets
[PROOF STEP]
by (unfold A_def, rule ce_rel_lm_6)
[PROOF STATE]
proof (state)
this:
A \<in> ce_sets

goal (1 subgoal):
 1. r \<in> ce_rels \<Longrightarrow> \<exists>p\<in>PrimRec3. \<forall>x y. ((x, y) \<in> r) = (\<exists>u. p x y u = 0)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
A \<in> ce_sets
[PROOF STEP]
have "\<exists> p \<in> PrimRec2. A = fn_to_set p"
[PROOF STATE]
proof (prove)
using this:
A \<in> ce_sets

goal (1 subgoal):
 1. \<exists>p\<in>PrimRec2. A = fn_to_set p
[PROOF STEP]
by (rule ce_set_lm_3)
[PROOF STATE]
proof (state)
this:
\<exists>p\<in>PrimRec2. A = fn_to_set p

goal (1 subgoal):
 1. r \<in> ce_rels \<Longrightarrow> \<exists>p\<in>PrimRec3. \<forall>x y. ((x, y) \<in> r) = (\<exists>u. p x y u = 0)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>p\<in>PrimRec2. A = fn_to_set p
[PROOF STEP]
obtain q where q_is_pr: "q \<in> PrimRec2" and A_def1: "A = fn_to_set q"
[PROOF STATE]
proof (prove)
using this:
\<exists>p\<in>PrimRec2. A = fn_to_set p

goal (1 subgoal):
 1. (\<And>q. \<lbrakk>q \<in> PrimRec2; A = fn_to_set q\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
q \<in> PrimRec2
A = fn_to_set q

goal (1 subgoal):
 1. r \<in> ce_rels \<Longrightarrow> \<exists>p\<in>PrimRec3. \<forall>x y. ((x, y) \<in> r) = (\<exists>u. p x y u = 0)
[PROOF STEP]
from A_def1
[PROOF STATE]
proof (chain)
picking this:
A = fn_to_set q
[PROOF STEP]
have A_def2: "A = { x. \<exists> y. q x y = 0}"
[PROOF STATE]
proof (prove)
using this:
A = fn_to_set q

goal (1 subgoal):
 1. A = {x. \<exists>y. q x y = 0}
[PROOF STEP]
by (unfold fn_to_set_def)
[PROOF STATE]
proof (state)
this:
A = {x. \<exists>y. q x y = 0}

goal (1 subgoal):
 1. r \<in> ce_rels \<Longrightarrow> \<exists>p\<in>PrimRec3. \<forall>x y. ((x, y) \<in> r) = (\<exists>u. p x y u = 0)
[PROOF STEP]
define p where "p x y u = q (c_pair x y) u" for x y u
[PROOF STATE]
proof (state)
this:
p ?x ?y ?u = q (c_pair ?x ?y) ?u

goal (1 subgoal):
 1. r \<in> ce_rels \<Longrightarrow> \<exists>p\<in>PrimRec3. \<forall>x y. ((x, y) \<in> r) = (\<exists>u. p x y u = 0)
[PROOF STEP]
from q_is_pr
[PROOF STATE]
proof (chain)
picking this:
q \<in> PrimRec2
[PROOF STEP]
have p_is_pr: "p \<in> PrimRec3"
[PROOF STATE]
proof (prove)
using this:
q \<in> PrimRec2

goal (1 subgoal):
 1. p \<in> PrimRec3
[PROOF STEP]
unfolding p_def
[PROOF STATE]
proof (prove)
using this:
q \<in> PrimRec2

goal (1 subgoal):
 1. (\<lambda>x y. q (c_pair x y)) \<in> PrimRec3
[PROOF STEP]
by prec
[PROOF STATE]
proof (state)
this:
p \<in> PrimRec3

goal (1 subgoal):
 1. r \<in> ce_rels \<Longrightarrow> \<exists>p\<in>PrimRec3. \<forall>x y. ((x, y) \<in> r) = (\<exists>u. p x y u = 0)
[PROOF STEP]
have "\<And> x y. ((x,y) \<in> r) = (\<exists> u. p x y u = 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. ((x, y) \<in> r) = (\<exists>u. p x y u = 0)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. ((x, y) \<in> r) = (\<exists>u. p x y u = 0)
[PROOF STEP]
fix x y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. ((x, y) \<in> r) = (\<exists>u. p x y u = 0)
[PROOF STEP]
show "((x,y) \<in> r) = (\<exists> u. p x y u = 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((x, y) \<in> r) = (\<exists>u. p x y u = 0)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (x, y) \<in> r \<Longrightarrow> \<exists>u. p x y u = 0
 2. \<exists>u. p x y u = 0 \<Longrightarrow> (x, y) \<in> r
[PROOF STEP]
assume A: "(x,y) \<in> r"
[PROOF STATE]
proof (state)
this:
(x, y) \<in> r

goal (2 subgoals):
 1. (x, y) \<in> r \<Longrightarrow> \<exists>u. p x y u = 0
 2. \<exists>u. p x y u = 0 \<Longrightarrow> (x, y) \<in> r
[PROOF STEP]
define z where "z = c_pair x y"
[PROOF STATE]
proof (state)
this:
z = c_pair x y

goal (2 subgoals):
 1. (x, y) \<in> r \<Longrightarrow> \<exists>u. p x y u = 0
 2. \<exists>u. p x y u = 0 \<Longrightarrow> (x, y) \<in> r
[PROOF STEP]
with A_def A
[PROOF STATE]
proof (chain)
picking this:
A = ce_rel_to_set r
(x, y) \<in> r
z = c_pair x y
[PROOF STEP]
have z_in_A: "z \<in> A"
[PROOF STATE]
proof (prove)
using this:
A = ce_rel_to_set r
(x, y) \<in> r
z = c_pair x y

goal (1 subgoal):
 1. z \<in> A
[PROOF STEP]
by (unfold ce_rel_to_set_def, auto)
[PROOF STATE]
proof (state)
this:
z \<in> A

goal (2 subgoals):
 1. (x, y) \<in> r \<Longrightarrow> \<exists>u. p x y u = 0
 2. \<exists>u. p x y u = 0 \<Longrightarrow> (x, y) \<in> r
[PROOF STEP]
with A_def2
[PROOF STATE]
proof (chain)
picking this:
A = {x. \<exists>y. q x y = 0}
z \<in> A
[PROOF STEP]
have "z \<in> { x. \<exists> y. q x y = 0}"
[PROOF STATE]
proof (prove)
using this:
A = {x. \<exists>y. q x y = 0}
z \<in> A

goal (1 subgoal):
 1. z \<in> {x. \<exists>y. q x y = 0}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
z \<in> {x. \<exists>y. q x y = 0}

goal (2 subgoals):
 1. (x, y) \<in> r \<Longrightarrow> \<exists>u. p x y u = 0
 2. \<exists>u. p x y u = 0 \<Longrightarrow> (x, y) \<in> r
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
z \<in> {x. \<exists>y. q x y = 0}
[PROOF STEP]
obtain u where "q z u = 0"
[PROOF STATE]
proof (prove)
using this:
z \<in> {x. \<exists>y. q x y = 0}

goal (1 subgoal):
 1. (\<And>u. q z u = 0 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
q z u = 0

goal (2 subgoals):
 1. (x, y) \<in> r \<Longrightarrow> \<exists>u. p x y u = 0
 2. \<exists>u. p x y u = 0 \<Longrightarrow> (x, y) \<in> r
[PROOF STEP]
with z_def
[PROOF STATE]
proof (chain)
picking this:
z = c_pair x y
q z u = 0
[PROOF STEP]
have "p x y u = 0"
[PROOF STATE]
proof (prove)
using this:
z = c_pair x y
q z u = 0

goal (1 subgoal):
 1. p x y u = 0
[PROOF STEP]
by (simp add: z_def p_def)
[PROOF STATE]
proof (state)
this:
p x y u = 0

goal (2 subgoals):
 1. (x, y) \<in> r \<Longrightarrow> \<exists>u. p x y u = 0
 2. \<exists>u. p x y u = 0 \<Longrightarrow> (x, y) \<in> r
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p x y u = 0
[PROOF STEP]
show "\<exists> u. p x y u = 0"
[PROOF STATE]
proof (prove)
using this:
p x y u = 0

goal (1 subgoal):
 1. \<exists>u. p x y u = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>u. p x y u = 0

goal (1 subgoal):
 1. \<exists>u. p x y u = 0 \<Longrightarrow> (x, y) \<in> r
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>u. p x y u = 0 \<Longrightarrow> (x, y) \<in> r
[PROOF STEP]
assume A: "\<exists> u. p x y u = 0"
[PROOF STATE]
proof (state)
this:
\<exists>u. p x y u = 0

goal (1 subgoal):
 1. \<exists>u. p x y u = 0 \<Longrightarrow> (x, y) \<in> r
[PROOF STEP]
define z where "z = c_pair x y"
[PROOF STATE]
proof (state)
this:
z = c_pair x y

goal (1 subgoal):
 1. \<exists>u. p x y u = 0 \<Longrightarrow> (x, y) \<in> r
[PROOF STEP]
from A
[PROOF STATE]
proof (chain)
picking this:
\<exists>u. p x y u = 0
[PROOF STEP]
obtain u where "p x y u = 0"
[PROOF STATE]
proof (prove)
using this:
\<exists>u. p x y u = 0

goal (1 subgoal):
 1. (\<And>u. p x y u = 0 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p x y u = 0

goal (1 subgoal):
 1. \<exists>u. p x y u = 0 \<Longrightarrow> (x, y) \<in> r
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p x y u = 0
[PROOF STEP]
have q_z: "q z u = 0"
[PROOF STATE]
proof (prove)
using this:
p x y u = 0

goal (1 subgoal):
 1. q z u = 0
[PROOF STEP]
by (simp add: z_def p_def)
[PROOF STATE]
proof (state)
this:
q z u = 0

goal (1 subgoal):
 1. \<exists>u. p x y u = 0 \<Longrightarrow> (x, y) \<in> r
[PROOF STEP]
with A_def2
[PROOF STATE]
proof (chain)
picking this:
A = {x. \<exists>y. q x y = 0}
q z u = 0
[PROOF STEP]
have z_in_A: "z \<in> A"
[PROOF STATE]
proof (prove)
using this:
A = {x. \<exists>y. q x y = 0}
q z u = 0

goal (1 subgoal):
 1. z \<in> A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
z \<in> A

goal (1 subgoal):
 1. \<exists>u. p x y u = 0 \<Longrightarrow> (x, y) \<in> r
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
z \<in> A
[PROOF STEP]
have "c_pair x y \<in> A"
[PROOF STATE]
proof (prove)
using this:
z \<in> A

goal (1 subgoal):
 1. c_pair x y \<in> A
[PROOF STEP]
by (unfold z_def)
[PROOF STATE]
proof (state)
this:
c_pair x y \<in> A

goal (1 subgoal):
 1. \<exists>u. p x y u = 0 \<Longrightarrow> (x, y) \<in> r
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
c_pair x y \<in> A
[PROOF STEP]
have "c_pair x y \<in> ce_rel_to_set r"
[PROOF STATE]
proof (prove)
using this:
c_pair x y \<in> A

goal (1 subgoal):
 1. c_pair x y \<in> ce_rel_to_set r
[PROOF STEP]
by (unfold A_def)
[PROOF STATE]
proof (state)
this:
c_pair x y \<in> ce_rel_to_set r

goal (1 subgoal):
 1. \<exists>u. p x y u = 0 \<Longrightarrow> (x, y) \<in> r
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
c_pair x y \<in> ce_rel_to_set r
[PROOF STEP]
show "(x,y) \<in> r"
[PROOF STATE]
proof (prove)
using this:
c_pair x y \<in> ce_rel_to_set r

goal (1 subgoal):
 1. (x, y) \<in> r
[PROOF STEP]
by (rule ce_rel_lm_11)
[PROOF STATE]
proof (state)
this:
(x, y) \<in> r

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
((x, y) \<in> r) = (\<exists>u. p x y u = 0)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
((?x, ?y) \<in> r) = (\<exists>u. p ?x ?y u = 0)

goal (1 subgoal):
 1. r \<in> ce_rels \<Longrightarrow> \<exists>p\<in>PrimRec3. \<forall>x y. ((x, y) \<in> r) = (\<exists>u. p x y u = 0)
[PROOF STEP]
with p_is_pr
[PROOF STATE]
proof (chain)
picking this:
p \<in> PrimRec3
((?x, ?y) \<in> r) = (\<exists>u. p ?x ?y u = 0)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
p \<in> PrimRec3
((?x, ?y) \<in> r) = (\<exists>u. p ?x ?y u = 0)

goal (1 subgoal):
 1. \<exists>p\<in>PrimRec3. \<forall>x y. ((x, y) \<in> r) = (\<exists>u. p x y u = 0)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>p\<in>PrimRec3. \<forall>x y. ((x, y) \<in> r) = (\<exists>u. p x y u = 0)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ce_rel_lm_22: "r \<in> ce_rels \<Longrightarrow> \<exists> p \<in> PrimRec3. r = { (x,y). \<exists> u. p x y u = 0 }"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r \<in> ce_rels \<Longrightarrow> \<exists>p\<in>PrimRec3. r = {(x, y). \<exists>u. p x y u = 0}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. r \<in> ce_rels \<Longrightarrow> \<exists>p\<in>PrimRec3. r = {(x, y). \<exists>u. p x y u = 0}
[PROOF STEP]
assume r_ce: "r \<in> ce_rels"
[PROOF STATE]
proof (state)
this:
r \<in> ce_rels

goal (1 subgoal):
 1. r \<in> ce_rels \<Longrightarrow> \<exists>p\<in>PrimRec3. r = {(x, y). \<exists>u. p x y u = 0}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
r \<in> ce_rels
[PROOF STEP]
have "\<exists> p \<in> PrimRec3. \<forall> x y. ((x,y) \<in> r) = (\<exists> u. p x y u = 0)"
[PROOF STATE]
proof (prove)
using this:
r \<in> ce_rels

goal (1 subgoal):
 1. \<exists>p\<in>PrimRec3. \<forall>x y. ((x, y) \<in> r) = (\<exists>u. p x y u = 0)
[PROOF STEP]
by (rule ce_rel_lm_21)
[PROOF STATE]
proof (state)
this:
\<exists>p\<in>PrimRec3. \<forall>x y. ((x, y) \<in> r) = (\<exists>u. p x y u = 0)

goal (1 subgoal):
 1. r \<in> ce_rels \<Longrightarrow> \<exists>p\<in>PrimRec3. r = {(x, y). \<exists>u. p x y u = 0}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>p\<in>PrimRec3. \<forall>x y. ((x, y) \<in> r) = (\<exists>u. p x y u = 0)
[PROOF STEP]
obtain p where p_is_pr: "p \<in> PrimRec3" and L1: "\<forall> x y. ((x,y) \<in> r) = (\<exists> u. p x y u = 0)"
[PROOF STATE]
proof (prove)
using this:
\<exists>p\<in>PrimRec3. \<forall>x y. ((x, y) \<in> r) = (\<exists>u. p x y u = 0)

goal (1 subgoal):
 1. (\<And>p. \<lbrakk>p \<in> PrimRec3; \<forall>x y. ((x, y) \<in> r) = (\<exists>u. p x y u = 0)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p \<in> PrimRec3
\<forall>x y. ((x, y) \<in> r) = (\<exists>u. p x y u = 0)

goal (1 subgoal):
 1. r \<in> ce_rels \<Longrightarrow> \<exists>p\<in>PrimRec3. r = {(x, y). \<exists>u. p x y u = 0}
[PROOF STEP]
from p_is_pr L1
[PROOF STATE]
proof (chain)
picking this:
p \<in> PrimRec3
\<forall>x y. ((x, y) \<in> r) = (\<exists>u. p x y u = 0)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
p \<in> PrimRec3
\<forall>x y. ((x, y) \<in> r) = (\<exists>u. p x y u = 0)

goal (1 subgoal):
 1. \<exists>p\<in>PrimRec3. r = {(x, y). \<exists>u. p x y u = 0}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>p\<in>PrimRec3. r = {(x, y). \<exists>u. p x y u = 0}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ce_rel_lm_23: "\<lbrakk> p \<in> PrimRec3; \<forall> x y. ((x,y) \<in> r) = (\<exists> u. p x y u = 0) \<rbrakk> \<Longrightarrow> r \<in> ce_rels"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> PrimRec3; \<forall>x y. ((x, y) \<in> r) = (\<exists>u. p x y u = 0)\<rbrakk> \<Longrightarrow> r \<in> ce_rels
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>p \<in> PrimRec3; \<forall>x y. ((x, y) \<in> r) = (\<exists>u. p x y u = 0)\<rbrakk> \<Longrightarrow> r \<in> ce_rels
[PROOF STEP]
assume p_is_pr: "p \<in> PrimRec3"
[PROOF STATE]
proof (state)
this:
p \<in> PrimRec3

goal (1 subgoal):
 1. \<lbrakk>p \<in> PrimRec3; \<forall>x y. ((x, y) \<in> r) = (\<exists>u. p x y u = 0)\<rbrakk> \<Longrightarrow> r \<in> ce_rels
[PROOF STEP]
assume A: "\<forall> x y. ((x,y) \<in> r) = (\<exists> u. p x y u = 0)"
[PROOF STATE]
proof (state)
this:
\<forall>x y. ((x, y) \<in> r) = (\<exists>u. p x y u = 0)

goal (1 subgoal):
 1. \<lbrakk>p \<in> PrimRec3; \<forall>x y. ((x, y) \<in> r) = (\<exists>u. p x y u = 0)\<rbrakk> \<Longrightarrow> r \<in> ce_rels
[PROOF STEP]
define q where "q z u = p (c_fst z) (c_snd z) u" for z u
[PROOF STATE]
proof (state)
this:
q ?z ?u = p (c_fst ?z) (c_snd ?z) ?u

goal (1 subgoal):
 1. \<lbrakk>p \<in> PrimRec3; \<forall>x y. ((x, y) \<in> r) = (\<exists>u. p x y u = 0)\<rbrakk> \<Longrightarrow> r \<in> ce_rels
[PROOF STEP]
from p_is_pr
[PROOF STATE]
proof (chain)
picking this:
p \<in> PrimRec3
[PROOF STEP]
have q_is_pr: "q \<in> PrimRec2"
[PROOF STATE]
proof (prove)
using this:
p \<in> PrimRec3

goal (1 subgoal):
 1. q \<in> PrimRec2
[PROOF STEP]
unfolding q_def
[PROOF STATE]
proof (prove)
using this:
p \<in> PrimRec3

goal (1 subgoal):
 1. (\<lambda>z. p (c_fst z) (c_snd z)) \<in> PrimRec2
[PROOF STEP]
by prec
[PROOF STATE]
proof (state)
this:
q \<in> PrimRec2

goal (1 subgoal):
 1. \<lbrakk>p \<in> PrimRec3; \<forall>x y. ((x, y) \<in> r) = (\<exists>u. p x y u = 0)\<rbrakk> \<Longrightarrow> r \<in> ce_rels
[PROOF STEP]
define A where "A = { x. \<exists> y. q x y = 0}"
[PROOF STATE]
proof (state)
this:
A = {x. \<exists>y. q x y = 0}

goal (1 subgoal):
 1. \<lbrakk>p \<in> PrimRec3; \<forall>x y. ((x, y) \<in> r) = (\<exists>u. p x y u = 0)\<rbrakk> \<Longrightarrow> r \<in> ce_rels
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
A = {x. \<exists>y. q x y = 0}
[PROOF STEP]
have A_def1: "A = fn_to_set q"
[PROOF STATE]
proof (prove)
using this:
A = {x. \<exists>y. q x y = 0}

goal (1 subgoal):
 1. A = fn_to_set q
[PROOF STEP]
by (unfold fn_to_set_def, auto)
[PROOF STATE]
proof (state)
this:
A = fn_to_set q

goal (1 subgoal):
 1. \<lbrakk>p \<in> PrimRec3; \<forall>x y. ((x, y) \<in> r) = (\<exists>u. p x y u = 0)\<rbrakk> \<Longrightarrow> r \<in> ce_rels
[PROOF STEP]
from q_is_pr A_def1
[PROOF STATE]
proof (chain)
picking this:
q \<in> PrimRec2
A = fn_to_set q
[PROOF STEP]
have A_ce: "A \<in> ce_sets"
[PROOF STATE]
proof (prove)
using this:
q \<in> PrimRec2
A = fn_to_set q

goal (1 subgoal):
 1. A \<in> ce_sets
[PROOF STEP]
by (simp add: ce_set_lm_1)
[PROOF STATE]
proof (state)
this:
A \<in> ce_sets

goal (1 subgoal):
 1. \<lbrakk>p \<in> PrimRec3; \<forall>x y. ((x, y) \<in> r) = (\<exists>u. p x y u = 0)\<rbrakk> \<Longrightarrow> r \<in> ce_rels
[PROOF STEP]
have main: "A = ce_rel_to_set r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A = ce_rel_to_set r
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. A \<subseteq> ce_rel_to_set r
 2. ce_rel_to_set r \<subseteq> A
[PROOF STEP]
show "A \<subseteq> ce_rel_to_set r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<subseteq> ce_rel_to_set r
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> A \<Longrightarrow> x \<in> ce_rel_to_set r
[PROOF STEP]
fix z
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> A \<Longrightarrow> x \<in> ce_rel_to_set r
[PROOF STEP]
assume z_in_A: "z \<in> A"
[PROOF STATE]
proof (state)
this:
z \<in> A

goal (1 subgoal):
 1. \<And>x. x \<in> A \<Longrightarrow> x \<in> ce_rel_to_set r
[PROOF STEP]
show "z \<in> ce_rel_to_set r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. z \<in> ce_rel_to_set r
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. z \<in> ce_rel_to_set r
[PROOF STEP]
define x where "x = c_fst z"
[PROOF STATE]
proof (state)
this:
x = c_fst z

goal (1 subgoal):
 1. z \<in> ce_rel_to_set r
[PROOF STEP]
define y where "y = c_snd z"
[PROOF STATE]
proof (state)
this:
y = c_snd z

goal (1 subgoal):
 1. z \<in> ce_rel_to_set r
[PROOF STEP]
from z_in_A A_def
[PROOF STATE]
proof (chain)
picking this:
z \<in> A
A = {x. \<exists>y. q x y = 0}
[PROOF STEP]
obtain u where L2: "q z u = 0"
[PROOF STATE]
proof (prove)
using this:
z \<in> A
A = {x. \<exists>y. q x y = 0}

goal (1 subgoal):
 1. (\<And>u. q z u = 0 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
q z u = 0

goal (1 subgoal):
 1. z \<in> ce_rel_to_set r
[PROOF STEP]
with x_def y_def q_def
[PROOF STATE]
proof (chain)
picking this:
x = c_fst z
y = c_snd z
q ?z ?u = p (c_fst ?z) (c_snd ?z) ?u
q z u = 0
[PROOF STEP]
have L3: "p x y u = 0"
[PROOF STATE]
proof (prove)
using this:
x = c_fst z
y = c_snd z
q ?z ?u = p (c_fst ?z) (c_snd ?z) ?u
q z u = 0

goal (1 subgoal):
 1. p x y u = 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
p x y u = 0

goal (1 subgoal):
 1. z \<in> ce_rel_to_set r
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p x y u = 0
[PROOF STEP]
have "\<exists>u. p x y u = 0"
[PROOF STATE]
proof (prove)
using this:
p x y u = 0

goal (1 subgoal):
 1. \<exists>u. p x y u = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>u. p x y u = 0

goal (1 subgoal):
 1. z \<in> ce_rel_to_set r
[PROOF STEP]
with A
[PROOF STATE]
proof (chain)
picking this:
\<forall>x y. ((x, y) \<in> r) = (\<exists>u. p x y u = 0)
\<exists>u. p x y u = 0
[PROOF STEP]
have "(x,y) \<in> r"
[PROOF STATE]
proof (prove)
using this:
\<forall>x y. ((x, y) \<in> r) = (\<exists>u. p x y u = 0)
\<exists>u. p x y u = 0

goal (1 subgoal):
 1. (x, y) \<in> r
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(x, y) \<in> r

goal (1 subgoal):
 1. z \<in> ce_rel_to_set r
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(x, y) \<in> r
[PROOF STEP]
have "c_pair x y \<in> ce_rel_to_set r"
[PROOF STATE]
proof (prove)
using this:
(x, y) \<in> r

goal (1 subgoal):
 1. c_pair x y \<in> ce_rel_to_set r
[PROOF STEP]
by (rule ce_rel_lm_9)
[PROOF STATE]
proof (state)
this:
c_pair x y \<in> ce_rel_to_set r

goal (1 subgoal):
 1. z \<in> ce_rel_to_set r
[PROOF STEP]
with x_def y_def
[PROOF STATE]
proof (chain)
picking this:
x = c_fst z
y = c_snd z
c_pair x y \<in> ce_rel_to_set r
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x = c_fst z
y = c_snd z
c_pair x y \<in> ce_rel_to_set r

goal (1 subgoal):
 1. z \<in> ce_rel_to_set r
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
z \<in> ce_rel_to_set r

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
z \<in> ce_rel_to_set r

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
A \<subseteq> ce_rel_to_set r

goal (1 subgoal):
 1. ce_rel_to_set r \<subseteq> A
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ce_rel_to_set r \<subseteq> A
[PROOF STEP]
show "ce_rel_to_set r \<subseteq> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ce_rel_to_set r \<subseteq> A
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> ce_rel_to_set r \<Longrightarrow> x \<in> A
[PROOF STEP]
fix z
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> ce_rel_to_set r \<Longrightarrow> x \<in> A
[PROOF STEP]
assume z_in_r: "z \<in> ce_rel_to_set r"
[PROOF STATE]
proof (state)
this:
z \<in> ce_rel_to_set r

goal (1 subgoal):
 1. \<And>x. x \<in> ce_rel_to_set r \<Longrightarrow> x \<in> A
[PROOF STEP]
show "z \<in> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. z \<in> A
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. z \<in> A
[PROOF STEP]
define x where "x = c_fst z"
[PROOF STATE]
proof (state)
this:
x = c_fst z

goal (1 subgoal):
 1. z \<in> A
[PROOF STEP]
define y where "y = c_snd z"
[PROOF STATE]
proof (state)
this:
y = c_snd z

goal (1 subgoal):
 1. z \<in> A
[PROOF STEP]
from z_in_r
[PROOF STATE]
proof (chain)
picking this:
z \<in> ce_rel_to_set r
[PROOF STEP]
have "(c_fst z, c_snd z) \<in> r"
[PROOF STATE]
proof (prove)
using this:
z \<in> ce_rel_to_set r

goal (1 subgoal):
 1. (c_fst z, c_snd z) \<in> r
[PROOF STEP]
by (rule ce_rel_lm_16)
[PROOF STATE]
proof (state)
this:
(c_fst z, c_snd z) \<in> r

goal (1 subgoal):
 1. z \<in> A
[PROOF STEP]
with x_def y_def
[PROOF STATE]
proof (chain)
picking this:
x = c_fst z
y = c_snd z
(c_fst z, c_snd z) \<in> r
[PROOF STEP]
have "(x,y) \<in> r"
[PROOF STATE]
proof (prove)
using this:
x = c_fst z
y = c_snd z
(c_fst z, c_snd z) \<in> r

goal (1 subgoal):
 1. (x, y) \<in> r
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(x, y) \<in> r

goal (1 subgoal):
 1. z \<in> A
[PROOF STEP]
with A
[PROOF STATE]
proof (chain)
picking this:
\<forall>x y. ((x, y) \<in> r) = (\<exists>u. p x y u = 0)
(x, y) \<in> r
[PROOF STEP]
obtain u where L1: "p x y u = 0"
[PROOF STATE]
proof (prove)
using this:
\<forall>x y. ((x, y) \<in> r) = (\<exists>u. p x y u = 0)
(x, y) \<in> r

goal (1 subgoal):
 1. (\<And>u. p x y u = 0 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p x y u = 0

goal (1 subgoal):
 1. z \<in> A
[PROOF STEP]
with x_def y_def q_def
[PROOF STATE]
proof (chain)
picking this:
x = c_fst z
y = c_snd z
q ?z ?u = p (c_fst ?z) (c_snd ?z) ?u
p x y u = 0
[PROOF STEP]
have "q z u = 0"
[PROOF STATE]
proof (prove)
using this:
x = c_fst z
y = c_snd z
q ?z ?u = p (c_fst ?z) (c_snd ?z) ?u
p x y u = 0

goal (1 subgoal):
 1. q z u = 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
q z u = 0

goal (1 subgoal):
 1. z \<in> A
[PROOF STEP]
with A_def
[PROOF STATE]
proof (chain)
picking this:
A = {x. \<exists>y. q x y = 0}
q z u = 0
[PROOF STEP]
show "z \<in> A"
[PROOF STATE]
proof (prove)
using this:
A = {x. \<exists>y. q x y = 0}
q z u = 0

goal (1 subgoal):
 1. z \<in> A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
z \<in> A

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
z \<in> A

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
ce_rel_to_set r \<subseteq> A

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
A = ce_rel_to_set r

goal (1 subgoal):
 1. \<lbrakk>p \<in> PrimRec3; \<forall>x y. ((x, y) \<in> r) = (\<exists>u. p x y u = 0)\<rbrakk> \<Longrightarrow> r \<in> ce_rels
[PROOF STEP]
with A_ce
[PROOF STATE]
proof (chain)
picking this:
A \<in> ce_sets
A = ce_rel_to_set r
[PROOF STEP]
have "ce_rel_to_set r \<in> ce_sets"
[PROOF STATE]
proof (prove)
using this:
A \<in> ce_sets
A = ce_rel_to_set r

goal (1 subgoal):
 1. ce_rel_to_set r \<in> ce_sets
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ce_rel_to_set r \<in> ce_sets

goal (1 subgoal):
 1. \<lbrakk>p \<in> PrimRec3; \<forall>x y. ((x, y) \<in> r) = (\<exists>u. p x y u = 0)\<rbrakk> \<Longrightarrow> r \<in> ce_rels
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ce_rel_to_set r \<in> ce_sets
[PROOF STEP]
show "r \<in> ce_rels"
[PROOF STATE]
proof (prove)
using this:
ce_rel_to_set r \<in> ce_sets

goal (1 subgoal):
 1. r \<in> ce_rels
[PROOF STEP]
by (rule ce_rel_lm_7)
[PROOF STATE]
proof (state)
this:
r \<in> ce_rels

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ce_rel_lm_24: "\<lbrakk> r \<in> ce_rels; s \<in> ce_rels \<rbrakk> \<Longrightarrow> s O r \<in> ce_rels"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>r \<in> ce_rels; s \<in> ce_rels\<rbrakk> \<Longrightarrow> s O r \<in> ce_rels
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>r \<in> ce_rels; s \<in> ce_rels\<rbrakk> \<Longrightarrow> s O r \<in> ce_rels
[PROOF STEP]
assume r_ce: "r \<in> ce_rels"
[PROOF STATE]
proof (state)
this:
r \<in> ce_rels

goal (1 subgoal):
 1. \<lbrakk>r \<in> ce_rels; s \<in> ce_rels\<rbrakk> \<Longrightarrow> s O r \<in> ce_rels
[PROOF STEP]
assume s_ce: "s \<in> ce_rels"
[PROOF STATE]
proof (state)
this:
s \<in> ce_rels

goal (1 subgoal):
 1. \<lbrakk>r \<in> ce_rels; s \<in> ce_rels\<rbrakk> \<Longrightarrow> s O r \<in> ce_rels
[PROOF STEP]
from r_ce
[PROOF STATE]
proof (chain)
picking this:
r \<in> ce_rels
[PROOF STEP]
have "\<exists> p \<in> PrimRec3. \<forall> x y. ((x,y) \<in> r)=(\<exists> u. p x y u = 0)"
[PROOF STATE]
proof (prove)
using this:
r \<in> ce_rels

goal (1 subgoal):
 1. \<exists>p\<in>PrimRec3. \<forall>x y. ((x, y) \<in> r) = (\<exists>u. p x y u = 0)
[PROOF STEP]
by (rule ce_rel_lm_21)
[PROOF STATE]
proof (state)
this:
\<exists>p\<in>PrimRec3. \<forall>x y. ((x, y) \<in> r) = (\<exists>u. p x y u = 0)

goal (1 subgoal):
 1. \<lbrakk>r \<in> ce_rels; s \<in> ce_rels\<rbrakk> \<Longrightarrow> s O r \<in> ce_rels
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>p\<in>PrimRec3. \<forall>x y. ((x, y) \<in> r) = (\<exists>u. p x y u = 0)
[PROOF STEP]
obtain p_r where p_r_is_pr: "p_r \<in> PrimRec3" and R1: "\<forall> x y. ((x,y) \<in> r)=(\<exists> u. p_r x y u = 0)"
[PROOF STATE]
proof (prove)
using this:
\<exists>p\<in>PrimRec3. \<forall>x y. ((x, y) \<in> r) = (\<exists>u. p x y u = 0)

goal (1 subgoal):
 1. (\<And>p_r. \<lbrakk>p_r \<in> PrimRec3; \<forall>x y. ((x, y) \<in> r) = (\<exists>u. p_r x y u = 0)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p_r \<in> PrimRec3
\<forall>x y. ((x, y) \<in> r) = (\<exists>u. p_r x y u = 0)

goal (1 subgoal):
 1. \<lbrakk>r \<in> ce_rels; s \<in> ce_rels\<rbrakk> \<Longrightarrow> s O r \<in> ce_rels
[PROOF STEP]
from s_ce
[PROOF STATE]
proof (chain)
picking this:
s \<in> ce_rels
[PROOF STEP]
have "\<exists> p \<in> PrimRec3. \<forall> x y. ((x,y) \<in> s)=(\<exists> u. p x y u = 0)"
[PROOF STATE]
proof (prove)
using this:
s \<in> ce_rels

goal (1 subgoal):
 1. \<exists>p\<in>PrimRec3. \<forall>x y. ((x, y) \<in> s) = (\<exists>u. p x y u = 0)
[PROOF STEP]
by (rule ce_rel_lm_21)
[PROOF STATE]
proof (state)
this:
\<exists>p\<in>PrimRec3. \<forall>x y. ((x, y) \<in> s) = (\<exists>u. p x y u = 0)

goal (1 subgoal):
 1. \<lbrakk>r \<in> ce_rels; s \<in> ce_rels\<rbrakk> \<Longrightarrow> s O r \<in> ce_rels
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>p\<in>PrimRec3. \<forall>x y. ((x, y) \<in> s) = (\<exists>u. p x y u = 0)
[PROOF STEP]
obtain p_s where p_s_is_pr: "p_s \<in> PrimRec3" and S1: "\<forall> x y. ((x,y) \<in> s)=(\<exists> u. p_s x y u = 0)"
[PROOF STATE]
proof (prove)
using this:
\<exists>p\<in>PrimRec3. \<forall>x y. ((x, y) \<in> s) = (\<exists>u. p x y u = 0)

goal (1 subgoal):
 1. (\<And>p_s. \<lbrakk>p_s \<in> PrimRec3; \<forall>x y. ((x, y) \<in> s) = (\<exists>u. p_s x y u = 0)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p_s \<in> PrimRec3
\<forall>x y. ((x, y) \<in> s) = (\<exists>u. p_s x y u = 0)

goal (1 subgoal):
 1. \<lbrakk>r \<in> ce_rels; s \<in> ce_rels\<rbrakk> \<Longrightarrow> s O r \<in> ce_rels
[PROOF STEP]
define p where "p x z u = (p_s x (c_fst u) (c_fst (c_snd u))) + (p_r (c_fst u) z (c_snd (c_snd u)))"
    for x z u
[PROOF STATE]
proof (state)
this:
p ?x ?z ?u = p_s ?x (c_fst ?u) (c_fst (c_snd ?u)) + p_r (c_fst ?u) ?z (c_snd (c_snd ?u))

goal (1 subgoal):
 1. \<lbrakk>r \<in> ce_rels; s \<in> ce_rels\<rbrakk> \<Longrightarrow> s O r \<in> ce_rels
[PROOF STEP]
from p_r_is_pr p_s_is_pr
[PROOF STATE]
proof (chain)
picking this:
p_r \<in> PrimRec3
p_s \<in> PrimRec3
[PROOF STEP]
have p_is_pr: "p \<in> PrimRec3"
[PROOF STATE]
proof (prove)
using this:
p_r \<in> PrimRec3
p_s \<in> PrimRec3

goal (1 subgoal):
 1. p \<in> PrimRec3
[PROOF STEP]
unfolding p_def
[PROOF STATE]
proof (prove)
using this:
p_r \<in> PrimRec3
p_s \<in> PrimRec3

goal (1 subgoal):
 1. (\<lambda>x z u. p_s x (c_fst u) (c_fst (c_snd u)) + p_r (c_fst u) z (c_snd (c_snd u))) \<in> PrimRec3
[PROOF STEP]
by prec
[PROOF STATE]
proof (state)
this:
p \<in> PrimRec3

goal (1 subgoal):
 1. \<lbrakk>r \<in> ce_rels; s \<in> ce_rels\<rbrakk> \<Longrightarrow> s O r \<in> ce_rels
[PROOF STEP]
define sr where "sr = s O r"
[PROOF STATE]
proof (state)
this:
sr = s O r

goal (1 subgoal):
 1. \<lbrakk>r \<in> ce_rels; s \<in> ce_rels\<rbrakk> \<Longrightarrow> s O r \<in> ce_rels
[PROOF STEP]
have main: "\<forall> x z. ((x,z) \<in> sr) = (\<exists> u. p x z u = 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x z. ((x, z) \<in> sr) = (\<exists>u. p x z u = 0)
[PROOF STEP]
proof (rule allI, rule allI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x z. ((x, z) \<in> sr) = (\<exists>u. p x z u = 0)
[PROOF STEP]
fix x z
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x z. ((x, z) \<in> sr) = (\<exists>u. p x z u = 0)
[PROOF STEP]
show "((x, z) \<in> sr) = (\<exists>u. p x z u = 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((x, z) \<in> sr) = (\<exists>u. p x z u = 0)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (x, z) \<in> sr \<Longrightarrow> \<exists>u. p x z u = 0
 2. \<exists>u. p x z u = 0 \<Longrightarrow> (x, z) \<in> sr
[PROOF STEP]
assume A: "(x, z) \<in> sr"
[PROOF STATE]
proof (state)
this:
(x, z) \<in> sr

goal (2 subgoals):
 1. (x, z) \<in> sr \<Longrightarrow> \<exists>u. p x z u = 0
 2. \<exists>u. p x z u = 0 \<Longrightarrow> (x, z) \<in> sr
[PROOF STEP]
show "\<exists>u. p x z u = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>u. p x z u = 0
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>u. p x z u = 0
[PROOF STEP]
from A sr_def
[PROOF STATE]
proof (chain)
picking this:
(x, z) \<in> sr
sr = s O r
[PROOF STEP]
obtain y where L1: "(x,y) \<in> s" and L2: "(y,z) \<in> r"
[PROOF STATE]
proof (prove)
using this:
(x, z) \<in> sr
sr = s O r

goal (1 subgoal):
 1. (\<And>y. \<lbrakk>(x, y) \<in> s; (y, z) \<in> r\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(x, y) \<in> s
(y, z) \<in> r

goal (1 subgoal):
 1. \<exists>u. p x z u = 0
[PROOF STEP]
from L1 S1
[PROOF STATE]
proof (chain)
picking this:
(x, y) \<in> s
\<forall>x y. ((x, y) \<in> s) = (\<exists>u. p_s x y u = 0)
[PROOF STEP]
obtain u_s where L3: "p_s x y u_s = 0"
[PROOF STATE]
proof (prove)
using this:
(x, y) \<in> s
\<forall>x y. ((x, y) \<in> s) = (\<exists>u. p_s x y u = 0)

goal (1 subgoal):
 1. (\<And>u_s. p_s x y u_s = 0 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p_s x y u_s = 0

goal (1 subgoal):
 1. \<exists>u. p x z u = 0
[PROOF STEP]
from L2 R1
[PROOF STATE]
proof (chain)
picking this:
(y, z) \<in> r
\<forall>x y. ((x, y) \<in> r) = (\<exists>u. p_r x y u = 0)
[PROOF STEP]
obtain u_r where L4: "p_r y z u_r = 0"
[PROOF STATE]
proof (prove)
using this:
(y, z) \<in> r
\<forall>x y. ((x, y) \<in> r) = (\<exists>u. p_r x y u = 0)

goal (1 subgoal):
 1. (\<And>u_r. p_r y z u_r = 0 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p_r y z u_r = 0

goal (1 subgoal):
 1. \<exists>u. p x z u = 0
[PROOF STEP]
define u where "u = c_pair y (c_pair u_s u_r)"
[PROOF STATE]
proof (state)
this:
u = c_pair y (c_pair u_s u_r)

goal (1 subgoal):
 1. \<exists>u. p x z u = 0
[PROOF STEP]
from L3 L4
[PROOF STATE]
proof (chain)
picking this:
p_s x y u_s = 0
p_r y z u_r = 0
[PROOF STEP]
have "p x z u = 0"
[PROOF STATE]
proof (prove)
using this:
p_s x y u_s = 0
p_r y z u_r = 0

goal (1 subgoal):
 1. p x z u = 0
[PROOF STEP]
by (unfold p_def, unfold u_def, simp)
[PROOF STATE]
proof (state)
this:
p x z u = 0

goal (1 subgoal):
 1. \<exists>u. p x z u = 0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p x z u = 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
p x z u = 0

goal (1 subgoal):
 1. \<exists>u. p x z u = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>u. p x z u = 0

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>u. p x z u = 0

goal (1 subgoal):
 1. \<exists>u. p x z u = 0 \<Longrightarrow> (x, z) \<in> sr
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>u. p x z u = 0 \<Longrightarrow> (x, z) \<in> sr
[PROOF STEP]
assume A: "\<exists>u. p x z u = 0"
[PROOF STATE]
proof (state)
this:
\<exists>u. p x z u = 0

goal (1 subgoal):
 1. \<exists>u. p x z u = 0 \<Longrightarrow> (x, z) \<in> sr
[PROOF STEP]
show "(x, z) \<in> sr"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x, z) \<in> sr
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (x, z) \<in> sr
[PROOF STEP]
from A
[PROOF STATE]
proof (chain)
picking this:
\<exists>u. p x z u = 0
[PROOF STEP]
obtain u where L1: "p x z u = 0"
[PROOF STATE]
proof (prove)
using this:
\<exists>u. p x z u = 0

goal (1 subgoal):
 1. (\<And>u. p x z u = 0 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p x z u = 0

goal (1 subgoal):
 1. (x, z) \<in> sr
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p x z u = 0
[PROOF STEP]
have L2: "(p_s x (c_fst u) (c_fst (c_snd u))) + (p_r (c_fst u) z (c_snd (c_snd u))) = 0"
[PROOF STATE]
proof (prove)
using this:
p x z u = 0

goal (1 subgoal):
 1. p_s x (c_fst u) (c_fst (c_snd u)) + p_r (c_fst u) z (c_snd (c_snd u)) = 0
[PROOF STEP]
by (unfold p_def)
[PROOF STATE]
proof (state)
this:
p_s x (c_fst u) (c_fst (c_snd u)) + p_r (c_fst u) z (c_snd (c_snd u)) = 0

goal (1 subgoal):
 1. (x, z) \<in> sr
[PROOF STEP]
from L2
[PROOF STATE]
proof (chain)
picking this:
p_s x (c_fst u) (c_fst (c_snd u)) + p_r (c_fst u) z (c_snd (c_snd u)) = 0
[PROOF STEP]
have L3: "p_s x (c_fst u) (c_fst (c_snd u)) = 0"
[PROOF STATE]
proof (prove)
using this:
p_s x (c_fst u) (c_fst (c_snd u)) + p_r (c_fst u) z (c_snd (c_snd u)) = 0

goal (1 subgoal):
 1. p_s x (c_fst u) (c_fst (c_snd u)) = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p_s x (c_fst u) (c_fst (c_snd u)) = 0

goal (1 subgoal):
 1. (x, z) \<in> sr
[PROOF STEP]
from L2
[PROOF STATE]
proof (chain)
picking this:
p_s x (c_fst u) (c_fst (c_snd u)) + p_r (c_fst u) z (c_snd (c_snd u)) = 0
[PROOF STEP]
have L4: "p_r (c_fst u) z (c_snd (c_snd u)) = 0"
[PROOF STATE]
proof (prove)
using this:
p_s x (c_fst u) (c_fst (c_snd u)) + p_r (c_fst u) z (c_snd (c_snd u)) = 0

goal (1 subgoal):
 1. p_r (c_fst u) z (c_snd (c_snd u)) = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p_r (c_fst u) z (c_snd (c_snd u)) = 0

goal (1 subgoal):
 1. (x, z) \<in> sr
[PROOF STEP]
from L3 S1
[PROOF STATE]
proof (chain)
picking this:
p_s x (c_fst u) (c_fst (c_snd u)) = 0
\<forall>x y. ((x, y) \<in> s) = (\<exists>u. p_s x y u = 0)
[PROOF STEP]
have L5: "(x,(c_fst u)) \<in> s"
[PROOF STATE]
proof (prove)
using this:
p_s x (c_fst u) (c_fst (c_snd u)) = 0
\<forall>x y. ((x, y) \<in> s) = (\<exists>u. p_s x y u = 0)

goal (1 subgoal):
 1. (x, c_fst u) \<in> s
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(x, c_fst u) \<in> s

goal (1 subgoal):
 1. (x, z) \<in> sr
[PROOF STEP]
from L4 R1
[PROOF STATE]
proof (chain)
picking this:
p_r (c_fst u) z (c_snd (c_snd u)) = 0
\<forall>x y. ((x, y) \<in> r) = (\<exists>u. p_r x y u = 0)
[PROOF STEP]
have L6: "((c_fst u),z) \<in> r"
[PROOF STATE]
proof (prove)
using this:
p_r (c_fst u) z (c_snd (c_snd u)) = 0
\<forall>x y. ((x, y) \<in> r) = (\<exists>u. p_r x y u = 0)

goal (1 subgoal):
 1. (c_fst u, z) \<in> r
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(c_fst u, z) \<in> r

goal (1 subgoal):
 1. (x, z) \<in> sr
[PROOF STEP]
from L5 L6
[PROOF STATE]
proof (chain)
picking this:
(x, c_fst u) \<in> s
(c_fst u, z) \<in> r
[PROOF STEP]
have "(x,z) \<in> s O r"
[PROOF STATE]
proof (prove)
using this:
(x, c_fst u) \<in> s
(c_fst u, z) \<in> r

goal (1 subgoal):
 1. (x, z) \<in> s O r
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(x, z) \<in> s O r

goal (1 subgoal):
 1. (x, z) \<in> sr
[PROOF STEP]
with sr_def
[PROOF STATE]
proof (chain)
picking this:
sr = s O r
(x, z) \<in> s O r
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
sr = s O r
(x, z) \<in> s O r

goal (1 subgoal):
 1. (x, z) \<in> sr
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(x, z) \<in> sr

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(x, z) \<in> sr

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
((x, z) \<in> sr) = (\<exists>u. p x z u = 0)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>x z. ((x, z) \<in> sr) = (\<exists>u. p x z u = 0)

goal (1 subgoal):
 1. \<lbrakk>r \<in> ce_rels; s \<in> ce_rels\<rbrakk> \<Longrightarrow> s O r \<in> ce_rels
[PROOF STEP]
from p_is_pr main
[PROOF STATE]
proof (chain)
picking this:
p \<in> PrimRec3
\<forall>x z. ((x, z) \<in> sr) = (\<exists>u. p x z u = 0)
[PROOF STEP]
have "sr \<in> ce_rels"
[PROOF STATE]
proof (prove)
using this:
p \<in> PrimRec3
\<forall>x z. ((x, z) \<in> sr) = (\<exists>u. p x z u = 0)

goal (1 subgoal):
 1. sr \<in> ce_rels
[PROOF STEP]
by (rule ce_rel_lm_23)
[PROOF STATE]
proof (state)
this:
sr \<in> ce_rels

goal (1 subgoal):
 1. \<lbrakk>r \<in> ce_rels; s \<in> ce_rels\<rbrakk> \<Longrightarrow> s O r \<in> ce_rels
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
sr \<in> ce_rels
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
sr \<in> ce_rels

goal (1 subgoal):
 1. s O r \<in> ce_rels
[PROOF STEP]
by (unfold sr_def)
[PROOF STATE]
proof (state)
this:
s O r \<in> ce_rels

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ce_rel_lm_25: "r \<in> ce_rels \<Longrightarrow> r^-1 \<in> ce_rels"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r \<in> ce_rels \<Longrightarrow> r\<inverse> \<in> ce_rels
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. r \<in> ce_rels \<Longrightarrow> r\<inverse> \<in> ce_rels
[PROOF STEP]
assume r_ce: "r \<in> ce_rels"
[PROOF STATE]
proof (state)
this:
r \<in> ce_rels

goal (1 subgoal):
 1. r \<in> ce_rels \<Longrightarrow> r\<inverse> \<in> ce_rels
[PROOF STEP]
have "r^-1 = {(y,x). (x,y) \<in> r}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r\<inverse> = {(y, x). (x, y) \<in> r}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
r\<inverse> = {(y, x). (x, y) \<in> r}

goal (1 subgoal):
 1. r \<in> ce_rels \<Longrightarrow> r\<inverse> \<in> ce_rels
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
r\<inverse> = {(y, x). (x, y) \<in> r}
[PROOF STEP]
have L1: "\<forall> x y. ((x,y) \<in> r) = ((y,x) \<in> r^-1)"
[PROOF STATE]
proof (prove)
using this:
r\<inverse> = {(y, x). (x, y) \<in> r}

goal (1 subgoal):
 1. \<forall>x y. ((x, y) \<in> r) = ((y, x) \<in> r\<inverse>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>x y. ((x, y) \<in> r) = ((y, x) \<in> r\<inverse>)

goal (1 subgoal):
 1. r \<in> ce_rels \<Longrightarrow> r\<inverse> \<in> ce_rels
[PROOF STEP]
from r_ce
[PROOF STATE]
proof (chain)
picking this:
r \<in> ce_rels
[PROOF STEP]
have "\<exists> p \<in> PrimRec3. \<forall> x y. ((x,y) \<in> r) = (\<exists> u. p x y u = 0)"
[PROOF STATE]
proof (prove)
using this:
r \<in> ce_rels

goal (1 subgoal):
 1. \<exists>p\<in>PrimRec3. \<forall>x y. ((x, y) \<in> r) = (\<exists>u. p x y u = 0)
[PROOF STEP]
by (rule ce_rel_lm_21)
[PROOF STATE]
proof (state)
this:
\<exists>p\<in>PrimRec3. \<forall>x y. ((x, y) \<in> r) = (\<exists>u. p x y u = 0)

goal (1 subgoal):
 1. r \<in> ce_rels \<Longrightarrow> r\<inverse> \<in> ce_rels
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>p\<in>PrimRec3. \<forall>x y. ((x, y) \<in> r) = (\<exists>u. p x y u = 0)
[PROOF STEP]
obtain p where p_is_pr: "p \<in> PrimRec3" and R1: "\<forall> x y. ((x,y) \<in> r) = (\<exists> u. p x y u = 0)"
[PROOF STATE]
proof (prove)
using this:
\<exists>p\<in>PrimRec3. \<forall>x y. ((x, y) \<in> r) = (\<exists>u. p x y u = 0)

goal (1 subgoal):
 1. (\<And>p. \<lbrakk>p \<in> PrimRec3; \<forall>x y. ((x, y) \<in> r) = (\<exists>u. p x y u = 0)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p \<in> PrimRec3
\<forall>x y. ((x, y) \<in> r) = (\<exists>u. p x y u = 0)

goal (1 subgoal):
 1. r \<in> ce_rels \<Longrightarrow> r\<inverse> \<in> ce_rels
[PROOF STEP]
define q where "q x y u = p y x u" for x y u
[PROOF STATE]
proof (state)
this:
q ?x ?y ?u = p ?y ?x ?u

goal (1 subgoal):
 1. r \<in> ce_rels \<Longrightarrow> r\<inverse> \<in> ce_rels
[PROOF STEP]
from p_is_pr
[PROOF STATE]
proof (chain)
picking this:
p \<in> PrimRec3
[PROOF STEP]
have q_is_pr: "q \<in> PrimRec3"
[PROOF STATE]
proof (prove)
using this:
p \<in> PrimRec3

goal (1 subgoal):
 1. q \<in> PrimRec3
[PROOF STEP]
unfolding q_def
[PROOF STATE]
proof (prove)
using this:
p \<in> PrimRec3

goal (1 subgoal):
 1. (\<lambda>x y. p y x) \<in> PrimRec3
[PROOF STEP]
by prec
[PROOF STATE]
proof (state)
this:
q \<in> PrimRec3

goal (1 subgoal):
 1. r \<in> ce_rels \<Longrightarrow> r\<inverse> \<in> ce_rels
[PROOF STEP]
from L1 R1
[PROOF STATE]
proof (chain)
picking this:
\<forall>x y. ((x, y) \<in> r) = ((y, x) \<in> r\<inverse>)
\<forall>x y. ((x, y) \<in> r) = (\<exists>u. p x y u = 0)
[PROOF STEP]
have L2: "\<forall> x y. ((x,y) \<in> r^-1) = (\<exists> u. p y x u = 0)"
[PROOF STATE]
proof (prove)
using this:
\<forall>x y. ((x, y) \<in> r) = ((y, x) \<in> r\<inverse>)
\<forall>x y. ((x, y) \<in> r) = (\<exists>u. p x y u = 0)

goal (1 subgoal):
 1. \<forall>x y. ((x, y) \<in> r\<inverse>) = (\<exists>u. p y x u = 0)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>x y. ((x, y) \<in> r\<inverse>) = (\<exists>u. p y x u = 0)

goal (1 subgoal):
 1. r \<in> ce_rels \<Longrightarrow> r\<inverse> \<in> ce_rels
[PROOF STEP]
with q_def
[PROOF STATE]
proof (chain)
picking this:
q ?x ?y ?u = p ?y ?x ?u
\<forall>x y. ((x, y) \<in> r\<inverse>) = (\<exists>u. p y x u = 0)
[PROOF STEP]
have L3: "\<forall> x y. ((x,y) \<in> r^-1) = (\<exists> u. q x y u = 0)"
[PROOF STATE]
proof (prove)
using this:
q ?x ?y ?u = p ?y ?x ?u
\<forall>x y. ((x, y) \<in> r\<inverse>) = (\<exists>u. p y x u = 0)

goal (1 subgoal):
 1. \<forall>x y. ((x, y) \<in> r\<inverse>) = (\<exists>u. q x y u = 0)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>x y. ((x, y) \<in> r\<inverse>) = (\<exists>u. q x y u = 0)

goal (1 subgoal):
 1. r \<in> ce_rels \<Longrightarrow> r\<inverse> \<in> ce_rels
[PROOF STEP]
with q_is_pr
[PROOF STATE]
proof (chain)
picking this:
q \<in> PrimRec3
\<forall>x y. ((x, y) \<in> r\<inverse>) = (\<exists>u. q x y u = 0)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
q \<in> PrimRec3
\<forall>x y. ((x, y) \<in> r\<inverse>) = (\<exists>u. q x y u = 0)

goal (1 subgoal):
 1. r\<inverse> \<in> ce_rels
[PROOF STEP]
by (rule ce_rel_lm_23)
[PROOF STATE]
proof (state)
this:
r\<inverse> \<in> ce_rels

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ce_rel_lm_26: "r \<in> ce_rels \<Longrightarrow> Domain r \<in> ce_sets"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r \<in> ce_rels \<Longrightarrow> Domain r \<in> ce_sets
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. r \<in> ce_rels \<Longrightarrow> Domain r \<in> ce_sets
[PROOF STEP]
assume r_ce: "r \<in> ce_rels"
[PROOF STATE]
proof (state)
this:
r \<in> ce_rels

goal (1 subgoal):
 1. r \<in> ce_rels \<Longrightarrow> Domain r \<in> ce_sets
[PROOF STEP]
have L1: "\<forall> x. (x \<in> Domain r) = (\<exists> y. (x,y) \<in> r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x. (x \<in> Domain r) = (\<exists>y. (x, y) \<in> r)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>x. (x \<in> Domain r) = (\<exists>y. (x, y) \<in> r)

goal (1 subgoal):
 1. r \<in> ce_rels \<Longrightarrow> Domain r \<in> ce_sets
[PROOF STEP]
define A where "A = ce_rel_to_set r"
[PROOF STATE]
proof (state)
this:
A = ce_rel_to_set r

goal (1 subgoal):
 1. r \<in> ce_rels \<Longrightarrow> Domain r \<in> ce_sets
[PROOF STEP]
from r_ce
[PROOF STATE]
proof (chain)
picking this:
r \<in> ce_rels
[PROOF STEP]
have "ce_rel_to_set r \<in> ce_sets"
[PROOF STATE]
proof (prove)
using this:
r \<in> ce_rels

goal (1 subgoal):
 1. ce_rel_to_set r \<in> ce_sets
[PROOF STEP]
by (rule ce_rel_lm_6)
[PROOF STATE]
proof (state)
this:
ce_rel_to_set r \<in> ce_sets

goal (1 subgoal):
 1. r \<in> ce_rels \<Longrightarrow> Domain r \<in> ce_sets
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ce_rel_to_set r \<in> ce_sets
[PROOF STEP]
have A_ce: "A \<in> ce_sets"
[PROOF STATE]
proof (prove)
using this:
ce_rel_to_set r \<in> ce_sets

goal (1 subgoal):
 1. A \<in> ce_sets
[PROOF STEP]
by (unfold A_def)
[PROOF STATE]
proof (state)
this:
A \<in> ce_sets

goal (1 subgoal):
 1. r \<in> ce_rels \<Longrightarrow> Domain r \<in> ce_sets
[PROOF STEP]
have "\<forall> x y. ((x,y) \<in> r) = (c_pair x y \<in> ce_rel_to_set r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x y. ((x, y) \<in> r) = (c_pair x y \<in> ce_rel_to_set r)
[PROOF STEP]
by (simp add: ce_rel_lm_12)
[PROOF STATE]
proof (state)
this:
\<forall>x y. ((x, y) \<in> r) = (c_pair x y \<in> ce_rel_to_set r)

goal (1 subgoal):
 1. r \<in> ce_rels \<Longrightarrow> Domain r \<in> ce_sets
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>x y. ((x, y) \<in> r) = (c_pair x y \<in> ce_rel_to_set r)
[PROOF STEP]
have L2: "\<forall> x y. ((x,y) \<in> r) = (c_pair x y \<in> A)"
[PROOF STATE]
proof (prove)
using this:
\<forall>x y. ((x, y) \<in> r) = (c_pair x y \<in> ce_rel_to_set r)

goal (1 subgoal):
 1. \<forall>x y. ((x, y) \<in> r) = (c_pair x y \<in> A)
[PROOF STEP]
by (unfold A_def)
[PROOF STATE]
proof (state)
this:
\<forall>x y. ((x, y) \<in> r) = (c_pair x y \<in> A)

goal (1 subgoal):
 1. r \<in> ce_rels \<Longrightarrow> Domain r \<in> ce_sets
[PROOF STEP]
from A_ce c_fst_is_pr
[PROOF STATE]
proof (chain)
picking this:
A \<in> ce_sets
c_fst \<in> PrimRec1
[PROOF STEP]
have L3: "{ c_fst z |z.  z \<in> A } \<in> ce_sets"
[PROOF STATE]
proof (prove)
using this:
A \<in> ce_sets
c_fst \<in> PrimRec1

goal (1 subgoal):
 1. {c_fst z |z. z \<in> A} \<in> ce_sets
[PROOF STEP]
by (rule ce_set_lm_7)
[PROOF STATE]
proof (state)
this:
{c_fst z |z. z \<in> A} \<in> ce_sets

goal (1 subgoal):
 1. r \<in> ce_rels \<Longrightarrow> Domain r \<in> ce_sets
[PROOF STEP]
have L4: "\<forall> x. (x \<in> { c_fst z |z.  z \<in> A }) =(\<exists> y. c_pair x y \<in> A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x. (x \<in> {c_fst z |z. z \<in> A}) = (\<exists>y. c_pair x y \<in> A)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. (x \<in> {c_fst z |z. z \<in> A}) = (\<exists>y. c_pair x y \<in> A)
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. (x \<in> {c_fst z |z. z \<in> A}) = (\<exists>y. c_pair x y \<in> A)
[PROOF STEP]
show "(x \<in> { c_fst z |z.  z \<in> A }) =(\<exists> y. c_pair x y \<in> A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<in> {c_fst z |z. z \<in> A}) = (\<exists>y. c_pair x y \<in> A)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x \<in> {c_fst z |z. z \<in> A} \<Longrightarrow> \<exists>y. c_pair x y \<in> A
 2. \<exists>y. c_pair x y \<in> A \<Longrightarrow> x \<in> {c_fst z |z. z \<in> A}
[PROOF STEP]
assume A: "x \<in> {c_fst z |z. z \<in> A}"
[PROOF STATE]
proof (state)
this:
x \<in> {c_fst z |z. z \<in> A}

goal (2 subgoals):
 1. x \<in> {c_fst z |z. z \<in> A} \<Longrightarrow> \<exists>y. c_pair x y \<in> A
 2. \<exists>y. c_pair x y \<in> A \<Longrightarrow> x \<in> {c_fst z |z. z \<in> A}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> {c_fst z |z. z \<in> A}
[PROOF STEP]
obtain z where z_in_A: "z \<in> A" and x_z: "x = c_fst z"
[PROOF STATE]
proof (prove)
using this:
x \<in> {c_fst z |z. z \<in> A}

goal (1 subgoal):
 1. (\<And>z. \<lbrakk>z \<in> A; x = c_fst z\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
z \<in> A
x = c_fst z

goal (2 subgoals):
 1. x \<in> {c_fst z |z. z \<in> A} \<Longrightarrow> \<exists>y. c_pair x y \<in> A
 2. \<exists>y. c_pair x y \<in> A \<Longrightarrow> x \<in> {c_fst z |z. z \<in> A}
[PROOF STEP]
from x_z
[PROOF STATE]
proof (chain)
picking this:
x = c_fst z
[PROOF STEP]
have "z = c_pair x (c_snd z)"
[PROOF STATE]
proof (prove)
using this:
x = c_fst z

goal (1 subgoal):
 1. z = c_pair x (c_snd z)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
z = c_pair x (c_snd z)

goal (2 subgoals):
 1. x \<in> {c_fst z |z. z \<in> A} \<Longrightarrow> \<exists>y. c_pair x y \<in> A
 2. \<exists>y. c_pair x y \<in> A \<Longrightarrow> x \<in> {c_fst z |z. z \<in> A}
[PROOF STEP]
with z_in_A
[PROOF STATE]
proof (chain)
picking this:
z \<in> A
z = c_pair x (c_snd z)
[PROOF STEP]
have "c_pair x (c_snd z) \<in> A"
[PROOF STATE]
proof (prove)
using this:
z \<in> A
z = c_pair x (c_snd z)

goal (1 subgoal):
 1. c_pair x (c_snd z) \<in> A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
c_pair x (c_snd z) \<in> A

goal (2 subgoals):
 1. x \<in> {c_fst z |z. z \<in> A} \<Longrightarrow> \<exists>y. c_pair x y \<in> A
 2. \<exists>y. c_pair x y \<in> A \<Longrightarrow> x \<in> {c_fst z |z. z \<in> A}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
c_pair x (c_snd z) \<in> A
[PROOF STEP]
show "\<exists>y. c_pair x y \<in> A"
[PROOF STATE]
proof (prove)
using this:
c_pair x (c_snd z) \<in> A

goal (1 subgoal):
 1. \<exists>y. c_pair x y \<in> A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>y. c_pair x y \<in> A

goal (1 subgoal):
 1. \<exists>y. c_pair x y \<in> A \<Longrightarrow> x \<in> {c_fst z |z. z \<in> A}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>y. c_pair x y \<in> A \<Longrightarrow> x \<in> {c_fst z |z. z \<in> A}
[PROOF STEP]
assume A: "\<exists>y. c_pair x y \<in> A"
[PROOF STATE]
proof (state)
this:
\<exists>y. c_pair x y \<in> A

goal (1 subgoal):
 1. \<exists>y. c_pair x y \<in> A \<Longrightarrow> x \<in> {c_fst z |z. z \<in> A}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>y. c_pair x y \<in> A
[PROOF STEP]
obtain y where y_1: "c_pair x y \<in> A"
[PROOF STATE]
proof (prove)
using this:
\<exists>y. c_pair x y \<in> A

goal (1 subgoal):
 1. (\<And>y. c_pair x y \<in> A \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
c_pair x y \<in> A

goal (1 subgoal):
 1. \<exists>y. c_pair x y \<in> A \<Longrightarrow> x \<in> {c_fst z |z. z \<in> A}
[PROOF STEP]
define z where "z = c_pair x y"
[PROOF STATE]
proof (state)
this:
z = c_pair x y

goal (1 subgoal):
 1. \<exists>y. c_pair x y \<in> A \<Longrightarrow> x \<in> {c_fst z |z. z \<in> A}
[PROOF STEP]
from y_1
[PROOF STATE]
proof (chain)
picking this:
c_pair x y \<in> A
[PROOF STEP]
have z_in_A: "z \<in> A"
[PROOF STATE]
proof (prove)
using this:
c_pair x y \<in> A

goal (1 subgoal):
 1. z \<in> A
[PROOF STEP]
by (unfold z_def)
[PROOF STATE]
proof (state)
this:
z \<in> A

goal (1 subgoal):
 1. \<exists>y. c_pair x y \<in> A \<Longrightarrow> x \<in> {c_fst z |z. z \<in> A}
[PROOF STEP]
from z_def
[PROOF STATE]
proof (chain)
picking this:
z = c_pair x y
[PROOF STEP]
have x_z: "x = c_fst z"
[PROOF STATE]
proof (prove)
using this:
z = c_pair x y

goal (1 subgoal):
 1. x = c_fst z
[PROOF STEP]
by (unfold z_def, simp)
[PROOF STATE]
proof (state)
this:
x = c_fst z

goal (1 subgoal):
 1. \<exists>y. c_pair x y \<in> A \<Longrightarrow> x \<in> {c_fst z |z. z \<in> A}
[PROOF STEP]
from z_in_A x_z
[PROOF STATE]
proof (chain)
picking this:
z \<in> A
x = c_fst z
[PROOF STEP]
show "x \<in> {c_fst z |z. z \<in> A}"
[PROOF STATE]
proof (prove)
using this:
z \<in> A
x = c_fst z

goal (1 subgoal):
 1. x \<in> {c_fst z |z. z \<in> A}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> {c_fst z |z. z \<in> A}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(x \<in> {c_fst z |z. z \<in> A}) = (\<exists>y. c_pair x y \<in> A)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>x. (x \<in> {c_fst z |z. z \<in> A}) = (\<exists>y. c_pair x y \<in> A)

goal (1 subgoal):
 1. r \<in> ce_rels \<Longrightarrow> Domain r \<in> ce_sets
[PROOF STEP]
from L1 L2
[PROOF STATE]
proof (chain)
picking this:
\<forall>x. (x \<in> Domain r) = (\<exists>y. (x, y) \<in> r)
\<forall>x y. ((x, y) \<in> r) = (c_pair x y \<in> A)
[PROOF STEP]
have L5: "\<forall> x. (x \<in> Domain r) = (\<exists> y. c_pair x y \<in> A)"
[PROOF STATE]
proof (prove)
using this:
\<forall>x. (x \<in> Domain r) = (\<exists>y. (x, y) \<in> r)
\<forall>x y. ((x, y) \<in> r) = (c_pair x y \<in> A)

goal (1 subgoal):
 1. \<forall>x. (x \<in> Domain r) = (\<exists>y. c_pair x y \<in> A)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>x. (x \<in> Domain r) = (\<exists>y. c_pair x y \<in> A)

goal (1 subgoal):
 1. r \<in> ce_rels \<Longrightarrow> Domain r \<in> ce_sets
[PROOF STEP]
from L4 L5
[PROOF STATE]
proof (chain)
picking this:
\<forall>x. (x \<in> {c_fst z |z. z \<in> A}) = (\<exists>y. c_pair x y \<in> A)
\<forall>x. (x \<in> Domain r) = (\<exists>y. c_pair x y \<in> A)
[PROOF STEP]
have L6: "\<forall> x. (x \<in> Domain r) = (x \<in> { c_fst z |z.  z \<in> A })"
[PROOF STATE]
proof (prove)
using this:
\<forall>x. (x \<in> {c_fst z |z. z \<in> A}) = (\<exists>y. c_pair x y \<in> A)
\<forall>x. (x \<in> Domain r) = (\<exists>y. c_pair x y \<in> A)

goal (1 subgoal):
 1. \<forall>x. (x \<in> Domain r) = (x \<in> {c_fst z |z. z \<in> A})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>x. (x \<in> Domain r) = (x \<in> {c_fst z |z. z \<in> A})

goal (1 subgoal):
 1. r \<in> ce_rels \<Longrightarrow> Domain r \<in> ce_sets
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>x. (x \<in> Domain r) = (x \<in> {c_fst z |z. z \<in> A})
[PROOF STEP]
have "Domain r = { c_fst z |z.  z \<in> A }"
[PROOF STATE]
proof (prove)
using this:
\<forall>x. (x \<in> Domain r) = (x \<in> {c_fst z |z. z \<in> A})

goal (1 subgoal):
 1. Domain r = {c_fst z |z. z \<in> A}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Domain r = {c_fst z |z. z \<in> A}

goal (1 subgoal):
 1. r \<in> ce_rels \<Longrightarrow> Domain r \<in> ce_sets
[PROOF STEP]
with L3
[PROOF STATE]
proof (chain)
picking this:
{c_fst z |z. z \<in> A} \<in> ce_sets
Domain r = {c_fst z |z. z \<in> A}
[PROOF STEP]
show "Domain r \<in> ce_sets"
[PROOF STATE]
proof (prove)
using this:
{c_fst z |z. z \<in> A} \<in> ce_sets
Domain r = {c_fst z |z. z \<in> A}

goal (1 subgoal):
 1. Domain r \<in> ce_sets
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Domain r \<in> ce_sets

goal:
No subgoals!
[PROOF STEP]
qed