[STATEMENT]
lemma ce_rel_lm_27: "r \<in> ce_rels \<Longrightarrow> Range r \<in> ce_sets"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r \<in> ce_rels \<Longrightarrow> Range r \<in> ce_sets
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. r \<in> ce_rels \<Longrightarrow> Range 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> Range r \<in> ce_sets
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
r \<in> ce_rels
[PROOF STEP]
have "r^-1 \<in> ce_rels"
[PROOF STATE]
proof (prove)
using this:
r \<in> ce_rels

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

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

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

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

goal (1 subgoal):
 1. Range r \<in> ce_sets
[PROOF STEP]
by (unfold Domain_converse [symmetric])
[PROOF STATE]
proof (state)
this:
Range r \<in> ce_sets

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ce_rel_lm_28: "r \<in> ce_rels \<Longrightarrow> Field r \<in> ce_sets"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r \<in> ce_rels \<Longrightarrow> Field r \<in> ce_sets
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. r \<in> ce_rels \<Longrightarrow> Field 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> Field r \<in> ce_sets
[PROOF STEP]
from r_ce
[PROOF STATE]
proof (chain)
picking this:
r \<in> ce_rels
[PROOF STEP]
have L1: "Domain r \<in> ce_sets"
[PROOF STATE]
proof (prove)
using this:
r \<in> ce_rels

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

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

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

goal (1 subgoal):
 1. r \<in> ce_rels \<Longrightarrow> Field r \<in> ce_sets
[PROOF STEP]
from L1 L2
[PROOF STATE]
proof (chain)
picking this:
Domain r \<in> ce_sets
Range r \<in> ce_sets
[PROOF STEP]
have L3: "Domain r \<union> Range r \<in> ce_sets"
[PROOF STATE]
proof (prove)
using this:
Domain r \<in> ce_sets
Range r \<in> ce_sets

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ce_rel_lm_29: "\<lbrakk> A \<in> ce_sets; B \<in> ce_sets \<rbrakk> \<Longrightarrow> A \<times> B \<in> ce_rels"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A \<in> ce_sets; B \<in> ce_sets\<rbrakk> \<Longrightarrow> A \<times> B \<in> ce_rels
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>A \<in> ce_sets; B \<in> ce_sets\<rbrakk> \<Longrightarrow> A \<times> B \<in> ce_rels
[PROOF STEP]
assume A_ce: "A \<in> ce_sets"
[PROOF STATE]
proof (state)
this:
A \<in> ce_sets

goal (1 subgoal):
 1. \<lbrakk>A \<in> ce_sets; B \<in> ce_sets\<rbrakk> \<Longrightarrow> A \<times> B \<in> ce_rels
[PROOF STEP]
assume B_ce: "B \<in> ce_sets"
[PROOF STATE]
proof (state)
this:
B \<in> ce_sets

goal (1 subgoal):
 1. \<lbrakk>A \<in> ce_sets; B \<in> ce_sets\<rbrakk> \<Longrightarrow> A \<times> B \<in> ce_rels
[PROOF STEP]
define r_a where "r_a = {(x,(0::nat)) | x. x \<in> A}"
[PROOF STATE]
proof (state)
this:
r_a = {(x, 0) |x. x \<in> A}

goal (1 subgoal):
 1. \<lbrakk>A \<in> ce_sets; B \<in> ce_sets\<rbrakk> \<Longrightarrow> A \<times> B \<in> ce_rels
[PROOF STEP]
define r_b where "r_b = {((0::nat),z) | z. z \<in> B}"
[PROOF STATE]
proof (state)
this:
r_b = {(0, z) |z. z \<in> B}

goal (1 subgoal):
 1. \<lbrakk>A \<in> ce_sets; B \<in> ce_sets\<rbrakk> \<Longrightarrow> A \<times> B \<in> ce_rels
[PROOF STEP]
have L1: "r_a O r_b = A \<times> B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r_a O r_b = A \<times> B
[PROOF STEP]
by (unfold r_a_def, unfold r_b_def, auto)
[PROOF STATE]
proof (state)
this:
r_a O r_b = A \<times> B

goal (1 subgoal):
 1. \<lbrakk>A \<in> ce_sets; B \<in> ce_sets\<rbrakk> \<Longrightarrow> A \<times> B \<in> ce_rels
[PROOF STEP]
have r_a_ce: "r_a \<in> ce_rels"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r_a \<in> ce_rels
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. r_a \<in> ce_rels
[PROOF STEP]
have loc1: "ce_rel_to_set r_a = { c_pair x 0 | x. x \<in> A}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ce_rel_to_set r_a = {c_pair x 0 |x. x \<in> A}
[PROOF STEP]
by (unfold r_a_def, unfold ce_rel_to_set_def, auto)
[PROOF STATE]
proof (state)
this:
ce_rel_to_set r_a = {c_pair x 0 |x. x \<in> A}

goal (1 subgoal):
 1. r_a \<in> ce_rels
[PROOF STEP]
define p where "p x = c_pair x 0" for x
[PROOF STATE]
proof (state)
this:
p ?x = c_pair ?x 0

goal (1 subgoal):
 1. r_a \<in> ce_rels
[PROOF STEP]
have p_is_pr: "p \<in> PrimRec1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<in> PrimRec1
[PROOF STEP]
unfolding p_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. c_pair x 0) \<in> PrimRec1
[PROOF STEP]
by prec
[PROOF STATE]
proof (state)
this:
p \<in> PrimRec1

goal (1 subgoal):
 1. r_a \<in> ce_rels
[PROOF STEP]
from A_ce p_is_pr
[PROOF STATE]
proof (chain)
picking this:
A \<in> ce_sets
p \<in> PrimRec1
[PROOF STEP]
have "{ c_pair x 0 | x. x \<in> A} \<in> ce_sets"
[PROOF STATE]
proof (prove)
using this:
A \<in> ce_sets
p \<in> PrimRec1

goal (1 subgoal):
 1. {c_pair x 0 |x. x \<in> A} \<in> ce_sets
[PROOF STEP]
unfolding p_def
[PROOF STATE]
proof (prove)
using this:
A \<in> ce_sets
(\<lambda>x. c_pair x 0) \<in> PrimRec1

goal (1 subgoal):
 1. {c_pair x 0 |x. x \<in> A} \<in> ce_sets
[PROOF STEP]
by (simp add: ce_set_lm_7)
[PROOF STATE]
proof (state)
this:
{c_pair x 0 |x. x \<in> A} \<in> ce_sets

goal (1 subgoal):
 1. r_a \<in> ce_rels
[PROOF STEP]
with loc1
[PROOF STATE]
proof (chain)
picking this:
ce_rel_to_set r_a = {c_pair x 0 |x. x \<in> A}
{c_pair x 0 |x. x \<in> A} \<in> ce_sets
[PROOF STEP]
have "ce_rel_to_set r_a \<in> ce_sets"
[PROOF STATE]
proof (prove)
using this:
ce_rel_to_set r_a = {c_pair x 0 |x. x \<in> A}
{c_pair x 0 |x. x \<in> A} \<in> ce_sets

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

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

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

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

goal (1 subgoal):
 1. \<lbrakk>A \<in> ce_sets; B \<in> ce_sets\<rbrakk> \<Longrightarrow> A \<times> B \<in> ce_rels
[PROOF STEP]
have r_b_ce: "r_b \<in> ce_rels"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r_b \<in> ce_rels
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. r_b \<in> ce_rels
[PROOF STEP]
have loc1: "ce_rel_to_set r_b = { c_pair 0 z | z. z \<in> B}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ce_rel_to_set r_b = {c_pair 0 z |z. z \<in> B}
[PROOF STEP]
by (unfold r_b_def, unfold ce_rel_to_set_def, auto)
[PROOF STATE]
proof (state)
this:
ce_rel_to_set r_b = {c_pair 0 z |z. z \<in> B}

goal (1 subgoal):
 1. r_b \<in> ce_rels
[PROOF STEP]
define p where "p z = c_pair 0 z" for z
[PROOF STATE]
proof (state)
this:
p ?z = c_pair 0 ?z

goal (1 subgoal):
 1. r_b \<in> ce_rels
[PROOF STEP]
have p_is_pr: "p \<in> PrimRec1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<in> PrimRec1
[PROOF STEP]
unfolding p_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c_pair 0 \<in> PrimRec1
[PROOF STEP]
by prec
[PROOF STATE]
proof (state)
this:
p \<in> PrimRec1

goal (1 subgoal):
 1. r_b \<in> ce_rels
[PROOF STEP]
from B_ce p_is_pr
[PROOF STATE]
proof (chain)
picking this:
B \<in> ce_sets
p \<in> PrimRec1
[PROOF STEP]
have "{ c_pair 0 z | z. z \<in> B} \<in> ce_sets"
[PROOF STATE]
proof (prove)
using this:
B \<in> ce_sets
p \<in> PrimRec1

goal (1 subgoal):
 1. {c_pair 0 z |z. z \<in> B} \<in> ce_sets
[PROOF STEP]
unfolding p_def
[PROOF STATE]
proof (prove)
using this:
B \<in> ce_sets
c_pair 0 \<in> PrimRec1

goal (1 subgoal):
 1. {c_pair 0 z |z. z \<in> B} \<in> ce_sets
[PROOF STEP]
by (simp add: ce_set_lm_7)
[PROOF STATE]
proof (state)
this:
{c_pair 0 z |z. z \<in> B} \<in> ce_sets

goal (1 subgoal):
 1. r_b \<in> ce_rels
[PROOF STEP]
with loc1
[PROOF STATE]
proof (chain)
picking this:
ce_rel_to_set r_b = {c_pair 0 z |z. z \<in> B}
{c_pair 0 z |z. z \<in> B} \<in> ce_sets
[PROOF STEP]
have "ce_rel_to_set r_b \<in> ce_sets"
[PROOF STATE]
proof (prove)
using this:
ce_rel_to_set r_b = {c_pair 0 z |z. z \<in> B}
{c_pair 0 z |z. z \<in> B} \<in> ce_sets

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

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

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

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

goal (1 subgoal):
 1. \<lbrakk>A \<in> ce_sets; B \<in> ce_sets\<rbrakk> \<Longrightarrow> A \<times> B \<in> ce_rels
[PROOF STEP]
from r_b_ce r_a_ce
[PROOF STATE]
proof (chain)
picking this:
r_b \<in> ce_rels
r_a \<in> ce_rels
[PROOF STEP]
have "r_a O r_b \<in> ce_rels"
[PROOF STATE]
proof (prove)
using this:
r_b \<in> ce_rels
r_a \<in> ce_rels

goal (1 subgoal):
 1. r_a O r_b \<in> ce_rels
[PROOF STEP]
by (rule ce_rel_lm_24)
[PROOF STATE]
proof (state)
this:
r_a O r_b \<in> ce_rels

goal (1 subgoal):
 1. \<lbrakk>A \<in> ce_sets; B \<in> ce_sets\<rbrakk> \<Longrightarrow> A \<times> B \<in> ce_rels
