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

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

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

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

goal (1 subgoal):
 1. \<lbrakk>many_reducible_to_via A B f; many_reducible_to_via B C g\<rbrakk> \<Longrightarrow> many_reducible_to_via A C (g \<circ> f)
[PROOF STEP]
from A1
[PROOF STATE]
proof (chain)
picking this:
many_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:
many_reducible_to_via A B f

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

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

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

goal (1 subgoal):
 1. \<lbrakk>many_reducible_to_via A B f; many_reducible_to_via B C g\<rbrakk> \<Longrightarrow> many_reducible_to_via A C (g \<circ> f)
[PROOF STEP]
from A2
[PROOF STATE]
proof (chain)
picking this:
many_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:
many_reducible_to_via B C g

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

goal (1 subgoal):
 1. \<lbrakk>many_reducible_to_via A B f; many_reducible_to_via B C g\<rbrakk> \<Longrightarrow> many_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>many_reducible_to_via A B f; many_reducible_to_via B C g\<rbrakk> \<Longrightarrow> many_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>many_reducible_to_via A B f; many_reducible_to_via B C g\<rbrakk> \<Longrightarrow> many_reducible_to_via A C (g \<circ> f)
[PROOF STEP]
with fg_tr
[PROOF STATE]
proof (chain)
picking this:
total_recursive (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)
\<forall>x. (x \<in> A) = ((g \<circ> f) x \<in> C)

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

goal:
No subgoals!
[PROOF STEP]
qed


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

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

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

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

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

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

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

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

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

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

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma one_reducibility_via_is_many: "one_reducible_to_via A B f \<Longrightarrow> many_reducible_to_via A B f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. one_reducible_to_via A B f \<Longrightarrow> many_reducible_to_via A B f
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. one_reducible_to_via A B f \<Longrightarrow> many_reducible_to_via A B f
[PROOF STEP]
assume A: "one_reducible_to_via A B f"
[PROOF STATE]
proof (state)
this:
one_reducible_to_via A B f

goal (1 subgoal):
 1. one_reducible_to_via A B f \<Longrightarrow> many_reducible_to_via A B f
