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

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

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

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

goal (1 subgoal):
 1. total_recursive (chf A) \<Longrightarrow> computable A
[PROOF STEP]
have L2: "\<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. total_recursive (chf A) \<Longrightarrow> computable A
[PROOF STEP]
from L1 L2
[PROOF STATE]
proof (chain)
picking this:
c_graph (chf A) = {c_pair x (chf A x) |x. x \<in> UNIV}
(?x \<in> A \<and> ?y = 0 \<or> ?x \<notin> A \<and> ?y = 1) = (?y = chf A ?x)
[PROOF STEP]
have L3: "?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:
c_graph (chf A) = {c_pair x (chf A x) |x. x \<in> UNIV}
(?x \<in> A \<and> ?y = 0 \<or> ?x \<notin> A \<and> ?y = 1) = (?y = chf A ?x)

goal (1 subgoal):
 1. c_graph (chf A) = {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:
c_graph (chf A) = {c_pair x y |x y. x \<in> A \<and> y = 0 \<or> x \<notin> A \<and> y = 1}

goal (1 subgoal):
 1. total_recursive (chf A) \<Longrightarrow> computable 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. total_recursive (chf A) \<Longrightarrow> computable 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. total_recursive (chf A) \<Longrightarrow> computable A
[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. total_recursive (chf A) \<Longrightarrow> computable A
[PROOF STEP]
have q_is_pr: "q \<in> PrimRec1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. q \<in> PrimRec1
[PROOF STEP]
unfolding q_def
[PROOF STATE]
proof (prove)
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. total_recursive (chf A) \<Longrightarrow> computable A
[PROOF STEP]
define V where "V = { c_pair x y | x y. (x \<in> A \<and> y=0) \<or> (x \<notin> A \<and> y=1)}"
[PROOF STATE]
proof (state)
this:
V = {c_pair x y |x y. x \<in> A \<and> y = 0 \<or> x \<notin> A \<and> y = 1}

goal (1 subgoal):
 1. total_recursive (chf A) \<Longrightarrow> computable A
[PROOF STEP]
from V_def L3 A1
[PROOF STATE]
proof (chain)
picking this:
V = {c_pair x y |x y. x \<in> A \<and> y = 0 \<or> x \<notin> A \<and> y = 1}
c_graph (chf A) = {c_pair x y |x y. x \<in> A \<and> y = 0 \<or> x \<notin> A \<and> y = 1}
c_graph (chf A) \<in> ce_sets
[PROOF STEP]
have V_ce: "V \<in> ce_sets"
[PROOF STATE]
proof (prove)
using this:
V = {c_pair x y |x y. x \<in> A \<and> y = 0 \<or> x \<notin> A \<and> y = 1}
c_graph (chf A) = {c_pair x y |x y. x \<in> A \<and> y = 0 \<or> x \<notin> A \<and> y = 1}
c_graph (chf A) \<in> ce_sets

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. total_recursive (chf A) \<Longrightarrow> computable A
[PROOF STEP]
from V_def
[PROOF STATE]
proof (chain)
picking this:
V = {c_pair x y |x y. x \<in> A \<and> y = 0 \<or> x \<notin> A \<and> y = 1}
[PROOF STEP]
have L4: "\<forall> z. (z \<in> V) = (\<exists> x y. z = c_pair x y \<and>  ((x \<in> A \<and> y=0) \<or> (x \<notin> A \<and> y=1)))"
[PROOF STATE]
proof (prove)
using this:
V = {c_pair x y |x y. x \<in> A \<and> y = 0 \<or> x \<notin> A \<and> y = 1}

goal (1 subgoal):
 1. \<forall>z. (z \<in> V) = (\<exists>x y. z = c_pair x y \<and> (x \<in> A \<and> y = 0 \<or> x \<notin> A \<and> y = 1))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>z. (z \<in> V) = (\<exists>x y. z = c_pair x y \<and> (x \<in> A \<and> y = 0 \<or> x \<notin> A \<and> y = 1))

goal (1 subgoal):
 1. total_recursive (chf A) \<Longrightarrow> computable A
[PROOF STEP]
have L5: "\<And> x. (p x \<in> V) = (x \<in> A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. (p x \<in> V) = (x \<in> A)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. (p x \<in> V) = (x \<in> A)
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. (p x \<in> V) = (x \<in> A)
[PROOF STEP]
show "(p x \<in> V) = (x \<in> A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (p x \<in> V) = (x \<in> A)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. p x \<in> V \<Longrightarrow> x \<in> A
 2. x \<in> A \<Longrightarrow> p x \<in> V
[PROOF STEP]
assume A: "p x \<in> V"
[PROOF STATE]
proof (state)
this:
p x \<in> V

goal (2 subgoals):
 1. p x \<in> V \<Longrightarrow> x \<in> A
 2. x \<in> A \<Longrightarrow> p x \<in> V
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p x \<in> V
[PROOF STEP]
have "c_pair x 0 \<in> V"
[PROOF STATE]
proof (prove)
using this:
p x \<in> V

goal (1 subgoal):
 1. c_pair x 0 \<in> V
[PROOF STEP]
by (unfold p_def)
[PROOF STATE]
proof (state)
this:
c_pair x 0 \<in> V

goal (2 subgoals):
 1. p x \<in> V \<Longrightarrow> x \<in> A
 2. x \<in> A \<Longrightarrow> p x \<in> V
[PROOF STEP]
with V_def
[PROOF STATE]
proof (chain)
picking this:
V = {c_pair x y |x y. x \<in> A \<and> y = 0 \<or> x \<notin> A \<and> y = 1}
c_pair x 0 \<in> V
[PROOF STEP]
obtain x1 y1 where L5_2: "c_pair x 0 = c_pair x1 y1"
        and L5_3: "((x1 \<in> A \<and> y1=0) \<or> (x1 \<notin> A \<and> y1=1))"
[PROOF STATE]
proof (prove)
using this:
V = {c_pair x y |x y. x \<in> A \<and> y = 0 \<or> x \<notin> A \<and> y = 1}
c_pair x 0 \<in> V

goal (1 subgoal):
 1. (\<And>x1 y1. \<lbrakk>c_pair x 0 = c_pair x1 y1; x1 \<in> A \<and> y1 = 0 \<or> x1 \<notin> A \<and> y1 = 1\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
c_pair x 0 = c_pair x1 y1
x1 \<in> A \<and> y1 = 0 \<or> x1 \<notin> A \<and> y1 = 1

goal (2 subgoals):
 1. p x \<in> V \<Longrightarrow> x \<in> A
 2. x \<in> A \<Longrightarrow> p x \<in> V
[PROOF STEP]
from L5_2
[PROOF STATE]
proof (chain)
picking this:
c_pair x 0 = c_pair x1 y1
[PROOF STEP]
have X_eq_X1: "x=x1"
[PROOF STATE]
proof (prove)
using this:
c_pair x 0 = c_pair x1 y1

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

goal (2 subgoals):
 1. p x \<in> V \<Longrightarrow> x \<in> A
 2. x \<in> A \<Longrightarrow> p x \<in> V
[PROOF STEP]
from L5_2
[PROOF STATE]
proof (chain)
picking this:
c_pair x 0 = c_pair x1 y1
[PROOF STEP]
have Y1_eq_0: "0=y1"
[PROOF STATE]
proof (prove)
using this:
c_pair x 0 = c_pair x1 y1

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

goal (2 subgoals):
 1. p x \<in> V \<Longrightarrow> x \<in> A
 2. x \<in> A \<Longrightarrow> p x \<in> V
[PROOF STEP]
from L5_3 X_eq_X1 Y1_eq_0
[PROOF STATE]
proof (chain)
picking this:
x1 \<in> A \<and> y1 = 0 \<or> x1 \<notin> A \<and> y1 = 1
x = x1
0 = y1
[PROOF STEP]
show "x \<in> A"
[PROOF STATE]
proof (prove)
using this:
x1 \<in> A \<and> y1 = 0 \<or> x1 \<notin> A \<and> y1 = 1
x = x1
0 = y1

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

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

goal (1 subgoal):
 1. x \<in> A \<Longrightarrow> p x \<in> V
[PROOF STEP]
let ?z = "c_pair x 0"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<in> A \<Longrightarrow> p x \<in> V
[PROOF STEP]
from A
[PROOF STATE]
proof (chain)
picking this:
x \<in> A
[PROOF STEP]
have L5_1: "\<exists> x1 y1. c_pair x 0 = c_pair x1 y1 \<and>  ((x1 \<in> A \<and> y1=0) \<or> (x1 \<notin> A \<and> y1=1))"
[PROOF STATE]
proof (prove)
using this:
x \<in> A

goal (1 subgoal):
 1. \<exists>x1 y1. c_pair x 0 = c_pair x1 y1 \<and> (x1 \<in> A \<and> y1 = 0 \<or> x1 \<notin> A \<and> y1 = 1)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>x1 y1. c_pair x 0 = c_pair x1 y1 \<and> (x1 \<in> A \<and> y1 = 0 \<or> x1 \<notin> A \<and> y1 = 1)

goal (1 subgoal):
 1. x \<in> A \<Longrightarrow> p x \<in> V
[PROOF STEP]
with V_def
[PROOF STATE]
proof (chain)
picking this:
V = {c_pair x y |x y. x \<in> A \<and> y = 0 \<or> x \<notin> A \<and> y = 1}
\<exists>x1 y1. c_pair x 0 = c_pair x1 y1 \<and> (x1 \<in> A \<and> y1 = 0 \<or> x1 \<notin> A \<and> y1 = 1)
[PROOF STEP]
have "c_pair x 0 \<in> V"
[PROOF STATE]
proof (prove)
using this:
V = {c_pair x y |x y. x \<in> A \<and> y = 0 \<or> x \<notin> A \<and> y = 1}
\<exists>x1 y1. c_pair x 0 = c_pair x1 y1 \<and> (x1 \<in> A \<and> y1 = 0 \<or> x1 \<notin> A \<and> y1 = 1)

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

goal (1 subgoal):
 1. x \<in> A \<Longrightarrow> p x \<in> V
[PROOF STEP]
with p_def
[PROOF STATE]
proof (chain)
picking this:
p ?x = c_pair ?x 0
c_pair x 0 \<in> V
[PROOF STEP]
show "p x \<in> V"
[PROOF STATE]
proof (prove)
using this:
p ?x = c_pair ?x 0
c_pair x 0 \<in> V

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

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(p ?x \<in> V) = (?x \<in> A)

goal (1 subgoal):
 1. total_recursive (chf A) \<Longrightarrow> computable A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(p ?x \<in> V) = (?x \<in> A)
[PROOF STEP]
have A_eq: "A = { x. p x \<in> V}"
[PROOF STATE]
proof (prove)
using this:
(p ?x \<in> V) = (?x \<in> A)

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

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

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

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

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

goal (1 subgoal):
 1. total_recursive (chf A) \<Longrightarrow> computable A
[PROOF STEP]
have CA_eq: "- A = {x. q x \<in> V}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - A = {x. q x \<in> V}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. - A = {x. q x \<in> V}
[PROOF STEP]
have "\<And> x. (q x \<in> V) = (x \<notin> A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. (q x \<in> V) = (x \<notin> A)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. (q x \<in> V) = (x \<notin> A)
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. (q x \<in> V) = (x \<notin> A)
[PROOF STEP]
show "(q x \<in> V) = (x \<notin> A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (q x \<in> V) = (x \<notin> A)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. q x \<in> V \<Longrightarrow> x \<notin> A
 2. x \<notin> A \<Longrightarrow> q x \<in> V
[PROOF STEP]
assume A: "q x \<in> V"
[PROOF STATE]
proof (state)
this:
q x \<in> V

goal (2 subgoals):
 1. q x \<in> V \<Longrightarrow> x \<notin> A
 2. x \<notin> A \<Longrightarrow> q x \<in> V
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
q x \<in> V
[PROOF STEP]
have "c_pair x 1 \<in> V"
[PROOF STATE]
proof (prove)
using this:
q x \<in> V

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

goal (2 subgoals):
 1. q x \<in> V \<Longrightarrow> x \<notin> A
 2. x \<notin> A \<Longrightarrow> q x \<in> V
[PROOF STEP]
with V_def
[PROOF STATE]
proof (chain)
picking this:
V = {c_pair x y |x y. x \<in> A \<and> y = 0 \<or> x \<notin> A \<and> y = 1}
c_pair x 1 \<in> V
[PROOF STEP]
obtain x1 y1 where L5_2: "c_pair x 1 = c_pair x1 y1"
          and L5_3: "((x1 \<in> A \<and> y1=0) \<or> (x1 \<notin> A \<and> y1=1))"
[PROOF STATE]
proof (prove)
using this:
V = {c_pair x y |x y. x \<in> A \<and> y = 0 \<or> x \<notin> A \<and> y = 1}
c_pair x 1 \<in> V

goal (1 subgoal):
 1. (\<And>x1 y1. \<lbrakk>c_pair x 1 = c_pair x1 y1; x1 \<in> A \<and> y1 = 0 \<or> x1 \<notin> A \<and> y1 = 1\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
c_pair x 1 = c_pair x1 y1
x1 \<in> A \<and> y1 = 0 \<or> x1 \<notin> A \<and> y1 = 1

goal (2 subgoals):
 1. q x \<in> V \<Longrightarrow> x \<notin> A
 2. x \<notin> A \<Longrightarrow> q x \<in> V
[PROOF STEP]
from L5_2
[PROOF STATE]
proof (chain)
picking this:
c_pair x 1 = c_pair x1 y1
[PROOF STEP]
have X_eq_X1: "x=x1"
[PROOF STATE]
proof (prove)
using this:
c_pair x 1 = c_pair x1 y1

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

goal (2 subgoals):
 1. q x \<in> V \<Longrightarrow> x \<notin> A
 2. x \<notin> A \<Longrightarrow> q x \<in> V
[PROOF STEP]
from L5_2
[PROOF STATE]
proof (chain)
picking this:
c_pair x 1 = c_pair x1 y1
[PROOF STEP]
have Y1_eq_1: "1=y1"
[PROOF STATE]
proof (prove)
using this:
c_pair x 1 = c_pair x1 y1

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

goal (2 subgoals):
 1. q x \<in> V \<Longrightarrow> x \<notin> A
 2. x \<notin> A \<Longrightarrow> q x \<in> V
[PROOF STEP]
from L5_3 X_eq_X1 Y1_eq_1
[PROOF STATE]
proof (chain)
picking this:
x1 \<in> A \<and> y1 = 0 \<or> x1 \<notin> A \<and> y1 = 1
x = x1
1 = y1
[PROOF STEP]
show "x \<notin> A"
[PROOF STATE]
proof (prove)
using this:
x1 \<in> A \<and> y1 = 0 \<or> x1 \<notin> A \<and> y1 = 1
x = x1
1 = y1

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

goal (1 subgoal):
 1. x \<notin> A \<Longrightarrow> q x \<in> V
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<notin> A \<Longrightarrow> q x \<in> V
[PROOF STEP]
assume A: "x \<notin> A"
[PROOF STATE]
proof (state)
this:
x \<notin> A

goal (1 subgoal):
 1. x \<notin> A \<Longrightarrow> q x \<in> V
[PROOF STEP]
from A
[PROOF STATE]
proof (chain)
picking this:
x \<notin> A
[PROOF STEP]
have L5_1: "\<exists> x1 y1. c_pair x 1 = c_pair x1 y1 \<and>  ((x1 \<in> A \<and> y1=0) \<or> (x1 \<notin> A \<and> y1=1))"
[PROOF STATE]
proof (prove)
using this:
x \<notin> A

goal (1 subgoal):
 1. \<exists>x1 y1. c_pair x 1 = c_pair x1 y1 \<and> (x1 \<in> A \<and> y1 = 0 \<or> x1 \<notin> A \<and> y1 = 1)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>x1 y1. c_pair x 1 = c_pair x1 y1 \<and> (x1 \<in> A \<and> y1 = 0 \<or> x1 \<notin> A \<and> y1 = 1)

goal (1 subgoal):
 1. x \<notin> A \<Longrightarrow> q x \<in> V
[PROOF STEP]
with V_def
[PROOF STATE]
proof (chain)
picking this:
V = {c_pair x y |x y. x \<in> A \<and> y = 0 \<or> x \<notin> A \<and> y = 1}
\<exists>x1 y1. c_pair x 1 = c_pair x1 y1 \<and> (x1 \<in> A \<and> y1 = 0 \<or> x1 \<notin> A \<and> y1 = 1)
[PROOF STEP]
have "c_pair x 1 \<in> V"
[PROOF STATE]
proof (prove)
using this:
V = {c_pair x y |x y. x \<in> A \<and> y = 0 \<or> x \<notin> A \<and> y = 1}
\<exists>x1 y1. c_pair x 1 = c_pair x1 y1 \<and> (x1 \<in> A \<and> y1 = 0 \<or> x1 \<notin> A \<and> y1 = 1)

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

goal (1 subgoal):
 1. x \<notin> A \<Longrightarrow> q x \<in> V
[PROOF STEP]
with q_def
[PROOF STATE]
proof (chain)
picking this:
q ?x = c_pair ?x 1
c_pair x 1 \<in> V
[PROOF STEP]
show "q x \<in> V"
[PROOF STATE]
proof (prove)
using this:
q ?x = c_pair ?x 1
c_pair x 1 \<in> V

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(q x \<in> V) = (x \<notin> A)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(q ?x \<in> V) = (?x \<notin> A)

goal (1 subgoal):
 1. - A = {x. q x \<in> V}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(q ?x \<in> V) = (?x \<notin> A)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(q ?x \<in> V) = (?x \<notin> A)

goal (1 subgoal):
 1. - A = {x. q x \<in> V}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
- A = {x. q x \<in> V}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
- A = {x. q x \<in> V}

goal (1 subgoal):
 1. total_recursive (chf A) \<Longrightarrow> computable A
[PROOF STEP]
from V_ce q_is_pr
[PROOF STATE]
proof (chain)
picking this:
V \<in> ce_sets
q \<in> PrimRec1
[PROOF STEP]
have "{ x. q x \<in> V} \<in> ce_sets"
[PROOF STATE]
proof (prove)
using this:
V \<in> ce_sets
q \<in> PrimRec1

goal (1 subgoal):
 1. {x. q x \<in> V} \<in> ce_sets
[PROOF STEP]
by (rule ce_set_lm_5)
[PROOF STATE]
proof (state)
this:
{x. q x \<in> V} \<in> ce_sets

goal (1 subgoal):
 1. total_recursive (chf A) \<Longrightarrow> computable A
[PROOF STEP]
with CA_eq
[PROOF STATE]
proof (chain)
picking this:
- A = {x. q x \<in> V}
{x. q x \<in> V} \<in> ce_sets
[PROOF STEP]
have CA_ce: "- A \<in> ce_sets"
[PROOF STATE]
proof (prove)
using this:
- A = {x. q x \<in> V}
{x. q x \<in> V} \<in> ce_sets

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

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

goal (1 subgoal):
 1. computable A
[PROOF STEP]
by (simp add: computable_def)
[PROOF STATE]
proof (state)
this:
computable A

goal:
No subgoals!
[PROOF STEP]
qed


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

goal (2 subgoals):
 1. computable A \<Longrightarrow> total_recursive (chf A)
 2. total_recursive (chf A) \<Longrightarrow> computable A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
computable A
[PROOF STEP]
show "total_recursive (chf A)"
[PROOF STATE]
proof (prove)
using this:
computable A

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

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

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

goal (1 subgoal):
 1. computable A
[PROOF STEP]
by (rule tot_rec_impl_comp)
[PROOF STATE]
proof (state)
this:
computable A

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma univ_for_pr_lm: "univ_for_pr (c_pair n x) = (nat_to_pr n) x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. univ_for_pr (c_pair n x) = nat_to_pr n x
[PROOF STEP]
by (simp add: univ_for_pr_def pr_conv_2_to_1_def)


[STATEMENT]
theorem univ_is_ce: "univ_ce \<in> ce_sets"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. univ_ce \<in> ce_sets
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. univ_ce \<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. univ_ce \<in> ce_sets
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
A = c_graph univ_for_pr
[PROOF STEP]
have "A \<in> ce_sets"
[PROOF STATE]
proof (prove)
using this:
A = c_graph univ_for_pr

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

goal (1 subgoal):
 1. univ_ce \<in> ce_sets
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
A \<in> ce_sets
[PROOF STEP]
have "\<exists> pA \<in> PrimRec2. A = fn_to_set pA"
[PROOF STATE]
proof (prove)
using this:
A \<in> ce_sets

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

goal (1 subgoal):
 1. univ_ce \<in> ce_sets
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>pA\<in>PrimRec2. A = fn_to_set pA
[PROOF STEP]
obtain pA where pA_is_pr: "pA \<in> PrimRec2" and S1: "A = fn_to_set pA"
[PROOF STATE]
proof (prove)
using this:
\<exists>pA\<in>PrimRec2. A = fn_to_set pA

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

goal (1 subgoal):
 1. univ_ce \<in> ce_sets
[PROOF STEP]
from S1
[PROOF STATE]
proof (chain)
picking this:
A = fn_to_set pA
[PROOF STEP]
have S2: "A = { x. \<exists> y. pA x y = 0 }"
[PROOF STATE]
proof (prove)
using this:
A = fn_to_set pA

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

goal (1 subgoal):
 1. univ_ce \<in> ce_sets
[PROOF STEP]
define p where "p z y = pA (c_pair (c_pair (c_fst z) (c_pair (c_snd z) (c_fst y))) 0) (c_snd y)"
    for z y
[PROOF STATE]
proof (state)
this:
p ?z ?y = pA (c_pair (c_pair (c_fst ?z) (c_pair (c_snd ?z) (c_fst ?y))) 0) (c_snd ?y)

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

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

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

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

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

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

goal (2 subgoals):
 1. \<exists>n x. z = c_pair n x \<and> x \<in> nat_to_ce_set n \<Longrightarrow> c_snd z \<in> nat_to_ce_set (c_fst z)
 2. c_snd z \<in> nat_to_ce_set (c_fst z) \<Longrightarrow> \<exists>n x. z = c_pair n x \<and> x \<in> nat_to_ce_set n
[PROOF STEP]
from L1
[PROOF STATE]
proof (chain)
picking this:
z = c_pair n x \<and> x \<in> nat_to_ce_set n
[PROOF STEP]
have L2: "z = c_pair n x"
[PROOF STATE]
proof (prove)
using this:
z = c_pair n x \<and> x \<in> nat_to_ce_set n

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

goal (2 subgoals):
 1. \<exists>n x. z = c_pair n x \<and> x \<in> nat_to_ce_set n \<Longrightarrow> c_snd z \<in> nat_to_ce_set (c_fst z)
 2. c_snd z \<in> nat_to_ce_set (c_fst z) \<Longrightarrow> \<exists>n x. z = c_pair n x \<and> x \<in> nat_to_ce_set n
[PROOF STEP]
from L1
[PROOF STATE]
proof (chain)
picking this:
z = c_pair n x \<and> x \<in> nat_to_ce_set n
[PROOF STEP]
have L3: "x \<in> nat_to_ce_set n"
[PROOF STATE]
proof (prove)
using this:
z = c_pair n x \<and> x \<in> nat_to_ce_set n

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

goal (2 subgoals):
 1. \<exists>n x. z = c_pair n x \<and> x \<in> nat_to_ce_set n \<Longrightarrow> c_snd z \<in> nat_to_ce_set (c_fst z)
 2. c_snd z \<in> nat_to_ce_set (c_fst z) \<Longrightarrow> \<exists>n x. z = c_pair n x \<and> x \<in> nat_to_ce_set n
[PROOF STEP]
from L1
[PROOF STATE]
proof (chain)
picking this:
z = c_pair n x \<and> x \<in> nat_to_ce_set n
[PROOF STEP]
have L4: "c_fst z = n"
[PROOF STATE]
proof (prove)
using this:
z = c_pair n x \<and> x \<in> nat_to_ce_set n

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

goal (2 subgoals):
 1. \<exists>n x. z = c_pair n x \<and> x \<in> nat_to_ce_set n \<Longrightarrow> c_snd z \<in> nat_to_ce_set (c_fst z)
 2. c_snd z \<in> nat_to_ce_set (c_fst z) \<Longrightarrow> \<exists>n x. z = c_pair n x \<and> x \<in> nat_to_ce_set n
[PROOF STEP]
from L1
[PROOF STATE]
proof (chain)
picking this:
z = c_pair n x \<and> x \<in> nat_to_ce_set n
[PROOF STEP]
have L5: "c_snd z = x"
[PROOF STATE]
proof (prove)
using this:
z = c_pair n x \<and> x \<in> nat_to_ce_set n

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

goal (2 subgoals):
 1. \<exists>n x. z = c_pair n x \<and> x \<in> nat_to_ce_set n \<Longrightarrow> c_snd z \<in> nat_to_ce_set (c_fst z)
 2. c_snd z \<in> nat_to_ce_set (c_fst z) \<Longrightarrow> \<exists>n x. z = c_pair n x \<and> x \<in> nat_to_ce_set n
[PROOF STEP]
from L3 L4 L5
[PROOF STATE]
proof (chain)
picking this:
x \<in> nat_to_ce_set n
c_fst z = n
c_snd z = x
[PROOF STEP]
show "c_snd z \<in> nat_to_ce_set (c_fst z)"
[PROOF STATE]
proof (prove)
using this:
x \<in> nat_to_ce_set n
c_fst z = n
c_snd z = x

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

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

goal (1 subgoal):
 1. c_snd z \<in> nat_to_ce_set (c_fst z) \<Longrightarrow> \<exists>n x. z = c_pair n x \<and> x \<in> nat_to_ce_set n
[PROOF STEP]
let ?n = "c_fst z"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. c_snd z \<in> nat_to_ce_set (c_fst z) \<Longrightarrow> \<exists>n x. z = c_pair n x \<and> x \<in> nat_to_ce_set n
[PROOF STEP]
let ?x = "c_snd z"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. c_snd z \<in> nat_to_ce_set (c_fst z) \<Longrightarrow> \<exists>n x. z = c_pair n x \<and> x \<in> nat_to_ce_set n
[PROOF STEP]
have L1: "z = c_pair ?n ?x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. z = c_pair (c_fst z) (c_snd z)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
z = c_pair (c_fst z) (c_snd z)

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

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

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

goal (1 subgoal):
 1. \<exists>n x. z = c_pair n x \<and> x \<in> nat_to_ce_set n
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>n x. z = c_pair n x \<and> x \<in> nat_to_ce_set n

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

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

goal (1 subgoal):
 1. univ_ce \<in> ce_sets
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<exists>n x. ?z = c_pair n x \<and> x \<in> nat_to_ce_set n) = (c_snd ?z \<in> nat_to_ce_set (c_fst ?z))
[PROOF STEP]
have "{ c_pair n x | n x. x \<in> nat_to_ce_set n } = { z. c_snd z \<in> nat_to_ce_set (c_fst z)}"
[PROOF STATE]
proof (prove)
using this:
(\<exists>n x. ?z = c_pair n x \<and> x \<in> nat_to_ce_set n) = (c_snd ?z \<in> nat_to_ce_set (c_fst ?z))

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

goal (1 subgoal):
 1. univ_ce \<in> ce_sets
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
{c_pair n x |n x. x \<in> nat_to_ce_set n} = {z. c_snd z \<in> nat_to_ce_set (c_fst z)}
[PROOF STEP]
have S3: "univ_ce  = { z. c_snd z \<in> nat_to_ce_set (c_fst z)}"
[PROOF STATE]
proof (prove)
using this:
{c_pair n x |n x. x \<in> nat_to_ce_set n} = {z. c_snd z \<in> nat_to_ce_set (c_fst z)}

goal (1 subgoal):
 1. univ_ce = {z. c_snd z \<in> nat_to_ce_set (c_fst z)}
[PROOF STEP]
by (simp add: univ_ce_def)
[PROOF STATE]
proof (state)
this:
univ_ce = {z. c_snd z \<in> nat_to_ce_set (c_fst z)}

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

goal (2 subgoals):
 1. c_snd z \<in> nat_to_ce_set (c_fst z) \<Longrightarrow> \<exists>y. p z y = 0
 2. \<exists>y. p z y = 0 \<Longrightarrow> c_snd z \<in> nat_to_ce_set (c_fst z)
[PROOF STEP]
have "nat_to_ce_set (c_fst z) = { x . \<exists> y. (nat_to_pr (c_fst z)) (c_pair x y) = 0 }"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nat_to_ce_set (c_fst z) = {x. \<exists>y. nat_to_pr (c_fst z) (c_pair x y) = 0}
[PROOF STEP]
by (simp add: nat_to_ce_set_lm_1)
[PROOF STATE]
proof (state)
this:
nat_to_ce_set (c_fst z) = {x. \<exists>y. nat_to_pr (c_fst z) (c_pair x y) = 0}

goal (2 subgoals):
 1. c_snd z \<in> nat_to_ce_set (c_fst z) \<Longrightarrow> \<exists>y. p z y = 0
 2. \<exists>y. p z y = 0 \<Longrightarrow> c_snd z \<in> nat_to_ce_set (c_fst z)
[PROOF STEP]
with A
[PROOF STATE]
proof (chain)
picking this:
c_snd z \<in> nat_to_ce_set (c_fst z)
nat_to_ce_set (c_fst z) = {x. \<exists>y. nat_to_pr (c_fst z) (c_pair x y) = 0}
[PROOF STEP]
obtain u where S4_1: "(nat_to_pr (c_fst z)) (c_pair (c_snd z) u) = 0"
[PROOF STATE]
proof (prove)
using this:
c_snd z \<in> nat_to_ce_set (c_fst z)
nat_to_ce_set (c_fst z) = {x. \<exists>y. nat_to_pr (c_fst z) (c_pair x y) = 0}

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

goal (2 subgoals):
 1. c_snd z \<in> nat_to_ce_set (c_fst z) \<Longrightarrow> \<exists>y. p z y = 0
 2. \<exists>y. p z y = 0 \<Longrightarrow> c_snd z \<in> nat_to_ce_set (c_fst z)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
nat_to_pr (c_fst z) (c_pair (c_snd z) u) = 0
[PROOF STEP]
have S4_2: "univ_for_pr (c_pair (c_fst z) (c_pair (c_snd z) u)) = 0"
[PROOF STATE]
proof (prove)
using this:
nat_to_pr (c_fst z) (c_pair (c_snd z) u) = 0

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

goal (2 subgoals):
 1. c_snd z \<in> nat_to_ce_set (c_fst z) \<Longrightarrow> \<exists>y. p z y = 0
 2. \<exists>y. p z y = 0 \<Longrightarrow> c_snd z \<in> nat_to_ce_set (c_fst z)
[PROOF STEP]
from A_def
[PROOF STATE]
proof (chain)
picking this:
A = c_graph univ_for_pr
[PROOF STEP]
have S4_3: "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 (2 subgoals):
 1. c_snd z \<in> nat_to_ce_set (c_fst z) \<Longrightarrow> \<exists>y. p z y = 0
 2. \<exists>y. p z y = 0 \<Longrightarrow> c_snd z \<in> nat_to_ce_set (c_fst z)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
A = {c_pair x (univ_for_pr x) |x. x \<in> UNIV}
[PROOF STEP]
have S4_4: "\<And> x. c_pair x (univ_for_pr x) \<in> A"
[PROOF STATE]
proof (prove)
using this:
A = {c_pair x (univ_for_pr x) |x. x \<in> UNIV}

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

goal (2 subgoals):
 1. c_snd z \<in> nat_to_ce_set (c_fst z) \<Longrightarrow> \<exists>y. p z y = 0
 2. \<exists>y. p z y = 0 \<Longrightarrow> c_snd z \<in> nat_to_ce_set (c_fst z)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
c_pair ?x (univ_for_pr ?x) \<in> A
[PROOF STEP]
have "c_pair (c_pair (c_fst z) (c_pair (c_snd z) u)) (univ_for_pr (c_pair (c_fst z) (c_pair (c_snd z) u))) \<in> A"
[PROOF STATE]
proof (prove)
using this:
c_pair ?x (univ_for_pr ?x) \<in> A

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

goal (2 subgoals):
 1. c_snd z \<in> nat_to_ce_set (c_fst z) \<Longrightarrow> \<exists>y. p z y = 0
 2. \<exists>y. p z y = 0 \<Longrightarrow> c_snd z \<in> nat_to_ce_set (c_fst z)
[PROOF STEP]
with S4_2
[PROOF STATE]
proof (chain)
picking this:
univ_for_pr (c_pair (c_fst z) (c_pair (c_snd z) u)) = 0
c_pair (c_pair (c_fst z) (c_pair (c_snd z) u)) (univ_for_pr (c_pair (c_fst z) (c_pair (c_snd z) u))) \<in> A
[PROOF STEP]
have S4_5: "c_pair (c_pair (c_fst z) (c_pair (c_snd z) u)) 0 \<in> A"
[PROOF STATE]
proof (prove)
using this:
univ_for_pr (c_pair (c_fst z) (c_pair (c_snd z) u)) = 0
c_pair (c_pair (c_fst z) (c_pair (c_snd z) u)) (univ_for_pr (c_pair (c_fst z) (c_pair (c_snd z) u))) \<in> A

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

goal (2 subgoals):
 1. c_snd z \<in> nat_to_ce_set (c_fst z) \<Longrightarrow> \<exists>y. p z y = 0
 2. \<exists>y. p z y = 0 \<Longrightarrow> c_snd z \<in> nat_to_ce_set (c_fst z)
[PROOF STEP]
with S2
[PROOF STATE]
proof (chain)
picking this:
A = {x. \<exists>y. pA x y = 0}
c_pair (c_pair (c_fst z) (c_pair (c_snd z) u)) 0 \<in> A
[PROOF STEP]
obtain v where S4_6: "pA (c_pair (c_pair (c_fst z) (c_pair (c_snd z) u)) 0) v = 0"
[PROOF STATE]
proof (prove)
using this:
A = {x. \<exists>y. pA x y = 0}
c_pair (c_pair (c_fst z) (c_pair (c_snd z) u)) 0 \<in> A

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

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

goal (2 subgoals):
 1. c_snd z \<in> nat_to_ce_set (c_fst z) \<Longrightarrow> \<exists>y. p z y = 0
 2. \<exists>y. p z y = 0 \<Longrightarrow> c_snd z \<in> nat_to_ce_set (c_fst z)
[PROOF STEP]
from y_def
[PROOF STATE]
proof (chain)
picking this:
y = c_pair u v
[PROOF STEP]
have S4_7: "u = c_fst y"
[PROOF STATE]
proof (prove)
using this:
y = c_pair u v

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

goal (2 subgoals):
 1. c_snd z \<in> nat_to_ce_set (c_fst z) \<Longrightarrow> \<exists>y. p z y = 0
 2. \<exists>y. p z y = 0 \<Longrightarrow> c_snd z \<in> nat_to_ce_set (c_fst z)
[PROOF STEP]
from y_def
[PROOF STATE]
proof (chain)
picking this:
y = c_pair u v
[PROOF STEP]
have S4_8: "v = c_snd y"
[PROOF STATE]
proof (prove)
using this:
y = c_pair u v

goal (1 subgoal):
 1. v = c_snd y
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
v = c_snd y

goal (2 subgoals):
 1. c_snd z \<in> nat_to_ce_set (c_fst z) \<Longrightarrow> \<exists>y. p z y = 0
 2. \<exists>y. p z y = 0 \<Longrightarrow> c_snd z \<in> nat_to_ce_set (c_fst z)
[PROOF STEP]
from S4_6 S4_7 S4_8 p_def
[PROOF STATE]
proof (chain)
picking this:
pA (c_pair (c_pair (c_fst z) (c_pair (c_snd z) u)) 0) v = 0
u = c_fst y
v = c_snd y
p ?z ?y = pA (c_pair (c_pair (c_fst ?z) (c_pair (c_snd ?z) (c_fst ?y))) 0) (c_snd ?y)
[PROOF STEP]
have "p z y = 0"
[PROOF STATE]
proof (prove)
using this:
pA (c_pair (c_pair (c_fst z) (c_pair (c_snd z) u)) 0) v = 0
u = c_fst y
v = c_snd y
p ?z ?y = pA (c_pair (c_pair (c_fst ?z) (c_pair (c_snd ?z) (c_fst ?y))) 0) (c_snd ?y)

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

goal (2 subgoals):
 1. c_snd z \<in> nat_to_ce_set (c_fst z) \<Longrightarrow> \<exists>y. p z y = 0
 2. \<exists>y. p z y = 0 \<Longrightarrow> c_snd z \<in> nat_to_ce_set (c_fst z)
[PROOF STEP]
thus "\<exists> y. p z y = 0"
[PROOF STATE]
proof (prove)
using this:
p z y = 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> c_snd z \<in> nat_to_ce_set (c_fst z)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>y. p z y = 0 \<Longrightarrow> c_snd z \<in> nat_to_ce_set (c_fst 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> c_snd z \<in> nat_to_ce_set (c_fst z)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>y. p z y = 0
[PROOF STEP]
obtain y where S4_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> c_snd z \<in> nat_to_ce_set (c_fst z)
[PROOF STEP]
from S4_1 p_def
[PROOF STATE]
proof (chain)
picking this:
p z y = 0
p ?z ?y = pA (c_pair (c_pair (c_fst ?z) (c_pair (c_snd ?z) (c_fst ?y))) 0) (c_snd ?y)
[PROOF STEP]
have S4_2: "pA (c_pair (c_pair (c_fst z) (c_pair (c_snd z) (c_fst y))) 0) (c_snd y) = 0"
[PROOF STATE]
proof (prove)
using this:
p z y = 0
p ?z ?y = pA (c_pair (c_pair (c_fst ?z) (c_pair (c_snd ?z) (c_fst ?y))) 0) (c_snd ?y)

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

goal (1 subgoal):
 1. \<exists>y. p z y = 0 \<Longrightarrow> c_snd z \<in> nat_to_ce_set (c_fst z)
[PROOF STEP]
with S2
[PROOF STATE]
proof (chain)
picking this:
A = {x. \<exists>y. pA x y = 0}
pA (c_pair (c_pair (c_fst z) (c_pair (c_snd z) (c_fst y))) 0) (c_snd y) = 0
[PROOF STEP]
have S4_3: "c_pair (c_pair (c_fst z) (c_pair (c_snd z) (c_fst y))) 0 \<in> A"
[PROOF STATE]
proof (prove)
using this:
A = {x. \<exists>y. pA x y = 0}
pA (c_pair (c_pair (c_fst z) (c_pair (c_snd z) (c_fst y))) 0) (c_snd y) = 0

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

goal (1 subgoal):
 1. \<exists>y. p z y = 0 \<Longrightarrow> c_snd z \<in> nat_to_ce_set (c_fst z)
[PROOF STEP]
with A_def
[PROOF STATE]
proof (chain)
picking this:
A = c_graph univ_for_pr
c_pair (c_pair (c_fst z) (c_pair (c_snd z) (c_fst y))) 0 \<in> A
[PROOF STEP]
have "c_pair (c_pair (c_fst z) (c_pair (c_snd z) (c_fst y))) 0 \<in> c_graph univ_for_pr"
[PROOF STATE]
proof (prove)
using this:
A = c_graph univ_for_pr
c_pair (c_pair (c_fst z) (c_pair (c_snd z) (c_fst y))) 0 \<in> A

goal (1 subgoal):
 1. c_pair (c_pair (c_fst z) (c_pair (c_snd z) (c_fst y))) 0 \<in> c_graph univ_for_pr
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
c_pair (c_pair (c_fst z) (c_pair (c_snd z) (c_fst y))) 0 \<in> c_graph univ_for_pr

goal (1 subgoal):
 1. \<exists>y. p z y = 0 \<Longrightarrow> c_snd z \<in> nat_to_ce_set (c_fst z)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
c_pair (c_pair (c_fst z) (c_pair (c_snd z) (c_fst y))) 0 \<in> c_graph univ_for_pr
[PROOF STEP]
have S4_4: "0 = univ_for_pr (c_pair (c_fst z) (c_pair (c_snd z) (c_fst y)))"
[PROOF STATE]
proof (prove)
using this:
c_pair (c_pair (c_fst z) (c_pair (c_snd z) (c_fst y))) 0 \<in> c_graph univ_for_pr

goal (1 subgoal):
 1. 0 = univ_for_pr (c_pair (c_fst z) (c_pair (c_snd z) (c_fst y)))
[PROOF STEP]
by (rule c_graph_lm_1)
[PROOF STATE]
proof (state)
this:
0 = univ_for_pr (c_pair (c_fst z) (c_pair (c_snd z) (c_fst y)))

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

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

goal (1 subgoal):
 1. \<exists>y. p z y = 0 \<Longrightarrow> c_snd z \<in> nat_to_ce_set (c_fst z)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
univ_for_pr (c_pair (c_fst z) (c_pair (c_snd z) (c_fst y))) = 0
[PROOF STEP]
have S4_6: "(nat_to_pr (c_fst z)) (c_pair (c_snd z) (c_fst y)) = 0"
[PROOF STATE]
proof (prove)
using this:
univ_for_pr (c_pair (c_fst z) (c_pair (c_snd z) (c_fst y))) = 0

goal (1 subgoal):
 1. nat_to_pr (c_fst z) (c_pair (c_snd z) (c_fst y)) = 0
[PROOF STEP]
by (simp add: univ_for_pr_lm)
[PROOF STATE]
proof (state)
this:
nat_to_pr (c_fst z) (c_pair (c_snd z) (c_fst y)) = 0

goal (1 subgoal):
 1. \<exists>y. p z y = 0 \<Longrightarrow> c_snd z \<in> nat_to_ce_set (c_fst z)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
nat_to_pr (c_fst z) (c_pair (c_snd z) (c_fst y)) = 0
[PROOF STEP]
have S4_7: "\<exists> y. (nat_to_pr (c_fst z)) (c_pair (c_snd z) y) = 0"
[PROOF STATE]
proof (prove)
using this:
nat_to_pr (c_fst z) (c_pair (c_snd z) (c_fst y)) = 0

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

goal (1 subgoal):
 1. \<exists>y. p z y = 0 \<Longrightarrow> c_snd z \<in> nat_to_ce_set (c_fst z)
[PROOF STEP]
have S4_8: "nat_to_ce_set (c_fst z) = { x . \<exists> y. (nat_to_pr (c_fst z)) (c_pair x y) = 0 }"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nat_to_ce_set (c_fst z) = {x. \<exists>y. nat_to_pr (c_fst z) (c_pair x y) = 0}
[PROOF STEP]
by (simp add: nat_to_ce_set_lm_1)
[PROOF STATE]
proof (state)
this:
nat_to_ce_set (c_fst z) = {x. \<exists>y. nat_to_pr (c_fst z) (c_pair x y) = 0}

goal (1 subgoal):
 1. \<exists>y. p z y = 0 \<Longrightarrow> c_snd z \<in> nat_to_ce_set (c_fst z)
[PROOF STEP]
from S4_7
[PROOF STATE]
proof (chain)
picking this:
\<exists>y. nat_to_pr (c_fst z) (c_pair (c_snd z) y) = 0
[PROOF STEP]
have S4_9: "c_snd z \<in> { x . \<exists> y. (nat_to_pr (c_fst z)) (c_pair x y) = 0 }"
[PROOF STATE]
proof (prove)
using this:
\<exists>y. nat_to_pr (c_fst z) (c_pair (c_snd z) y) = 0

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

goal (1 subgoal):
 1. \<exists>y. p z y = 0 \<Longrightarrow> c_snd z \<in> nat_to_ce_set (c_fst z)
[PROOF STEP]
with S4_8
[PROOF STATE]
proof (chain)
picking this:
nat_to_ce_set (c_fst z) = {x. \<exists>y. nat_to_pr (c_fst z) (c_pair x y) = 0}
c_snd z \<in> {x. \<exists>y. nat_to_pr (c_fst z) (c_pair x y) = 0}
[PROOF STEP]
show "c_snd z \<in> nat_to_ce_set (c_fst z)"
[PROOF STATE]
proof (prove)
using this:
nat_to_ce_set (c_fst z) = {x. \<exists>y. nat_to_pr (c_fst z) (c_pair x y) = 0}
c_snd z \<in> {x. \<exists>y. nat_to_pr (c_fst z) (c_pair x y) = 0}

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

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

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

goal (1 subgoal):
 1. univ_ce \<in> ce_sets
[PROOF STEP]
with S3
[PROOF STATE]
proof (chain)
picking this:
univ_ce = {z. c_snd z \<in> nat_to_ce_set (c_fst z)}
(c_snd ?z \<in> nat_to_ce_set (c_fst ?z)) = (\<exists>y. p ?z y = 0)
[PROOF STEP]
have "univ_ce = {z. \<exists> y. p z y = 0}"
[PROOF STATE]
proof (prove)
using this:
univ_ce = {z. c_snd z \<in> nat_to_ce_set (c_fst z)}
(c_snd ?z \<in> nat_to_ce_set (c_fst ?z)) = (\<exists>y. p ?z y = 0)

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

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

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

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

goal (1 subgoal):
 1. univ_ce \<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. univ_ce \<in> ce_sets
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
univ_ce = fn_to_set p
fn_to_set p \<in> ce_sets
[PROOF STEP]
show "univ_ce \<in> ce_sets"
[PROOF STATE]
proof (prove)
using this:
univ_ce = fn_to_set p
fn_to_set p \<in> ce_sets

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma univ_ce_lm_1: "(c_pair n x \<in> univ_ce) = (x \<in> nat_to_ce_set n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (c_pair n x \<in> univ_ce) = (x \<in> nat_to_ce_set n)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (c_pair n x \<in> univ_ce) = (x \<in> nat_to_ce_set n)
[PROOF STEP]
from univ_ce_def
[PROOF STATE]
proof (chain)
picking this:
univ_ce = {c_pair n x |n x. x \<in> nat_to_ce_set n}
[PROOF STEP]
have S1: "univ_ce = {z . \<exists> n x. z = c_pair n x \<and> x \<in> nat_to_ce_set n}"
[PROOF STATE]
proof (prove)
using this:
univ_ce = {c_pair n x |n x. x \<in> nat_to_ce_set n}

goal (1 subgoal):
 1. univ_ce = {c_pair n x |n x. x \<in> nat_to_ce_set n}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
univ_ce = {c_pair n x |n x. x \<in> nat_to_ce_set n}

goal (1 subgoal):
 1. (c_pair n x \<in> univ_ce) = (x \<in> nat_to_ce_set n)
[PROOF STEP]
have S2: "(\<exists> n1 x1. c_pair n x = c_pair n1 x1 \<and> x1 \<in> nat_to_ce_set n1) = (x \<in> nat_to_ce_set n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>n1 x1. c_pair n x = c_pair n1 x1 \<and> x1 \<in> nat_to_ce_set n1) = (x \<in> nat_to_ce_set n)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<exists>n1 x1. c_pair n x = c_pair n1 x1 \<and> x1 \<in> nat_to_ce_set n1 \<Longrightarrow> x \<in> nat_to_ce_set n
 2. x \<in> nat_to_ce_set n \<Longrightarrow> \<exists>n1 x1. c_pair n x = c_pair n1 x1 \<and> x1 \<in> nat_to_ce_set n1
[PROOF STEP]
assume "\<exists>n1 x1. c_pair n x = c_pair n1 x1 \<and> x1 \<in> nat_to_ce_set n1"
[PROOF STATE]
proof (state)
this:
\<exists>n1 x1. c_pair n x = c_pair n1 x1 \<and> x1 \<in> nat_to_ce_set n1

goal (2 subgoals):
 1. \<exists>n1 x1. c_pair n x = c_pair n1 x1 \<and> x1 \<in> nat_to_ce_set n1 \<Longrightarrow> x \<in> nat_to_ce_set n
 2. x \<in> nat_to_ce_set n \<Longrightarrow> \<exists>n1 x1. c_pair n x = c_pair n1 x1 \<and> x1 \<in> nat_to_ce_set n1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>n1 x1. c_pair n x = c_pair n1 x1 \<and> x1 \<in> nat_to_ce_set n1
[PROOF STEP]
obtain n1 x1 where L1: "c_pair n x = c_pair n1 x1" and L2: "x1 \<in> nat_to_ce_set n1"
[PROOF STATE]
proof (prove)
using this:
\<exists>n1 x1. c_pair n x = c_pair n1 x1 \<and> x1 \<in> nat_to_ce_set n1

goal (1 subgoal):
 1. (\<And>n1 x1. \<lbrakk>c_pair n x = c_pair n1 x1; x1 \<in> nat_to_ce_set n1\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
c_pair n x = c_pair n1 x1
x1 \<in> nat_to_ce_set n1

goal (2 subgoals):
 1. \<exists>n1 x1. c_pair n x = c_pair n1 x1 \<and> x1 \<in> nat_to_ce_set n1 \<Longrightarrow> x \<in> nat_to_ce_set n
 2. x \<in> nat_to_ce_set n \<Longrightarrow> \<exists>n1 x1. c_pair n x = c_pair n1 x1 \<and> x1 \<in> nat_to_ce_set n1
[PROOF STEP]
from L1
[PROOF STATE]
proof (chain)
picking this:
c_pair n x = c_pair n1 x1
[PROOF STEP]
have L3: "n = n1"
[PROOF STATE]
proof (prove)
using this:
c_pair n x = c_pair n1 x1

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

goal (2 subgoals):
 1. \<exists>n1 x1. c_pair n x = c_pair n1 x1 \<and> x1 \<in> nat_to_ce_set n1 \<Longrightarrow> x \<in> nat_to_ce_set n
 2. x \<in> nat_to_ce_set n \<Longrightarrow> \<exists>n1 x1. c_pair n x = c_pair n1 x1 \<and> x1 \<in> nat_to_ce_set n1
[PROOF STEP]
from L1
[PROOF STATE]
proof (chain)
picking this:
c_pair n x = c_pair n1 x1
[PROOF STEP]
have L4: "x = x1"
[PROOF STATE]
proof (prove)
using this:
c_pair n x = c_pair n1 x1

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

goal (2 subgoals):
 1. \<exists>n1 x1. c_pair n x = c_pair n1 x1 \<and> x1 \<in> nat_to_ce_set n1 \<Longrightarrow> x \<in> nat_to_ce_set n
 2. x \<in> nat_to_ce_set n \<Longrightarrow> \<exists>n1 x1. c_pair n x = c_pair n1 x1 \<and> x1 \<in> nat_to_ce_set n1
[PROOF STEP]
from L2 L3 L4
[PROOF STATE]
proof (chain)
picking this:
x1 \<in> nat_to_ce_set n1
n = n1
x = x1
[PROOF STEP]
show "x \<in> nat_to_ce_set n"
[PROOF STATE]
proof (prove)
using this:
x1 \<in> nat_to_ce_set n1
n = n1
x = x1

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

goal (1 subgoal):
 1. x \<in> nat_to_ce_set n \<Longrightarrow> \<exists>n1 x1. c_pair n x = c_pair n1 x1 \<and> x1 \<in> nat_to_ce_set n1
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<in> nat_to_ce_set n \<Longrightarrow> \<exists>n1 x1. c_pair n x = c_pair n1 x1 \<and> x1 \<in> nat_to_ce_set n1
[PROOF STEP]
assume A: "x \<in> nat_to_ce_set n"
[PROOF STATE]
proof (state)
this:
x \<in> nat_to_ce_set n

goal (1 subgoal):
 1. x \<in> nat_to_ce_set n \<Longrightarrow> \<exists>n1 x1. c_pair n x = c_pair n1 x1 \<and> x1 \<in> nat_to_ce_set n1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> nat_to_ce_set n
[PROOF STEP]
have "c_pair n x = c_pair n x \<and> x \<in> nat_to_ce_set n"
[PROOF STATE]
proof (prove)
using this:
x \<in> nat_to_ce_set n

goal (1 subgoal):
 1. c_pair n x = c_pair n x \<and> x \<in> nat_to_ce_set n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
c_pair n x = c_pair n x \<and> x \<in> nat_to_ce_set n

goal (1 subgoal):
 1. x \<in> nat_to_ce_set n \<Longrightarrow> \<exists>n1 x1. c_pair n x = c_pair n1 x1 \<and> x1 \<in> nat_to_ce_set n1
[PROOF STEP]
thus "\<exists> n1 x1. c_pair n x = c_pair n1 x1 \<and> x1 \<in> nat_to_ce_set n1"
[PROOF STATE]
proof (prove)
using this:
c_pair n x = c_pair n x \<and> x \<in> nat_to_ce_set n

goal (1 subgoal):
 1. \<exists>n1 x1. c_pair n x = c_pair n1 x1 \<and> x1 \<in> nat_to_ce_set n1
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>n1 x1. c_pair n x = c_pair n1 x1 \<and> x1 \<in> nat_to_ce_set n1

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<exists>n1 x1. c_pair n x = c_pair n1 x1 \<and> x1 \<in> nat_to_ce_set n1) = (x \<in> nat_to_ce_set n)

goal (1 subgoal):
 1. (c_pair n x \<in> univ_ce) = (x \<in> nat_to_ce_set n)
[PROOF STEP]
with S1
[PROOF STATE]
proof (chain)
picking this:
univ_ce = {c_pair n x |n x. x \<in> nat_to_ce_set n}
(\<exists>n1 x1. c_pair n x = c_pair n1 x1 \<and> x1 \<in> nat_to_ce_set n1) = (x \<in> nat_to_ce_set n)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
univ_ce = {c_pair n x |n x. x \<in> nat_to_ce_set n}
(\<exists>n1 x1. c_pair n x = c_pair n1 x1 \<and> x1 \<in> nat_to_ce_set n1) = (x \<in> nat_to_ce_set n)

goal (1 subgoal):
 1. (c_pair n x \<in> univ_ce) = (x \<in> nat_to_ce_set n)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(c_pair n x \<in> univ_ce) = (x \<in> nat_to_ce_set n)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem univ_ce_is_not_comp1: "- univ_ce \<notin> ce_sets"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - univ_ce \<notin> ce_sets
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> - univ_ce \<notin> ce_sets \<Longrightarrow> False
[PROOF STEP]
assume "\<not> - univ_ce \<notin> ce_sets"
[PROOF STATE]
proof (state)
this:
\<not> - univ_ce \<notin> ce_sets

goal (1 subgoal):
 1. \<not> - univ_ce \<notin> ce_sets \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> - univ_ce \<notin> ce_sets
[PROOF STEP]
have A: "- univ_ce \<in> ce_sets"
[PROOF STATE]
proof (prove)
using this:
\<not> - univ_ce \<notin> ce_sets

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

goal (1 subgoal):
 1. \<not> - univ_ce \<notin> ce_sets \<Longrightarrow> False
[PROOF STEP]
define p where "p x = c_pair x x" for x
[PROOF STATE]
proof (state)
this:
p ?x = c_pair ?x ?x

goal (1 subgoal):
 1. \<not> - univ_ce \<notin> ce_sets \<Longrightarrow> False
[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 x) \<in> PrimRec1
[PROOF STEP]
by prec
[PROOF STATE]
proof (state)
this:
p \<in> PrimRec1

goal (1 subgoal):
 1. \<not> - univ_ce \<notin> ce_sets \<Longrightarrow> False
[PROOF STEP]
define A where "A = { x. p x \<in> - univ_ce }"
[PROOF STATE]
proof (state)
this:
A = {x. p x \<in> - univ_ce}

goal (1 subgoal):
 1. \<not> - univ_ce \<notin> ce_sets \<Longrightarrow> False
[PROOF STEP]
from A p_is_pr
[PROOF STATE]
proof (chain)
picking this:
- univ_ce \<in> ce_sets
p \<in> PrimRec1
[PROOF STEP]
have "{ x. p x \<in> - univ_ce } \<in> ce_sets"
[PROOF STATE]
proof (prove)
using this:
- univ_ce \<in> ce_sets
p \<in> PrimRec1

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

goal (1 subgoal):
 1. \<not> - univ_ce \<notin> ce_sets \<Longrightarrow> False
[PROOF STEP]
with A_def
[PROOF STATE]
proof (chain)
picking this:
A = {x. p x \<in> - univ_ce}
{x. p x \<in> - univ_ce} \<in> ce_sets
[PROOF STEP]
have S1: "A \<in> ce_sets"
[PROOF STATE]
proof (prove)
using this:
A = {x. p x \<in> - univ_ce}
{x. p x \<in> - univ_ce} \<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. \<not> - univ_ce \<notin> ce_sets \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
A \<in> ce_sets
[PROOF STEP]
have "\<exists> n. A = nat_to_ce_set n"
[PROOF STATE]
proof (prove)
using this:
A \<in> ce_sets

goal (1 subgoal):
 1. \<exists>n. A = nat_to_ce_set n
[PROOF STEP]
by (rule nat_to_ce_set_srj)
[PROOF STATE]
proof (state)
this:
\<exists>n. A = nat_to_ce_set n

goal (1 subgoal):
 1. \<not> - univ_ce \<notin> ce_sets \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>n. A = nat_to_ce_set n
[PROOF STEP]
obtain n where S2: "A = nat_to_ce_set n"
[PROOF STATE]
proof (prove)
using this:
\<exists>n. A = nat_to_ce_set n

goal (1 subgoal):
 1. (\<And>n. A = nat_to_ce_set n \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
A = nat_to_ce_set n

goal (1 subgoal):
 1. \<not> - univ_ce \<notin> ce_sets \<Longrightarrow> False
[PROOF STEP]
from A_def
[PROOF STATE]
proof (chain)
picking this:
A = {x. p x \<in> - univ_ce}
[PROOF STEP]
have "(n \<in> A) = (p n \<in> - univ_ce)"
[PROOF STATE]
proof (prove)
using this:
A = {x. p x \<in> - univ_ce}

goal (1 subgoal):
 1. (n \<in> A) = (p n \<in> - univ_ce)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(n \<in> A) = (p n \<in> - univ_ce)

goal (1 subgoal):
 1. \<not> - univ_ce \<notin> ce_sets \<Longrightarrow> False
[PROOF STEP]
with p_def
[PROOF STATE]
proof (chain)
picking this:
p ?x = c_pair ?x ?x
(n \<in> A) = (p n \<in> - univ_ce)
[PROOF STEP]
have "(n \<in> A) = (c_pair n n \<notin> univ_ce)"
[PROOF STATE]
proof (prove)
using this:
p ?x = c_pair ?x ?x
(n \<in> A) = (p n \<in> - univ_ce)

goal (1 subgoal):
 1. (n \<in> A) = (c_pair n n \<notin> univ_ce)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(n \<in> A) = (c_pair n n \<notin> univ_ce)

goal (1 subgoal):
 1. \<not> - univ_ce \<notin> ce_sets \<Longrightarrow> False
[PROOF STEP]
with univ_ce_def univ_ce_lm_1
[PROOF STATE]
proof (chain)
picking this:
univ_ce = {c_pair n x |n x. x \<in> nat_to_ce_set n}
(c_pair ?n ?x \<in> univ_ce) = (?x \<in> nat_to_ce_set ?n)
(n \<in> A) = (c_pair n n \<notin> univ_ce)
[PROOF STEP]
have "(n \<in> A) = (n \<notin> nat_to_ce_set n)"
[PROOF STATE]
proof (prove)
using this:
univ_ce = {c_pair n x |n x. x \<in> nat_to_ce_set n}
(c_pair ?n ?x \<in> univ_ce) = (?x \<in> nat_to_ce_set ?n)
(n \<in> A) = (c_pair n n \<notin> univ_ce)

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

goal (1 subgoal):
 1. \<not> - univ_ce \<notin> ce_sets \<Longrightarrow> False
[PROOF STEP]
with S2
[PROOF STATE]
proof (chain)
picking this:
A = nat_to_ce_set n
(n \<in> A) = (n \<notin> nat_to_ce_set n)
[PROOF STEP]
have "(n \<in> A) = (n \<notin> A)"
[PROOF STATE]
proof (prove)
using this:
A = nat_to_ce_set n
(n \<in> A) = (n \<notin> nat_to_ce_set n)

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

goal (1 subgoal):
 1. \<not> - univ_ce \<notin> ce_sets \<Longrightarrow> False
[PROOF STEP]
thus False
[PROOF STATE]
proof (prove)
using this:
(n \<in> A) = (n \<notin> A)

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem univ_ce_is_not_comp2: "\<not> total_recursive (chf univ_ce)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> total_recursive (chf univ_ce)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. total_recursive (chf univ_ce) \<Longrightarrow> False
[PROOF STEP]
assume "total_recursive (chf univ_ce)"
[PROOF STATE]
proof (state)
this:
total_recursive (chf univ_ce)

goal (1 subgoal):
 1. total_recursive (chf univ_ce) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
total_recursive (chf univ_ce)
[PROOF STEP]
have "computable univ_ce"
[PROOF STATE]
proof (prove)
using this:
total_recursive (chf univ_ce)

goal (1 subgoal):
 1. computable univ_ce
[PROOF STEP]
by (rule tot_rec_impl_comp)
[PROOF STATE]
proof (state)
this:
computable univ_ce

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

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

goal (1 subgoal):
 1. total_recursive (chf univ_ce) \<Longrightarrow> False
[PROOF STEP]
with univ_ce_is_not_comp1
[PROOF STATE]
proof (chain)
picking this:
- univ_ce \<notin> ce_sets
- univ_ce \<in> ce_sets
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
- univ_ce \<notin> ce_sets
- univ_ce \<in> ce_sets

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem univ_ce_is_not_comp3: "\<not> computable univ_ce"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> computable univ_ce
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> \<not> computable univ_ce \<Longrightarrow> False
[PROOF STEP]
assume "\<not> \<not> computable univ_ce"
[PROOF STATE]
proof (state)
this:
\<not> \<not> computable univ_ce

goal (1 subgoal):
 1. \<not> \<not> computable univ_ce \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> \<not> computable univ_ce
[PROOF STEP]
have "computable univ_ce"
[PROOF STATE]
proof (prove)
using this:
\<not> \<not> computable univ_ce

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

goal (1 subgoal):
 1. \<not> \<not> computable univ_ce \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
computable univ_ce
[PROOF STEP]
have "total_recursive (chf univ_ce)"
[PROOF STATE]
proof (prove)
using this:
computable univ_ce

goal (1 subgoal):
 1. total_recursive (chf univ_ce)
[PROOF STEP]
by (rule comp_impl_tot_rec)
[PROOF STATE]
proof (state)
this:
total_recursive (chf univ_ce)

goal (1 subgoal):
 1. \<not> \<not> computable univ_ce \<Longrightarrow> False
[PROOF STEP]
with univ_ce_is_not_comp2
[PROOF STATE]
proof (chain)
picking this:
\<not> total_recursive (chf univ_ce)
total_recursive (chf univ_ce)
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
\<not> total_recursive (chf univ_ce)
total_recursive (chf univ_ce)

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma index_of_r_to_l_lm: "nat_to_pr index_of_r_to_l (c_pair x (c_pair y z)) = c_pair (c_pair x y) z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nat_to_pr index_of_r_to_l (c_pair x (c_pair y z)) = c_pair (c_pair x y) z
[PROOF STEP]
apply(unfold index_of_r_to_l_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nat_to_pr (pair_by_index (pair_by_index index_of_c_fst (comp_by_index index_of_c_fst index_of_c_snd)) (comp_by_index index_of_c_snd index_of_c_snd)) (c_pair x (c_pair y z)) = c_pair (c_pair x y) z
[PROOF STEP]
apply(simp add: pair_by_index_main)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c_f_pair (c_f_pair (nat_to_pr index_of_c_fst) (nat_to_pr (comp_by_index index_of_c_fst index_of_c_snd))) (nat_to_pr (comp_by_index index_of_c_snd index_of_c_snd)) (c_pair x (c_pair y z)) = c_pair (c_pair x y) z
[PROOF STEP]
apply(unfold c_f_pair_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c_pair (c_pair (nat_to_pr index_of_c_fst (c_pair x (c_pair y z))) (nat_to_pr (comp_by_index index_of_c_fst index_of_c_snd) (c_pair x (c_pair y z)))) (nat_to_pr (comp_by_index index_of_c_snd index_of_c_snd) (c_pair x (c_pair y z))) = c_pair (c_pair x y) z
[PROOF STEP]
apply(simp add: index_of_c_fst_main)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c_pair (c_pair x (nat_to_pr (comp_by_index index_of_c_fst index_of_c_snd) (c_pair x (c_pair y z)))) (nat_to_pr (comp_by_index index_of_c_snd index_of_c_snd) (c_pair x (c_pair y z))) = c_pair (c_pair x y) z
[PROOF STEP]
apply(simp add: comp_by_index_main)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c_pair (c_pair x (nat_to_pr index_of_c_fst (nat_to_pr index_of_c_snd (c_pair x (c_pair y z))))) (nat_to_pr index_of_c_snd (nat_to_pr index_of_c_snd (c_pair x (c_pair y z)))) = c_pair (c_pair x y) z
[PROOF STEP]
apply(simp add: index_of_c_fst_main)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c_pair (c_pair x (c_fst (nat_to_pr index_of_c_snd (c_pair x (c_pair y z))))) (nat_to_pr index_of_c_snd (nat_to_pr index_of_c_snd (c_pair x (c_pair y z)))) = c_pair (c_pair x y) z
[PROOF STEP]
apply(simp add: index_of_c_snd_main)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma s_ce_is_pr: "s_ce \<in> PrimRec2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s_ce \<in> PrimRec2
[PROOF STEP]
unfolding s_ce_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>e. s1_1 (comp_by_index e index_of_r_to_l)) \<in> PrimRec2
[PROOF STEP]
using comp_by_index_is_pr s1_1_is_pr
[PROOF STATE]
proof (prove)
using this:
comp_by_index \<in> PrimRec2
s1_1 \<in> PrimRec2

goal (1 subgoal):
 1. (\<lambda>e. s1_1 (comp_by_index e index_of_r_to_l)) \<in> PrimRec2
[PROOF STEP]
by prec


[STATEMENT]
lemma s_ce_inj1: "s_ce e1 x = s_ce e2 x \<Longrightarrow> e1=e2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s_ce e1 x = s_ce e2 x \<Longrightarrow> e1 = e2
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. s_ce e1 x = s_ce e2 x \<Longrightarrow> e1 = e2
[PROOF STEP]
assume "s_ce e1 x = s_ce e2 x"
[PROOF STATE]
proof (state)
this:
s_ce e1 x = s_ce e2 x

goal (1 subgoal):
 1. s_ce e1 x = s_ce e2 x \<Longrightarrow> e1 = e2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
s_ce e1 x = s_ce e2 x
[PROOF STEP]
have "e1=e2 \<and> x=x"
[PROOF STATE]
proof (prove)
using this:
s_ce e1 x = s_ce e2 x

goal (1 subgoal):
 1. e1 = e2 \<and> x = x
[PROOF STEP]
by (rule s_ce_inj)
[PROOF STATE]
proof (state)
this:
e1 = e2 \<and> x = x

goal (1 subgoal):
 1. s_ce e1 x = s_ce e2 x \<Longrightarrow> e1 = e2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
e1 = e2 \<and> x = x
[PROOF STEP]
show "e1=e2"
[PROOF STATE]
proof (prove)
using this:
e1 = e2 \<and> x = x

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma s_ce_inj2: "s_ce e x1 = s_ce e x2 \<Longrightarrow> x1=x2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s_ce e x1 = s_ce e x2 \<Longrightarrow> x1 = x2
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. s_ce e x1 = s_ce e x2 \<Longrightarrow> x1 = x2
[PROOF STEP]
assume "s_ce e x1 = s_ce e x2"
[PROOF STATE]
proof (state)
this:
s_ce e x1 = s_ce e x2

goal (1 subgoal):
 1. s_ce e x1 = s_ce e x2 \<Longrightarrow> x1 = x2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
s_ce e x1 = s_ce e x2
[PROOF STEP]
have "e=e \<and> x1=x2"
[PROOF STATE]
proof (prove)
using this:
s_ce e x1 = s_ce e x2

goal (1 subgoal):
 1. e = e \<and> x1 = x2
[PROOF STEP]
by (rule s_ce_inj)
[PROOF STATE]
proof (state)
this:
e = e \<and> x1 = x2

goal (1 subgoal):
 1. s_ce e x1 = s_ce e x2 \<Longrightarrow> x1 = x2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
e = e \<and> x1 = x2
[PROOF STEP]
show "x1=x2"
[PROOF STATE]
proof (prove)
using this:
e = e \<and> x1 = x2

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem s1_1_th1: "\<forall> n x y. ((nat_to_pr n) (c_pair x y)) = (nat_to_pr (s1_1 n x)) y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>n x y. nat_to_pr n (c_pair x y) = nat_to_pr (s1_1 n x) y
[PROOF STEP]
proof (rule allI, rule allI, rule allI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n x y. nat_to_pr n (c_pair x y) = nat_to_pr (s1_1 n x) y
[PROOF STEP]
fix n x y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n x y. nat_to_pr n (c_pair x y) = nat_to_pr (s1_1 n x) y
[PROOF STEP]
show "nat_to_pr n (c_pair x y) = nat_to_pr (s1_1 n x) y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nat_to_pr n (c_pair x y) = nat_to_pr (s1_1 n x) y
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. nat_to_pr n (c_pair x y) = nat_to_pr (s1_1 n x) y
[PROOF STEP]
have "(\<lambda> y. (nat_to_pr n) (c_pair x y)) = nat_to_pr (s1_1 n x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>y. nat_to_pr n (c_pair x y)) = nat_to_pr (s1_1 n x)
[PROOF STEP]
by (rule s1_1_th)
[PROOF STATE]
proof (state)
this:
(\<lambda>y. nat_to_pr n (c_pair x y)) = nat_to_pr (s1_1 n x)

goal (1 subgoal):
 1. nat_to_pr n (c_pair x y) = nat_to_pr (s1_1 n x) y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>y. nat_to_pr n (c_pair x y)) = nat_to_pr (s1_1 n x)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<lambda>y. nat_to_pr n (c_pair x y)) = nat_to_pr (s1_1 n x)

goal (1 subgoal):
 1. nat_to_pr n (c_pair x y) = nat_to_pr (s1_1 n x) y
[PROOF STEP]
by (simp add: fun_eq_iff)
[PROOF STATE]
proof (state)
this:
nat_to_pr n (c_pair x y) = nat_to_pr (s1_1 n x) y

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
nat_to_pr n (c_pair x y) = nat_to_pr (s1_1 n x) y

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma s_lm: "(nat_to_pr (s_ce e x)) (c_pair y z) = (nat_to_pr e) (c_pair (c_pair x y) z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nat_to_pr (s_ce e x) (c_pair y z) = nat_to_pr e (c_pair (c_pair x y) z)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. nat_to_pr (s_ce e x) (c_pair y z) = nat_to_pr e (c_pair (c_pair x y) z)
[PROOF STEP]
let ?n1 = "index_of_r_to_l"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. nat_to_pr (s_ce e x) (c_pair y z) = nat_to_pr e (c_pair (c_pair x y) z)
[PROOF STEP]
have "(nat_to_pr (s_ce e x)) (c_pair y z) = nat_to_pr (s1_1 (comp_by_index e ?n1) x) (c_pair y z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nat_to_pr (s_ce e x) (c_pair y z) = nat_to_pr (s1_1 (comp_by_index e index_of_r_to_l) x) (c_pair y z)
[PROOF STEP]
by (unfold s_ce_def, simp)
[PROOF STATE]
proof (state)
this:
nat_to_pr (s_ce e x) (c_pair y z) = nat_to_pr (s1_1 (comp_by_index e index_of_r_to_l) x) (c_pair y z)

goal (1 subgoal):
 1. nat_to_pr (s_ce e x) (c_pair y z) = nat_to_pr e (c_pair (c_pair x y) z)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
nat_to_pr (s_ce e x) (c_pair y z) = nat_to_pr (s1_1 (comp_by_index e index_of_r_to_l) x) (c_pair y z)

goal (1 subgoal):
 1. nat_to_pr (s_ce e x) (c_pair y z) = nat_to_pr e (c_pair (c_pair x y) z)
[PROOF STEP]
have "\<dots> = (nat_to_pr (comp_by_index e ?n1)) (c_pair x (c_pair y z))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nat_to_pr (s1_1 (comp_by_index e index_of_r_to_l) x) (c_pair y z) = nat_to_pr (comp_by_index e index_of_r_to_l) (c_pair x (c_pair y z))
[PROOF STEP]
by (simp add: s1_1_th1)
[PROOF STATE]
proof (state)
this:
nat_to_pr (s1_1 (comp_by_index e index_of_r_to_l) x) (c_pair y z) = nat_to_pr (comp_by_index e index_of_r_to_l) (c_pair x (c_pair y z))

goal (1 subgoal):
 1. nat_to_pr (s_ce e x) (c_pair y z) = nat_to_pr e (c_pair (c_pair x y) z)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
nat_to_pr (s1_1 (comp_by_index e index_of_r_to_l) x) (c_pair y z) = nat_to_pr (comp_by_index e index_of_r_to_l) (c_pair x (c_pair y z))

goal (1 subgoal):
 1. nat_to_pr (s_ce e x) (c_pair y z) = nat_to_pr e (c_pair (c_pair x y) z)
[PROOF STEP]
have "\<dots> = (nat_to_pr e) ((nat_to_pr ?n1) (c_pair x (c_pair y z)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nat_to_pr (comp_by_index e index_of_r_to_l) (c_pair x (c_pair y z)) = nat_to_pr e (nat_to_pr index_of_r_to_l (c_pair x (c_pair y z)))
[PROOF STEP]
by (simp add: comp_by_index_main)
[PROOF STATE]
proof (state)
this:
nat_to_pr (comp_by_index e index_of_r_to_l) (c_pair x (c_pair y z)) = nat_to_pr e (nat_to_pr index_of_r_to_l (c_pair x (c_pair y z)))

goal (1 subgoal):
 1. nat_to_pr (s_ce e x) (c_pair y z) = nat_to_pr e (c_pair (c_pair x y) z)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
nat_to_pr (s_ce e x) (c_pair y z) = nat_to_pr e (nat_to_pr index_of_r_to_l (c_pair x (c_pair y z)))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
nat_to_pr (s_ce e x) (c_pair y z) = nat_to_pr e (nat_to_pr index_of_r_to_l (c_pair x (c_pair y z)))

goal (1 subgoal):
 1. nat_to_pr (s_ce e x) (c_pair y z) = nat_to_pr e (c_pair (c_pair x y) z)
[PROOF STEP]
by (simp add: index_of_r_to_l_lm)
[PROOF STATE]
proof (state)
this:
nat_to_pr (s_ce e x) (c_pair y z) = nat_to_pr e (c_pair (c_pair x y) z)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem s_ce_1_1_th: "(c_pair x y \<in> nat_to_ce_set e) = (y \<in> nat_to_ce_set (s_ce e x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (c_pair x y \<in> nat_to_ce_set e) = (y \<in> nat_to_ce_set (s_ce e x))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. c_pair x y \<in> nat_to_ce_set e \<Longrightarrow> y \<in> nat_to_ce_set (s_ce e x)
 2. y \<in> nat_to_ce_set (s_ce e x) \<Longrightarrow> c_pair x y \<in> nat_to_ce_set e
[PROOF STEP]
assume A: "c_pair x y \<in> nat_to_ce_set e"
[PROOF STATE]
proof (state)
this:
c_pair x y \<in> nat_to_ce_set e

goal (2 subgoals):
 1. c_pair x y \<in> nat_to_ce_set e \<Longrightarrow> y \<in> nat_to_ce_set (s_ce e x)
 2. y \<in> nat_to_ce_set (s_ce e x) \<Longrightarrow> c_pair x y \<in> nat_to_ce_set e
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
c_pair x y \<in> nat_to_ce_set e
[PROOF STEP]
obtain z where L1: "(nat_to_pr e) (c_pair (c_pair x y) z) = 0"
[PROOF STATE]
proof (prove)
using this:
c_pair x y \<in> nat_to_ce_set e

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

goal (2 subgoals):
 1. c_pair x y \<in> nat_to_ce_set e \<Longrightarrow> y \<in> nat_to_ce_set (s_ce e x)
 2. y \<in> nat_to_ce_set (s_ce e x) \<Longrightarrow> c_pair x y \<in> nat_to_ce_set e
[PROOF STEP]
have "(nat_to_pr (s_ce e x)) (c_pair y z) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nat_to_pr (s_ce e x) (c_pair y z) = 0
[PROOF STEP]
by (simp add: s_lm L1)
[PROOF STATE]
proof (state)
this:
nat_to_pr (s_ce e x) (c_pair y z) = 0

goal (2 subgoals):
 1. c_pair x y \<in> nat_to_ce_set e \<Longrightarrow> y \<in> nat_to_ce_set (s_ce e x)
 2. y \<in> nat_to_ce_set (s_ce e x) \<Longrightarrow> c_pair x y \<in> nat_to_ce_set e
[PROOF STEP]
with nat_to_ce_set_lm_1
[PROOF STATE]
proof (chain)
picking this:
nat_to_ce_set ?n = {x. \<exists>y. nat_to_pr ?n (c_pair x y) = 0}
nat_to_pr (s_ce e x) (c_pair y z) = 0
[PROOF STEP]
show "y \<in> nat_to_ce_set (s_ce e x)"
[PROOF STATE]
proof (prove)
using this:
nat_to_ce_set ?n = {x. \<exists>y. nat_to_pr ?n (c_pair x y) = 0}
nat_to_pr (s_ce e x) (c_pair y z) = 0

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

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

goal (1 subgoal):
 1. y \<in> nat_to_ce_set (s_ce e x) \<Longrightarrow> c_pair x y \<in> nat_to_ce_set e
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
y \<in> nat_to_ce_set (s_ce e x)
[PROOF STEP]
obtain z where L1: "(nat_to_pr (s_ce e x)) (c_pair y z) = 0"
[PROOF STATE]
proof (prove)
using this:
y \<in> nat_to_ce_set (s_ce e x)

goal (1 subgoal):
 1. (\<And>z. nat_to_pr (s_ce e x) (c_pair y z) = 0 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp add: nat_to_ce_set_lm_1)
[PROOF STATE]
proof (state)
this:
nat_to_pr (s_ce e x) (c_pair y z) = 0

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

goal (1 subgoal):
 1. nat_to_pr e (c_pair (c_pair x y) z) = 0
[PROOF STEP]
by (simp add: s_lm)
[PROOF STATE]
proof (state)
this:
nat_to_pr e (c_pair (c_pair x y) z) = 0

goal (1 subgoal):
 1. y \<in> nat_to_ce_set (s_ce e x) \<Longrightarrow> c_pair x y \<in> nat_to_ce_set e
[PROOF STEP]
with nat_to_ce_set_lm_1
[PROOF STATE]
proof (chain)
picking this:
nat_to_ce_set ?n = {x. \<exists>y. nat_to_pr ?n (c_pair x y) = 0}
nat_to_pr e (c_pair (c_pair x y) z) = 0
[PROOF STEP]
show "c_pair x y \<in> nat_to_ce_set e"
[PROOF STATE]
proof (prove)
using this:
nat_to_ce_set ?n = {x. \<exists>y. nat_to_pr ?n (c_pair x y) = 0}
nat_to_pr e (c_pair (c_pair x y) z) = 0

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma one_reducible_to_via_trans: "\<lbrakk> one_reducible_to_via A B f; one_reducible_to_via B C g \<rbrakk> \<Longrightarrow> one_reducible_to_via A C (g o f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>one_reducible_to_via A B f; one_reducible_to_via B C g\<rbrakk> \<Longrightarrow> one_reducible_to_via A C (g \<circ> f)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>one_reducible_to_via A B f; one_reducible_to_via B C g\<rbrakk> \<Longrightarrow> one_reducible_to_via A C (g \<circ> f)
[PROOF STEP]
assume A1: "one_reducible_to_via A B f"
[PROOF STATE]
proof (state)
this:
one_reducible_to_via A B f

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

goal (1 subgoal):
 1. \<lbrakk>one_reducible_to_via A B f; one_reducible_to_via B C g\<rbrakk> \<Longrightarrow> one_reducible_to_via A C (g \<circ> f)
[PROOF STEP]
from A1
[PROOF STATE]
proof (chain)
picking this:
one_reducible_to_via A B f
[PROOF STEP]
have f_tr: "total_recursive f"
[PROOF STATE]
proof (prove)
using this:
one_reducible_to_via A B f

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

goal (1 subgoal):
 1. \<lbrakk>one_reducible_to_via A B f; one_reducible_to_via B C g\<rbrakk> \<Longrightarrow> one_reducible_to_via A C (g \<circ> f)
[PROOF STEP]
from A1
[PROOF STATE]
proof (chain)
picking this:
one_reducible_to_via A B f
[PROOF STEP]
have f_inj: "inj f"
[PROOF STATE]
proof (prove)
using this:
one_reducible_to_via A B f

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

goal (1 subgoal):
 1. \<lbrakk>one_reducible_to_via A B f; one_reducible_to_via B C g\<rbrakk> \<Longrightarrow> one_reducible_to_via A C (g \<circ> f)
[PROOF STEP]
from A1
[PROOF STATE]
proof (chain)
picking this:
one_reducible_to_via A B f
[PROOF STEP]
have L1: "\<forall> x. (x \<in> A) = (f x \<in> B)"
[PROOF STATE]
proof (prove)
using this:
one_reducible_to_via A B f

goal (1 subgoal):
 1. \<forall>x. (x \<in> A) = (f x \<in> B)
[PROOF STEP]
by (unfold one_reducible_to_via_def, auto)
[PROOF STATE]
proof (state)
this:
\<forall>x. (x \<in> A) = (f x \<in> B)

goal (1 subgoal):
 1. \<lbrakk>one_reducible_to_via A B f; one_reducible_to_via B C g\<rbrakk> \<Longrightarrow> one_reducible_to_via A C (g \<circ> f)
[PROOF STEP]
from A2
[PROOF STATE]
proof (chain)
picking this:
one_reducible_to_via B C g
[PROOF STEP]
have g_tr: "total_recursive g"
[PROOF STATE]
proof (prove)
using this:
one_reducible_to_via B C g

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

goal (1 subgoal):
 1. \<lbrakk>one_reducible_to_via A B f; one_reducible_to_via B C g\<rbrakk> \<Longrightarrow> one_reducible_to_via A C (g \<circ> f)
[PROOF STEP]
from A2
[PROOF STATE]
proof (chain)
picking this:
one_reducible_to_via B C g
[PROOF STEP]
have g_inj: "inj g"
[PROOF STATE]
proof (prove)
using this:
one_reducible_to_via B C g

goal (1 subgoal):
 1. inj g
[PROOF STEP]
by (unfold one_reducible_to_via_def, auto)
[PROOF STATE]
proof (state)
this:
inj g

goal (1 subgoal):
 1. \<lbrakk>one_reducible_to_via A B f; one_reducible_to_via B C g\<rbrakk> \<Longrightarrow> one_reducible_to_via A C (g \<circ> f)
[PROOF STEP]
from A2
[PROOF STATE]
proof (chain)
picking this:
one_reducible_to_via B C g
[PROOF STEP]
have L2: "\<forall> x. (x \<in> B) = (g x \<in> C)"
[PROOF STATE]
proof (prove)
using this:
one_reducible_to_via B C g

goal (1 subgoal):
 1. \<forall>x. (x \<in> B) = (g x \<in> C)
[PROOF STEP]
by (unfold one_reducible_to_via_def, auto)
[PROOF STATE]
proof (state)
this:
\<forall>x. (x \<in> B) = (g x \<in> C)

goal (1 subgoal):
 1. \<lbrakk>one_reducible_to_via A B f; one_reducible_to_via B C g\<rbrakk> \<Longrightarrow> one_reducible_to_via A C (g \<circ> f)
[PROOF STEP]
from g_tr f_tr
[PROOF STATE]
proof (chain)
picking this:
total_recursive g
total_recursive f
[PROOF STEP]
have fg_tr: "total_recursive (g o f)"
[PROOF STATE]
proof (prove)
using this:
total_recursive g
total_recursive f

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

goal (1 subgoal):
 1. \<lbrakk>one_reducible_to_via A B f; one_reducible_to_via B C g\<rbrakk> \<Longrightarrow> one_reducible_to_via A C (g \<circ> f)
[PROOF STEP]
from g_inj f_inj
[PROOF STATE]
proof (chain)
picking this:
inj g
inj f
[PROOF STEP]
have fg_inj: "inj (g o f)"
[PROOF STATE]
proof (prove)
using this:
inj g
inj f

goal (1 subgoal):
 1. inj (g \<circ> f)
[PROOF STEP]
by (rule inj_compose)
[PROOF STATE]
proof (state)
this:
inj (g \<circ> f)

goal (1 subgoal):
 1. \<lbrakk>one_reducible_to_via A B f; one_reducible_to_via B C g\<rbrakk> \<Longrightarrow> one_reducible_to_via A C (g \<circ> f)
[PROOF STEP]
from L1 L2
[PROOF STATE]
proof (chain)
picking this:
\<forall>x. (x \<in> A) = (f x \<in> B)
\<forall>x. (x \<in> B) = (g x \<in> C)
[PROOF STEP]
have L3: "(\<forall> x. (x \<in> A) = ((g o f) x \<in> C))"
[PROOF STATE]
proof (prove)
using this:
\<forall>x. (x \<in> A) = (f x \<in> B)
\<forall>x. (x \<in> B) = (g x \<in> C)

goal (1 subgoal):
 1. \<forall>x. (x \<in> A) = ((g \<circ> f) x \<in> C)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>x. (x \<in> A) = ((g \<circ> f) x \<in> C)

goal (1 subgoal):
 1. \<lbrakk>one_reducible_to_via A B f; one_reducible_to_via B C g\<rbrakk> \<Longrightarrow> one_reducible_to_via A C (g \<circ> f)
[PROOF STEP]
with fg_tr fg_inj
[PROOF STATE]
proof (chain)
picking this:
total_recursive (g \<circ> f)
inj (g \<circ> f)
\<forall>x. (x \<in> A) = ((g \<circ> f) x \<in> C)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
total_recursive (g \<circ> f)
inj (g \<circ> f)
\<forall>x. (x \<in> A) = ((g \<circ> f) x \<in> C)

goal (1 subgoal):
 1. one_reducible_to_via A C (g \<circ> f)
[PROOF STEP]
by (unfold one_reducible_to_via_def, auto)
[PROOF STATE]
proof (state)
this:
one_reducible_to_via A C (g \<circ> f)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma one_reducible_to_trans: "\<lbrakk> one_reducible_to A B; one_reducible_to B C \<rbrakk> \<Longrightarrow> one_reducible_to A C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>one_reducible_to A B; one_reducible_to B C\<rbrakk> \<Longrightarrow> one_reducible_to A C
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>one_reducible_to A B; one_reducible_to B C\<rbrakk> \<Longrightarrow> one_reducible_to A C
[PROOF STEP]
assume "one_reducible_to A B"
[PROOF STATE]
proof (state)
this:
one_reducible_to A B

goal (1 subgoal):
 1. \<lbrakk>one_reducible_to A B; one_reducible_to B C\<rbrakk> \<Longrightarrow> one_reducible_to A C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
one_reducible_to A B
[PROOF STEP]
obtain f where A1: "one_reducible_to_via A B f"
[PROOF STATE]
proof (prove)
using this:
one_reducible_to A B

goal (1 subgoal):
 1. (\<And>f. one_reducible_to_via A B f \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding one_reducible_to_def
[PROOF STATE]
proof (prove)
using this:
Ex (one_reducible_to_via A B)

goal (1 subgoal):
 1. (\<And>f. one_reducible_to_via A B f \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
one_reducible_to_via A B f

goal (1 subgoal):
 1. \<lbrakk>one_reducible_to A B; one_reducible_to B C\<rbrakk> \<Longrightarrow> one_reducible_to A C
[PROOF STEP]
assume "one_reducible_to B C"
[PROOF STATE]
proof (state)
this:
one_reducible_to B C

goal (1 subgoal):
 1. \<lbrakk>one_reducible_to A B; one_reducible_to B C\<rbrakk> \<Longrightarrow> one_reducible_to A C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
one_reducible_to B C
[PROOF STEP]
obtain g where A2: "one_reducible_to_via B C g"
[PROOF STATE]
proof (prove)
using this:
one_reducible_to B C

goal (1 subgoal):
 1. (\<And>g. one_reducible_to_via B C g \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding one_reducible_to_def
[PROOF STATE]
proof (prove)
using this:
Ex (one_reducible_to_via B C)

goal (1 subgoal):
 1. (\<And>g. one_reducible_to_via B C g \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
one_reducible_to_via B C g

goal (1 subgoal):
 1. \<lbrakk>one_reducible_to A B; one_reducible_to B C\<rbrakk> \<Longrightarrow> one_reducible_to A C
[PROOF STEP]
from A1 A2
[PROOF STATE]
proof (chain)
picking this:
one_reducible_to_via A B f
one_reducible_to_via B C g
[PROOF STEP]
have "one_reducible_to_via A C (g o f)"
[PROOF STATE]
proof (prove)
using this:
one_reducible_to_via A B f
one_reducible_to_via B C g

goal (1 subgoal):
 1. one_reducible_to_via A C (g \<circ> f)
[PROOF STEP]
by (rule one_reducible_to_via_trans)
[PROOF STATE]
proof (state)
this:
one_reducible_to_via A C (g \<circ> f)

goal (1 subgoal):
 1. \<lbrakk>one_reducible_to A B; one_reducible_to B C\<rbrakk> \<Longrightarrow> one_reducible_to A C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
one_reducible_to_via A C (g \<circ> f)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
one_reducible_to_via A C (g \<circ> f)

goal (1 subgoal):
 1. one_reducible_to A C
[PROOF STEP]
unfolding one_reducible_to_def
[PROOF STATE]
proof (prove)
using this:
one_reducible_to_via A C (g \<circ> f)

goal (1 subgoal):
 1. Ex (one_reducible_to_via A C)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
one_reducible_to A C

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma one_reducible_to_via_refl: "one_reducible_to_via A A (\<lambda> x. x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. one_reducible_to_via A A (\<lambda>x. x)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. one_reducible_to_via A A (\<lambda>x. x)
[PROOF STEP]
have is_pr: "(\<lambda> x. x) \<in> PrimRec1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. x) \<in> PrimRec1
[PROOF STEP]
by (rule pr_id1_1)
[PROOF STATE]
proof (state)
this:
(\<lambda>x. x) \<in> PrimRec1

goal (1 subgoal):
 1. one_reducible_to_via A A (\<lambda>x. x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>x. x) \<in> PrimRec1
[PROOF STEP]
have is_tr: "total_recursive (\<lambda> x. x)"
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. x) \<in> PrimRec1

goal (1 subgoal):
 1. total_recursive (\<lambda>x. x)
[PROOF STEP]
by (rule pr_is_total_rec)
[PROOF STATE]
proof (state)
this:
total_recursive (\<lambda>x. x)

goal (1 subgoal):
 1. one_reducible_to_via A A (\<lambda>x. x)
[PROOF STEP]
have is_inj: "inj (\<lambda> x. x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj (\<lambda>x. x)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
inj (\<lambda>x. x)

goal (1 subgoal):
 1. one_reducible_to_via A A (\<lambda>x. x)
[PROOF STEP]
have L1: "\<forall> x. (x \<in> A) = (((\<lambda> x. x) x) \<in> A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x. (x \<in> A) = (x \<in> A)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>x. (x \<in> A) = (x \<in> A)

goal (1 subgoal):
 1. one_reducible_to_via A A (\<lambda>x. x)
[PROOF STEP]
with is_tr is_inj
[PROOF STATE]
proof (chain)
picking this:
total_recursive (\<lambda>x. x)
inj (\<lambda>x. x)
\<forall>x. (x \<in> A) = (x \<in> A)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
total_recursive (\<lambda>x. x)
inj (\<lambda>x. x)
\<forall>x. (x \<in> A) = (x \<in> A)

goal (1 subgoal):
 1. one_reducible_to_via A A (\<lambda>x. x)
[PROOF STEP]
by (unfold one_reducible_to_via_def, auto)
[PROOF STATE]
proof (state)
this:
one_reducible_to_via A A (\<lambda>x. x)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma one_reducible_to_refl: "one_reducible_to A A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. one_reducible_to A A
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. one_reducible_to A A
[PROOF STEP]
have "one_reducible_to_via A A (\<lambda> x. x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. one_reducible_to_via A A (\<lambda>x. x)
[PROOF STEP]
by (rule one_reducible_to_via_refl)
[PROOF STATE]
proof (state)
this:
one_reducible_to_via A A (\<lambda>x. x)

goal (1 subgoal):
 1. one_reducible_to A A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
one_reducible_to_via A A (\<lambda>x. x)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
one_reducible_to_via A A (\<lambda>x. x)

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

goal:
No subgoals!
[PROOF STEP]
qed