[PROOF STEP]
with L1
[PROOF STATE]
proof (chain)
picking this:
r_a O r_b = A \<times> B
r_a O r_b \<in> ce_rels
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
r_a O r_b = A \<times> B
r_a O r_b \<in> ce_rels

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ce_rel_lm_30: "{} \<in> ce_rels"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {} \<in> ce_rels
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. {} \<in> ce_rels
[PROOF STEP]
have "ce_rel_to_set {} = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ce_rel_to_set {} = {}
[PROOF STEP]
by (unfold ce_rel_to_set_def, auto)
[PROOF STATE]
proof (state)
this:
ce_rel_to_set {} = {}

goal (1 subgoal):
 1. {} \<in> ce_rels
[PROOF STEP]
with ce_empty
[PROOF STATE]
proof (chain)
picking this:
{} \<in> ce_sets
ce_rel_to_set {} = {}
[PROOF STEP]
have "ce_rel_to_set {} \<in> ce_sets"
[PROOF STATE]
proof (prove)
using this:
{} \<in> ce_sets
ce_rel_to_set {} = {}

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ce_rel_lm_31: "UNIV \<in> ce_rels"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. UNIV \<in> ce_rels
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. UNIV \<in> ce_rels
[PROOF STEP]
from ce_univ ce_univ
[PROOF STATE]
proof (chain)
picking this:
UNIV \<in> ce_sets
UNIV \<in> ce_sets
[PROOF STEP]
have "UNIV \<times> UNIV \<in> ce_rels"
[PROOF STATE]
proof (prove)
using this:
UNIV \<in> ce_sets
UNIV \<in> ce_sets

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ce_rel_lm_32: "ce_rel_to_set (r \<union> s) = (ce_rel_to_set r) \<union> (ce_rel_to_set s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ce_rel_to_set (r \<union> s) = ce_rel_to_set r \<union> ce_rel_to_set s
[PROOF STEP]
by (unfold ce_rel_to_set_def, auto)


[STATEMENT]
lemma ce_rel_lm_33: "\<lbrakk> r \<in> ce_rels; s \<in> ce_rels \<rbrakk> \<Longrightarrow> r \<union> s \<in> ce_rels"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>r \<in> ce_rels; s \<in> ce_rels\<rbrakk> \<Longrightarrow> r \<union> s \<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> r \<union> s \<in> ce_rels
[PROOF STEP]
assume "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> r \<union> s \<in> ce_rels
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
r \<in> ce_rels
[PROOF STEP]
have r_ce: "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. \<lbrakk>r \<in> ce_rels; s \<in> ce_rels\<rbrakk> \<Longrightarrow> r \<union> s \<in> ce_rels
[PROOF STEP]
assume "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> r \<union> s \<in> ce_rels
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
s \<in> ce_rels
[PROOF STEP]
have s_ce: "ce_rel_to_set s \<in> ce_sets"
[PROOF STATE]
proof (prove)
using this:
s \<in> ce_rels

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

goal (1 subgoal):
 1. \<lbrakk>r \<in> ce_rels; s \<in> ce_rels\<rbrakk> \<Longrightarrow> r \<union> s \<in> ce_rels
[PROOF STEP]
have "ce_rel_to_set (r \<union> s) = (ce_rel_to_set r) \<union> (ce_rel_to_set s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ce_rel_to_set (r \<union> s) = ce_rel_to_set r \<union> ce_rel_to_set s
[PROOF STEP]
by (unfold ce_rel_to_set_def, auto)
[PROOF STATE]
proof (state)
this:
ce_rel_to_set (r \<union> s) = ce_rel_to_set r \<union> ce_rel_to_set s

goal (1 subgoal):
 1. \<lbrakk>r \<in> ce_rels; s \<in> ce_rels\<rbrakk> \<Longrightarrow> r \<union> s \<in> ce_rels
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
ce_rel_to_set (r \<union> s) = ce_rel_to_set r \<union> ce_rel_to_set s

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

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

goal (1 subgoal):
 1. \<lbrakk>r \<in> ce_rels; s \<in> ce_rels\<rbrakk> \<Longrightarrow> r \<union> s \<in> ce_rels
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
ce_rel_to_set (r \<union> s) = ce_rel_to_set r \<union> ce_rel_to_set s
ce_rel_to_set r \<union> ce_rel_to_set s \<in> ce_sets
[PROOF STEP]
have "ce_rel_to_set (r \<union> s) \<in> ce_sets"
[PROOF STATE]
proof (prove)
using this:
ce_rel_to_set (r \<union> s) = ce_rel_to_set r \<union> ce_rel_to_set s
ce_rel_to_set r \<union> ce_rel_to_set s \<in> ce_sets

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ce_rel_lm_34: "ce_rel_to_set (r \<inter> s) = (ce_rel_to_set r) \<inter> (ce_rel_to_set s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ce_rel_to_set (r \<inter> s) = ce_rel_to_set r \<inter> ce_rel_to_set s
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ce_rel_to_set (r \<inter> s) \<subseteq> ce_rel_to_set r \<inter> ce_rel_to_set s
 2. ce_rel_to_set r \<inter> ce_rel_to_set s \<subseteq> ce_rel_to_set (r \<inter> s)
[PROOF STEP]
show "ce_rel_to_set (r \<inter> s) \<subseteq> ce_rel_to_set r \<inter> ce_rel_to_set s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ce_rel_to_set (r \<inter> s) \<subseteq> ce_rel_to_set r \<inter> ce_rel_to_set s
[PROOF STEP]
by (unfold ce_rel_to_set_def, auto)
[PROOF STATE]
proof (state)
this:
ce_rel_to_set (r \<inter> s) \<subseteq> ce_rel_to_set r \<inter> ce_rel_to_set s

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

goal (1 subgoal):
 1. \<And>x. x \<in> ce_rel_to_set r \<inter> ce_rel_to_set s \<Longrightarrow> x \<in> ce_rel_to_set (r \<inter> s)
[PROOF STEP]
from A
[PROOF STATE]
proof (chain)
picking this:
x \<in> ce_rel_to_set r \<inter> ce_rel_to_set s
[PROOF STEP]
have L1: "x \<in> ce_rel_to_set r"
[PROOF STATE]
proof (prove)
using this:
x \<in> ce_rel_to_set r \<inter> ce_rel_to_set s

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

goal (1 subgoal):
 1. \<And>x. x \<in> ce_rel_to_set r \<inter> ce_rel_to_set s \<Longrightarrow> x \<in> ce_rel_to_set (r \<inter> s)
[PROOF STEP]
from A
[PROOF STATE]
proof (chain)
picking this:
x \<in> ce_rel_to_set r \<inter> ce_rel_to_set s
[PROOF STEP]
have L2: "x \<in> ce_rel_to_set s"
[PROOF STATE]
proof (prove)
using this:
x \<in> ce_rel_to_set r \<inter> ce_rel_to_set s

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

goal (1 subgoal):
 1. \<And>x. x \<in> ce_rel_to_set r \<inter> ce_rel_to_set s \<Longrightarrow> x \<in> ce_rel_to_set (r \<inter> s)
[PROOF STEP]
from L1
[PROOF STATE]
proof (chain)
picking this:
x \<in> ce_rel_to_set r
[PROOF STEP]
obtain u v where L3: "(u,v) \<in> r" and L4: "x = c_pair u v"
[PROOF STATE]
proof (prove)
using this:
x \<in> ce_rel_to_set r

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

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

goal (1 subgoal):
 1. \<And>x. x \<in> ce_rel_to_set r \<inter> ce_rel_to_set s \<Longrightarrow> x \<in> ce_rel_to_set (r \<inter> s)
[PROOF STEP]
from L2
[PROOF STATE]
proof (chain)
picking this:
x \<in> ce_rel_to_set s
[PROOF STEP]
obtain u1 v1 where L5: "(u1,v1) \<in> s" and L6: "x = c_pair u1 v1"
[PROOF STATE]
proof (prove)
using this:
x \<in> ce_rel_to_set s

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

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

goal (1 subgoal):
 1. \<And>x. x \<in> ce_rel_to_set r \<inter> ce_rel_to_set s \<Longrightarrow> x \<in> ce_rel_to_set (r \<inter> s)
[PROOF STEP]
from L4 L6
[PROOF STATE]
proof (chain)
picking this:
x = c_pair u v
x = c_pair u1 v1
[PROOF STEP]
have L7: "c_pair u1 v1 = c_pair u v"
[PROOF STATE]
proof (prove)
using this:
x = c_pair u v
x = c_pair u1 v1

goal (1 subgoal):
 1. c_pair u1 v1 = c_pair u v
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
c_pair u1 v1 = c_pair u v

goal (1 subgoal):
 1. \<And>x. x \<in> ce_rel_to_set r \<inter> ce_rel_to_set s \<Longrightarrow> x \<in> ce_rel_to_set (r \<inter> s)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
c_pair u1 v1 = c_pair u v
[PROOF STEP]
have "u1=u"
[PROOF STATE]
proof (prove)
using this:
c_pair u1 v1 = c_pair u v

goal (1 subgoal):
 1. u1 = u
[PROOF STEP]
by (rule c_pair_inj1)
[PROOF STATE]
proof (state)
this:
u1 = u

goal (1 subgoal):
 1. \<And>x. x \<in> ce_rel_to_set r \<inter> ce_rel_to_set s \<Longrightarrow> x \<in> ce_rel_to_set (r \<inter> s)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
u1 = u

goal (1 subgoal):
 1. \<And>x. x \<in> ce_rel_to_set r \<inter> ce_rel_to_set s \<Longrightarrow> x \<in> ce_rel_to_set (r \<inter> s)
[PROOF STEP]
from L7
[PROOF STATE]
proof (chain)
picking this:
c_pair u1 v1 = c_pair u v
[PROOF STEP]
have "v1=v"
[PROOF STATE]
proof (prove)
using this:
c_pair u1 v1 = c_pair u v

goal (1 subgoal):
 1. v1 = v
[PROOF STEP]
by (rule c_pair_inj2)
[PROOF STATE]
proof (state)
this:
v1 = v

goal (1 subgoal):
 1. \<And>x. x \<in> ce_rel_to_set r \<inter> ce_rel_to_set s \<Longrightarrow> x \<in> ce_rel_to_set (r \<inter> s)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
u1 = u
v1 = v
[PROOF STEP]
have "(u,v)=(u1,v1)"
[PROOF STATE]
proof (prove)
using this:
u1 = u
v1 = v

goal (1 subgoal):
 1. (u, v) = (u1, v1)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(u, v) = (u1, v1)

goal (1 subgoal):
 1. \<And>x. x \<in> ce_rel_to_set r \<inter> ce_rel_to_set s \<Longrightarrow> x \<in> ce_rel_to_set (r \<inter> s)
[PROOF STEP]
with L3 L5
[PROOF STATE]
proof (chain)
picking this:
(u, v) \<in> r
(u1, v1) \<in> s
(u, v) = (u1, v1)
[PROOF STEP]
have "(u,v) \<in> r \<inter> s"
[PROOF STATE]
proof (prove)
using this:
(u, v) \<in> r
(u1, v1) \<in> s
(u, v) = (u1, v1)

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