[PROOF STEP]
from A
[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. one_reducible_to_via A B f \<Longrightarrow> many_reducible_to_via A B f
[PROOF STEP]
from A
[PROOF STATE]
proof (chain)
picking this:
one_reducible_to_via A B f
[PROOF STEP]
have "\<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. one_reducible_to_via A B f \<Longrightarrow> many_reducible_to_via A B f
[PROOF STEP]
with f_tr
[PROOF STATE]
proof (chain)
picking this:
total_recursive f
\<forall>x. (x \<in> A) = (f x \<in> B)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
total_recursive f
\<forall>x. (x \<in> A) = (f x \<in> B)

goal (1 subgoal):
 1. many_reducible_to_via A B f
[PROOF STEP]
by (unfold many_reducible_to_via_def, auto)
[PROOF STATE]
proof (state)
this:
many_reducible_to_via A B f

goal:
No subgoals!
[PROOF STEP]
qed


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

goal (1 subgoal):
 1. one_reducible_to A B \<Longrightarrow> many_reducible_to A B
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
one_reducible_to A B
[PROOF STEP]
obtain f where A: "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. one_reducible_to A B \<Longrightarrow> many_reducible_to A B
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
one_reducible_to_via A B f
[PROOF STEP]
have "many_reducible_to_via A B f"
[PROOF STATE]
proof (prove)
using this:
one_reducible_to_via A B f

goal (1 subgoal):
 1. many_reducible_to_via A B f
[PROOF STEP]
by (rule one_reducibility_via_is_many)
[PROOF STATE]
proof (state)
this:
many_reducible_to_via A B f

goal (1 subgoal):
 1. one_reducible_to A B \<Longrightarrow> many_reducible_to A B
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
many_reducible_to_via A B f
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
many_reducible_to_via A B f

goal (1 subgoal):
 1. many_reducible_to A B
[PROOF STEP]
unfolding many_reducible_to_def
[PROOF STATE]
proof (prove)
using this:
many_reducible_to_via A B f

goal (1 subgoal):
 1. Ex (many_reducible_to_via A B)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
many_reducible_to A B

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma many_reducible_to_via_refl: "many_reducible_to_via A A (\<lambda> x. x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. many_reducible_to_via A A (\<lambda>x. x)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. many_reducible_to_via A A (\<lambda>x. x)
[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. many_reducible_to_via A A (\<lambda>x. x)
[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. many_reducible_to_via A A (\<lambda>x. x)
[PROOF STEP]
by (rule one_reducibility_via_is_many)
[PROOF STATE]
proof (state)
this:
many_reducible_to_via A A (\<lambda>x. x)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma many_reducible_to_refl: "many_reducible_to A A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. many_reducible_to A A
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. many_reducible_to A A
[PROOF STEP]
have "one_reducible_to A A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. one_reducible_to A A
[PROOF STEP]
by (rule one_reducible_to_refl)
[PROOF STATE]
proof (state)
this:
one_reducible_to A A

goal (1 subgoal):
 1. many_reducible_to A A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
one_reducible_to A A
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
one_reducible_to A A

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem m_red_to_comp: "\<lbrakk> many_reducible_to A B; computable B \<rbrakk> \<Longrightarrow> computable A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>many_reducible_to A B; computable B\<rbrakk> \<Longrightarrow> computable A
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>many_reducible_to A B; computable B\<rbrakk> \<Longrightarrow> computable A
[PROOF STEP]
assume "many_reducible_to A B"
[PROOF STATE]
proof (state)
this:
many_reducible_to A B

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

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

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

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

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

goal (1 subgoal):
 1. \<lbrakk>many_reducible_to A B; computable B\<rbrakk> \<Longrightarrow> computable A
[PROOF STEP]
from A1
[PROOF STATE]
proof (chain)
picking this:
many_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:
many_reducible_to_via A B f

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

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

goal (1 subgoal):
 1. \<lbrakk>many_reducible_to A B; computable B\<rbrakk> \<Longrightarrow> computable A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
computable B
[PROOF STEP]
have L2: "total_recursive (chf B)"
[PROOF STATE]
proof (prove)
using this:
computable B

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

goal (1 subgoal):
 1. \<lbrakk>many_reducible_to A B; computable B\<rbrakk> \<Longrightarrow> computable A
[PROOF STEP]
have L3: "chf A = (chf B) o f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. chf A = chf B \<circ> f
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. chf A x = (chf B \<circ> f) x
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. chf A x = (chf B \<circ> f) x
[PROOF STEP]
have "chf A x = (chf B) (f x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. chf A x = chf B (f x)
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> chf A x = chf B (f x)
 2. \<not> ?P \<Longrightarrow> chf A x = chf B (f x)
[PROOF STEP]
assume A: "x \<in> A"
[PROOF STATE]
proof (state)
this:
x \<in> A

goal (2 subgoals):
 1. ?P \<Longrightarrow> chf A x = chf B (f x)
 2. \<not> ?P \<Longrightarrow> chf A x = chf B (f x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> A
[PROOF STEP]
have L3_1: "chf A x = 0"
[PROOF STATE]
proof (prove)
using this:
x \<in> A

goal (1 subgoal):
 1. chf A x = 0
[PROOF STEP]
by (simp add: chf_lm_2)
[PROOF STATE]
proof (state)
this:
chf A x = 0

goal (2 subgoals):
 1. ?P \<Longrightarrow> chf A x = chf B (f x)
 2. \<not> ?P \<Longrightarrow> chf A x = chf B (f x)
[PROOF STEP]
from A L1
[PROOF STATE]
proof (chain)
picking this:
x \<in> A
\<forall>x. (x \<in> A) = (f x \<in> B)
[PROOF STEP]
have "f x \<in> B"
[PROOF STATE]
proof (prove)
using this:
x \<in> A
\<forall>x. (x \<in> A) = (f x \<in> B)

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

goal (2 subgoals):
 1. ?P \<Longrightarrow> chf A x = chf B (f x)
 2. \<not> ?P \<Longrightarrow> chf A x = chf B (f x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
f x \<in> B
[PROOF STEP]
have L3_2: "(chf B) (f x) = 0"
[PROOF STATE]
proof (prove)
using this:
f x \<in> B

goal (1 subgoal):
 1. chf B (f x) = 0
[PROOF STEP]
by (simp add: chf_lm_2)
[PROOF STATE]
proof (state)
this:
chf B (f x) = 0

goal (2 subgoals):
 1. ?P \<Longrightarrow> chf A x = chf B (f x)
 2. \<not> ?P \<Longrightarrow> chf A x = chf B (f x)
[PROOF STEP]
from L3_1 L3_2
[PROOF STATE]
proof (chain)
picking this:
chf A x = 0
chf B (f x) = 0
[PROOF STEP]
show "chf A x = (chf B) (f x)"
[PROOF STATE]
proof (prove)
using this:
chf A x = 0
chf B (f x) = 0

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

goal (1 subgoal):
 1. x \<notin> A \<Longrightarrow> chf A x = chf B (f x)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<notin> A \<Longrightarrow> chf A x = chf B (f x)
[PROOF STEP]
assume A: "x \<notin> A"
[PROOF STATE]
proof (state)
this:
x \<notin> A

goal (1 subgoal):
 1. x \<notin> A \<Longrightarrow> chf A x = chf B (f x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<notin> A
[PROOF STEP]
have L3_1: "chf A x = 1"
[PROOF STATE]
proof (prove)
using this:
x \<notin> A

goal (1 subgoal):
 1. chf A x = 1
[PROOF STEP]
by (simp add: chf_lm_3)
[PROOF STATE]
proof (state)
this:
chf A x = 1

goal (1 subgoal):
 1. x \<notin> A \<Longrightarrow> chf A x = chf B (f x)
[PROOF STEP]
from A L1
[PROOF STATE]
proof (chain)
picking this:
x \<notin> A
\<forall>x. (x \<in> A) = (f x \<in> B)
[PROOF STEP]
have "f x \<notin> B"
[PROOF STATE]
proof (prove)
using this:
x \<notin> A
\<forall>x. (x \<in> A) = (f x \<in> B)

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

goal (1 subgoal):
 1. x \<notin> A \<Longrightarrow> chf A x = chf B (f x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
f x \<notin> B
[PROOF STEP]
have L3_2: "(chf B) (f x) = 1"
[PROOF STATE]
proof (prove)
using this:
f x \<notin> B

goal (1 subgoal):
 1. chf B (f x) = 1
[PROOF STEP]
by (simp add: chf_lm_3)
[PROOF STATE]
proof (state)
this:
chf B (f x) = 1

goal (1 subgoal):
 1. x \<notin> A \<Longrightarrow> chf A x = chf B (f x)
[PROOF STEP]
from L3_1 L3_2
[PROOF STATE]
proof (chain)
picking this:
chf A x = 1
chf B (f x) = 1
[PROOF STEP]
show "chf A x = (chf B) (f x)"
[PROOF STATE]
proof (prove)
using this:
chf A x = 1
chf B (f x) = 1

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
chf A x = chf B (f x)

goal (1 subgoal):
 1. \<And>x. chf A x = (chf B \<circ> f) x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
chf A x = chf B (f x)
[PROOF STEP]
show "chf A x = (chf B \<circ> f) x"
[PROOF STATE]
proof (prove)
using this:
chf A x = chf B (f x)

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
chf A = chf B \<circ> f

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

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

goal (1 subgoal):
 1. \<lbrakk>many_reducible_to A B; computable B\<rbrakk> \<Longrightarrow> computable A
[PROOF STEP]
with L3
[PROOF STATE]
proof (chain)
picking this:
chf A = chf B \<circ> f
total_recursive (chf B \<circ> f)
[PROOF STEP]
have "total_recursive (chf A)"
[PROOF STATE]
proof (prove)
using this:
chf A = chf B \<circ> f
total_recursive (chf B \<circ> f)

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

goal (1 subgoal):
 1. \<lbrakk>many_reducible_to A B; computable B\<rbrakk> \<Longrightarrow> computable A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
total_recursive (chf A)
[PROOF STEP]
show ?thesis
[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 many_reducible_lm_1: "many_reducible_to univ_ce A \<Longrightarrow> \<not> computable A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. many_reducible_to univ_ce A \<Longrightarrow> \<not> computable A
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>many_reducible_to univ_ce A; \<not> \<not> computable A\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume A1: "many_reducible_to univ_ce A"
[PROOF STATE]
proof (state)
this:
many_reducible_to univ_ce A

goal (1 subgoal):
 1. \<lbrakk>many_reducible_to univ_ce A; \<not> \<not> computable A\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume "\<not> \<not> computable A"
[PROOF STATE]
proof (state)
this:
\<not> \<not> computable A

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

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

goal (1 subgoal):
 1. \<lbrakk>many_reducible_to univ_ce A; \<not> \<not> computable A\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
from A1 A2
[PROOF STATE]
proof (chain)
picking this:
many_reducible_to univ_ce A
computable A
[PROOF STEP]
have "computable univ_ce"
[PROOF STATE]
proof (prove)
using this:
many_reducible_to univ_ce A
computable A

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

goal (1 subgoal):
 1. \<lbrakk>many_reducible_to univ_ce A; \<not> \<not> computable A\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
with univ_ce_is_not_comp3
[PROOF STATE]
proof (chain)
picking this:
\<not> computable univ_ce
computable univ_ce
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
\<not> computable univ_ce
computable 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 one_reducible_lm_1: "one_reducible_to univ_ce A \<Longrightarrow> \<not> computable A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. one_reducible_to univ_ce A \<Longrightarrow> \<not> computable A
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. one_reducible_to univ_ce A \<Longrightarrow> \<not> computable A
[PROOF STEP]
assume "one_reducible_to univ_ce A"
[PROOF STATE]
proof (state)
this:
one_reducible_to univ_ce A

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

goal (1 subgoal):
 1. many_reducible_to univ_ce A
[PROOF STEP]
by (rule one_reducibility_is_many)
[PROOF STATE]
proof (state)
this:
many_reducible_to univ_ce A

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

goal (1 subgoal):
 1. \<not> computable A
[PROOF STEP]
by (rule many_reducible_lm_1)
[PROOF STATE]
proof (state)
this:
\<not> computable A

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma one_reducible_lm_2: "one_reducible_to_via (nat_to_ce_set n) univ_ce (\<lambda> x. c_pair n x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. one_reducible_to_via (nat_to_ce_set n) univ_ce (c_pair n)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. one_reducible_to_via (nat_to_ce_set n) univ_ce (c_pair n)
[PROOF STEP]
define f where "f x = c_pair n x" for x
[PROOF STATE]
proof (state)
this:
f ?x = c_pair n ?x

goal (1 subgoal):
 1. one_reducible_to_via (nat_to_ce_set n) univ_ce (c_pair n)
[PROOF STEP]
have f_is_pr: "f \<in> PrimRec1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<in> PrimRec1
[PROOF STEP]
unfolding f_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c_pair n \<in> PrimRec1
[PROOF STEP]
by prec
[PROOF STATE]
proof (state)
this:
f \<in> PrimRec1

goal (1 subgoal):
 1. one_reducible_to_via (nat_to_ce_set n) univ_ce (c_pair n)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
f \<in> PrimRec1
[PROOF STEP]
have f_tr: "total_recursive f"
[PROOF STATE]
proof (prove)
using this:
f \<in> PrimRec1

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

goal (1 subgoal):
 1. one_reducible_to_via (nat_to_ce_set n) univ_ce (c_pair n)
[PROOF STEP]
have f_inj: "inj f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj f
[PROOF STEP]
proof (rule injI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. f x = f y \<Longrightarrow> x = y
[PROOF STEP]
fix x y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. f x = f y \<Longrightarrow> x = y
[PROOF STEP]
assume A: "f x = f y"
[PROOF STATE]
proof (state)
this:
f x = f y

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

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

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

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

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

goal (1 subgoal):
 1. one_reducible_to_via (nat_to_ce_set n) univ_ce (c_pair n)
[PROOF STEP]
have "\<forall> x. (x \<in> (nat_to_ce_set n)) = (f x \<in> univ_ce)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x. (x \<in> nat_to_ce_set n) = (f x \<in> univ_ce)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. (x \<in> nat_to_ce_set n) = (f x \<in> univ_ce)
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. (x \<in> nat_to_ce_set n) = (f x \<in> univ_ce)
[PROOF STEP]
show "(x \<in> nat_to_ce_set n) = (f x \<in> univ_ce)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<in> nat_to_ce_set n) = (f x \<in> univ_ce)
[PROOF STEP]
by (unfold f_def, simp add: univ_ce_lm_1)
[PROOF STATE]
proof (state)
this:
(x \<in> nat_to_ce_set n) = (f x \<in> univ_ce)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>x. (x \<in> nat_to_ce_set n) = (f x \<in> univ_ce)

goal (1 subgoal):
 1. one_reducible_to_via (nat_to_ce_set n) univ_ce (c_pair n)
[PROOF STEP]
with f_tr f_inj
[PROOF STATE]
proof (chain)
picking this:
total_recursive f
inj f
\<forall>x. (x \<in> nat_to_ce_set n) = (f x \<in> univ_ce)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
total_recursive f
inj f
\<forall>x. (x \<in> nat_to_ce_set n) = (f x \<in> univ_ce)

goal (1 subgoal):
 1. one_reducible_to_via (nat_to_ce_set n) univ_ce (c_pair n)
[PROOF STEP]
by (unfold f_def, unfold one_reducible_to_via_def, auto)
[PROOF STATE]
proof (state)
this:
one_reducible_to_via (nat_to_ce_set n) univ_ce (c_pair n)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma one_reducible_lm_3: "one_reducible_to (nat_to_ce_set n) univ_ce"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. one_reducible_to (nat_to_ce_set n) univ_ce
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. one_reducible_to (nat_to_ce_set n) univ_ce
[PROOF STEP]
have "one_reducible_to_via (nat_to_ce_set n) univ_ce (\<lambda> x. c_pair n x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. one_reducible_to_via (nat_to_ce_set n) univ_ce (c_pair n)
[PROOF STEP]
by (rule one_reducible_lm_2)
[PROOF STATE]
proof (state)
this:
one_reducible_to_via (nat_to_ce_set n) univ_ce (c_pair n)

goal (1 subgoal):
 1. one_reducible_to (nat_to_ce_set n) univ_ce
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
one_reducible_to_via (nat_to_ce_set n) univ_ce (c_pair n)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
one_reducible_to_via (nat_to_ce_set n) univ_ce (c_pair n)

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

goal:
No subgoals!
[PROOF STEP]
qed


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

goal (1 subgoal):
 1. A \<in> ce_sets \<Longrightarrow> one_reducible_to A univ_ce
[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. A \<in> ce_sets \<Longrightarrow> one_reducible_to A univ_ce
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>n. A = nat_to_ce_set n
[PROOF STEP]
obtain n where "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]
by auto
[PROOF STATE]
proof (state)
this:
A = nat_to_ce_set n

goal (1 subgoal):
 1. A \<in> ce_sets \<Longrightarrow> one_reducible_to A univ_ce
[PROOF STEP]
with one_reducible_lm_3
[PROOF STATE]
proof (chain)
picking this:
one_reducible_to (nat_to_ce_set ?n) univ_ce
A = nat_to_ce_set n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
one_reducible_to (nat_to_ce_set ?n) univ_ce
A = nat_to_ce_set n

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem univ_is_complete: "one_complete univ_ce"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. one_complete univ_ce
[PROOF STEP]
proof (unfold one_complete_def)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. univ_ce \<in> ce_sets \<and> (\<forall>B. B \<in> ce_sets \<longrightarrow> one_reducible_to B univ_ce)
[PROOF STEP]
show "univ_ce \<in> ce_sets \<and> (\<forall>B. B \<in> ce_sets \<longrightarrow> one_reducible_to B univ_ce)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. univ_ce \<in> ce_sets \<and> (\<forall>B. B \<in> ce_sets \<longrightarrow> one_reducible_to B univ_ce)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. univ_ce \<in> ce_sets
 2. \<forall>B. B \<in> ce_sets \<longrightarrow> one_reducible_to B univ_ce
[PROOF STEP]
show "univ_ce \<in> ce_sets"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. univ_ce \<in> ce_sets
[PROOF STEP]
by (rule univ_is_ce)
[PROOF STATE]
proof (state)
this:
univ_ce \<in> ce_sets

goal (1 subgoal):
 1. \<forall>B. B \<in> ce_sets \<longrightarrow> one_reducible_to B univ_ce
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>B. B \<in> ce_sets \<longrightarrow> one_reducible_to B univ_ce
[PROOF STEP]
show "\<forall>B. B \<in> ce_sets \<longrightarrow> one_reducible_to B univ_ce"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>B. B \<in> ce_sets \<longrightarrow> one_reducible_to B univ_ce
[PROOF STEP]
proof (rule allI, rule impI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>B. B \<in> ce_sets \<Longrightarrow> one_reducible_to B univ_ce
[PROOF STEP]
fix B
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>B. B \<in> ce_sets \<Longrightarrow> one_reducible_to B univ_ce
[PROOF STEP]
assume "B \<in> ce_sets"
[PROOF STATE]
proof (state)
this:
B \<in> ce_sets

goal (1 subgoal):
 1. \<And>B. B \<in> ce_sets \<Longrightarrow> one_reducible_to B univ_ce
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
B \<in> ce_sets
[PROOF STEP]
show "one_reducible_to B univ_ce"
[PROOF STATE]
proof (prove)
using this:
B \<in> ce_sets

goal (1 subgoal):
 1. one_reducible_to B univ_ce
[PROOF STEP]
by (rule one_reducible_lm_4)
[PROOF STATE]
proof (state)
this:
one_reducible_to B univ_ce

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>B. B \<in> ce_sets \<longrightarrow> one_reducible_to B univ_ce

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
univ_ce \<in> ce_sets \<and> (\<forall>B. B \<in> ce_sets \<longrightarrow> one_reducible_to B univ_ce)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma index_set_lm_1: "\<lbrakk> index_set A; n\<in> A; nat_to_ce_set n = nat_to_ce_set m \<rbrakk> \<Longrightarrow> m \<in> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>index_set A; n \<in> A; nat_to_ce_set n = nat_to_ce_set m\<rbrakk> \<Longrightarrow> m \<in> A
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>index_set A; n \<in> A; nat_to_ce_set n = nat_to_ce_set m\<rbrakk> \<Longrightarrow> m \<in> A
[PROOF STEP]
assume A1: "index_set A"
[PROOF STATE]
proof (state)
this:
index_set A

goal (1 subgoal):
 1. \<lbrakk>index_set A; n \<in> A; nat_to_ce_set n = nat_to_ce_set m\<rbrakk> \<Longrightarrow> m \<in> A
[PROOF STEP]
assume A2: "n \<in> A"
[PROOF STATE]
proof (state)
this:
n \<in> A

goal (1 subgoal):
 1. \<lbrakk>index_set A; n \<in> A; nat_to_ce_set n = nat_to_ce_set m\<rbrakk> \<Longrightarrow> m \<in> A
[PROOF STEP]
assume A3: "nat_to_ce_set n = nat_to_ce_set m"
[PROOF STATE]
proof (state)
this:
nat_to_ce_set n = nat_to_ce_set m

goal (1 subgoal):
 1. \<lbrakk>index_set A; n \<in> A; nat_to_ce_set n = nat_to_ce_set m\<rbrakk> \<Longrightarrow> m \<in> A
[PROOF STEP]
from A2 A3
[PROOF STATE]
proof (chain)
picking this:
n \<in> A
nat_to_ce_set n = nat_to_ce_set m
[PROOF STEP]
have L1: "n \<in> A \<and> (nat_to_ce_set n = nat_to_ce_set m)"
[PROOF STATE]
proof (prove)
using this:
n \<in> A
nat_to_ce_set n = nat_to_ce_set m

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

goal (1 subgoal):
 1. \<lbrakk>index_set A; n \<in> A; nat_to_ce_set n = nat_to_ce_set m\<rbrakk> \<Longrightarrow> m \<in> A
[PROOF STEP]
from A1
[PROOF STATE]
proof (chain)
picking this:
index_set A
[PROOF STEP]
have L2: "\<forall> n m. n \<in> A \<and> (nat_to_ce_set n = nat_to_ce_set m) \<longrightarrow> m \<in> A"
[PROOF STATE]
proof (prove)
using this:
index_set A

goal (1 subgoal):
 1. \<forall>n m. n \<in> A \<and> nat_to_ce_set n = nat_to_ce_set m \<longrightarrow> m \<in> A
[PROOF STEP]
by (unfold index_set_def)
[PROOF STATE]
proof (state)
this:
\<forall>n m. n \<in> A \<and> nat_to_ce_set n = nat_to_ce_set m \<longrightarrow> m \<in> A

goal (1 subgoal):
 1. \<lbrakk>index_set A; n \<in> A; nat_to_ce_set n = nat_to_ce_set m\<rbrakk> \<Longrightarrow> m \<in> A
[PROOF STEP]
from L1 L2
[PROOF STATE]
proof (chain)
picking this:
n \<in> A \<and> nat_to_ce_set n = nat_to_ce_set m
\<forall>n m. n \<in> A \<and> nat_to_ce_set n = nat_to_ce_set m \<longrightarrow> m \<in> A
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
n \<in> A \<and> nat_to_ce_set n = nat_to_ce_set m
\<forall>n m. n \<in> A \<and> nat_to_ce_set n = nat_to_ce_set m \<longrightarrow> m \<in> A

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

goal:
No subgoals!
[PROOF STEP]
qed


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

goal (1 subgoal):
 1. index_set A \<Longrightarrow> index_set (- A)
[PROOF STEP]
show "index_set (-A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. index_set (- A)
[PROOF STEP]
proof (unfold index_set_def)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>n m. n \<in> - A \<and> nat_to_ce_set n = nat_to_ce_set m \<longrightarrow> m \<in> - A
[PROOF STEP]
show "\<forall>n m. n \<in> - A \<and> nat_to_ce_set n = nat_to_ce_set m \<longrightarrow> m \<in> - A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>n m. n \<in> - A \<and> nat_to_ce_set n = nat_to_ce_set m \<longrightarrow> m \<in> - A
[PROOF STEP]
proof (rule allI, rule allI, rule impI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n m. n \<in> - A \<and> nat_to_ce_set n = nat_to_ce_set m \<Longrightarrow> m \<in> - A
[PROOF STEP]
fix n m
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n m. n \<in> - A \<and> nat_to_ce_set n = nat_to_ce_set m \<Longrightarrow> m \<in> - A
[PROOF STEP]
assume A1: "n \<in> - A \<and> nat_to_ce_set n = nat_to_ce_set m"
[PROOF STATE]
proof (state)
this:
n \<in> - A \<and> nat_to_ce_set n = nat_to_ce_set m

goal (1 subgoal):
 1. \<And>n m. n \<in> - A \<and> nat_to_ce_set n = nat_to_ce_set m \<Longrightarrow> m \<in> - A
[PROOF STEP]
from A1
[PROOF STATE]
proof (chain)
picking this:
n \<in> - A \<and> nat_to_ce_set n = nat_to_ce_set m
[PROOF STEP]
have A2: "n \<in> -A"
[PROOF STATE]
proof (prove)
using this:
n \<in> - A \<and> nat_to_ce_set n = nat_to_ce_set m

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

goal (1 subgoal):
 1. \<And>n m. n \<in> - A \<and> nat_to_ce_set n = nat_to_ce_set m \<Longrightarrow> m \<in> - A
[PROOF STEP]
from A1
[PROOF STATE]
proof (chain)
picking this:
n \<in> - A \<and> nat_to_ce_set n = nat_to_ce_set m
[PROOF STEP]
have A3: "nat_to_ce_set m = nat_to_ce_set n"
[PROOF STATE]
proof (prove)
using this:
n \<in> - A \<and> nat_to_ce_set n = nat_to_ce_set m

goal (1 subgoal):
 1. nat_to_ce_set m = nat_to_ce_set n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nat_to_ce_set m = nat_to_ce_set n

goal (1 subgoal):
 1. \<And>n m. n \<in> - A \<and> nat_to_ce_set n = nat_to_ce_set m \<Longrightarrow> m \<in> - A
[PROOF STEP]
show "m \<in> - A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m \<in> - A
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. m \<in> A \<Longrightarrow> False
[PROOF STEP]
assume "m \<in> A"
[PROOF STATE]
proof (state)
this:
m \<in> A

goal (1 subgoal):
 1. m \<in> A \<Longrightarrow> False
[PROOF STEP]
from A this A3
[PROOF STATE]
proof (chain)
picking this:
index_set A
m \<in> A
nat_to_ce_set m = nat_to_ce_set n
[PROOF STEP]
have "n \<in> A"
[PROOF STATE]
proof (prove)
using this:
index_set A
m \<in> A
nat_to_ce_set m = nat_to_ce_set n

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

goal (1 subgoal):
 1. m \<in> A \<Longrightarrow> False
[PROOF STEP]
with A2
[PROOF STATE]
proof (chain)
picking this:
n \<in> - A
n \<in> A
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
n \<in> - A
n \<in> A

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

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>n m. n \<in> - A \<and> nat_to_ce_set n = nat_to_ce_set m \<longrightarrow> m \<in> - A

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
index_set (- A)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Rice_lm_1: "\<lbrakk> index_set A; A \<noteq> {}; A \<noteq> UNIV; \<exists> n \<in> A. nat_to_ce_set n = {} \<rbrakk> \<Longrightarrow> one_reducible_to univ_ce (- A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>index_set A; A \<noteq> {}; A \<noteq> UNIV; \<exists>n\<in>A. nat_to_ce_set n = {}\<rbrakk> \<Longrightarrow> one_reducible_to univ_ce (- A)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>index_set A; A \<noteq> {}; A \<noteq> UNIV; \<exists>n\<in>A. nat_to_ce_set n = {}\<rbrakk> \<Longrightarrow> one_reducible_to univ_ce (- A)
[PROOF STEP]
assume A1: "index_set A"
[PROOF STATE]
proof (state)
this:
index_set A

goal (1 subgoal):
 1. \<lbrakk>index_set A; A \<noteq> {}; A \<noteq> UNIV; \<exists>n\<in>A. nat_to_ce_set n = {}\<rbrakk> \<Longrightarrow> one_reducible_to univ_ce (- A)
[PROOF STEP]
assume A2: "A \<noteq> {}"
[PROOF STATE]
proof (state)
this:
A \<noteq> {}

goal (1 subgoal):
 1. \<lbrakk>index_set A; A \<noteq> {}; A \<noteq> UNIV; \<exists>n\<in>A. nat_to_ce_set n = {}\<rbrakk> \<Longrightarrow> one_reducible_to univ_ce (- A)
[PROOF STEP]
assume A3: "A \<noteq> UNIV"
[PROOF STATE]
proof (state)
this:
A \<noteq> UNIV

goal (1 subgoal):
 1. \<lbrakk>index_set A; A \<noteq> {}; A \<noteq> UNIV; \<exists>n\<in>A. nat_to_ce_set n = {}\<rbrakk> \<Longrightarrow> one_reducible_to univ_ce (- A)
[PROOF STEP]
assume "\<exists> n \<in> A. nat_to_ce_set n = {}"
[PROOF STATE]
proof (state)
this:
\<exists>n\<in>A. nat_to_ce_set n = {}

goal (1 subgoal):
 1. \<lbrakk>index_set A; A \<noteq> {}; A \<noteq> UNIV; \<exists>n\<in>A. nat_to_ce_set n = {}\<rbrakk> \<Longrightarrow> one_reducible_to univ_ce (- A)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>n\<in>A. nat_to_ce_set n = {}
[PROOF STEP]
obtain e_0 where e_0_in_A: "e_0 \<in> A" and e_0_empty: "nat_to_ce_set e_0 = {}"
[PROOF STATE]
proof (prove)
using this:
\<exists>n\<in>A. nat_to_ce_set n = {}

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

goal (1 subgoal):
 1. \<lbrakk>index_set A; A \<noteq> {}; A \<noteq> UNIV; \<exists>n\<in>A. nat_to_ce_set n = {}\<rbrakk> \<Longrightarrow> one_reducible_to univ_ce (- A)
[PROOF STEP]
from e_0_in_A A3
[PROOF STATE]
proof (chain)
picking this:
e_0 \<in> A
A \<noteq> UNIV
[PROOF STEP]
obtain e_1 where e_1_not_in_A: "e_1 \<in> (- A)"
[PROOF STATE]
proof (prove)
using this:
e_0 \<in> A
A \<noteq> UNIV

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

goal (1 subgoal):
 1. \<lbrakk>index_set A; A \<noteq> {}; A \<noteq> UNIV; \<exists>n\<in>A. nat_to_ce_set n = {}\<rbrakk> \<Longrightarrow> one_reducible_to univ_ce (- A)
[PROOF STEP]
with e_0_in_A
[PROOF STATE]
proof (chain)
picking this:
e_0 \<in> A
e_1 \<in> - A
[PROOF STEP]
have e_0_neq_e_1: "e_0 \<noteq> e_1"
[PROOF STATE]
proof (prove)
using this:
e_0 \<in> A
e_1 \<in> - A

goal (1 subgoal):
 1. e_0 \<noteq> e_1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
e_0 \<noteq> e_1

goal (1 subgoal):
 1. \<lbrakk>index_set A; A \<noteq> {}; A \<noteq> UNIV; \<exists>n\<in>A. nat_to_ce_set n = {}\<rbrakk> \<Longrightarrow> one_reducible_to univ_ce (- A)
[PROOF STEP]
have "nat_to_ce_set e_0 \<noteq> nat_to_ce_set e_1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nat_to_ce_set e_0 \<noteq> nat_to_ce_set e_1
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. nat_to_ce_set e_0 = nat_to_ce_set e_1 \<Longrightarrow> False
[PROOF STEP]
assume "nat_to_ce_set e_0 = nat_to_ce_set e_1"
[PROOF STATE]
proof (state)
this:
nat_to_ce_set e_0 = nat_to_ce_set e_1

goal (1 subgoal):
 1. nat_to_ce_set e_0 = nat_to_ce_set e_1 \<Longrightarrow> False
[PROOF STEP]
with A1 e_0_in_A
[PROOF STATE]
proof (chain)
picking this:
index_set A
e_0 \<in> A
nat_to_ce_set e_0 = nat_to_ce_set e_1
[PROOF STEP]
have "e_1 \<in> A"
[PROOF STATE]
proof (prove)
using this:
index_set A
e_0 \<in> A
nat_to_ce_set e_0 = nat_to_ce_set e_1

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

goal (1 subgoal):
 1. nat_to_ce_set e_0 = nat_to_ce_set e_1 \<Longrightarrow> False
[PROOF STEP]
with e_1_not_in_A
[PROOF STATE]
proof (chain)
picking this:
e_1 \<in> - A
e_1 \<in> A
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
e_1 \<in> - A
e_1 \<in> A

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
nat_to_ce_set e_0 \<noteq> nat_to_ce_set e_1

goal (1 subgoal):
 1. \<lbrakk>index_set A; A \<noteq> {}; A \<noteq> UNIV; \<exists>n\<in>A. nat_to_ce_set n = {}\<rbrakk> \<Longrightarrow> one_reducible_to univ_ce (- A)
[PROOF STEP]
with e_0_empty
[PROOF STATE]
proof (chain)
picking this:
nat_to_ce_set e_0 = {}
nat_to_ce_set e_0 \<noteq> nat_to_ce_set e_1
[PROOF STEP]
have e1_not_empty: "nat_to_ce_set e_1 \<noteq> {}"
[PROOF STATE]
proof (prove)
using this:
nat_to_ce_set e_0 = {}
nat_to_ce_set e_0 \<noteq> nat_to_ce_set e_1

goal (1 subgoal):
 1. nat_to_ce_set e_1 \<noteq> {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nat_to_ce_set e_1 \<noteq> {}

goal (1 subgoal):
 1. \<lbrakk>index_set A; A \<noteq> {}; A \<noteq> UNIV; \<exists>n\<in>A. nat_to_ce_set n = {}\<rbrakk> \<Longrightarrow> one_reducible_to univ_ce (- A)
[PROOF STEP]
define we_1 where "we_1 = nat_to_ce_set e_1"
[PROOF STATE]
proof (state)
this:
we_1 = nat_to_ce_set e_1

goal (1 subgoal):
 1. \<lbrakk>index_set A; A \<noteq> {}; A \<noteq> UNIV; \<exists>n\<in>A. nat_to_ce_set n = {}\<rbrakk> \<Longrightarrow> one_reducible_to univ_ce (- A)
[PROOF STEP]
from e1_not_empty
[PROOF STATE]
proof (chain)
picking this:
nat_to_ce_set e_1 \<noteq> {}
[PROOF STEP]
have we_1_not_empty: "we_1 \<noteq> {}"
[PROOF STATE]
proof (prove)
using this:
nat_to_ce_set e_1 \<noteq> {}

goal (1 subgoal):
 1. we_1 \<noteq> {}
[PROOF STEP]
by (unfold we_1_def)
[PROOF STATE]
proof (state)
this:
we_1 \<noteq> {}

goal (1 subgoal):
 1. \<lbrakk>index_set A; A \<noteq> {}; A \<noteq> UNIV; \<exists>n\<in>A. nat_to_ce_set n = {}\<rbrakk> \<Longrightarrow> one_reducible_to univ_ce (- A)
[PROOF STEP]
define r where "r = univ_ce \<times> we_1"
[PROOF STATE]
proof (state)
this:
r = univ_ce \<times> we_1

goal (1 subgoal):
 1. \<lbrakk>index_set A; A \<noteq> {}; A \<noteq> UNIV; \<exists>n\<in>A. nat_to_ce_set n = {}\<rbrakk> \<Longrightarrow> one_reducible_to univ_ce (- A)
[PROOF STEP]
have loc_lm_1: "\<And> x. x \<in> univ_ce \<Longrightarrow> \<forall> y. (y \<in> we_1) = ((x,y) \<in> r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> univ_ce \<Longrightarrow> \<forall>y. (y \<in> we_1) = ((x, y) \<in> r)
[PROOF STEP]
by (unfold r_def, auto)
[PROOF STATE]
proof (state)
this:
?x \<in> univ_ce \<Longrightarrow> \<forall>y. (y \<in> we_1) = ((?x, y) \<in> r)

goal (1 subgoal):
 1. \<lbrakk>index_set A; A \<noteq> {}; A \<noteq> UNIV; \<exists>n\<in>A. nat_to_ce_set n = {}\<rbrakk> \<Longrightarrow> one_reducible_to univ_ce (- A)
[PROOF STEP]
have loc_lm_2: "\<And> x. x \<notin> univ_ce \<Longrightarrow> \<forall> y. (y \<in> {}) = ((x,y) \<in> r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<notin> univ_ce \<Longrightarrow> \<forall>y. (y \<in> {}) = ((x, y) \<in> r)
[PROOF STEP]
by (unfold r_def, auto)
[PROOF STATE]
proof (state)
this:
?x \<notin> univ_ce \<Longrightarrow> \<forall>y. (y \<in> {}) = ((?x, y) \<in> r)

goal (1 subgoal):
 1. \<lbrakk>index_set A; A \<noteq> {}; A \<noteq> UNIV; \<exists>n\<in>A. nat_to_ce_set n = {}\<rbrakk> \<Longrightarrow> one_reducible_to univ_ce (- A)
[PROOF STEP]
have r_ce: "r \<in> ce_rels"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r \<in> ce_rels
[PROOF STEP]
proof (unfold r_def, rule ce_rel_lm_29)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. univ_ce \<in> ce_sets
 2. we_1 \<in> ce_sets
[PROOF STEP]
show "univ_ce \<in> ce_sets"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. univ_ce \<in> ce_sets
[PROOF STEP]
by (rule univ_is_ce)
[PROOF STATE]
proof (state)
this:
univ_ce \<in> ce_sets

goal (1 subgoal):
 1. we_1 \<in> ce_sets
[PROOF STEP]
show "we_1 \<in> ce_sets"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. we_1 \<in> ce_sets
[PROOF STEP]
by (unfold we_1_def, rule nat_to_ce_set_into_ce)
[PROOF STATE]
proof (state)
this:
we_1 \<in> ce_sets

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

goal (1 subgoal):
 1. \<lbrakk>index_set A; A \<noteq> {}; A \<noteq> UNIV; \<exists>n\<in>A. nat_to_ce_set n = {}\<rbrakk> \<Longrightarrow> one_reducible_to univ_ce (- A)
[PROOF STEP]
define we_n where "we_n = ce_rel_to_set r"
[PROOF STATE]
proof (state)
this:
we_n = ce_rel_to_set r

goal (1 subgoal):
 1. \<lbrakk>index_set A; A \<noteq> {}; A \<noteq> UNIV; \<exists>n\<in>A. nat_to_ce_set n = {}\<rbrakk> \<Longrightarrow> one_reducible_to univ_ce (- A)
[PROOF STEP]
from r_ce
[PROOF STATE]
proof (chain)
picking this:
r \<in> ce_rels
[PROOF STEP]
have we_n_ce: "we_n \<in> ce_sets"
[PROOF STATE]
proof (prove)
using this:
r \<in> ce_rels

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

goal (1 subgoal):
 1. \<lbrakk>index_set A; A \<noteq> {}; A \<noteq> UNIV; \<exists>n\<in>A. nat_to_ce_set n = {}\<rbrakk> \<Longrightarrow> one_reducible_to univ_ce (- A)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
we_n \<in> ce_sets
[PROOF STEP]
have "\<exists> n. we_n = nat_to_ce_set n"
[PROOF STATE]
proof (prove)
using this:
we_n \<in> ce_sets

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

goal (1 subgoal):
 1. \<lbrakk>index_set A; A \<noteq> {}; A \<noteq> UNIV; \<exists>n\<in>A. nat_to_ce_set n = {}\<rbrakk> \<Longrightarrow> one_reducible_to univ_ce (- A)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>n. we_n = nat_to_ce_set n
[PROOF STEP]
obtain n where we_n_df1: "we_n = nat_to_ce_set n"
[PROOF STATE]
proof (prove)
using this:
\<exists>n. we_n = nat_to_ce_set n

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

goal (1 subgoal):
 1. \<lbrakk>index_set A; A \<noteq> {}; A \<noteq> UNIV; \<exists>n\<in>A. nat_to_ce_set n = {}\<rbrakk> \<Longrightarrow> one_reducible_to univ_ce (- A)
[PROOF STEP]
define f where "f x = s_ce n x" for x
[PROOF STATE]
proof (state)
this:
f ?x = s_ce n ?x

goal (1 subgoal):
 1. \<lbrakk>index_set A; A \<noteq> {}; A \<noteq> UNIV; \<exists>n\<in>A. nat_to_ce_set n = {}\<rbrakk> \<Longrightarrow> one_reducible_to univ_ce (- A)
[PROOF STEP]
from s_ce_is_pr
[PROOF STATE]
proof (chain)
picking this:
s_ce \<in> PrimRec2
[PROOF STEP]
have f_is_pr: "f \<in> PrimRec1"
[PROOF STATE]
proof (prove)
using this:
s_ce \<in> PrimRec2

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

goal (1 subgoal):
 1. s_ce n \<in> PrimRec1
[PROOF STEP]
by prec
[PROOF STATE]
proof (state)
this:
f \<in> PrimRec1

goal (1 subgoal):
 1. \<lbrakk>index_set A; A \<noteq> {}; A \<noteq> UNIV; \<exists>n\<in>A. nat_to_ce_set n = {}\<rbrakk> \<Longrightarrow> one_reducible_to univ_ce (- A)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
f \<in> PrimRec1
[PROOF STEP]
have f_tr: "total_recursive f"
[PROOF STATE]
proof (prove)
using this:
f \<in> PrimRec1

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

goal (1 subgoal):
 1. \<lbrakk>index_set A; A \<noteq> {}; A \<noteq> UNIV; \<exists>n\<in>A. nat_to_ce_set n = {}\<rbrakk> \<Longrightarrow> one_reducible_to univ_ce (- A)
[PROOF STEP]
have f_inj: "inj f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj f
[PROOF STEP]
proof (rule injI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. f x = f y \<Longrightarrow> x = y
[PROOF STEP]
fix x y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. f x = f y \<Longrightarrow> x = y
[PROOF STEP]
assume "f x = f y"
[PROOF STATE]
proof (state)
this:
f x = f y

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

goal (1 subgoal):
 1. s_ce n x = s_ce n y
[PROOF STEP]
by (unfold f_def)
[PROOF STATE]
proof (state)
this:
s_ce n x = s_ce n y

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

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

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

goal (1 subgoal):
 1. \<lbrakk>index_set A; A \<noteq> {}; A \<noteq> UNIV; \<exists>n\<in>A. nat_to_ce_set n = {}\<rbrakk> \<Longrightarrow> one_reducible_to univ_ce (- A)
[PROOF STEP]
have loc_lm_3: "\<forall> x y. (c_pair x y \<in> we_n) = (y \<in> nat_to_ce_set (f x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x y. (c_pair x y \<in> we_n) = (y \<in> nat_to_ce_set (f x))
[PROOF STEP]
proof (rule allI, rule allI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. (c_pair x y \<in> we_n) = (y \<in> nat_to_ce_set (f x))
[PROOF STEP]
fix x y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. (c_pair x y \<in> we_n) = (y \<in> nat_to_ce_set (f x))
[PROOF STEP]
show "(c_pair x y \<in> we_n) = (y \<in> nat_to_ce_set (f x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (c_pair x y \<in> we_n) = (y \<in> nat_to_ce_set (f x))
[PROOF STEP]
by (unfold f_def, unfold we_n_df1, simp add: s_ce_1_1_th)
[PROOF STATE]
proof (state)
this:
(c_pair x y \<in> we_n) = (y \<in> nat_to_ce_set (f x))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>x y. (c_pair x y \<in> we_n) = (y \<in> nat_to_ce_set (f x))

goal (1 subgoal):
 1. \<lbrakk>index_set A; A \<noteq> {}; A \<noteq> UNIV; \<exists>n\<in>A. nat_to_ce_set n = {}\<rbrakk> \<Longrightarrow> one_reducible_to univ_ce (- A)
[PROOF STEP]
from A1
[PROOF STATE]
proof (chain)
picking this:
index_set A
[PROOF STEP]
have loc_lm_4: "index_set (- A)"
[PROOF STATE]
proof (prove)
using this:
index_set A

goal (1 subgoal):
 1. index_set (- A)
[PROOF STEP]
by (rule index_set_lm_2)
[PROOF STATE]
proof (state)
this:
index_set (- A)

goal (1 subgoal):
 1. \<lbrakk>index_set A; A \<noteq> {}; A \<noteq> UNIV; \<exists>n\<in>A. nat_to_ce_set n = {}\<rbrakk> \<Longrightarrow> one_reducible_to univ_ce (- A)
[PROOF STEP]
have loc_lm_5: "\<forall> x. (x \<in> univ_ce) = (f x \<in> -A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x. (x \<in> univ_ce) = (f x \<in> - A)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. (x \<in> univ_ce) = (f x \<in> - A)
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. (x \<in> univ_ce) = (f x \<in> - A)
[PROOF STEP]
show "(x \<in> univ_ce) = (f x \<in> -A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<in> univ_ce) = (f x \<in> - A)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x \<in> univ_ce \<Longrightarrow> f x \<in> - A
 2. f x \<in> - A \<Longrightarrow> x \<in> univ_ce
[PROOF STEP]
assume A: "x \<in> univ_ce"
[PROOF STATE]
proof (state)
this:
x \<in> univ_ce

goal (2 subgoals):
 1. x \<in> univ_ce \<Longrightarrow> f x \<in> - A
 2. f x \<in> - A \<Longrightarrow> x \<in> univ_ce
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> univ_ce
[PROOF STEP]
have S1: "\<forall> y. (y \<in> we_1) = ((x,y) \<in> r)"
[PROOF STATE]
proof (prove)
using this:
x \<in> univ_ce

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

goal (2 subgoals):
 1. x \<in> univ_ce \<Longrightarrow> f x \<in> - A
 2. f x \<in> - A \<Longrightarrow> x \<in> univ_ce
[PROOF STEP]
from ce_rel_lm_12
[PROOF STATE]
proof (chain)
picking this:
(c_pair ?x ?y \<in> ce_rel_to_set ?r) = ((?x, ?y) \<in> ?r)
[PROOF STEP]
have "\<forall> y. (c_pair x y \<in> ce_rel_to_set r) = ((x,y) \<in> r)"
[PROOF STATE]
proof (prove)
using this:
(c_pair ?x ?y \<in> ce_rel_to_set ?r) = ((?x, ?y) \<in> ?r)

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

goal (2 subgoals):
 1. x \<in> univ_ce \<Longrightarrow> f x \<in> - A
 2. f x \<in> - A \<Longrightarrow> x \<in> univ_ce
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>y. (c_pair x y \<in> ce_rel_to_set r) = ((x, y) \<in> r)
[PROOF STEP]
have "\<forall> y. ((x,y) \<in> r) = (c_pair x y \<in> we_n)"
[PROOF STATE]
proof (prove)
using this:
\<forall>y. (c_pair x y \<in> ce_rel_to_set r) = ((x, y) \<in> r)

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

goal (2 subgoals):
 1. x \<in> univ_ce \<Longrightarrow> f x \<in> - A
 2. f x \<in> - A \<Longrightarrow> x \<in> univ_ce
[PROOF STEP]
with S1
[PROOF STATE]
proof (chain)
picking this:
\<forall>y. (y \<in> we_1) = ((x, y) \<in> r)
\<forall>y. ((x, y) \<in> r) = (c_pair x y \<in> we_n)
[PROOF STEP]
have "\<forall> y. (y \<in> we_1) = (c_pair x y \<in> we_n)"
[PROOF STATE]
proof (prove)
using this:
\<forall>y. (y \<in> we_1) = ((x, y) \<in> r)
\<forall>y. ((x, y) \<in> r) = (c_pair x y \<in> we_n)

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

goal (2 subgoals):
 1. x \<in> univ_ce \<Longrightarrow> f x \<in> - A
 2. f x \<in> - A \<Longrightarrow> x \<in> univ_ce
[PROOF STEP]
with loc_lm_3
[PROOF STATE]
proof (chain)
picking this:
\<forall>x y. (c_pair x y \<in> we_n) = (y \<in> nat_to_ce_set (f x))
\<forall>y. (y \<in> we_1) = (c_pair x y \<in> we_n)
[PROOF STEP]
have "\<forall> y. (y \<in> we_1) = (y \<in> nat_to_ce_set (f x))"
[PROOF STATE]
proof (prove)
using this:
\<forall>x y. (c_pair x y \<in> we_n) = (y \<in> nat_to_ce_set (f x))
\<forall>y. (y \<in> we_1) = (c_pair x y \<in> we_n)

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

goal (2 subgoals):
 1. x \<in> univ_ce \<Longrightarrow> f x \<in> - A
 2. f x \<in> - A \<Longrightarrow> x \<in> univ_ce
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>y. (y \<in> we_1) = (y \<in> nat_to_ce_set (f x))
[PROOF STEP]
have S2: "we_1 = nat_to_ce_set (f x)"
[PROOF STATE]
proof (prove)
using this:
\<forall>y. (y \<in> we_1) = (y \<in> nat_to_ce_set (f x))

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

goal (2 subgoals):
 1. x \<in> univ_ce \<Longrightarrow> f x \<in> - A
 2. f x \<in> - A \<Longrightarrow> x \<in> univ_ce
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
we_1 = nat_to_ce_set (f x)
[PROOF STEP]
have "nat_to_ce_set e_1 = nat_to_ce_set (f x)"
[PROOF STATE]
proof (prove)
using this:
we_1 = nat_to_ce_set (f x)

goal (1 subgoal):
 1. nat_to_ce_set e_1 = nat_to_ce_set (f x)
[PROOF STEP]
by (unfold we_1_def)
[PROOF STATE]
proof (state)
this:
nat_to_ce_set e_1 = nat_to_ce_set (f x)

goal (2 subgoals):
 1. x \<in> univ_ce \<Longrightarrow> f x \<in> - A
 2. f x \<in> - A \<Longrightarrow> x \<in> univ_ce
[PROOF STEP]
with loc_lm_4 e_1_not_in_A
[PROOF STATE]
proof (chain)
picking this:
index_set (- A)
e_1 \<in> - A
nat_to_ce_set e_1 = nat_to_ce_set (f x)
[PROOF STEP]
show "f x \<in> -A"
[PROOF STATE]
proof (prove)
using this:
index_set (- A)
e_1 \<in> - A
nat_to_ce_set e_1 = nat_to_ce_set (f x)

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

goal (1 subgoal):
 1. f x \<in> - A \<Longrightarrow> x \<in> univ_ce
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. f x \<in> - A \<Longrightarrow> x \<in> univ_ce
[PROOF STEP]
show " f x \<in> - A \<Longrightarrow> x \<in> univ_ce"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f x \<in> - A \<Longrightarrow> x \<in> univ_ce
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>f x \<in> - A; x \<notin> univ_ce\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume fx_in_A: "f x \<in> - A"
[PROOF STATE]
proof (state)
this:
f x \<in> - A

goal (1 subgoal):
 1. \<lbrakk>f x \<in> - A; x \<notin> univ_ce\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume x_not_in_univ: "x \<notin> univ_ce"
[PROOF STATE]
proof (state)
this:
x \<notin> univ_ce

goal (1 subgoal):
 1. \<lbrakk>f x \<in> - A; x \<notin> univ_ce\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<notin> univ_ce
[PROOF STEP]
have S1: "\<forall> y. (y \<in> {}) = ((x,y) \<in> r)"
[PROOF STATE]
proof (prove)
using this:
x \<notin> univ_ce

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

goal (1 subgoal):
 1. \<lbrakk>f x \<in> - A; x \<notin> univ_ce\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
from ce_rel_lm_12
[PROOF STATE]
proof (chain)
picking this:
(c_pair ?x ?y \<in> ce_rel_to_set ?r) = ((?x, ?y) \<in> ?r)
[PROOF STEP]
have "\<forall> y. (c_pair x y \<in> ce_rel_to_set r) = ((x,y) \<in> r)"
[PROOF STATE]
proof (prove)
using this:
(c_pair ?x ?y \<in> ce_rel_to_set ?r) = ((?x, ?y) \<in> ?r)

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

goal (1 subgoal):
 1. \<lbrakk>f x \<in> - A; x \<notin> univ_ce\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>y. (c_pair x y \<in> ce_rel_to_set r) = ((x, y) \<in> r)
[PROOF STEP]
have "\<forall> y. ((x,y) \<in> r) = (c_pair x y \<in> we_n)"
[PROOF STATE]
proof (prove)
using this:
\<forall>y. (c_pair x y \<in> ce_rel_to_set r) = ((x, y) \<in> r)

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

goal (1 subgoal):
 1. \<lbrakk>f x \<in> - A; x \<notin> univ_ce\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
with S1
[PROOF STATE]
proof (chain)
picking this:
\<forall>y. (y \<in> {}) = ((x, y) \<in> r)
\<forall>y. ((x, y) \<in> r) = (c_pair x y \<in> we_n)
[PROOF STEP]
have "\<forall> y. (y \<in> {}) = (c_pair x y \<in> we_n)"
[PROOF STATE]
proof (prove)
using this:
\<forall>y. (y \<in> {}) = ((x, y) \<in> r)
\<forall>y. ((x, y) \<in> r) = (c_pair x y \<in> we_n)

goal (1 subgoal):
 1. \<forall>y. (y \<in> {}) = (c_pair x y \<in> we_n)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>y. (y \<in> {}) = (c_pair x y \<in> we_n)

goal (1 subgoal):
 1. \<lbrakk>f x \<in> - A; x \<notin> univ_ce\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
with loc_lm_3
[PROOF STATE]
proof (chain)
picking this:
\<forall>x y. (c_pair x y \<in> we_n) = (y \<in> nat_to_ce_set (f x))
\<forall>y. (y \<in> {}) = (c_pair x y \<in> we_n)
[PROOF STEP]
have "\<forall> y. (y \<in> {}) = (y \<in> nat_to_ce_set (f x))"
[PROOF STATE]
proof (prove)
using this:
\<forall>x y. (c_pair x y \<in> we_n) = (y \<in> nat_to_ce_set (f x))
\<forall>y. (y \<in> {}) = (c_pair x y \<in> we_n)

goal (1 subgoal):
 1. \<forall>y. (y \<in> {}) = (y \<in> nat_to_ce_set (f x))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>y. (y \<in> {}) = (y \<in> nat_to_ce_set (f x))

goal (1 subgoal):
 1. \<lbrakk>f x \<in> - A; x \<notin> univ_ce\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>y. (y \<in> {}) = (y \<in> nat_to_ce_set (f x))
[PROOF STEP]
have S2: "{} = nat_to_ce_set (f x)"
[PROOF STATE]
proof (prove)
using this:
\<forall>y. (y \<in> {}) = (y \<in> nat_to_ce_set (f x))

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

goal (1 subgoal):
 1. \<lbrakk>f x \<in> - A; x \<notin> univ_ce\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
{} = nat_to_ce_set (f x)
[PROOF STEP]
have "nat_to_ce_set e_0 = nat_to_ce_set (f x)"
[PROOF STATE]
proof (prove)
using this:
{} = nat_to_ce_set (f x)

goal (1 subgoal):
 1. nat_to_ce_set e_0 = nat_to_ce_set (f x)
[PROOF STEP]
by (unfold e_0_empty)
[PROOF STATE]
proof (state)
this:
nat_to_ce_set e_0 = nat_to_ce_set (f x)

goal (1 subgoal):
 1. \<lbrakk>f x \<in> - A; x \<notin> univ_ce\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
with A1 e_0_in_A
[PROOF STATE]
proof (chain)
picking this:
index_set A
e_0 \<in> A
nat_to_ce_set e_0 = nat_to_ce_set (f x)
[PROOF STEP]
have "f x \<in> A"
[PROOF STATE]
proof (prove)
using this:
index_set A
e_0 \<in> A
nat_to_ce_set e_0 = nat_to_ce_set (f x)

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

goal (1 subgoal):
 1. \<lbrakk>f x \<in> - A; x \<notin> univ_ce\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
with fx_in_A
[PROOF STATE]
proof (chain)
picking this:
f x \<in> - A
f x \<in> A
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
f x \<in> - A
f x \<in> A

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
f x \<in> - A \<Longrightarrow> x \<in> univ_ce

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>x. (x \<in> univ_ce) = (f x \<in> - A)

goal (1 subgoal):
 1. \<lbrakk>index_set A; A \<noteq> {}; A \<noteq> UNIV; \<exists>n\<in>A. nat_to_ce_set n = {}\<rbrakk> \<Longrightarrow> one_reducible_to univ_ce (- A)
[PROOF STEP]
with f_tr f_inj
[PROOF STATE]
proof (chain)
picking this:
total_recursive f
inj f
\<forall>x. (x \<in> univ_ce) = (f x \<in> - A)
[PROOF STEP]
have "one_reducible_to_via univ_ce (-A) f"
[PROOF STATE]
proof (prove)
using this:
total_recursive f
inj f
\<forall>x. (x \<in> univ_ce) = (f x \<in> - A)

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

goal (1 subgoal):
 1. \<lbrakk>index_set A; A \<noteq> {}; A \<noteq> UNIV; \<exists>n\<in>A. nat_to_ce_set n = {}\<rbrakk> \<Longrightarrow> one_reducible_to univ_ce (- A)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
one_reducible_to_via univ_ce (- A) f
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
one_reducible_to_via univ_ce (- A) f

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Rice_lm_2: "\<lbrakk> index_set A; A \<noteq> {}; A \<noteq> UNIV; n \<in> A;  nat_to_ce_set n = {} \<rbrakk> \<Longrightarrow> one_reducible_to univ_ce (- A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>index_set A; A \<noteq> {}; A \<noteq> UNIV; n \<in> A; nat_to_ce_set n = {}\<rbrakk> \<Longrightarrow> one_reducible_to univ_ce (- A)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>index_set A; A \<noteq> {}; A \<noteq> UNIV; n \<in> A; nat_to_ce_set n = {}\<rbrakk> \<Longrightarrow> one_reducible_to univ_ce (- A)
[PROOF STEP]
assume A1: "index_set A"
[PROOF STATE]
proof (state)
this:
index_set A

goal (1 subgoal):
 1. \<lbrakk>index_set A; A \<noteq> {}; A \<noteq> UNIV; n \<in> A; nat_to_ce_set n = {}\<rbrakk> \<Longrightarrow> one_reducible_to univ_ce (- A)
[PROOF STEP]
assume A2: "A \<noteq> {}"
[PROOF STATE]
proof (state)
this:
A \<noteq> {}

goal (1 subgoal):
 1. \<lbrakk>index_set A; A \<noteq> {}; A \<noteq> UNIV; n \<in> A; nat_to_ce_set n = {}\<rbrakk> \<Longrightarrow> one_reducible_to univ_ce (- A)
[PROOF STEP]
assume A3: "A \<noteq> UNIV"
[PROOF STATE]
proof (state)
this:
A \<noteq> UNIV

goal (1 subgoal):
 1. \<lbrakk>index_set A; A \<noteq> {}; A \<noteq> UNIV; n \<in> A; nat_to_ce_set n = {}\<rbrakk> \<Longrightarrow> one_reducible_to univ_ce (- A)
[PROOF STEP]
assume A4: "n \<in> A"
[PROOF STATE]
proof (state)
this:
n \<in> A

goal (1 subgoal):
 1. \<lbrakk>index_set A; A \<noteq> {}; A \<noteq> UNIV; n \<in> A; nat_to_ce_set n = {}\<rbrakk> \<Longrightarrow> one_reducible_to univ_ce (- A)
[PROOF STEP]
assume A5: "nat_to_ce_set n = {}"
[PROOF STATE]
proof (state)
this:
nat_to_ce_set n = {}

goal (1 subgoal):
 1. \<lbrakk>index_set A; A \<noteq> {}; A \<noteq> UNIV; n \<in> A; nat_to_ce_set n = {}\<rbrakk> \<Longrightarrow> one_reducible_to univ_ce (- A)
[PROOF STEP]
from A4 A5
[PROOF STATE]
proof (chain)
picking this:
n \<in> A
nat_to_ce_set n = {}
[PROOF STEP]
have S1: "\<exists> n \<in> A. nat_to_ce_set n = {}"
[PROOF STATE]
proof (prove)
using this:
n \<in> A
nat_to_ce_set n = {}

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

goal (1 subgoal):
 1. \<lbrakk>index_set A; A \<noteq> {}; A \<noteq> UNIV; n \<in> A; nat_to_ce_set n = {}\<rbrakk> \<Longrightarrow> one_reducible_to univ_ce (- A)
[PROOF STEP]
from A1 A2 A3 S1
[PROOF STATE]
proof (chain)
picking this:
index_set A
A \<noteq> {}
A \<noteq> UNIV
\<exists>n\<in>A. nat_to_ce_set n = {}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
index_set A
A \<noteq> {}
A \<noteq> UNIV
\<exists>n\<in>A. nat_to_ce_set n = {}

goal (1 subgoal):
 1. one_reducible_to univ_ce (- A)
[PROOF STEP]
by (rule Rice_lm_1)
[PROOF STATE]
proof (state)
this:
one_reducible_to univ_ce (- A)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem Rice_1: "\<lbrakk> index_set A; A \<noteq> {}; A \<noteq> UNIV \<rbrakk> \<Longrightarrow> one_reducible_to univ_ce A \<or> one_reducible_to univ_ce (- A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>index_set A; A \<noteq> {}; A \<noteq> UNIV\<rbrakk> \<Longrightarrow> one_reducible_to univ_ce A \<or> one_reducible_to univ_ce (- A)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>index_set A; A \<noteq> {}; A \<noteq> UNIV\<rbrakk> \<Longrightarrow> one_reducible_to univ_ce A \<or> one_reducible_to univ_ce (- A)
[PROOF STEP]
assume A1: "index_set A"
[PROOF STATE]
proof (state)
this:
index_set A

goal (1 subgoal):
 1. \<lbrakk>index_set A; A \<noteq> {}; A \<noteq> UNIV\<rbrakk> \<Longrightarrow> one_reducible_to univ_ce A \<or> one_reducible_to univ_ce (- A)
[PROOF STEP]
assume A2: "A \<noteq> {}"
[PROOF STATE]
proof (state)
this:
A \<noteq> {}

goal (1 subgoal):
 1. \<lbrakk>index_set A; A \<noteq> {}; A \<noteq> UNIV\<rbrakk> \<Longrightarrow> one_reducible_to univ_ce A \<or> one_reducible_to univ_ce (- A)
[PROOF STEP]
assume A3: "A \<noteq> UNIV"
[PROOF STATE]
proof (state)
this:
A \<noteq> UNIV

goal (1 subgoal):
 1. \<lbrakk>index_set A; A \<noteq> {}; A \<noteq> UNIV\<rbrakk> \<Longrightarrow> one_reducible_to univ_ce A \<or> one_reducible_to univ_ce (- A)
[PROOF STEP]
from ce_empty
[PROOF STATE]
proof (chain)
picking this:
{} \<in> ce_sets
[PROOF STEP]
have "\<exists> n. {} = nat_to_ce_set n"
[PROOF STATE]
proof (prove)
using this:
{} \<in> ce_sets

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

goal (1 subgoal):
 1. \<lbrakk>index_set A; A \<noteq> {}; A \<noteq> UNIV\<rbrakk> \<Longrightarrow> one_reducible_to univ_ce A \<or> one_reducible_to univ_ce (- A)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>n. {} = nat_to_ce_set n
[PROOF STEP]
obtain n where n_empty: "nat_to_ce_set n = {}"
[PROOF STATE]
proof (prove)
using this:
\<exists>n. {} = nat_to_ce_set n

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

goal (1 subgoal):
 1. \<lbrakk>index_set A; A \<noteq> {}; A \<noteq> UNIV\<rbrakk> \<Longrightarrow> one_reducible_to univ_ce A \<or> one_reducible_to univ_ce (- A)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. one_reducible_to univ_ce A \<or> one_reducible_to univ_ce (- A)
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> one_reducible_to univ_ce A \<or> one_reducible_to univ_ce (- A)
 2. \<not> ?P \<Longrightarrow> one_reducible_to univ_ce A \<or> one_reducible_to univ_ce (- A)
[PROOF STEP]
assume A: "n \<in> A"
[PROOF STATE]
proof (state)
this:
n \<in> A

goal (2 subgoals):
 1. ?P \<Longrightarrow> one_reducible_to univ_ce A \<or> one_reducible_to univ_ce (- A)
 2. \<not> ?P \<Longrightarrow> one_reducible_to univ_ce A \<or> one_reducible_to univ_ce (- A)
[PROOF STEP]
from A1 A2 A3 A n_empty
[PROOF STATE]
proof (chain)
picking this:
index_set A
A \<noteq> {}
A \<noteq> UNIV
n \<in> A
nat_to_ce_set n = {}
[PROOF STEP]
have "one_reducible_to univ_ce (- A)"
[PROOF STATE]
proof (prove)
using this:
index_set A
A \<noteq> {}
A \<noteq> UNIV
n \<in> A
nat_to_ce_set n = {}

goal (1 subgoal):
 1. one_reducible_to univ_ce (- A)
[PROOF STEP]
by (rule Rice_lm_2)
[PROOF STATE]
proof (state)
this:
one_reducible_to univ_ce (- A)

goal (2 subgoals):
 1. ?P \<Longrightarrow> one_reducible_to univ_ce A \<or> one_reducible_to univ_ce (- A)
 2. \<not> ?P \<Longrightarrow> one_reducible_to univ_ce A \<or> one_reducible_to univ_ce (- A)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
one_reducible_to univ_ce (- A)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
one_reducible_to univ_ce (- A)

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

goal (1 subgoal):
 1. n \<notin> A \<Longrightarrow> one_reducible_to univ_ce A \<or> one_reducible_to univ_ce (- A)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. n \<notin> A \<Longrightarrow> one_reducible_to univ_ce A \<or> one_reducible_to univ_ce (- A)
[PROOF STEP]
assume "n \<notin> A"
[PROOF STATE]
proof (state)
this:
n \<notin> A

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

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

goal (1 subgoal):
 1. n \<notin> A \<Longrightarrow> one_reducible_to univ_ce A \<or> one_reducible_to univ_ce (- A)
[PROOF STEP]
from A1
[PROOF STATE]
proof (chain)
picking this:
index_set A
[PROOF STEP]
have S1: "index_set (- A)"
[PROOF STATE]
proof (prove)
using this:
index_set A

goal (1 subgoal):
 1. index_set (- A)
[PROOF STEP]
by (rule index_set_lm_2)
[PROOF STATE]
proof (state)
this:
index_set (- A)

goal (1 subgoal):
 1. n \<notin> A \<Longrightarrow> one_reducible_to univ_ce A \<or> one_reducible_to univ_ce (- A)
[PROOF STEP]
from A3
[PROOF STATE]
proof (chain)
picking this:
A \<noteq> UNIV
[PROOF STEP]
have S2: "- A \<noteq> {}"
[PROOF STATE]
proof (prove)
using this:
A \<noteq> UNIV

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

goal (1 subgoal):
 1. n \<notin> A \<Longrightarrow> one_reducible_to univ_ce A \<or> one_reducible_to univ_ce (- A)
[PROOF STEP]
from A2
[PROOF STATE]
proof (chain)
picking this:
A \<noteq> {}
[PROOF STEP]
have S3: "- A \<noteq> UNIV"
[PROOF STATE]
proof (prove)
using this:
A \<noteq> {}

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

goal (1 subgoal):
 1. n \<notin> A \<Longrightarrow> one_reducible_to univ_ce A \<or> one_reducible_to univ_ce (- A)
[PROOF STEP]
from S1 S2 S3 A n_empty
[PROOF STATE]
proof (chain)
picking this:
index_set (- A)
- A \<noteq> {}
- A \<noteq> UNIV
n \<in> - A
nat_to_ce_set n = {}
[PROOF STEP]
have "one_reducible_to univ_ce (- (- A))"
[PROOF STATE]
proof (prove)
using this:
index_set (- A)
- A \<noteq> {}
- A \<noteq> UNIV
n \<in> - A
nat_to_ce_set n = {}

goal (1 subgoal):
 1. one_reducible_to univ_ce (- (- A))
[PROOF STEP]
by (rule Rice_lm_2)
[PROOF STATE]
proof (state)
this:
one_reducible_to univ_ce (- (- A))

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

goal (1 subgoal):
 1. one_reducible_to univ_ce A
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
one_reducible_to univ_ce A

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

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
one_reducible_to univ_ce A \<or> one_reducible_to univ_ce (- A)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem Rice_2: "\<lbrakk> index_set A; A \<noteq> {}; A \<noteq> UNIV \<rbrakk> \<Longrightarrow> \<not> computable A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>index_set A; A \<noteq> {}; A \<noteq> UNIV\<rbrakk> \<Longrightarrow> \<not> computable A
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>index_set A; A \<noteq> {}; A \<noteq> UNIV\<rbrakk> \<Longrightarrow> \<not> computable A
[PROOF STEP]
assume A1: "index_set A"
[PROOF STATE]
proof (state)
this:
index_set A

goal (1 subgoal):
 1. \<lbrakk>index_set A; A \<noteq> {}; A \<noteq> UNIV\<rbrakk> \<Longrightarrow> \<not> computable A
[PROOF STEP]
assume A2: "A \<noteq> {}"
[PROOF STATE]
proof (state)
this:
A \<noteq> {}

goal (1 subgoal):
 1. \<lbrakk>index_set A; A \<noteq> {}; A \<noteq> UNIV\<rbrakk> \<Longrightarrow> \<not> computable A
[PROOF STEP]
assume A3: "A \<noteq> UNIV"
[PROOF STATE]
proof (state)
this:
A \<noteq> UNIV

goal (1 subgoal):
 1. \<lbrakk>index_set A; A \<noteq> {}; A \<noteq> UNIV\<rbrakk> \<Longrightarrow> \<not> computable A
[PROOF STEP]
from A1 A2 A3
[PROOF STATE]
proof (chain)
picking this:
index_set A
A \<noteq> {}
A \<noteq> UNIV
[PROOF STEP]
have "one_reducible_to univ_ce A \<or> one_reducible_to univ_ce (- A)"
[PROOF STATE]
proof (prove)
using this:
index_set A
A \<noteq> {}
A \<noteq> UNIV

goal (1 subgoal):
 1. one_reducible_to univ_ce A \<or> one_reducible_to univ_ce (- A)
[PROOF STEP]
by (rule Rice_1)
[PROOF STATE]
proof (state)
this:
one_reducible_to univ_ce A \<or> one_reducible_to univ_ce (- A)

goal (1 subgoal):
 1. \<lbrakk>index_set A; A \<noteq> {}; A \<noteq> UNIV\<rbrakk> \<Longrightarrow> \<not> computable A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
one_reducible_to univ_ce A \<or> one_reducible_to univ_ce (- A)
[PROOF STEP]
have S1: "\<not> one_reducible_to univ_ce A \<longrightarrow> one_reducible_to univ_ce (- A)"
[PROOF STATE]
proof (prove)
using this:
one_reducible_to univ_ce A \<or> one_reducible_to univ_ce (- A)

goal (1 subgoal):
 1. \<not> one_reducible_to univ_ce A \<longrightarrow> one_reducible_to univ_ce (- A)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<not> one_reducible_to univ_ce A \<longrightarrow> one_reducible_to univ_ce (- A)

goal (1 subgoal):
 1. \<lbrakk>index_set A; A \<noteq> {}; A \<noteq> UNIV\<rbrakk> \<Longrightarrow> \<not> computable A
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> computable A
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> \<not> computable A
 2. \<not> ?P \<Longrightarrow> \<not> computable A
[PROOF STEP]
assume "one_reducible_to univ_ce A"
[PROOF STATE]
proof (state)
this:
one_reducible_to univ_ce A

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

goal (1 subgoal):
 1. \<not> computable A
[PROOF STEP]
by (rule one_reducible_lm_1)
[PROOF STATE]
proof (state)
this:
\<not> computable A

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

goal (1 subgoal):
 1. \<not> one_reducible_to univ_ce A \<Longrightarrow> \<not> computable A
[PROOF STEP]
with S1
[PROOF STATE]
proof (chain)
picking this:
\<not> one_reducible_to univ_ce A \<longrightarrow> one_reducible_to univ_ce (- A)
\<not> one_reducible_to univ_ce A
[PROOF STEP]
have "one_reducible_to univ_ce (- A)"
[PROOF STATE]
proof (prove)
using this:
\<not> one_reducible_to univ_ce A \<longrightarrow> one_reducible_to univ_ce (- A)
\<not> one_reducible_to univ_ce A

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

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

goal (1 subgoal):
 1. \<not> computable (- A)
[PROOF STEP]
by (rule one_reducible_lm_1)
[PROOF STATE]
proof (state)
this:
\<not> computable (- A)

goal (1 subgoal):
 1. \<not> one_reducible_to univ_ce A \<Longrightarrow> \<not> computable A
[PROOF STEP]
with computable_complement_3
[PROOF STATE]
proof (chain)
picking this:
computable ?A = computable (- ?A)
\<not> computable (- A)
[PROOF STEP]
show "\<not> computable A"
[PROOF STATE]
proof (prove)
using this:
computable ?A = computable (- ?A)
\<not> computable (- A)

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

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

goal:
No subgoals!
[PROOF STEP]
qed