goal (1 subgoal):
 1. \<And>x. x \<in> ce_rel_to_set r \<inter> ce_rel_to_set s \<Longrightarrow> x \<in> ce_rel_to_set (r \<inter> s)
[PROOF STEP]
with L4
[PROOF STATE]
proof (chain)
picking this:
x = c_pair u v
(u, v) \<in> r \<inter> s
[PROOF STEP]
show "x \<in> ce_rel_to_set (r \<inter> s)"
[PROOF STATE]
proof (prove)
using this:
x = c_pair u v
(u, v) \<in> r \<inter> s

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ce_rel_lm_35: "\<lbrakk> r \<in> ce_rels; s \<in> ce_rels \<rbrakk> \<Longrightarrow> r \<inter> s \<in> ce_rels"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>r \<in> ce_rels; s \<in> ce_rels\<rbrakk> \<Longrightarrow> r \<inter> s \<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> r \<inter> s \<in> ce_rels
[PROOF STEP]
assume "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> r \<inter> s \<in> ce_rels
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
r \<in> ce_rels
[PROOF STEP]
have r_ce: "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. \<lbrakk>r \<in> ce_rels; s \<in> ce_rels\<rbrakk> \<Longrightarrow> r \<inter> s \<in> ce_rels
[PROOF STEP]
assume "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> r \<inter> s \<in> ce_rels
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
s \<in> ce_rels
[PROOF STEP]
have s_ce: "ce_rel_to_set s \<in> ce_sets"
[PROOF STATE]
proof (prove)
using this:
s \<in> ce_rels

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

goal (1 subgoal):
 1. \<lbrakk>r \<in> ce_rels; s \<in> ce_rels\<rbrakk> \<Longrightarrow> r \<inter> s \<in> ce_rels
[PROOF STEP]
have "ce_rel_to_set (r \<inter> s) = (ce_rel_to_set r) \<inter> (ce_rel_to_set s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ce_rel_to_set (r \<inter> s) = ce_rel_to_set r \<inter> ce_rel_to_set s
[PROOF STEP]
by (rule ce_rel_lm_34)
[PROOF STATE]
proof (state)
this:
ce_rel_to_set (r \<inter> s) = ce_rel_to_set r \<inter> ce_rel_to_set s

goal (1 subgoal):
 1. \<lbrakk>r \<in> ce_rels; s \<in> ce_rels\<rbrakk> \<Longrightarrow> r \<inter> s \<in> ce_rels
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
ce_rel_to_set (r \<inter> s) = ce_rel_to_set r \<inter> ce_rel_to_set s

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

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

goal (1 subgoal):
 1. \<lbrakk>r \<in> ce_rels; s \<in> ce_rels\<rbrakk> \<Longrightarrow> r \<inter> s \<in> ce_rels
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
ce_rel_to_set (r \<inter> s) = ce_rel_to_set r \<inter> ce_rel_to_set s
ce_rel_to_set r \<inter> ce_rel_to_set s \<in> ce_sets
[PROOF STEP]
have "ce_rel_to_set (r \<inter> s) \<in> ce_sets"
[PROOF STATE]
proof (prove)
using this:
ce_rel_to_set (r \<inter> s) = ce_rel_to_set r \<inter> ce_rel_to_set s
ce_rel_to_set r \<inter> ce_rel_to_set s \<in> ce_sets

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ce_rel_lm_36: "ce_set_to_rel (A \<union> B) = (ce_set_to_rel A) \<union> (ce_set_to_rel B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ce_set_to_rel (A \<union> B) = ce_set_to_rel A \<union> ce_set_to_rel B
[PROOF STEP]
by (unfold ce_set_to_rel_def, auto)


[STATEMENT]
lemma ce_rel_lm_37: "ce_set_to_rel (A \<inter> B) = (ce_set_to_rel A) \<inter> (ce_set_to_rel B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ce_set_to_rel (A \<inter> B) = ce_set_to_rel A \<inter> ce_set_to_rel B
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ce_set_to_rel (A \<inter> B) = ce_set_to_rel A \<inter> ce_set_to_rel B
[PROOF STEP]
define f where "f x = (c_fst x, c_snd x)" for x
[PROOF STATE]
proof (state)
this:
f ?x = (c_fst ?x, c_snd ?x)

goal (1 subgoal):
 1. ce_set_to_rel (A \<inter> B) = ce_set_to_rel A \<inter> ce_set_to_rel B
[PROOF STEP]
have f_inj: "inj f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj f
[PROOF STEP]
proof (unfold f_def, rule inj_on_inverseI [where ?g="\<lambda> (u,v). c_pair u v"])
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> UNIV \<Longrightarrow> (case (c_fst x, c_snd x) of (u, v) \<Rightarrow> c_pair u v) = x
[PROOF STEP]
fix x :: nat
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> UNIV \<Longrightarrow> (case (c_fst x, c_snd x) of (u, v) \<Rightarrow> c_pair u v) = x
[PROOF STEP]
assume "x \<in> UNIV"
[PROOF STATE]
proof (state)
this:
x \<in> UNIV

goal (1 subgoal):
 1. \<And>x. x \<in> UNIV \<Longrightarrow> (case (c_fst x, c_snd x) of (u, v) \<Rightarrow> c_pair u v) = x
[PROOF STEP]
show "case_prod c_pair (c_fst x, c_snd x) = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (case (c_fst x, c_snd x) of (x, xa) \<Rightarrow> c_pair x xa) = x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(case (c_fst x, c_snd x) of (x, xa) \<Rightarrow> c_pair x xa) = x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
inj f

goal (1 subgoal):
 1. ce_set_to_rel (A \<inter> B) = ce_set_to_rel A \<inter> ce_set_to_rel B
[PROOF STEP]
from f_inj
[PROOF STATE]
proof (chain)
picking this:
inj f
[PROOF STEP]
have "f ` (A \<inter> B) = f ` A \<inter> f ` B"
[PROOF STATE]
proof (prove)
using this:
inj f

goal (1 subgoal):
 1. f ` (A \<inter> B) = f ` A \<inter> f ` B
[PROOF STEP]
by (rule image_Int)
[PROOF STATE]
proof (state)
this:
f ` (A \<inter> B) = f ` A \<inter> f ` B

goal (1 subgoal):
 1. ce_set_to_rel (A \<inter> B) = ce_set_to_rel A \<inter> ce_set_to_rel B
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
f ` (A \<inter> B) = f ` A \<inter> f ` B
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
f ` (A \<inter> B) = f ` A \<inter> f ` B

goal (1 subgoal):
 1. ce_set_to_rel (A \<inter> B) = ce_set_to_rel A \<inter> ce_set_to_rel B
[PROOF STEP]
by (unfold f_def, unfold ce_set_to_rel_def, auto)
[PROOF STATE]
proof (state)
this:
ce_set_to_rel (A \<inter> B) = ce_set_to_rel A \<inter> ce_set_to_rel B

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ce_rel_lm_38: "\<lbrakk> r \<in> ce_rels; A \<in> ce_sets \<rbrakk> \<Longrightarrow> r``A \<in> ce_sets"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>r \<in> ce_rels; A \<in> ce_sets\<rbrakk> \<Longrightarrow> r `` A \<in> ce_sets
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>r \<in> ce_rels; A \<in> ce_sets\<rbrakk> \<Longrightarrow> r `` A \<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. \<lbrakk>r \<in> ce_rels; A \<in> ce_sets\<rbrakk> \<Longrightarrow> r `` A \<in> ce_sets
[PROOF STEP]
assume A_ce: "A \<in> ce_sets"
[PROOF STATE]
proof (state)
this:
A \<in> ce_sets

goal (1 subgoal):
 1. \<lbrakk>r \<in> ce_rels; A \<in> ce_sets\<rbrakk> \<Longrightarrow> r `` A \<in> ce_sets
[PROOF STEP]
have L1: "r``A = Range (r \<inter> A \<times> UNIV)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r `` A = Range (r \<inter> A \<times> UNIV)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
r `` A = Range (r \<inter> A \<times> UNIV)

goal (1 subgoal):
 1. \<lbrakk>r \<in> ce_rels; A \<in> ce_sets\<rbrakk> \<Longrightarrow> r `` A \<in> ce_sets
[PROOF STEP]
have L2: "Range (r \<inter> A \<times> UNIV) \<in> ce_sets"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Range (r \<inter> A \<times> UNIV) \<in> ce_sets
[PROOF STEP]
proof (rule ce_rel_lm_27)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. r \<inter> A \<times> UNIV \<in> ce_rels
[PROOF STEP]
show "r \<inter> A \<times> UNIV \<in> ce_rels"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r \<inter> A \<times> UNIV \<in> ce_rels
[PROOF STEP]
proof (rule ce_rel_lm_35)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. r \<in> ce_rels
 2. A \<times> UNIV \<in> ce_rels
[PROOF STEP]
show "r \<in> ce_rels"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r \<in> ce_rels
[PROOF STEP]
by (rule r_ce)
[PROOF STATE]
proof (state)
this:
r \<in> ce_rels

goal (1 subgoal):
 1. A \<times> UNIV \<in> ce_rels
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. A \<times> UNIV \<in> ce_rels
[PROOF STEP]
show "A \<times> UNIV \<in> ce_rels"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<times> UNIV \<in> ce_rels
[PROOF STEP]
proof (rule ce_rel_lm_29)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. A \<in> ce_sets
 2. UNIV \<in> ce_sets
[PROOF STEP]
show "A \<in> ce_sets"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<in> ce_sets
[PROOF STEP]
by (rule A_ce)
[PROOF STATE]
proof (state)
this:
A \<in> ce_sets

goal (1 subgoal):
 1. UNIV \<in> ce_sets
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. UNIV \<in> ce_sets
[PROOF STEP]
show "UNIV \<in> ce_sets"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. UNIV \<in> ce_sets
[PROOF STEP]
by (rule ce_univ)
[PROOF STATE]
proof (state)
this:
UNIV \<in> ce_sets

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
r \<inter> A \<times> UNIV \<in> ce_rels

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Range (r \<inter> A \<times> UNIV) \<in> ce_sets

goal (1 subgoal):
 1. \<lbrakk>r \<in> ce_rels; A \<in> ce_sets\<rbrakk> \<Longrightarrow> r `` A \<in> ce_sets
[PROOF STEP]
from L1 L2
[PROOF STATE]
proof (chain)
picking this:
r `` A = Range (r \<inter> A \<times> UNIV)
Range (r \<inter> A \<times> UNIV) \<in> ce_sets
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
r `` A = Range (r \<inter> A \<times> UNIV)
Range (r \<inter> A \<times> UNIV) \<in> ce_sets

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma graph_lm_1: "(x,y) \<in> graph f \<Longrightarrow> y = f x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x, y) \<in> graph f \<Longrightarrow> y = f x
[PROOF STEP]
by (unfold graph_def, auto)


[STATEMENT]
lemma graph_lm_2: "y = f x \<Longrightarrow> (x,y) \<in> graph f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y = f x \<Longrightarrow> (x, y) \<in> graph f
[PROOF STEP]
by (unfold graph_def, auto)


[STATEMENT]
lemma graph_lm_3: "((x,y) \<in> graph f) = (y = f x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((x, y) \<in> graph f) = (y = f x)
[PROOF STEP]
by (unfold graph_def, auto)


[STATEMENT]
lemma graph_lm_4: "graph (f o g) = (graph g) O (graph f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. graph (f \<circ> g) = graph g O graph f
[PROOF STEP]
by (unfold graph_def, auto)


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

goal (1 subgoal):
 1. c_pair x y \<in> c_graph f \<Longrightarrow> y = f x
[PROOF STEP]
have S1: "c_graph f = {c_pair x (f x) | x. x \<in> UNIV}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c_graph f = {c_pair x (f x) |x. x \<in> UNIV}
[PROOF STEP]
by (simp add: c_graph_def)
[PROOF STATE]
proof (state)
this:
c_graph f = {c_pair x (f x) |x. x \<in> UNIV}

goal (1 subgoal):
 1. c_pair x y \<in> c_graph f \<Longrightarrow> y = f x
[PROOF STEP]
from A S1
[PROOF STATE]
proof (chain)
picking this:
c_pair x y \<in> c_graph f
c_graph f = {c_pair x (f x) |x. x \<in> UNIV}
[PROOF STEP]
obtain z where S2: "c_pair x y = c_pair z (f z)"
[PROOF STATE]
proof (prove)
using this:
c_pair x y \<in> c_graph f
c_graph f = {c_pair x (f x) |x. x \<in> UNIV}

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

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

goal (1 subgoal):
 1. x = z
[PROOF STEP]
by (rule c_pair_inj1)
[PROOF STATE]
proof (state)
this:
x = z

goal (1 subgoal):
 1. c_pair x y \<in> c_graph f \<Longrightarrow> y = f x
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
x = z

goal (1 subgoal):
 1. c_pair x y \<in> c_graph f \<Longrightarrow> y = f x
[PROOF STEP]
from S2
[PROOF STATE]
proof (chain)
picking this:
c_pair x y = c_pair z (f z)
[PROOF STEP]
have "y = f z"
[PROOF STATE]
proof (prove)
using this:
c_pair x y = c_pair z (f z)

goal (1 subgoal):
 1. y = f z
[PROOF STEP]
by (rule c_pair_inj2)
[PROOF STATE]
proof (state)
this:
y = f z

goal (1 subgoal):
 1. c_pair x y \<in> c_graph f \<Longrightarrow> y = f x
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
x = z
y = f z
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x = z
y = f z

goal (1 subgoal):
 1. y = f x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
y = f x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma c_graph_lm_2: "y = f x \<Longrightarrow> c_pair x y \<in> c_graph f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y = f x \<Longrightarrow> c_pair x y \<in> c_graph f
[PROOF STEP]
by (unfold c_graph_def, auto)


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

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

goal (1 subgoal):
 1. y = f x
[PROOF STEP]
by (rule c_graph_lm_1)
[PROOF STATE]
proof (state)
this:
y = f x

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma c_graph_lm_4: "c_graph f = ce_rel_to_set (graph f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c_graph f = ce_rel_to_set (graph f)
[PROOF STEP]
by (unfold c_graph_def ce_rel_to_set_def graph_def, auto)


[STATEMENT]
lemma c_graph_lm_5: "graph f = ce_set_to_rel (c_graph f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. graph f = ce_set_to_rel (c_graph f)
[PROOF STEP]
by (simp add: c_graph_lm_4)


[STATEMENT]
lemma total_recursive_def1: "total_recursive = (\<lambda> f. c_graph f \<in> ce_sets)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. total_recursive = (\<lambda>f. c_graph f \<in> ce_sets)
[PROOF STEP]
proof (rule ext)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>f. total_recursive f = (c_graph f \<in> ce_sets)
[PROOF STEP]
fix f
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>f. total_recursive f = (c_graph f \<in> ce_sets)
[PROOF STEP]
show " total_recursive f = (c_graph f \<in> ce_sets)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. total_recursive f = (c_graph f \<in> ce_sets)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. total_recursive f \<Longrightarrow> c_graph f \<in> ce_sets
 2. c_graph f \<in> ce_sets \<Longrightarrow> total_recursive f
[PROOF STEP]
assume A: "total_recursive f"
[PROOF STATE]
proof (state)
this:
total_recursive f

goal (2 subgoals):
 1. total_recursive f \<Longrightarrow> c_graph f \<in> ce_sets
 2. c_graph f \<in> ce_sets \<Longrightarrow> total_recursive f
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
total_recursive f
[PROOF STEP]
have "graph f \<in> ce_rels"
[PROOF STATE]
proof (prove)
using this:
total_recursive f

goal (1 subgoal):
 1. graph f \<in> ce_rels
[PROOF STEP]
by (unfold total_recursive_def)
[PROOF STATE]
proof (state)
this:
graph f \<in> ce_rels

goal (2 subgoals):
 1. total_recursive f \<Longrightarrow> c_graph f \<in> ce_sets
 2. c_graph f \<in> ce_sets \<Longrightarrow> total_recursive f
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
graph f \<in> ce_rels
[PROOF STEP]
have "ce_rel_to_set (graph f) \<in> ce_sets"
[PROOF STATE]
proof (prove)
using this:
graph f \<in> ce_rels

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

goal (2 subgoals):
 1. total_recursive f \<Longrightarrow> c_graph f \<in> ce_sets
 2. c_graph f \<in> ce_sets \<Longrightarrow> total_recursive f
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ce_rel_to_set (graph f) \<in> ce_sets
[PROOF STEP]
show "c_graph f \<in> ce_sets"
[PROOF STATE]
proof (prove)
using this:
ce_rel_to_set (graph f) \<in> ce_sets

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

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

goal (1 subgoal):
 1. c_graph f \<in> ce_sets \<Longrightarrow> total_recursive f
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
c_graph f \<in> ce_sets
[PROOF STEP]
have "ce_rel_to_set (graph f) \<in> ce_sets"
[PROOF STATE]
proof (prove)
using this:
c_graph f \<in> ce_sets

goal (1 subgoal):
 1. ce_rel_to_set (graph f) \<in> ce_sets
[PROOF STEP]
by (simp add: c_graph_lm_4)
[PROOF STATE]
proof (state)
this:
ce_rel_to_set (graph f) \<in> ce_sets

goal (1 subgoal):
 1. c_graph f \<in> ce_sets \<Longrightarrow> total_recursive f
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ce_rel_to_set (graph f) \<in> ce_sets
[PROOF STEP]
have "graph f \<in> ce_rels"
[PROOF STATE]
proof (prove)
using this:
ce_rel_to_set (graph f) \<in> ce_sets

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

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

goal (1 subgoal):
 1. total_recursive f
[PROOF STEP]
by (unfold total_recursive_def)
[PROOF STATE]
proof (state)
this:
total_recursive f

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
total_recursive f = (c_graph f \<in> ce_sets)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem pr_is_total_rec: "f \<in> PrimRec1 \<Longrightarrow> total_recursive f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<in> PrimRec1 \<Longrightarrow> total_recursive f
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. f \<in> PrimRec1 \<Longrightarrow> total_recursive f
[PROOF STEP]
assume A: "f \<in> PrimRec1"
[PROOF STATE]
proof (state)
this:
f \<in> PrimRec1

goal (1 subgoal):
 1. f \<in> PrimRec1 \<Longrightarrow> total_recursive f
[PROOF STEP]
define p where "p x = c_pair x (f x)" for x
[PROOF STATE]
proof (state)
this:
p ?x = c_pair ?x (f ?x)

goal (1 subgoal):
 1. f \<in> PrimRec1 \<Longrightarrow> total_recursive f
[PROOF STEP]
from A
[PROOF STATE]
proof (chain)
picking this:
f \<in> PrimRec1
[PROOF STEP]
have p_is_pr: "p \<in> PrimRec1"
[PROOF STATE]
proof (prove)
using this:
f \<in> PrimRec1

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

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

goal (1 subgoal):
 1. f \<in> PrimRec1 \<Longrightarrow> total_recursive f
[PROOF STEP]
let ?U = "{ p x | x. x \<in> UNIV }"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. f \<in> PrimRec1 \<Longrightarrow> total_recursive f
[PROOF STEP]
from ce_univ p_is_pr
[PROOF STATE]
proof (chain)
picking this:
UNIV \<in> ce_sets
p \<in> PrimRec1
[PROOF STEP]
have U_ce: "?U \<in> ce_sets"
[PROOF STATE]
proof (prove)
using this:
UNIV \<in> ce_sets
p \<in> PrimRec1

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

goal (1 subgoal):
 1. f \<in> PrimRec1 \<Longrightarrow> total_recursive f
[PROOF STEP]
have U_1: "?U = { c_pair x (f x) | x. x \<in> UNIV}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {p x |x. x \<in> UNIV} = {c_pair x (f x) |x. x \<in> UNIV}
[PROOF STEP]
by (simp add: p_def)
[PROOF STATE]
proof (state)
this:
{p x |x. x \<in> UNIV} = {c_pair x (f x) |x. x \<in> UNIV}

goal (1 subgoal):
 1. f \<in> PrimRec1 \<Longrightarrow> total_recursive f
[PROOF STEP]
with U_ce
[PROOF STATE]
proof (chain)
picking this:
{p x |x. x \<in> UNIV} \<in> ce_sets
{p x |x. x \<in> UNIV} = {c_pair x (f x) |x. x \<in> UNIV}
[PROOF STEP]
have S1: "{ c_pair x (f x) | x. x \<in> UNIV} \<in> ce_sets"
[PROOF STATE]
proof (prove)
using this:
{p x |x. x \<in> UNIV} \<in> ce_sets
{p x |x. x \<in> UNIV} = {c_pair x (f x) |x. x \<in> UNIV}

goal (1 subgoal):
 1. {c_pair x (f x) |x. x \<in> UNIV} \<in> ce_sets
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
{c_pair x (f x) |x. x \<in> UNIV} \<in> ce_sets

goal (1 subgoal):
 1. f \<in> PrimRec1 \<Longrightarrow> total_recursive f
[PROOF STEP]
with c_graph_def
[PROOF STATE]
proof (chain)
picking this:
c_graph = (\<lambda>f. {c_pair x (f x) |x. x \<in> UNIV})
{c_pair x (f x) |x. x \<in> UNIV} \<in> ce_sets
[PROOF STEP]
have c_graph_f_is_ce: "c_graph f \<in> ce_sets"
[PROOF STATE]
proof (prove)
using this:
c_graph = (\<lambda>f. {c_pair x (f x) |x. x \<in> UNIV})
{c_pair x (f x) |x. x \<in> UNIV} \<in> ce_sets

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

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

goal (1 subgoal):
 1. total_recursive f
[PROOF STEP]
by (unfold total_recursive_def1, auto)
[PROOF STATE]
proof (state)
this:
total_recursive f

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem comp_tot_rec: "\<lbrakk> total_recursive f; total_recursive g \<rbrakk> \<Longrightarrow> total_recursive (f o g)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>total_recursive f; total_recursive g\<rbrakk> \<Longrightarrow> total_recursive (f \<circ> g)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>total_recursive f; total_recursive g\<rbrakk> \<Longrightarrow> total_recursive (f \<circ> g)
[PROOF STEP]
assume "total_recursive f"
[PROOF STATE]
proof (state)
this:
total_recursive f

goal (1 subgoal):
 1. \<lbrakk>total_recursive f; total_recursive g\<rbrakk> \<Longrightarrow> total_recursive (f \<circ> g)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
total_recursive f
[PROOF STEP]
have f_ce: "graph f \<in> ce_rels"
[PROOF STATE]
proof (prove)
using this:
total_recursive f

goal (1 subgoal):
 1. graph f \<in> ce_rels
[PROOF STEP]
by (unfold total_recursive_def)
[PROOF STATE]
proof (state)
this:
graph f \<in> ce_rels

goal (1 subgoal):
 1. \<lbrakk>total_recursive f; total_recursive g\<rbrakk> \<Longrightarrow> total_recursive (f \<circ> g)
[PROOF STEP]
assume "total_recursive g"
[PROOF STATE]
proof (state)
this:
total_recursive g

goal (1 subgoal):
 1. \<lbrakk>total_recursive f; total_recursive g\<rbrakk> \<Longrightarrow> total_recursive (f \<circ> g)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
total_recursive g
[PROOF STEP]
have g_ce: "graph g \<in> ce_rels"
[PROOF STATE]
proof (prove)
using this:
total_recursive g

goal (1 subgoal):
 1. graph g \<in> ce_rels
[PROOF STEP]
by (unfold total_recursive_def)
[PROOF STATE]
proof (state)
this:
graph g \<in> ce_rels

goal (1 subgoal):
 1. \<lbrakk>total_recursive f; total_recursive g\<rbrakk> \<Longrightarrow> total_recursive (f \<circ> g)
[PROOF STEP]
from f_ce g_ce
[PROOF STATE]
proof (chain)
picking this:
graph f \<in> ce_rels
graph g \<in> ce_rels
[PROOF STEP]
have "graph g O graph f \<in> ce_rels"
[PROOF STATE]
proof (prove)
using this:
graph f \<in> ce_rels
graph g \<in> ce_rels

goal (1 subgoal):
 1. graph g O graph f \<in> ce_rels
[PROOF STEP]
by (rule ce_rel_lm_24)
[PROOF STATE]
proof (state)
this:
graph g O graph f \<in> ce_rels

goal (1 subgoal):
 1. \<lbrakk>total_recursive f; total_recursive g\<rbrakk> \<Longrightarrow> total_recursive (f \<circ> g)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
graph g O graph f \<in> ce_rels
[PROOF STEP]
have "graph (f o g) \<in> ce_rels"
[PROOF STATE]
proof (prove)
using this:
graph g O graph f \<in> ce_rels

goal (1 subgoal):
 1. graph (f \<circ> g) \<in> ce_rels
[PROOF STEP]
by (simp add: graph_lm_4)
[PROOF STATE]
proof (state)
this:
graph (f \<circ> g) \<in> ce_rels

goal (1 subgoal):
 1. \<lbrakk>total_recursive f; total_recursive g\<rbrakk> \<Longrightarrow> total_recursive (f \<circ> g)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
graph (f \<circ> g) \<in> ce_rels
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
graph (f \<circ> g) \<in> ce_rels

goal (1 subgoal):
 1. total_recursive (f \<circ> g)
[PROOF STEP]
by (unfold total_recursive_def)
[PROOF STATE]
proof (state)
this:
total_recursive (f \<circ> g)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma univ_for_pr_tot_rec_lm: "c_graph univ_for_pr \<in> ce_sets"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c_graph univ_for_pr \<in> ce_sets
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. c_graph univ_for_pr \<in> ce_sets
[PROOF STEP]
define A where "A = c_graph univ_for_pr"
[PROOF STATE]
proof (state)
this:
A = c_graph univ_for_pr

goal (1 subgoal):
 1. c_graph univ_for_pr \<in> ce_sets
[PROOF STEP]
from A_def
[PROOF STATE]
proof (chain)
picking this:
A = c_graph univ_for_pr
[PROOF STEP]
have S1: "A = { c_pair x (univ_for_pr x) | x. x \<in> UNIV }"
[PROOF STATE]
proof (prove)
using this:
A = c_graph univ_for_pr

goal (1 subgoal):
 1. A = {c_pair x (univ_for_pr x) |x. x \<in> UNIV}
[PROOF STEP]
by (simp add: c_graph_def)
[PROOF STATE]
proof (state)
this:
A = {c_pair x (univ_for_pr x) |x. x \<in> UNIV}

goal (1 subgoal):
 1. c_graph univ_for_pr \<in> ce_sets
[PROOF STEP]
from S1
[PROOF STATE]
proof (chain)
picking this:
A = {c_pair x (univ_for_pr x) |x. x \<in> UNIV}
[PROOF STEP]
have S2: "A = { z . \<exists> x. z = c_pair x (univ_for_pr x) }"
[PROOF STATE]
proof (prove)
using this:
A = {c_pair x (univ_for_pr x) |x. x \<in> UNIV}

goal (1 subgoal):
 1. A = {z. \<exists>x. z = c_pair x (univ_for_pr x)}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
A = {z. \<exists>x. z = c_pair x (univ_for_pr x)}

goal (1 subgoal):
 1. c_graph univ_for_pr \<in> ce_sets
[PROOF STEP]
have S3: "\<And> z. (\<exists> x. (z = c_pair x (univ_for_pr x))) = (univ_for_pr (c_fst z) = c_snd z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>z. (\<exists>x. z = c_pair x (univ_for_pr x)) = (univ_for_pr (c_fst z) = c_snd z)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>z. (\<exists>x. z = c_pair x (univ_for_pr x)) = (univ_for_pr (c_fst z) = c_snd z)
[PROOF STEP]
fix z
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>z. (\<exists>x. z = c_pair x (univ_for_pr x)) = (univ_for_pr (c_fst z) = c_snd z)
[PROOF STEP]
show "(\<exists> x. (z = c_pair x (univ_for_pr x))) = (univ_for_pr (c_fst z) = c_snd z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>x. z = c_pair x (univ_for_pr x)) = (univ_for_pr (c_fst z) = c_snd z)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<exists>x. z = c_pair x (univ_for_pr x) \<Longrightarrow> univ_for_pr (c_fst z) = c_snd z
 2. univ_for_pr (c_fst z) = c_snd z \<Longrightarrow> \<exists>x. z = c_pair x (univ_for_pr x)
[PROOF STEP]
assume A: "\<exists>x. z = c_pair x (univ_for_pr x)"
[PROOF STATE]
proof (state)
this:
\<exists>x. z = c_pair x (univ_for_pr x)

goal (2 subgoals):
 1. \<exists>x. z = c_pair x (univ_for_pr x) \<Longrightarrow> univ_for_pr (c_fst z) = c_snd z
 2. univ_for_pr (c_fst z) = c_snd z \<Longrightarrow> \<exists>x. z = c_pair x (univ_for_pr x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>x. z = c_pair x (univ_for_pr x)
[PROOF STEP]
obtain x where S3_1: "z = c_pair x (univ_for_pr x)"
[PROOF STATE]
proof (prove)
using this:
\<exists>x. z = c_pair x (univ_for_pr x)

goal (1 subgoal):
 1. (\<And>x. z = c_pair x (univ_for_pr x) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
z = c_pair x (univ_for_pr x)

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

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

goal (1 subgoal):
 1. univ_for_pr (c_fst z) = c_snd z \<Longrightarrow> \<exists>x. z = c_pair x (univ_for_pr x)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. univ_for_pr (c_fst z) = c_snd z \<Longrightarrow> \<exists>x. z = c_pair x (univ_for_pr x)
[PROOF STEP]
assume A: "univ_for_pr (c_fst z) = c_snd z"
[PROOF STATE]
proof (state)
this:
univ_for_pr (c_fst z) = c_snd z

goal (1 subgoal):
 1. univ_for_pr (c_fst z) = c_snd z \<Longrightarrow> \<exists>x. z = c_pair x (univ_for_pr x)
[PROOF STEP]
from A
[PROOF STATE]
proof (chain)
picking this:
univ_for_pr (c_fst z) = c_snd z
[PROOF STEP]
have "z = c_pair (c_fst z) (univ_for_pr (c_fst z))"
[PROOF STATE]
proof (prove)
using this:
univ_for_pr (c_fst z) = c_snd z

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

goal (1 subgoal):
 1. univ_for_pr (c_fst z) = c_snd z \<Longrightarrow> \<exists>x. z = c_pair x (univ_for_pr x)
[PROOF STEP]
thus "\<exists>x. z = c_pair x (univ_for_pr x)"
[PROOF STATE]
proof (prove)
using this:
z = c_pair (c_fst z) (univ_for_pr (c_fst z))

goal (1 subgoal):
 1. \<exists>x. z = c_pair x (univ_for_pr x)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
\<exists>x. z = c_pair x (univ_for_pr x)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<exists>x. z = c_pair x (univ_for_pr x)) = (univ_for_pr (c_fst z) = c_snd z)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<exists>x. ?z = c_pair x (univ_for_pr x)) = (univ_for_pr (c_fst ?z) = c_snd ?z)

goal (1 subgoal):
 1. c_graph univ_for_pr \<in> ce_sets
[PROOF STEP]
with S2
[PROOF STATE]
proof (chain)
picking this:
A = {z. \<exists>x. z = c_pair x (univ_for_pr x)}
(\<exists>x. ?z = c_pair x (univ_for_pr x)) = (univ_for_pr (c_fst ?z) = c_snd ?z)
[PROOF STEP]
have S4: "A = { z . univ_for_pr (c_fst z) = c_snd z }"
[PROOF STATE]
proof (prove)
using this:
A = {z. \<exists>x. z = c_pair x (univ_for_pr x)}
(\<exists>x. ?z = c_pair x (univ_for_pr x)) = (univ_for_pr (c_fst ?z) = c_snd ?z)

goal (1 subgoal):
 1. A = {z. univ_for_pr (c_fst z) = c_snd z}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
A = {z. univ_for_pr (c_fst z) = c_snd z}

goal (1 subgoal):
 1. c_graph univ_for_pr \<in> ce_sets
[PROOF STEP]
define p where "p x y =
    (if c_assoc_have_key (pr_gr y) (c_fst x) = 0 then
      (if c_assoc_value (pr_gr y) (c_fst x) = c_snd x then (0::nat) else 1)
    else 1)" for x y
[PROOF STATE]
proof (state)
this:
p ?x ?y = (if c_assoc_have_key (pr_gr ?y) (c_fst ?x) = 0 then if c_assoc_value (pr_gr ?y) (c_fst ?x) = c_snd ?x then 0 else 1 else 1)

goal (1 subgoal):
 1. c_graph univ_for_pr \<in> ce_sets
[PROOF STEP]
from c_assoc_have_key_is_pr c_assoc_value_is_pr pr_gr_is_pr
[PROOF STATE]
proof (chain)
picking this:
c_assoc_have_key \<in> PrimRec2
c_assoc_value \<in> PrimRec2
pr_gr \<in> PrimRec1
[PROOF STEP]
have p_is_pr: "p \<in> PrimRec2"
[PROOF STATE]
proof (prove)
using this:
c_assoc_have_key \<in> PrimRec2
c_assoc_value \<in> PrimRec2
pr_gr \<in> PrimRec1

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

goal (1 subgoal):
 1. (\<lambda>x y. if c_assoc_have_key (pr_gr y) (c_fst x) = 0 then if c_assoc_value (pr_gr y) (c_fst x) = c_snd x then 0 else 1 else 1) \<in> PrimRec2
[PROOF STEP]
by prec
[PROOF STATE]
proof (state)
this:
p \<in> PrimRec2

goal (1 subgoal):
 1. c_graph univ_for_pr \<in> ce_sets
[PROOF STEP]
have S5: "\<And> z. (univ_for_pr (c_fst z) = c_snd z) = (\<exists> y. p z y = 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>z. (univ_for_pr (c_fst z) = c_snd z) = (\<exists>y. p z y = 0)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>z. (univ_for_pr (c_fst z) = c_snd z) = (\<exists>y. p z y = 0)
[PROOF STEP]
fix z
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>z. (univ_for_pr (c_fst z) = c_snd z) = (\<exists>y. p z y = 0)
[PROOF STEP]
show "(univ_for_pr (c_fst z) = c_snd z) = (\<exists> y. p z y = 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (univ_for_pr (c_fst z) = c_snd z) = (\<exists>y. p z y = 0)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. univ_for_pr (c_fst z) = c_snd z \<Longrightarrow> \<exists>y. p z y = 0
 2. \<exists>y. p z y = 0 \<Longrightarrow> univ_for_pr (c_fst z) = c_snd z
[PROOF STEP]
assume A: "univ_for_pr (c_fst z) = c_snd z"
[PROOF STATE]
proof (state)
this:
univ_for_pr (c_fst z) = c_snd z

goal (2 subgoals):
 1. univ_for_pr (c_fst z) = c_snd z \<Longrightarrow> \<exists>y. p z y = 0
 2. \<exists>y. p z y = 0 \<Longrightarrow> univ_for_pr (c_fst z) = c_snd z
[PROOF STEP]
let ?n = "c_fst (c_fst z)"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. univ_for_pr (c_fst z) = c_snd z \<Longrightarrow> \<exists>y. p z y = 0
 2. \<exists>y. p z y = 0 \<Longrightarrow> univ_for_pr (c_fst z) = c_snd z
[PROOF STEP]
let ?x = "c_snd (c_fst z)"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. univ_for_pr (c_fst z) = c_snd z \<Longrightarrow> \<exists>y. p z y = 0
 2. \<exists>y. p z y = 0 \<Longrightarrow> univ_for_pr (c_fst z) = c_snd z
[PROOF STEP]
let ?y = "loc_upb ?n ?x"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. univ_for_pr (c_fst z) = c_snd z \<Longrightarrow> \<exists>y. p z y = 0
 2. \<exists>y. p z y = 0 \<Longrightarrow> univ_for_pr (c_fst z) = c_snd z
[PROOF STEP]
have S5_1: "c_assoc_have_key (pr_gr ?y) (c_pair ?n ?x) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c_assoc_have_key (pr_gr (loc_upb (c_fst (c_fst z)) (c_snd (c_fst z)))) (c_pair (c_fst (c_fst z)) (c_snd (c_fst z))) = 0
[PROOF STEP]
by (rule loc_upb_main)
[PROOF STATE]
proof (state)
this:
c_assoc_have_key (pr_gr (loc_upb (c_fst (c_fst z)) (c_snd (c_fst z)))) (c_pair (c_fst (c_fst z)) (c_snd (c_fst z))) = 0

goal (2 subgoals):
 1. univ_for_pr (c_fst z) = c_snd z \<Longrightarrow> \<exists>y. p z y = 0
 2. \<exists>y. p z y = 0 \<Longrightarrow> univ_for_pr (c_fst z) = c_snd z
[PROOF STEP]
have S5_2: "c_assoc_value (pr_gr ?y) (c_pair ?n ?x) = univ_for_pr (c_pair ?n ?x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c_assoc_value (pr_gr (loc_upb (c_fst (c_fst z)) (c_snd (c_fst z)))) (c_pair (c_fst (c_fst z)) (c_snd (c_fst z))) = univ_for_pr (c_pair (c_fst (c_fst z)) (c_snd (c_fst z)))
[PROOF STEP]
by (rule pr_gr_value)
[PROOF STATE]
proof (state)
this:
c_assoc_value (pr_gr (loc_upb (c_fst (c_fst z)) (c_snd (c_fst z)))) (c_pair (c_fst (c_fst z)) (c_snd (c_fst z))) = univ_for_pr (c_pair (c_fst (c_fst z)) (c_snd (c_fst z)))

goal (2 subgoals):
 1. univ_for_pr (c_fst z) = c_snd z \<Longrightarrow> \<exists>y. p z y = 0
 2. \<exists>y. p z y = 0 \<Longrightarrow> univ_for_pr (c_fst z) = c_snd z
[PROOF STEP]
from S5_1
[PROOF STATE]
proof (chain)
picking this:
c_assoc_have_key (pr_gr (loc_upb (c_fst (c_fst z)) (c_snd (c_fst z)))) (c_pair (c_fst (c_fst z)) (c_snd (c_fst z))) = 0
[PROOF STEP]
have S5_3: "c_assoc_have_key (pr_gr ?y) (c_fst z) = 0"
[PROOF STATE]
proof (prove)
using this:
c_assoc_have_key (pr_gr (loc_upb (c_fst (c_fst z)) (c_snd (c_fst z)))) (c_pair (c_fst (c_fst z)) (c_snd (c_fst z))) = 0

goal (1 subgoal):
 1. c_assoc_have_key (pr_gr (loc_upb (c_fst (c_fst z)) (c_snd (c_fst z)))) (c_fst z) = 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
c_assoc_have_key (pr_gr (loc_upb (c_fst (c_fst z)) (c_snd (c_fst z)))) (c_fst z) = 0

goal (2 subgoals):
 1. univ_for_pr (c_fst z) = c_snd z \<Longrightarrow> \<exists>y. p z y = 0
 2. \<exists>y. p z y = 0 \<Longrightarrow> univ_for_pr (c_fst z) = c_snd z
[PROOF STEP]
from S5_2 A
[PROOF STATE]
proof (chain)
picking this:
c_assoc_value (pr_gr (loc_upb (c_fst (c_fst z)) (c_snd (c_fst z)))) (c_pair (c_fst (c_fst z)) (c_snd (c_fst z))) = univ_for_pr (c_pair (c_fst (c_fst z)) (c_snd (c_fst z)))
univ_for_pr (c_fst z) = c_snd z
[PROOF STEP]
have S5_4: "c_assoc_value (pr_gr ?y) (c_fst z) = c_snd z"
[PROOF STATE]
proof (prove)
using this:
c_assoc_value (pr_gr (loc_upb (c_fst (c_fst z)) (c_snd (c_fst z)))) (c_pair (c_fst (c_fst z)) (c_snd (c_fst z))) = univ_for_pr (c_pair (c_fst (c_fst z)) (c_snd (c_fst z)))
univ_for_pr (c_fst z) = c_snd z

goal (1 subgoal):
 1. c_assoc_value (pr_gr (loc_upb (c_fst (c_fst z)) (c_snd (c_fst z)))) (c_fst z) = c_snd z
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
c_assoc_value (pr_gr (loc_upb (c_fst (c_fst z)) (c_snd (c_fst z)))) (c_fst z) = c_snd z

goal (2 subgoals):
 1. univ_for_pr (c_fst z) = c_snd z \<Longrightarrow> \<exists>y. p z y = 0
 2. \<exists>y. p z y = 0 \<Longrightarrow> univ_for_pr (c_fst z) = c_snd z
[PROOF STEP]
from S5_3 S5_4
[PROOF STATE]
proof (chain)
picking this:
c_assoc_have_key (pr_gr (loc_upb (c_fst (c_fst z)) (c_snd (c_fst z)))) (c_fst z) = 0
c_assoc_value (pr_gr (loc_upb (c_fst (c_fst z)) (c_snd (c_fst z)))) (c_fst z) = c_snd z
[PROOF STEP]
have "p z ?y = 0"
[PROOF STATE]
proof (prove)
using this:
c_assoc_have_key (pr_gr (loc_upb (c_fst (c_fst z)) (c_snd (c_fst z)))) (c_fst z) = 0
c_assoc_value (pr_gr (loc_upb (c_fst (c_fst z)) (c_snd (c_fst z)))) (c_fst z) = c_snd z

goal (1 subgoal):
 1. p z (loc_upb (c_fst (c_fst z)) (c_snd (c_fst z))) = 0
[PROOF STEP]
by (simp add: p_def)
[PROOF STATE]
proof (state)
this:
p z (loc_upb (c_fst (c_fst z)) (c_snd (c_fst z))) = 0

goal (2 subgoals):
 1. univ_for_pr (c_fst z) = c_snd z \<Longrightarrow> \<exists>y. p z y = 0
 2. \<exists>y. p z y = 0 \<Longrightarrow> univ_for_pr (c_fst z) = c_snd z
[PROOF STEP]
thus "\<exists> y. p z y = 0"
[PROOF STATE]
proof (prove)
using this:
p z (loc_upb (c_fst (c_fst z)) (c_snd (c_fst z))) = 0

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

goal (1 subgoal):
 1. \<exists>y. p z y = 0 \<Longrightarrow> univ_for_pr (c_fst z) = c_snd z
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>y. p z y = 0 \<Longrightarrow> univ_for_pr (c_fst z) = c_snd z
[PROOF STEP]
assume A: "\<exists>y. p z y = 0"
[PROOF STATE]
proof (state)
this:
\<exists>y. p z y = 0

goal (1 subgoal):
 1. \<exists>y. p z y = 0 \<Longrightarrow> univ_for_pr (c_fst z) = c_snd z
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>y. p z y = 0
[PROOF STEP]
obtain y where S5_1: "p z y = 0"
[PROOF STATE]
proof (prove)
using this:
\<exists>y. p z y = 0

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

goal (1 subgoal):
 1. \<exists>y. p z y = 0 \<Longrightarrow> univ_for_pr (c_fst z) = c_snd z
[PROOF STEP]
have S5_2: "c_assoc_have_key (pr_gr y) (c_fst z) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c_assoc_have_key (pr_gr y) (c_fst z) = 0
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. c_assoc_have_key (pr_gr y) (c_fst z) \<noteq> 0 \<Longrightarrow> False
[PROOF STEP]
assume A_1: "c_assoc_have_key (pr_gr y) (c_fst z) \<noteq> 0"
[PROOF STATE]
proof (state)
this:
c_assoc_have_key (pr_gr y) (c_fst z) \<noteq> 0

goal (1 subgoal):
 1. c_assoc_have_key (pr_gr y) (c_fst z) \<noteq> 0 \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
c_assoc_have_key (pr_gr y) (c_fst z) \<noteq> 0
[PROOF STEP]
have "p z y = 1"
[PROOF STATE]
proof (prove)
using this:
c_assoc_have_key (pr_gr y) (c_fst z) \<noteq> 0

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

goal (1 subgoal):
 1. c_assoc_have_key (pr_gr y) (c_fst z) \<noteq> 0 \<Longrightarrow> False
[PROOF STEP]
with S5_1
[PROOF STATE]
proof (chain)
picking this:
p z y = 0
p z y = 1
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
p z y = 0
p z y = 1

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
c_assoc_have_key (pr_gr y) (c_fst z) = 0

goal (1 subgoal):
 1. \<exists>y. p z y = 0 \<Longrightarrow> univ_for_pr (c_fst z) = c_snd z
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
c_assoc_have_key (pr_gr y) (c_fst z) = 0
[PROOF STEP]
have S5_3: "p z y = (if c_assoc_value (pr_gr y) (c_fst z) = c_snd z then (0::nat) else 1)"
[PROOF STATE]
proof (prove)
using this:
c_assoc_have_key (pr_gr y) (c_fst z) = 0

goal (1 subgoal):
 1. p z y = (if c_assoc_value (pr_gr y) (c_fst z) = c_snd z then 0 else 1)
[PROOF STEP]
by (simp add: p_def)
[PROOF STATE]
proof (state)
this:
p z y = (if c_assoc_value (pr_gr y) (c_fst z) = c_snd z then 0 else 1)

goal (1 subgoal):
 1. \<exists>y. p z y = 0 \<Longrightarrow> univ_for_pr (c_fst z) = c_snd z
[PROOF STEP]
have S5_4: "c_assoc_value (pr_gr y) (c_fst z) = c_snd z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c_assoc_value (pr_gr y) (c_fst z) = c_snd z
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. c_assoc_value (pr_gr y) (c_fst z) \<noteq> c_snd z \<Longrightarrow> False
[PROOF STEP]
assume A_2: "c_assoc_value (pr_gr y) (c_fst z) \<noteq> c_snd z"
[PROOF STATE]
proof (state)
this:
c_assoc_value (pr_gr y) (c_fst z) \<noteq> c_snd z

goal (1 subgoal):
 1. c_assoc_value (pr_gr y) (c_fst z) \<noteq> c_snd z \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
c_assoc_value (pr_gr y) (c_fst z) \<noteq> c_snd z
[PROOF STEP]
have "p z y = 1"
[PROOF STATE]
proof (prove)
using this:
c_assoc_value (pr_gr y) (c_fst z) \<noteq> c_snd z

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

goal (1 subgoal):
 1. c_assoc_value (pr_gr y) (c_fst z) \<noteq> c_snd z \<Longrightarrow> False
[PROOF STEP]
with S5_1
[PROOF STATE]
proof (chain)
picking this:
p z y = 0
p z y = 1
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
p z y = 0
p z y = 1

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
c_assoc_value (pr_gr y) (c_fst z) = c_snd z

goal (1 subgoal):
 1. \<exists>y. p z y = 0 \<Longrightarrow> univ_for_pr (c_fst z) = c_snd z
[PROOF STEP]
have S5_5: "c_is_sub_fun (pr_gr y) univ_for_pr"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c_is_sub_fun (pr_gr y) univ_for_pr
[PROOF STEP]
by (rule pr_gr_1)
[PROOF STATE]
proof (state)
this:
c_is_sub_fun (pr_gr y) univ_for_pr

goal (1 subgoal):
 1. \<exists>y. p z y = 0 \<Longrightarrow> univ_for_pr (c_fst z) = c_snd z
[PROOF STEP]
from S5_5 S5_2
[PROOF STATE]
proof (chain)
picking this:
c_is_sub_fun (pr_gr y) univ_for_pr
c_assoc_have_key (pr_gr y) (c_fst z) = 0
[PROOF STEP]
have S5_6: "c_assoc_value (pr_gr y) (c_fst z) = univ_for_pr (c_fst z)"
[PROOF STATE]
proof (prove)
using this:
c_is_sub_fun (pr_gr y) univ_for_pr
c_assoc_have_key (pr_gr y) (c_fst z) = 0

goal (1 subgoal):
 1. c_assoc_value (pr_gr y) (c_fst z) = univ_for_pr (c_fst z)
[PROOF STEP]
by (rule c_is_sub_fun_lm_1)
[PROOF STATE]
proof (state)
this:
c_assoc_value (pr_gr y) (c_fst z) = univ_for_pr (c_fst z)

goal (1 subgoal):
 1. \<exists>y. p z y = 0 \<Longrightarrow> univ_for_pr (c_fst z) = c_snd z
[PROOF STEP]
with S5_4
[PROOF STATE]
proof (chain)
picking this:
c_assoc_value (pr_gr y) (c_fst z) = c_snd z
c_assoc_value (pr_gr y) (c_fst z) = univ_for_pr (c_fst z)
[PROOF STEP]
show "univ_for_pr (c_fst z) = c_snd z"
[PROOF STATE]
proof (prove)
using this:
c_assoc_value (pr_gr y) (c_fst z) = c_snd z
c_assoc_value (pr_gr y) (c_fst z) = univ_for_pr (c_fst z)

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

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(univ_for_pr (c_fst ?z) = c_snd ?z) = (\<exists>y. p ?z y = 0)

goal (1 subgoal):
 1. c_graph univ_for_pr \<in> ce_sets
[PROOF STEP]
from S5 S4
[PROOF STATE]
proof (chain)
picking this:
(univ_for_pr (c_fst ?z) = c_snd ?z) = (\<exists>y. p ?z y = 0)
A = {z. univ_for_pr (c_fst z) = c_snd z}
[PROOF STEP]
have "A = {z. \<exists> y. p z y = 0}"
[PROOF STATE]
proof (prove)
using this:
(univ_for_pr (c_fst ?z) = c_snd ?z) = (\<exists>y. p ?z y = 0)
A = {z. univ_for_pr (c_fst z) = c_snd z}

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

goal (1 subgoal):
 1. c_graph univ_for_pr \<in> ce_sets
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
A = {z. \<exists>y. p z y = 0}
[PROOF STEP]
have "A = fn_to_set p"
[PROOF STATE]
proof (prove)
using this:
A = {z. \<exists>y. p z y = 0}

goal (1 subgoal):
 1. A = fn_to_set p
[PROOF STEP]
by (simp add: fn_to_set_def)
[PROOF STATE]
proof (state)
this:
A = fn_to_set p

goal (1 subgoal):
 1. c_graph univ_for_pr \<in> ce_sets
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
A = fn_to_set p

goal (1 subgoal):
 1. c_graph univ_for_pr \<in> ce_sets
[PROOF STEP]
from p_is_pr
[PROOF STATE]
proof (chain)
picking this:
p \<in> PrimRec2
[PROOF STEP]
have "fn_to_set p \<in> ce_sets"
[PROOF STATE]
proof (prove)
using this:
p \<in> PrimRec2

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

goal (1 subgoal):
 1. c_graph univ_for_pr \<in> ce_sets
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
A = fn_to_set p
fn_to_set p \<in> ce_sets
[PROOF STEP]
have "A \<in> ce_sets"
[PROOF STATE]
proof (prove)
using this:
A = fn_to_set p
fn_to_set p \<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. c_graph univ_for_pr \<in> ce_sets
[PROOF STEP]
with A_def
[PROOF STATE]
proof (chain)
picking this:
A = c_graph univ_for_pr
A \<in> ce_sets
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
A = c_graph univ_for_pr
A \<in> ce_sets

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem univ_for_pr_tot_rec: "total_recursive univ_for_pr"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. total_recursive univ_for_pr
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. total_recursive univ_for_pr
[PROOF STEP]
have "c_graph univ_for_pr \<in> ce_sets"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c_graph univ_for_pr \<in> ce_sets
[PROOF STEP]
by (rule univ_for_pr_tot_rec_lm)
[PROOF STATE]
proof (state)
this:
c_graph univ_for_pr \<in> ce_sets

goal (1 subgoal):
 1. total_recursive univ_for_pr
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
c_graph univ_for_pr \<in> ce_sets
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
c_graph univ_for_pr \<in> ce_sets

goal (1 subgoal):
 1. total_recursive univ_for_pr
[PROOF STEP]
by (unfold total_recursive_def1, auto)
[PROOF STATE]
proof (state)
this:
total_recursive univ_for_pr

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma computable_complement_1: "computable A \<Longrightarrow> computable (- A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. computable A \<Longrightarrow> computable (- A)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. computable A \<Longrightarrow> computable (- A)
[PROOF STEP]
assume "computable A"
[PROOF STATE]
proof (state)
this:
computable A

goal (1 subgoal):
 1. computable A \<Longrightarrow> computable (- A)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
computable A
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
computable A

goal (1 subgoal):
 1. computable (- A)
[PROOF STEP]
by (unfold computable_def, auto)
[PROOF STATE]
proof (state)
this:
computable (- A)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma computable_complement_2: "computable (- A) \<Longrightarrow> computable A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. computable (- A) \<Longrightarrow> computable A
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. computable (- A) \<Longrightarrow> computable A
[PROOF STEP]
assume "computable (- A)"
[PROOF STATE]
proof (state)
this:
computable (- A)

goal (1 subgoal):
 1. computable (- A) \<Longrightarrow> computable A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
computable (- A)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
computable (- A)

goal (1 subgoal):
 1. computable A
[PROOF STEP]
by (unfold computable_def, auto)
[PROOF STATE]
proof (state)
this:
computable A

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma computable_complement_3: "(computable A) = (computable (- A))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. computable A = computable (- A)
[PROOF STEP]
by (unfold computable_def, auto)


[STATEMENT]
theorem comp_impl_tot_rec: "computable A \<Longrightarrow> total_recursive (chf A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. computable A \<Longrightarrow> total_recursive (chf A)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. computable A \<Longrightarrow> total_recursive (chf A)
[PROOF STEP]
assume A: "computable A"
[PROOF STATE]
proof (state)
this:
computable A

goal (1 subgoal):
 1. computable A \<Longrightarrow> total_recursive (chf A)
[PROOF STEP]
from A
[PROOF STATE]
proof (chain)
picking this:
computable A
[PROOF STEP]
have A1: "A \<in> ce_sets"
[PROOF STATE]
proof (prove)
using this:
computable A

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

goal (1 subgoal):
 1. computable A \<Longrightarrow> total_recursive (chf A)
[PROOF STEP]
from A
[PROOF STATE]
proof (chain)
picking this:
computable A
[PROOF STEP]
have A2: "-A \<in> ce_sets"
[PROOF STATE]
proof (prove)
using this:
computable A

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

goal (1 subgoal):
 1. computable A \<Longrightarrow> total_recursive (chf A)
[PROOF STEP]
define p where "p x = c_pair x 0" for x
[PROOF STATE]
proof (state)
this:
p ?x = c_pair ?x 0

goal (1 subgoal):
 1. computable A \<Longrightarrow> total_recursive (chf A)
[PROOF STEP]
define q where "q x = c_pair x 1" for x
[PROOF STATE]
proof (state)
this:
q ?x = c_pair ?x 1

goal (1 subgoal):
 1. computable A \<Longrightarrow> total_recursive (chf A)
[PROOF STEP]
from p_def
[PROOF STATE]
proof (chain)
picking this:
p ?x = c_pair ?x 0
[PROOF STEP]
have p_is_pr: "p \<in> PrimRec1"
[PROOF STATE]
proof (prove)
using this:
p ?x = c_pair ?x 0

goal (1 subgoal):
 1. p \<in> PrimRec1
[PROOF STEP]
unfolding p_def
[PROOF STATE]
proof (prove)
using this:
c_pair ?x 0 = c_pair ?x 0

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

goal (1 subgoal):
 1. computable A \<Longrightarrow> total_recursive (chf A)
[PROOF STEP]
from q_def
[PROOF STATE]
proof (chain)
picking this:
q ?x = c_pair ?x 1
[PROOF STEP]
have q_is_pr: "q \<in> PrimRec1"
[PROOF STATE]
proof (prove)
using this:
q ?x = c_pair ?x 1

goal (1 subgoal):
 1. q \<in> PrimRec1
[PROOF STEP]
unfolding q_def
[PROOF STATE]
proof (prove)
using this:
c_pair ?x 1 = c_pair ?x 1

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

goal (1 subgoal):
 1. computable A \<Longrightarrow> total_recursive (chf A)
[PROOF STEP]
define U0 where "U0 = {p x | x. x \<in> A}"
[PROOF STATE]
proof (state)
this:
U0 = {p x |x. x \<in> A}

goal (1 subgoal):
 1. computable A \<Longrightarrow> total_recursive (chf A)
[PROOF STEP]
define U1 where "U1 = {q x | x. x \<in> - A}"
[PROOF STATE]
proof (state)
this:
U1 = {q x |x. x \<in> - A}

goal (1 subgoal):
 1. computable A \<Longrightarrow> total_recursive (chf A)
[PROOF STEP]
from A1 p_is_pr
[PROOF STATE]
proof (chain)
picking this:
A \<in> ce_sets
p \<in> PrimRec1
[PROOF STEP]
have U0_ce: "U0 \<in> ce_sets"
[PROOF STATE]
proof (prove)
using this:
A \<in> ce_sets
p \<in> PrimRec1

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

goal (1 subgoal):
 1. computable A \<Longrightarrow> total_recursive (chf A)
[PROOF STEP]
from A2 q_is_pr
[PROOF STATE]
proof (chain)
picking this:
- A \<in> ce_sets
q \<in> PrimRec1
[PROOF STEP]
have U1_ce: "U1 \<in> ce_sets"
[PROOF STATE]
proof (prove)
using this:
- A \<in> ce_sets
q \<in> PrimRec1

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

goal (1 subgoal):
 1. computable A \<Longrightarrow> total_recursive (chf A)
[PROOF STEP]
define U where "U = U0 \<union> U1"
[PROOF STATE]
proof (state)
this:
U = U0 \<union> U1

goal (1 subgoal):
 1. computable A \<Longrightarrow> total_recursive (chf A)
[PROOF STEP]
from U0_ce U1_ce
[PROOF STATE]
proof (chain)
picking this:
U0 \<in> ce_sets
U1 \<in> ce_sets
[PROOF STEP]
have U_ce: "U \<in> ce_sets"
[PROOF STATE]
proof (prove)
using this:
U0 \<in> ce_sets
U1 \<in> ce_sets

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

goal (1 subgoal):
 1. computable A \<Longrightarrow> total_recursive (chf A)
[PROOF STEP]
define V where "V = c_graph (chf A)"
[PROOF STATE]
proof (state)
this:
V = c_graph (chf A)

goal (1 subgoal):
 1. computable A \<Longrightarrow> total_recursive (chf A)
[PROOF STEP]
have V_1: "V = { c_pair x (chf A x) | x. x \<in> UNIV}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. V = {c_pair x (chf A x) |x. x \<in> UNIV}
[PROOF STEP]
by (simp add: V_def c_graph_def)
[PROOF STATE]
proof (state)
this:
V = {c_pair x (chf A x) |x. x \<in> UNIV}

goal (1 subgoal):
 1. computable A \<Longrightarrow> total_recursive (chf A)
[PROOF STEP]
from U0_def p_def
[PROOF STATE]
proof (chain)
picking this:
U0 = {p x |x. x \<in> A}
p ?x = c_pair ?x 0
[PROOF STEP]
have U0_1: "U0 = { c_pair x y | x y. x \<in> A \<and> y=0}"
[PROOF STATE]
proof (prove)
using this:
U0 = {p x |x. x \<in> A}
p ?x = c_pair ?x 0

goal (1 subgoal):
 1. U0 = {c_pair x y |x y. x \<in> A \<and> y = 0}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
U0 = {c_pair x y |x y. x \<in> A \<and> y = 0}

goal (1 subgoal):
 1. computable A \<Longrightarrow> total_recursive (chf A)
[PROOF STEP]
from U1_def q_def
[PROOF STATE]
proof (chain)
picking this:
U1 = {q x |x. x \<in> - A}
q ?x = c_pair ?x 1
[PROOF STEP]
have U1_1: "U1 = { c_pair x y | x y. x \<notin> A \<and> y=1}"
[PROOF STATE]
proof (prove)
using this:
U1 = {q x |x. x \<in> - A}
q ?x = c_pair ?x 1

goal (1 subgoal):
 1. U1 = {c_pair x y |x y. x \<notin> A \<and> y = 1}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
U1 = {c_pair x y |x y. x \<notin> A \<and> y = 1}

goal (1 subgoal):
 1. computable A \<Longrightarrow> total_recursive (chf A)
[PROOF STEP]
from U0_1 U1_1 U_def
[PROOF STATE]
proof (chain)
picking this:
U0 = {c_pair x y |x y. x \<in> A \<and> y = 0}
U1 = {c_pair x y |x y. x \<notin> A \<and> y = 1}
U = U0 \<union> U1
[PROOF STEP]
have U_1: "U = { c_pair x y | x y. (x \<in> A \<and> y=0) \<or> (x \<notin> A \<and> y=1)}"
[PROOF STATE]
proof (prove)
using this:
U0 = {c_pair x y |x y. x \<in> A \<and> y = 0}
U1 = {c_pair x y |x y. x \<notin> A \<and> y = 1}
U = U0 \<union> U1

goal (1 subgoal):
 1. U = {c_pair x y |x y. x \<in> A \<and> y = 0 \<or> x \<notin> A \<and> y = 1}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
U = {c_pair x y |x y. x \<in> A \<and> y = 0 \<or> x \<notin> A \<and> y = 1}

goal (1 subgoal):
 1. computable A \<Longrightarrow> total_recursive (chf A)
[PROOF STEP]
from V_1
[PROOF STATE]
proof (chain)
picking this:
V = {c_pair x (chf A x) |x. x \<in> UNIV}
[PROOF STEP]
have V_2: "V = { c_pair x y | x y. y = chf A x}"
[PROOF STATE]
proof (prove)
using this:
V = {c_pair x (chf A x) |x. x \<in> UNIV}

goal (1 subgoal):
 1. V = {c_pair x y |x y. y = chf A x}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
V = {c_pair x y |x y. y = chf A x}

goal (1 subgoal):
 1. computable A \<Longrightarrow> total_recursive (chf A)
[PROOF STEP]
have L1: "\<And> x y. ((x \<in> A \<and> y=0) \<or> (x \<notin> A \<and> y=1)) = (y = chf A x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. (x \<in> A \<and> y = 0 \<or> x \<notin> A \<and> y = 1) = (y = chf A x)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. (x \<in> A \<and> y = 0 \<or> x \<notin> A \<and> y = 1) = (y = chf A x)
[PROOF STEP]
fix x y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. (x \<in> A \<and> y = 0 \<or> x \<notin> A \<and> y = 1) = (y = chf A x)
[PROOF STEP]
show "((x \<in> A \<and> y=0) \<or> (x \<notin> A \<and> y=1)) = (y = chf A x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<in> A \<and> y = 0 \<or> x \<notin> A \<and> y = 1) = (y = chf A x)
[PROOF STEP]
by(unfold chf_def, auto)
[PROOF STATE]
proof (state)
this:
(x \<in> A \<and> y = 0 \<or> x \<notin> A \<and> y = 1) = (y = chf A x)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(?x \<in> A \<and> ?y = 0 \<or> ?x \<notin> A \<and> ?y = 1) = (?y = chf A ?x)

goal (1 subgoal):
 1. computable A \<Longrightarrow> total_recursive (chf A)
[PROOF STEP]
from V_2 U_1 L1
[PROOF STATE]
proof (chain)
picking this:
V = {c_pair x y |x y. y = chf A x}
U = {c_pair x y |x y. x \<in> A \<and> y = 0 \<or> x \<notin> A \<and> y = 1}
(?x \<in> A \<and> ?y = 0 \<or> ?x \<notin> A \<and> ?y = 1) = (?y = chf A ?x)
[PROOF STEP]
have "U=V"
[PROOF STATE]
proof (prove)
using this:
V = {c_pair x y |x y. y = chf A x}
U = {c_pair x y |x y. x \<in> A \<and> y = 0 \<or> x \<notin> A \<and> y = 1}
(?x \<in> A \<and> ?y = 0 \<or> ?x \<notin> A \<and> ?y = 1) = (?y = chf A ?x)

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

goal (1 subgoal):
 1. computable A \<Longrightarrow> total_recursive (chf A)
[PROOF STEP]
with U_ce
[PROOF STATE]
proof (chain)
picking this:
U \<in> ce_sets
U = V
[PROOF STEP]
have V_ce: "V \<in> ce_sets"
[PROOF STATE]
proof (prove)
using this:
U \<in> ce_sets
U = V

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

goal (1 subgoal):
 1. computable A \<Longrightarrow> total_recursive (chf A)
[PROOF STEP]
with V_def
[PROOF STATE]
proof (chain)
picking this:
V = c_graph (chf A)
V \<in> ce_sets
[PROOF STEP]
have "c_graph (chf A) \<in> ce_sets"
[PROOF STATE]
proof (prove)
using this:
V = c_graph (chf A)
V \<in> ce_sets

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

goal (1 subgoal):
 1. computable A \<Longrightarrow> total_recursive (chf A)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
c_graph (chf A) \<in> ce_sets
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
c_graph (chf A) \<in> ce_sets

goal (1 subgoal):
 1. total_recursive (chf A)
[PROOF STEP]
by (unfold total_recursive_def1)
[PROOF STATE]
proof (state)
this:
total_recursive (chf A)

goal:
No subgoals!
[PROOF STEP]
qed