Theory Recursion-Theory-I.RecEnSet

(*  Title:       Computably enumerable sets of natural numbers
    Author:      Michael Nedzelsky <MichaelNedzelsky at yandex.ru>, 2008
    Maintainer:  Michael Nedzelsky <MichaelNedzelsky at yandex.ru>
*)

section ‹Computably enumerable sets of natural numbers›

theory RecEnSet
imports PRecList PRecFun2 PRecFinSet PRecUnGr
begin

subsection ‹Basic definitions›

definition
  fn_to_set :: "(nat  nat  nat)  nat set" where
  "fn_to_set f = { x.  y. f x y = 0 }"

definition
  ce_sets :: "(nat set) set" where
  "ce_sets = { (fn_to_set p) | p. p  PrimRec2 }"

subsection ‹Basic properties of computably enumerable sets›

lemma ce_set_lm_1: "p  PrimRec2  fn_to_set p  ce_sets" by (auto simp add: ce_sets_def)

lemma ce_set_lm_2: " p  PrimRec2;  x. (x  A) = ( y. p x y = 0)  A  ce_sets"
proof -
  assume p_is_pr: "p  PrimRec2"
  assume " x. (x  A) = ( y. p x y = 0)"
  then have "A = fn_to_set p" by (unfold fn_to_set_def, auto)
  with p_is_pr show "A  ce_sets" by (simp add: ce_set_lm_1)
qed

lemma ce_set_lm_3: "A  ce_sets   p  PrimRec2. A = fn_to_set p"
proof -
  assume "A  ce_sets"
  then have "A  { (fn_to_set p) | p. p  PrimRec2 }" by (simp add: ce_sets_def)
  thus ?thesis by auto
qed

lemma ce_set_lm_4: "A  ce_sets   p  PrimRec2.  x. (x  A) = ( y. p x y = 0)"
proof -
  assume "A  ce_sets"
  then have " p  PrimRec2. A = fn_to_set p" by (rule ce_set_lm_3)
  then obtain p where p_is_pr: "p  PrimRec2" and L1: "A = fn_to_set p" ..
  from p_is_pr L1 show ?thesis by (unfold fn_to_set_def, auto)
qed

lemma ce_set_lm_5: " A  ce_sets; p  PrimRec1   { x . p x  A }  ce_sets"
proof -
  assume A1: "A  ce_sets"
  assume A2: "p  PrimRec1"
  from A1 have " pA  PrimRec2. A = fn_to_set pA" by (rule ce_set_lm_3)
  then obtain pA where pA_is_pr: "pA  PrimRec2" and S1: "A = fn_to_set pA" ..
  from S1 have S2: "A = { x .  y. pA x y = 0 }" by (simp add: fn_to_set_def)
  define q where "q x y = pA (p x) y" for x y
  from pA_is_pr A2 have q_is_pr: "q  PrimRec2" unfolding q_def by prec
  have " x. (p x  A) = ( y. q x y = 0)"
  proof -
    fix x show "(p x  A) = ( y. q x y = 0)"
    proof
      assume A: "p x  A"
      with S2 obtain y where L1: "pA (p x) y = 0" by auto
      then have "q x y = 0" by (simp add: q_def)
      thus " y. q x y = 0" ..
    next
      assume A: "y. q x y = 0"
      then obtain y where L1: "q x y = 0" ..
      then have "pA (p x) y = 0" by (simp add: q_def)
      with S2 show "p x  A" by auto
    qed
  qed
  then have "{ x . p x  A } = { x.  y. q x y = 0 }" by auto
  then have "{ x . p x  A } = fn_to_set q" by (simp add: fn_to_set_def)
  moreover from q_is_pr have "fn_to_set q  ce_sets" by (rule ce_set_lm_1)
  ultimately show ?thesis by auto
qed

lemma ce_set_lm_6: " A  ce_sets; A  {}   q  PrimRec1. A = { q x | x. x  UNIV }"
proof -
  assume A1: "A  ce_sets"
  assume A2: "A  {}"
  from A1 have " pA  PrimRec2. A = fn_to_set pA" by (rule ce_set_lm_3)
  then obtain pA where pA_is_pr: "pA  PrimRec2" and S1: "A = fn_to_set pA" ..
  from S1 have S2: "A = { x.  y. pA x y = 0 }" by (simp add: fn_to_set_def)
  from A2 obtain a where a_in: "a  A" by auto
  define q where "q z = (if pA (c_fst z) (c_snd z) = 0 then c_fst z else a)" for z
  from pA_is_pr have q_is_pr: "q  PrimRec1" unfolding q_def by prec
  have S3: " z. q z  A"
  proof
    fix z show "q z  A"
    proof cases
      assume A: "pA (c_fst z) (c_snd z) = 0"
      with S2 have "c_fst z  A" by auto
      moreover from A q_def have "q z = c_fst z" by simp
      ultimately show "q z  A" by auto
    next
      assume A: "pA (c_fst z) (c_snd z)  0"
      with q_def have "q z = a" by simp
      with a_in show "q z  A" by auto
    qed
  qed
  then have S4: "{ q x | x. x  UNIV }  A" by auto
  have S5: "A  { q x | x. x  UNIV }"
  proof
    fix x assume A: "x  A" show "x  {q x |x. x  UNIV}"
    proof
      from A S2 obtain y where L1: "pA x y = 0" by auto
      let ?z = "c_pair x y"
      from L1 have "q ?z = x" by (simp add: q_def)
      then have " u. q u = x" by blast
      then show "u. x = q u  u  UNIV" by auto
    qed
  qed
  from S4 S5 have S6: "A = { q x | x. x  UNIV }" by auto
  with q_is_pr show ?thesis by blast
qed

lemma ce_set_lm_7: " A  ce_sets; p  PrimRec1  { p x | x. x  A }  ce_sets"
proof -
  assume A1: "A  ce_sets"
  assume A2: "p  PrimRec1"
  let ?B = "{ p x | x. x  A }"
  fix y have S1: "(y  ?B) = ( x. x  A  (y = p x))" by auto
  from A1 have " pA  PrimRec2. A = fn_to_set pA" by (rule ce_set_lm_3)
  then obtain pA where pA_is_pr: "pA  PrimRec2" and S2: "A = fn_to_set pA" ..
  from S2 have S3: "A = { x.  y. pA x y = 0 }" by (simp add: fn_to_set_def)
  define q where "q y t = (if y = p (c_snd t) then pA (c_snd t) (c_fst t) else 1)" for y t
  from pA_is_pr A2 have q_is_pr: "q  PrimRec2" unfolding q_def by prec
  have L1: " y. (y  ?B) = ( z. q y z = 0)"
  proof - fix y show "(y  ?B) = ( z. q y z = 0)"
  proof
    assume AA1: "y  ?B"
    then obtain x0 where LL_2: "x0  A" and LL_3: "y = p x0" by auto
    from S3 have LL_4: "(x0  A) = ( z. pA x0 z = 0)" by auto
    from LL_2 LL_4 obtain z0 where LL_5: "pA x0 z0 = 0" by auto
    define t where "t = c_pair z0 x0"
    from t_def q_def LL_3 LL_5 have "q y t = 0" by simp
    then show " z. q y z = 0" by auto
  next
    assume A1: " z. q y z = 0"
    then obtain z0 where LL_1: "q y z0 = 0" ..
    have LL2: "y = p (c_snd z0)"
    proof (rule ccontr)
      assume "y  p (c_snd z0)"
      with q_def LL_1 have "q y z0 = 1" by auto
      with LL_1 show False by auto
    qed
    from LL2 LL_1 q_def have LL3: "pA (c_snd z0) (c_fst z0) = 0" by auto
    with S3 have LL4: "c_snd z0  A" by auto
    with LL2 show "y  {p x | x. x  A}" by auto
  qed
  qed
  then have L2: "?B = { y | y.  z. q y z = 0}" by auto
  with fn_to_set_def have "?B = fn_to_set q" by auto
  with q_is_pr ce_set_lm_1 show ?thesis by auto
qed

theorem ce_empty: "{}  ce_sets"
proof -
  let ?f = "(λ x a. (1::nat))"
  have S1: "?f  PrimRec2" by (rule const_is_pr_2)
  then have " x a. ?f x a  0" by simp
  then have "{x.  a. ?f x a = 0 }={}" by auto
  also have "fn_to_set ?f = " by (simp add: fn_to_set_def)
  with S1 show ?thesis by (auto simp add: ce_sets_def)
qed

theorem ce_univ: "UNIV  ce_sets"
proof -
  let ?f = "(λ x a. (0::nat))"
  have S1: "?f  PrimRec2" by (rule const_is_pr_2)
  then have " x a. ?f x a = 0" by simp
  then have "{x.  a. ?f x a = 0 }=UNIV" by auto
  also have "fn_to_set ?f = " by (simp add: fn_to_set_def)
  with S1 show ?thesis by (auto simp add: ce_sets_def)
qed

theorem ce_singleton: "{a}  ce_sets"
proof -
  let ?f = "λ x y. (abs_of_diff x a) + y"
  have S1: "?f  PrimRec2" using const_is_pr_2 [where ?n="a"] by prec
  then have " x y. (?f x y = 0) = (x=a  y=0)" by (simp add: abs_of_diff_eq)
  then have S2: "{x.  y. ?f x y = 0 }={a}" by auto
  have "fn_to_set ?f = {x.  y. ?f x y = 0 }" by (simp add: fn_to_set_def)
  with S2 have "fn_to_set ?f = {a}" by simp
  with S1 show ?thesis by (auto simp add: ce_sets_def)
qed

theorem ce_union: " A  ce_sets; B  ce_sets   A  B  ce_sets"
proof -
  assume A1: "A  ce_sets"
  then obtain p_a where S2: "p_a  PrimRec2" and S3: "A = fn_to_set p_a"
    by (auto simp add: ce_sets_def)
  assume A2: "B  ce_sets"
  then obtain p_b where S5: "p_b  PrimRec2" and S6: "B = fn_to_set p_b"
    by (auto simp add: ce_sets_def)
  let ?p = "(λ x y. (p_a x y) * (p_b x y))"
  from S2 S5 have S7: "?p  PrimRec2" by prec
  have S8: " x y. (?p x y = 0) = ((p_a x y = 0)  (p_b x y = 0))" by simp
  let ?C = "fn_to_set ?p"
  have S9: "?C = {x.  y. ?p x y = 0}" by (simp add: fn_to_set_def)
  from S3 have S10: "A = {x.  y. p_a x y = 0}" by (simp add: fn_to_set_def)
  from S6 have S11: "B = {x.  y. p_b x y = 0}" by (simp add: fn_to_set_def)
  from S10 S11 S9 S8 have S12: "?C = A  B" by auto
  from S7 have "?C  ce_sets" by (auto simp add: ce_sets_def)
  with S12 show ?thesis by simp
qed

theorem ce_intersect: " A  ce_sets; B  ce_sets   A  B  ce_sets"
proof -
  assume A1: "A  ce_sets"
  then obtain p_a where S2: "p_a  PrimRec2" and S3: "A = fn_to_set p_a"
    by (auto simp add: ce_sets_def)
  assume A2: "B  ce_sets"
  then obtain p_b where S5: "p_b  PrimRec2" and S6: "B = fn_to_set p_b"
    by (auto simp add: ce_sets_def)
  let ?p = "(λ x y. (p_a x (c_fst y)) + (p_b x (c_snd y)))"
  from S2 S5 have S7: "?p  PrimRec2" by prec
  have S8: " x. ( y. ?p x y = 0) = (( z. p_a x z = 0)  ( z. p_b x z = 0))"
  proof
    fix x show "( y. ?p x y = 0) = (( z. p_a x z = 0)  ( z. p_b x z = 0))"
    proof -
    have 1: "( y. ?p x y = 0)  (( z. p_a x z = 0)  ( z. p_b x z = 0))"
    by blast
    have 2: "(( z. p_a x z = 0)  ( z. p_b x z = 0))  ( y. ?p x y = 0)"
    proof -
      assume "(( z. p_a x z = 0)  ( z. p_b x z = 0))"
      then obtain z1 z2 where s_23: "p_a x z1 = 0" and s_24: "p_b x z2 = 0" by auto
      let ?y1 = "c_pair z1 z2"
      from s_23 have s_25: "p_a x (c_fst ?y1) = 0" by simp
      from s_24 have s_26: "p_b x (c_snd ?y1) = 0" by simp
      from s_25 s_26 have s_27: "p_a x (c_fst ?y1) + p_b x (c_snd ?y1) = 0" by simp
      then show ?thesis ..
    qed
    from 1 2 have "( y. ?p x y = 0) = (( z. p_a x z = 0)  ( z. p_b x z = 0))" by (rule iffI)
    then show ?thesis by auto
    qed
  qed
  let ?C = "fn_to_set ?p"
  have S9: "?C = {x.  y. ?p x y = 0}" by (simp add: fn_to_set_def)
  from S3 have S10: "A = {x.  y. p_a x y = 0}" by (simp add: fn_to_set_def)
  from S6 have S11: "B = {x.  y. p_b x y = 0}" by (simp add: fn_to_set_def)
  from S10 S11 S9 S8 have S12: "?C = A  B" by auto
  from S7 have "?C  ce_sets" by (auto simp add: ce_sets_def)
  with S12 show ?thesis by simp
qed

subsection ‹Enumeration of computably enumerable sets›

definition
  nat_to_ce_set :: "nat  (nat set)" where
  "nat_to_ce_set = (λ n. fn_to_set (pr_conv_1_to_2 (nat_to_pr n)))"

lemma nat_to_ce_set_lm_1: "nat_to_ce_set n = { x .  y. (nat_to_pr n) (c_pair x y) = 0 }"
proof -
  have S1: "nat_to_ce_set n = fn_to_set (pr_conv_1_to_2 (nat_to_pr n))" by (simp add: nat_to_ce_set_def)
  then have S2: "nat_to_ce_set n = { x .  y. (pr_conv_1_to_2 (nat_to_pr n)) x y = 0}" by (simp add: fn_to_set_def)
  have S3: " x y. (pr_conv_1_to_2 (nat_to_pr n)) x y = (nat_to_pr n) (c_pair x y)" by (simp add: pr_conv_1_to_2_def)
  from S2 S3 show ?thesis by auto
qed

lemma nat_to_ce_set_into_ce: "nat_to_ce_set n  ce_sets"
proof -
  have S1: "nat_to_ce_set n = fn_to_set (pr_conv_1_to_2 (nat_to_pr n))" by (simp add: nat_to_ce_set_def)
  have "(nat_to_pr n)  PrimRec1" by (rule nat_to_pr_into_pr)
  then have S2: "(pr_conv_1_to_2 (nat_to_pr n))  PrimRec2" by (rule pr_conv_1_to_2_lm)
  from S2 S1 show ?thesis by (simp add: ce_set_lm_1)
qed

lemma nat_to_ce_set_srj: "A  ce_sets   n. A = nat_to_ce_set n"
proof -
  assume A: "A  ce_sets"
  then have " p  PrimRec2. A = fn_to_set p" by (rule ce_set_lm_3)
  then obtain p where p_is_pr: "p  PrimRec2" and S1: "A = fn_to_set p" ..
  define q where "q = pr_conv_2_to_1 p"
  from p_is_pr have q_is_pr: "q  PrimRec1" by (unfold q_def, rule pr_conv_2_to_1_lm)
  from q_def have S2: "pr_conv_1_to_2 q = p" by simp
  let ?n = "index_of_pr q"
  from q_is_pr have "nat_to_pr ?n = q" by (rule index_of_pr_is_real)
  with S2 S1 have "A = fn_to_set (pr_conv_1_to_2 (nat_to_pr ?n))" by auto
  then have "A = nat_to_ce_set ?n" by (simp add: nat_to_ce_set_def)
  thus ?thesis ..
qed


subsection ‹Characteristic functions›

definition
  chf :: "nat set  (nat  nat)" ― ‹Characteristic function› where
  "chf = (λ A x. if x  A then 0 else 1 )"

definition
  zero_set :: "(nat  nat)  nat set" where
  "zero_set = (λ f. { x. f x = 0})"

lemma chf_lm_1 [simp]: "zero_set (chf A) = A" by (unfold chf_def, unfold zero_set_def, simp)

lemma chf_lm_2: "(x  A) = (chf A x = 0)" by (unfold chf_def, simp)

lemma chf_lm_3: "(x  A) = (chf A x = 1)" by (unfold chf_def, simp)

lemma chf_lm_4: "chf A  PrimRec1  A  ce_sets"
proof -
  assume A: "chf A  PrimRec1"
  define p where "p = chf A"
  from A p_def have p_is_pr: "p  PrimRec1" by auto
  define q where "q x y = p x" for x y :: nat
  from p_is_pr have q_is_pr: "q  PrimRec2" unfolding q_def by prec
  have S1: "A = {x. p(x) = 0}"
  proof -
    have "zero_set p = A" by (unfold p_def, simp)
    thus ?thesis by (simp add: zero_set_def)
  qed
  have S2: "fn_to_set q = {x.  y. q x y = 0}" by (simp add: fn_to_set_def)
  have S3: " x. (p x = 0) = ( y. q x y = 0)" by (unfold q_def, auto)
  then have S4: "{x. p x = 0} = {x.  y. q x y = 0}" by auto
  with S1 S2 have S5: "fn_to_set q = A" by auto
  from q_is_pr have "fn_to_set q  ce_sets" by (rule ce_set_lm_1)
  with S5 show ?thesis by auto
qed

lemma chf_lm_5: "finite A  chf A  PrimRec1"
proof -
  assume A: "finite A"
  define u where "u = set_to_nat A"
  from A have S1: "nat_to_set u = A" by (unfold u_def, rule nat_to_set_srj)
  have "chf A = (λ x. sgn2 (c_in x u))"
  proof
    fix x show "chf A x = sgn2 (c_in x u)"
    proof cases
      assume A: "x  A"
      then have S1_1: "chf A x = 0" by (simp add: chf_lm_2)
      from A S1 have "x  nat_to_set u" by auto
      then have "c_in x u = 1" by (simp add: x_in_u_eq)
      with S1_1 show ?thesis by simp
    next
      assume A: "x  A"
      then have S1_1: "chf A x = 1" by (simp add: chf_def)
      from A S1 have "x  nat_to_set u" by auto
      then have "c_in x u = 0" by (simp add: x_in_u_eq c_in_def)
      with S1_1 show ?thesis by simp
    qed
  qed
  moreover from c_in_is_pr have "(λ x. sgn2 (c_in x u))  PrimRec1" by prec
  ultimately show ?thesis by auto
qed

theorem ce_finite: "finite A  A  ce_sets"
proof -
  assume A: "finite A"
  then have "chf A  PrimRec1" by (rule chf_lm_5)
  then show ?thesis by (rule chf_lm_4)
qed

subsection ‹Computably enumerable relations›

definition
  ce_set_to_rel :: "nat set  (nat * nat) set" where
  "ce_set_to_rel = (λ A. { (c_fst x, c_snd x) | x. x  A})"

definition
  ce_rel_to_set :: "(nat * nat) set  nat set" where
  "ce_rel_to_set = (λ R. { c_pair x y | x y. (x,y)  R})"

definition
  ce_rels :: "((nat * nat) set) set" where
  "ce_rels = { R | R. ce_rel_to_set R  ce_sets }"

lemma ce_rel_lm_1 [simp]: "ce_set_to_rel (ce_rel_to_set r) = r"
proof
  show " ce_set_to_rel (ce_rel_to_set r)  r"
  proof fix z
    assume A: "z  ce_set_to_rel (ce_rel_to_set r)"
    then obtain u where L1: "u  (ce_rel_to_set r)" and L2: "z = (c_fst u, c_snd u)"
      unfolding ce_set_to_rel_def by auto
    from L1 obtain x y where L3: "(x,y)  r" and L4: "u = c_pair x y"
      unfolding ce_rel_to_set_def by auto
    from L4 have L5: "c_fst u = x" by simp
    from L4 have L6: "c_snd u = y" by simp
    from L5 L6 L2 have "z = (x,y)" by simp
    with L3 show "z  r" by auto
  qed
next
  show "r  ce_set_to_rel (ce_rel_to_set r)"
  proof fix z show "z  r  z  ce_set_to_rel (ce_rel_to_set r)"
    proof -
      assume A: "z  r"
      define x where "x = fst z"
      define y where "y = snd z"
      from x_def y_def have L1: "z = (x,y)" by simp
      define u where "u = c_pair x y"
      from A L1 u_def have L2: "u  ce_rel_to_set r" by (unfold ce_rel_to_set_def, auto)
      from L1 u_def have L3: "z = (c_fst u, c_snd u)" by simp
      from L2 L3 show "z  ce_set_to_rel (ce_rel_to_set r)" by (unfold ce_set_to_rel_def, auto)
    qed
  qed
qed

lemma ce_rel_lm_2 [simp]: "ce_rel_to_set (ce_set_to_rel A) = A"
proof
  show "ce_rel_to_set (ce_set_to_rel A)  A"
  proof fix z show "z  ce_rel_to_set (ce_set_to_rel A)  z  A"
    proof -
      assume A: "z  ce_rel_to_set (ce_set_to_rel A)"
      then obtain x y where L1: "z = c_pair x y" and L2: "(x,y)  ce_set_to_rel A"
        unfolding ce_rel_to_set_def by auto
      from L2 obtain u where L3: "(x,y) = (c_fst u, c_snd u)" and L4: "u  A"
        unfolding ce_set_to_rel_def by auto
      from L3 L1 have L5: "z = u" by simp
      with L4 show "z  A" by auto
    qed
  qed
next
  show "A  ce_rel_to_set (ce_set_to_rel A)"
  proof fix z show "z  A  z  ce_rel_to_set (ce_set_to_rel A)"
    proof -
      assume A: "z  A"
      then have L1: "(c_fst z, c_snd z)  ce_set_to_rel A" by (unfold ce_set_to_rel_def, auto)
      define x where "x = c_fst z"
      define y where "y = c_snd z"
      from L1 x_def y_def have L2: "(x,y)  ce_set_to_rel A" by simp
      then have L3: "c_pair x y  ce_rel_to_set (ce_set_to_rel A)" by (unfold ce_rel_to_set_def, auto)
      with x_def y_def show "z  ce_rel_to_set (ce_set_to_rel A)" by simp
    qed
  qed
qed

lemma ce_rels_def1: "ce_rels = { ce_set_to_rel A | A. A  ce_sets}"
proof
  show "ce_rels  {ce_set_to_rel A |A. A  ce_sets}"
  proof fix r show " r  ce_rels  r  {ce_set_to_rel A |A. A  ce_sets}"
    proof -
      assume A: "r  ce_rels"
      then have L1: "ce_rel_to_set r  ce_sets" by (unfold ce_rels_def, auto)
      define A where "A = ce_rel_to_set r"
      from A_def L1 have L2: "A  ce_sets" by auto
      from A_def have L3: "ce_set_to_rel A = r" by simp
      with L2 show "r  {ce_set_to_rel A |A. A  ce_sets}" by auto
    qed
  qed
next
  show "{ce_set_to_rel A |A. A  ce_sets}  ce_rels"
  proof fix r show "r  {ce_set_to_rel A |A. A  ce_sets}  r  ce_rels"
    proof -
      assume A: "r  {ce_set_to_rel A |A. A  ce_sets}"
      then obtain A where L1: "r = ce_set_to_rel A" and L2: "A  ce_sets" by auto
      from L1 have "ce_rel_to_set r = A" by simp
      with L2 show "r  ce_rels" unfolding ce_rels_def by auto
    qed
  qed
qed

lemma ce_rel_to_set_inj: "inj ce_rel_to_set"
proof (rule inj_on_inverseI)
  fix x assume A: "(x::(nat×nat) set)  UNIV" show "ce_set_to_rel (ce_rel_to_set x) = x" by (rule ce_rel_lm_1)
qed

lemma ce_rel_to_set_srj: "surj ce_rel_to_set"
proof (rule surjI [where ?f=ce_set_to_rel])
  fix x show "ce_rel_to_set (ce_set_to_rel x) = x" by (rule ce_rel_lm_2)
qed

lemma ce_rel_to_set_bij: "bij ce_rel_to_set"
proof (rule bijI)
  show "inj ce_rel_to_set" by (rule ce_rel_to_set_inj)
next
  show "surj ce_rel_to_set" by (rule ce_rel_to_set_srj)
qed

lemma ce_set_to_rel_inj: "inj ce_set_to_rel"
proof (rule inj_on_inverseI)
  fix x assume A: "(x::nat set)  UNIV" show "ce_rel_to_set (ce_set_to_rel x) = x" by (rule ce_rel_lm_2)
qed

lemma ce_set_to_rel_srj: "surj ce_set_to_rel"
proof (rule surjI [where ?f=ce_rel_to_set])
  fix x show "ce_set_to_rel (ce_rel_to_set x) = x" by (rule ce_rel_lm_1)
qed

lemma ce_set_to_rel_bij: "bij ce_set_to_rel"
proof (rule bijI)
  show "inj ce_set_to_rel" by (rule ce_set_to_rel_inj)
next
  show "surj ce_set_to_rel" by (rule ce_set_to_rel_srj)
qed

lemma ce_rel_lm_3: "A  ce_sets  ce_set_to_rel A  ce_rels"
proof -
  assume A: "A  ce_sets"
  from A ce_rels_def1 show ?thesis by auto
qed

lemma ce_rel_lm_4: "ce_set_to_rel A  ce_rels  A  ce_sets"
proof -
  assume A: "ce_set_to_rel A  ce_rels"
  from A show ?thesis by (unfold ce_rels_def, auto)
qed

lemma ce_rel_lm_5: "(A  ce_sets) = (ce_set_to_rel A  ce_rels)"
proof
  assume "A  ce_sets" then show "ce_set_to_rel A  ce_rels" by (rule ce_rel_lm_3)
next
  assume "ce_set_to_rel A  ce_rels" then show "A  ce_sets" by (rule ce_rel_lm_4)
qed

lemma ce_rel_lm_6: "r  ce_rels  ce_rel_to_set r  ce_sets"
proof -
  assume A: "r  ce_rels"
  then show ?thesis by (unfold ce_rels_def, auto)
qed

lemma ce_rel_lm_7: "ce_rel_to_set r  ce_sets  r  ce_rels"
proof -
  assume "ce_rel_to_set r  ce_sets"
  then show ?thesis by (unfold ce_rels_def, auto)
qed

lemma ce_rel_lm_8: "(r  ce_rels) = (ce_rel_to_set r  ce_sets)" by (unfold ce_rels_def, auto)

lemma ce_rel_lm_9: "(x,y)  r  c_pair x y  ce_rel_to_set r" by (unfold ce_rel_to_set_def, auto)

lemma ce_rel_lm_10: "x  A  (c_fst x, c_snd x)  ce_set_to_rel A" by (unfold ce_set_to_rel_def, auto)

lemma ce_rel_lm_11: "c_pair x y  ce_rel_to_set r  (x,y)  r"
proof -
  assume A: "c_pair x y  ce_rel_to_set r"
  let ?z = "c_pair x y"
  from A have "(c_fst ?z, c_snd ?z)  ce_set_to_rel (ce_rel_to_set r)" by (rule ce_rel_lm_10)
  then show "(x,y)  r" by simp
qed

lemma ce_rel_lm_12: "(c_pair x y  ce_rel_to_set r) = ((x,y)  r)"
proof
  assume "c_pair x y  ce_rel_to_set r" then show "(x, y)  r" by (rule ce_rel_lm_11)
next
  assume "(x, y)  r" then show "c_pair x y  ce_rel_to_set r" by (rule ce_rel_lm_9)
qed

lemma ce_rel_lm_13: "(x,y)  ce_set_to_rel A  c_pair x y  A"
proof -
  assume "(x,y)  ce_set_to_rel A"
  then have "c_pair x y  ce_rel_to_set (ce_set_to_rel A)" by (rule ce_rel_lm_9)
  then show ?thesis by simp
qed

lemma ce_rel_lm_14: "c_pair x y  A  (x,y)  ce_set_to_rel A"
proof -
  assume "c_pair x y  A"
  then have "c_pair x y  ce_rel_to_set (ce_set_to_rel A)" by simp
  then show ?thesis by (rule ce_rel_lm_11)
qed

lemma ce_rel_lm_15: "((x,y)  ce_set_to_rel A) = (c_pair x y  A)"
proof
  assume "(x, y)  ce_set_to_rel A" then show "c_pair x y  A" by (rule ce_rel_lm_13)
next
  assume "c_pair x y  A" then show "(x, y)  ce_set_to_rel A" by (rule ce_rel_lm_14)
qed

lemma ce_rel_lm_16: "x  ce_rel_to_set r  (c_fst x, c_snd x)  r"
proof -
  assume "x  ce_rel_to_set r"
  then have "(c_fst x, c_snd x)  ce_set_to_rel (ce_rel_to_set r)" by (rule ce_rel_lm_10)
  then show ?thesis by simp
qed

lemma ce_rel_lm_17: "(c_fst x, c_snd x)  ce_set_to_rel A  x  A"
proof -
  assume "(c_fst x, c_snd x)  ce_set_to_rel A"
  then have "c_pair (c_fst x) (c_snd x)  A" by (rule ce_rel_lm_13)
  then show ?thesis by simp
qed

lemma ce_rel_lm_18: "((c_fst x, c_snd x)  ce_set_to_rel A) = (x  A)"
proof
  assume "(c_fst x, c_snd x)  ce_set_to_rel A" then show "x  A" by (rule ce_rel_lm_17)
next
  assume "x  A" then show "(c_fst x, c_snd x)  ce_set_to_rel A" by (rule ce_rel_lm_10)
qed

lemma ce_rel_lm_19: "(c_fst x, c_snd x)  r  x  ce_rel_to_set r"
proof -
  assume "(c_fst x, c_snd x)  r"
  then have "(c_fst x, c_snd x)  ce_set_to_rel (ce_rel_to_set r)" by simp
  then show ?thesis by (rule ce_rel_lm_17)
qed

lemma ce_rel_lm_20: "((c_fst x, c_snd x)  r) = (x  ce_rel_to_set r)"
proof
  assume "(c_fst x, c_snd x)  r" then show "x  ce_rel_to_set r" by (rule ce_rel_lm_19)
next
  assume "x  ce_rel_to_set r" then show "(c_fst x, c_snd x)  r" by (rule ce_rel_lm_16)
qed

lemma ce_rel_lm_21: "r  ce_rels   p  PrimRec3.  x y. ((x,y)  r) = ( u. p x y u = 0)"
proof -
  assume r_ce: "r  ce_rels"
  define A where "A = ce_rel_to_set r"
  from r_ce have A_ce: "A  ce_sets" by (unfold A_def, rule ce_rel_lm_6)
  then have " p  PrimRec2. A = fn_to_set p" by (rule ce_set_lm_3)
  then obtain q where q_is_pr: "q  PrimRec2" and A_def1: "A = fn_to_set q" ..
  from A_def1 have A_def2: "A = { x.  y. q x y = 0}" by (unfold fn_to_set_def)
  define p where "p x y u = q (c_pair x y) u" for x y u
  from q_is_pr have p_is_pr: "p  PrimRec3" unfolding p_def by prec
  have " x y. ((x,y)  r) = ( u. p x y u = 0)"
  proof - fix x y show "((x,y)  r) = ( u. p x y u = 0)"
    proof
      assume A: "(x,y)  r"
      define z where "z = c_pair x y"
      with A_def A have z_in_A: "z  A" by (unfold ce_rel_to_set_def, auto)
      with A_def2 have "z  { x.  y. q x y = 0}" by auto
      then obtain u where "q z u = 0" by auto
      with z_def have "p x y u = 0" by (simp add: z_def p_def)
      then show " u. p x y u = 0" by auto
    next
      assume A: " u. p x y u = 0"
      define z where "z = c_pair x y"
      from A obtain u where "p x y u = 0" by auto
      then have q_z: "q z u = 0" by (simp add: z_def p_def)
      with A_def2 have z_in_A: "z  A" by auto
      then have "c_pair x y  A" by (unfold z_def)
      then have "c_pair x y  ce_rel_to_set r" by (unfold A_def)
      then show "(x,y)  r" by (rule ce_rel_lm_11)
    qed
  qed
  with p_is_pr show ?thesis by auto
qed

lemma ce_rel_lm_22: "r  ce_rels   p  PrimRec3. r = { (x,y).  u. p x y u = 0 }"
proof -
  assume r_ce: "r  ce_rels"
  then have " p  PrimRec3.  x y. ((x,y)  r) = ( u. p x y u = 0)" by (rule ce_rel_lm_21)
  then obtain p where p_is_pr: "p  PrimRec3" and L1: " x y. ((x,y)  r) = ( u. p x y u = 0)" by auto
  from p_is_pr L1 show ?thesis by blast
qed

lemma ce_rel_lm_23: " p  PrimRec3;  x y. ((x,y)  r) = ( u. p x y u = 0)   r  ce_rels"
proof -
  assume p_is_pr: "p  PrimRec3"
  assume A: " x y. ((x,y)  r) = ( u. p x y u = 0)"
  define q where "q z u = p (c_fst z) (c_snd z) u" for z u
  from p_is_pr have q_is_pr: "q  PrimRec2" unfolding q_def by prec
  define A where "A = { x.  y. q x y = 0}"
  then have A_def1: "A = fn_to_set q" by (unfold fn_to_set_def, auto)
  from q_is_pr A_def1 have A_ce: "A  ce_sets" by (simp add: ce_set_lm_1)
  have main: "A = ce_rel_to_set r"
  proof
    show "A  ce_rel_to_set r"
    proof
      fix z assume z_in_A: "z  A"
      show "z  ce_rel_to_set r"
      proof -
        define x where "x = c_fst z"
        define y where "y = c_snd z"
        from z_in_A A_def obtain u where L2: "q z u = 0" by auto
        with x_def y_def q_def have L3: "p x y u = 0" by simp
        then have "u. p x y u = 0" by auto
        with A have "(x,y)  r" by auto
        then have "c_pair x y  ce_rel_to_set r" by (rule ce_rel_lm_9)
        with x_def y_def show ?thesis by simp
      qed
    qed
  next
    show "ce_rel_to_set r  A"
    proof
      fix z assume z_in_r: "z  ce_rel_to_set r"
      show "z  A"
      proof -
        define x where "x = c_fst z"
        define y where "y = c_snd z"
        from z_in_r have "(c_fst z, c_snd z)  r" by (rule ce_rel_lm_16)
        with x_def y_def have "(x,y)  r" by simp
        with A obtain u where L1: "p x y u = 0" by auto
        with x_def y_def q_def have "q z u = 0" by simp
        with A_def show "z  A" by auto
      qed
    qed
  qed
  with A_ce have "ce_rel_to_set r  ce_sets" by auto
  then show "r  ce_rels" by (rule ce_rel_lm_7)
qed

lemma ce_rel_lm_24: " r  ce_rels; s  ce_rels   s O r  ce_rels"
proof -
  assume r_ce: "r  ce_rels"
  assume s_ce: "s  ce_rels"
  from r_ce have " p  PrimRec3.  x y. ((x,y)  r)=( u. p x y u = 0)" by (rule ce_rel_lm_21)
  then obtain p_r where p_r_is_pr: "p_r  PrimRec3" and R1: " x y. ((x,y)  r)=( u. p_r x y u = 0)"
    by auto
  from s_ce have " p  PrimRec3.  x y. ((x,y)  s)=( u. p x y u = 0)" by (rule ce_rel_lm_21)
  then obtain p_s where p_s_is_pr: "p_s  PrimRec3" and S1: " x y. ((x,y)  s)=( u. p_s x y u = 0)"
    by auto
  define p where "p x z u = (p_s x (c_fst u) (c_fst (c_snd u))) + (p_r (c_fst u) z (c_snd (c_snd u)))"
    for x z u
  from p_r_is_pr p_s_is_pr have p_is_pr: "p  PrimRec3" unfolding p_def by prec
  define sr where "sr = s O r"
  have main: " x z. ((x,z)  sr) = ( u. p x z u = 0)"
  proof (rule allI, rule allI)
    fix x z
    show "((x, z)  sr) = (u. p x z u = 0)"
    proof
      assume A: "(x, z)  sr"
      show "u. p x z u = 0"
      proof -
        from A sr_def obtain y where L1: "(x,y)  s" and L2: "(y,z)  r" by auto
        from L1 S1 obtain u_s where L3: "p_s x y u_s = 0" by auto
        from L2 R1 obtain u_r where L4: "p_r y z u_r = 0" by auto
        define u where "u = c_pair y (c_pair u_s u_r)"
        from L3 L4 have "p x z u = 0" by (unfold p_def, unfold u_def, simp)
        then show ?thesis by auto
      qed
    next
      assume A: "u. p x z u = 0"
      show "(x, z)  sr"
      proof -
        from A obtain u where L1: "p x z u = 0" by auto
        then have L2: "(p_s x (c_fst u) (c_fst (c_snd u))) + (p_r (c_fst u) z (c_snd (c_snd u))) = 0" by (unfold p_def)
        from L2 have L3: "p_s x (c_fst u) (c_fst (c_snd u)) = 0" by auto
        from L2 have L4: "p_r (c_fst u) z (c_snd (c_snd u)) = 0" by auto
        from L3 S1 have L5: "(x,(c_fst u))  s" by auto
        from L4 R1 have L6: "((c_fst u),z)  r" by auto
        from L5 L6 have "(x,z)  s O r" by auto
        with sr_def show ?thesis by auto
      qed
    qed
  qed
  from p_is_pr main have "sr  ce_rels" by (rule ce_rel_lm_23)
  then show ?thesis by (unfold sr_def)
qed

lemma ce_rel_lm_25: "r  ce_rels  r^-1  ce_rels"
proof -
  assume r_ce: "r  ce_rels"
  have "r^-1 = {(y,x). (x,y)  r}" by auto
  then have L1: " x y. ((x,y)  r) = ((y,x)  r^-1)" by auto
  from r_ce have " p  PrimRec3.  x y. ((x,y)  r) = ( u. p x y u = 0)" by (rule ce_rel_lm_21)
  then obtain p where p_is_pr: "p  PrimRec3" and R1: " x y. ((x,y)  r) = ( u. p x y u = 0)" by auto
  define q where "q x y u = p y x u" for x y u
  from p_is_pr have q_is_pr: "q  PrimRec3" unfolding q_def by prec
  from L1 R1 have L2: " x y. ((x,y)  r^-1) = ( u. p y x u = 0)" by auto
  with q_def have L3: " x y. ((x,y)  r^-1) = ( u. q x y u = 0)" by auto
  with q_is_pr show ?thesis by (rule ce_rel_lm_23)
qed

lemma ce_rel_lm_26: "r  ce_rels  Domain r  ce_sets"
proof -
  assume r_ce: "r  ce_rels"
  have L1: " x. (x  Domain r) = ( y. (x,y)  r)" by auto
  define A where "A = ce_rel_to_set r"
  from r_ce have "ce_rel_to_set r  ce_sets" by (rule ce_rel_lm_6)
  then have A_ce: "A  ce_sets" by (unfold A_def)
  have " x y. ((x,y)  r) = (c_pair x y  ce_rel_to_set r)" by (simp add: ce_rel_lm_12)
  then have L2: " x y. ((x,y)  r) = (c_pair x y  A)" by (unfold A_def)
  from A_ce c_fst_is_pr have L3: "{ c_fst z |z.  z  A }  ce_sets" by (rule ce_set_lm_7)
  have L4: " x. (x  { c_fst z |z.  z  A }) =( y. c_pair x y  A)"
  proof fix x show "(x  { c_fst z |z.  z  A }) =( y. c_pair x y  A)"
    proof
      assume A: "x  {c_fst z |z. z  A}"
      then obtain z where z_in_A: "z  A" and x_z: "x = c_fst z" by auto
      from x_z have "z = c_pair x (c_snd z)" by simp
      with z_in_A have "c_pair x (c_snd z)  A" by auto
      then show "y. c_pair x y  A" by auto
    next
      assume A: "y. c_pair x y  A"
      then obtain y where y_1: "c_pair x y  A" by auto
      define z where "z = c_pair x y"
      from y_1 have z_in_A: "z  A" by (unfold z_def)
      from z_def have x_z: "x = c_fst z" by (unfold z_def, simp)
      from z_in_A x_z show "x  {c_fst z |z. z  A}" by auto
    qed
  qed
  from L1 L2 have L5: " x. (x  Domain r) = ( y. c_pair x y  A)" by auto
  from L4 L5 have L6: " x. (x  Domain r) = (x  { c_fst z |z.  z  A })" by auto
  then have "Domain r = { c_fst z |z.  z  A }" by auto  
  with L3 show "Domain r  ce_sets" by auto
qed

lemma ce_rel_lm_27: "r  ce_rels  Range r  ce_sets"
proof -
  assume r_ce: "r  ce_rels"
  then have "r^-1  ce_rels" by (rule ce_rel_lm_25)
  then have "Domain (r^-1)  ce_sets" by (rule ce_rel_lm_26)
  then show ?thesis by (unfold Domain_converse [symmetric])
qed

lemma ce_rel_lm_28: "r  ce_rels  Field r  ce_sets"
proof -
  assume r_ce: "r  ce_rels"
  from r_ce have L1: "Domain r  ce_sets" by (rule ce_rel_lm_26)
  from r_ce have L2: "Range r  ce_sets" by (rule ce_rel_lm_27)
  from L1 L2 have L3: "Domain r  Range r  ce_sets" by (rule ce_union)
  then show ?thesis by (unfold Field_def)
qed

lemma ce_rel_lm_29: " A  ce_sets; B  ce_sets   A × B  ce_rels"
proof -
  assume A_ce: "A  ce_sets"
  assume B_ce: "B  ce_sets"
  define r_a where "r_a = {(x,(0::nat)) | x. x  A}"
  define r_b where "r_b = {((0::nat),z) | z. z  B}"
  have L1: "r_a O r_b = A × B" by (unfold r_a_def, unfold r_b_def, auto)
  have r_a_ce: "r_a  ce_rels"
  proof -
    have loc1: "ce_rel_to_set r_a = { c_pair x 0 | x. x  A}" by (unfold r_a_def, unfold ce_rel_to_set_def, auto)
    define p where "p x = c_pair x 0" for x
    have p_is_pr: "p  PrimRec1" unfolding p_def by prec
    from A_ce p_is_pr have "{ c_pair x 0 | x. x  A}  ce_sets"
      unfolding p_def by (simp add: ce_set_lm_7)
    with loc1 have "ce_rel_to_set r_a  ce_sets" by auto
    then show ?thesis by (rule ce_rel_lm_7)
  qed
  have r_b_ce: "r_b  ce_rels"
  proof -
    have loc1: "ce_rel_to_set r_b = { c_pair 0 z | z. z  B}"
      by (unfold r_b_def, unfold ce_rel_to_set_def, auto)
    define p where "p z = c_pair 0 z" for z
    have p_is_pr: "p  PrimRec1" unfolding p_def by prec
    from B_ce p_is_pr have "{ c_pair 0 z | z. z  B}  ce_sets"
      unfolding p_def by (simp add: ce_set_lm_7)
    with loc1 have "ce_rel_to_set r_b  ce_sets" by auto
    then show ?thesis by (rule ce_rel_lm_7)
  qed
  from r_b_ce r_a_ce have "r_a O r_b  ce_rels" by (rule ce_rel_lm_24)
  with L1 show ?thesis by auto
qed

lemma ce_rel_lm_30: "{}  ce_rels"
proof -
  have "ce_rel_to_set {} = {}" by (unfold ce_rel_to_set_def, auto)
  with ce_empty have "ce_rel_to_set {}  ce_sets" by auto
  then show ?thesis by (rule ce_rel_lm_7)
qed

lemma ce_rel_lm_31: "UNIV  ce_rels"
proof -
  from ce_univ ce_univ have "UNIV × UNIV  ce_rels" by (rule ce_rel_lm_29)
  then show ?thesis by auto
qed

lemma ce_rel_lm_32: "ce_rel_to_set (r  s) = (ce_rel_to_set r)  (ce_rel_to_set s)" by (unfold ce_rel_to_set_def, auto)

lemma ce_rel_lm_33: " r  ce_rels; s  ce_rels   r  s  ce_rels"
proof -
  assume "r  ce_rels"
  then have r_ce: "ce_rel_to_set r  ce_sets" by (rule ce_rel_lm_6)
  assume "s  ce_rels"
  then have s_ce: "ce_rel_to_set s  ce_sets" by (rule ce_rel_lm_6)  
  have "ce_rel_to_set (r  s) = (ce_rel_to_set r)  (ce_rel_to_set s)" by (unfold ce_rel_to_set_def, auto)
  moreover from r_ce s_ce have "(ce_rel_to_set r)  (ce_rel_to_set s)  ce_sets" by (rule ce_union)
  ultimately have "ce_rel_to_set (r  s)  ce_sets" by auto
  then show ?thesis by (rule ce_rel_lm_7)
qed

lemma ce_rel_lm_34: "ce_rel_to_set (r  s) = (ce_rel_to_set r)  (ce_rel_to_set s)"
proof
  show "ce_rel_to_set (r  s)  ce_rel_to_set r  ce_rel_to_set s" by (unfold ce_rel_to_set_def, auto)
next
  show "ce_rel_to_set r  ce_rel_to_set s  ce_rel_to_set (r  s)"
  proof fix x assume A: "x  ce_rel_to_set r  ce_rel_to_set s"
    from A have L1: "x  ce_rel_to_set r" by auto
    from A have L2: "x  ce_rel_to_set s" by auto
    from L1 obtain u v where L3: "(u,v)  r" and L4: "x = c_pair u v" 
      unfolding ce_rel_to_set_def by auto
    from L2 obtain u1 v1 where L5: "(u1,v1)  s" and L6: "x = c_pair u1 v1" 
      unfolding ce_rel_to_set_def by auto
    from L4 L6 have L7: "c_pair u1 v1 = c_pair u v" by auto
    then have "u1=u" by (rule c_pair_inj1)
    moreover from L7 have "v1=v" by (rule c_pair_inj2)
    ultimately have "(u,v)=(u1,v1)" by auto
    with L3 L5 have "(u,v)  r  s" by auto
    with L4 show "x  ce_rel_to_set (r  s)" by (unfold ce_rel_to_set_def, auto)
  qed
qed

lemma ce_rel_lm_35: " r  ce_rels; s  ce_rels   r  s  ce_rels"
proof -
  assume "r  ce_rels"
  then have r_ce: "ce_rel_to_set r  ce_sets" by (rule ce_rel_lm_6)
  assume "s  ce_rels"
  then have s_ce: "ce_rel_to_set s  ce_sets" by (rule ce_rel_lm_6)  
  have "ce_rel_to_set (r  s) = (ce_rel_to_set r)  (ce_rel_to_set s)" by (rule ce_rel_lm_34)
  moreover from r_ce s_ce have "(ce_rel_to_set r)  (ce_rel_to_set s)  ce_sets" by (rule ce_intersect)
  ultimately have "ce_rel_to_set (r  s)  ce_sets" by auto
  then show ?thesis by (rule ce_rel_lm_7)
qed

lemma ce_rel_lm_36: "ce_set_to_rel (A  B) = (ce_set_to_rel A)  (ce_set_to_rel B)"
  by (unfold ce_set_to_rel_def, auto)

lemma ce_rel_lm_37: "ce_set_to_rel (A  B) = (ce_set_to_rel A)  (ce_set_to_rel B)"
proof -
  define f where "f x = (c_fst x, c_snd x)" for x
  have f_inj: "inj f"
  proof (unfold f_def, rule inj_on_inverseI [where ?g="λ (u,v). c_pair u v"])
    fix x :: nat
    assume "x  UNIV"
    show "case_prod c_pair (c_fst x, c_snd x) = x" by simp
  qed
  from f_inj have "f ` (A  B) = f ` A  f ` B" by (rule image_Int)
  then show ?thesis by (unfold f_def, unfold ce_set_to_rel_def, auto)
qed

lemma ce_rel_lm_38: " r  ce_rels; A  ce_sets   r``A  ce_sets"
proof -
  assume r_ce: "r  ce_rels"
  assume A_ce: "A  ce_sets"
  have L1: "r``A = Range (r  A × UNIV)" by blast
  have L2: "Range (r  A × UNIV)  ce_sets"
  proof (rule ce_rel_lm_27)
    show "r  A × UNIV  ce_rels"
    proof (rule ce_rel_lm_35)
      show "r  ce_rels" by (rule r_ce)
    next
      show "A × UNIV  ce_rels"
      proof (rule ce_rel_lm_29)
        show "A  ce_sets" by (rule A_ce)
      next
        show "UNIV  ce_sets" by (rule ce_univ)
      qed
    qed
  qed
  from L1 L2 show ?thesis by auto
qed


subsection ‹Total computable functions›

definition
  graph :: "(nat  nat)  (nat × nat) set" where
  "graph = (λ f. { (x, f x) | x. x  UNIV})"

lemma graph_lm_1: "(x,y)  graph f  y = f x" by (unfold graph_def, auto)

lemma graph_lm_2: "y = f x  (x,y)  graph f" by (unfold graph_def, auto)

lemma graph_lm_3: "((x,y)  graph f) = (y = f x)" by (unfold graph_def, auto)

lemma graph_lm_4: "graph (f o g) = (graph g) O (graph f)" by (unfold graph_def, auto)

definition
  c_graph :: "(nat  nat)  nat set" where
  "c_graph = (λ f. { c_pair x (f x) | x. x  UNIV})"

lemma c_graph_lm_1: "c_pair x y  c_graph f  y = f x"
proof -
  assume A: "c_pair x y  c_graph f"
  have S1: "c_graph f = {c_pair x (f x) | x. x  UNIV}" by (simp add: c_graph_def)
  from A S1 obtain z where S2: "c_pair x y = c_pair z (f z)" by auto
  then have "x = z" by (rule c_pair_inj1)
  moreover from S2 have "y = f z" by (rule c_pair_inj2)
  ultimately show ?thesis by auto
qed

lemma c_graph_lm_2: "y = f x  c_pair x y  c_graph f" by (unfold c_graph_def, auto)

lemma c_graph_lm_3: "(c_pair x y  c_graph f) = (y = f x)"
proof
  assume "c_pair x y  c_graph f" then show "y = f x" by (rule c_graph_lm_1)
next
  assume "y = f x" then show "c_pair x y  c_graph f" by (rule c_graph_lm_2)
qed

lemma c_graph_lm_4: "c_graph f = ce_rel_to_set (graph f)" by (unfold c_graph_def ce_rel_to_set_def graph_def, auto)

lemma c_graph_lm_5: "graph f = ce_set_to_rel (c_graph f)" by (simp add: c_graph_lm_4)

definition
  total_recursive :: "(nat  nat)  bool" where
  "total_recursive = (λ f. graph f  ce_rels)"

lemma total_recursive_def1: "total_recursive = (λ f. c_graph f  ce_sets)"
proof (rule ext) fix f show " total_recursive f = (c_graph f  ce_sets)"
  proof
    assume A: "total_recursive f"
    then have "graph f  ce_rels" by (unfold total_recursive_def)
    then have "ce_rel_to_set (graph f)  ce_sets" by (rule ce_rel_lm_6)
    then show "c_graph f  ce_sets" by (simp add: c_graph_lm_4)
  next
    assume "c_graph f  ce_sets"
    then have "ce_rel_to_set (graph f)  ce_sets" by (simp add: c_graph_lm_4)
    then have "graph f  ce_rels" by (rule ce_rel_lm_7)
    then show "total_recursive f" by (unfold total_recursive_def)
  qed
qed

theorem pr_is_total_rec: "f  PrimRec1  total_recursive f"
proof -
  assume A: "f  PrimRec1"
  define p where "p x = c_pair x (f x)" for x
  from A have p_is_pr: "p  PrimRec1" unfolding p_def by prec
  let ?U = "{ p x | x. x  UNIV }"
  from ce_univ p_is_pr have U_ce: "?U  ce_sets" by (rule ce_set_lm_7)
  have U_1: "?U = { c_pair x (f x) | x. x  UNIV}" by (simp add: p_def)
  with U_ce have S1: "{ c_pair x (f x) | x. x  UNIV}  ce_sets" by simp
  with c_graph_def have c_graph_f_is_ce: "c_graph f  ce_sets" by (unfold c_graph_def, auto)
  then show ?thesis by (unfold total_recursive_def1, auto)
qed

theorem comp_tot_rec: " total_recursive f; total_recursive g   total_recursive (f o g)"
proof -
  assume "total_recursive f"
  then have f_ce: "graph f  ce_rels" by (unfold total_recursive_def)
  assume "total_recursive g"
  then have g_ce: "graph g  ce_rels" by (unfold total_recursive_def)
  from f_ce g_ce have "graph g O graph f  ce_rels" by (rule ce_rel_lm_24)
  then have "graph (f o g)  ce_rels" by (simp add: graph_lm_4)
  then show ?thesis by (unfold total_recursive_def)
qed

lemma univ_for_pr_tot_rec_lm: "c_graph univ_for_pr  ce_sets"
proof -
  define A where "A = c_graph univ_for_pr"
  from A_def have S1: "A = { c_pair x (univ_for_pr x) | x. x  UNIV }"
    by (simp add: c_graph_def)
  from S1 have S2: "A = { z .  x. z = c_pair x (univ_for_pr x) }" by auto
  have S3: " z. ( x. (z = c_pair x (univ_for_pr x))) = (univ_for_pr (c_fst z) = c_snd z)"
  proof -
    fix z show "( x. (z = c_pair x (univ_for_pr x))) = (univ_for_pr (c_fst z) = c_snd z)"
    proof
      assume A: "x. z = c_pair x (univ_for_pr x)"
      then obtain x where S3_1: "z = c_pair x (univ_for_pr x)" ..
      then show "univ_for_pr (c_fst z) = c_snd z" by simp
    next
      assume A: "univ_for_pr (c_fst z) = c_snd z"
      from A have "z = c_pair (c_fst z) (univ_for_pr (c_fst z))" by simp
      thus "x. z = c_pair x (univ_for_pr x)" ..
    qed
  qed
  with S2 have S4: "A = { z . univ_for_pr (c_fst z) = c_snd z }" by auto
  define p where "p x y =
    (if c_assoc_have_key (pr_gr y) (c_fst x) = 0 then
      (if c_assoc_value (pr_gr y) (c_fst x) = c_snd x then (0::nat) else 1)
    else 1)" for x y
  from c_assoc_have_key_is_pr c_assoc_value_is_pr pr_gr_is_pr have p_is_pr: "p  PrimRec2"
    unfolding p_def by prec
  have S5: " z. (univ_for_pr (c_fst z) = c_snd z) = ( y. p z y = 0)"
  proof -
    fix z show "(univ_for_pr (c_fst z) = c_snd z) = ( y. p z y = 0)"
    proof
      assume A: "univ_for_pr (c_fst z) = c_snd z"
      let ?n = "c_fst (c_fst z)"
      let ?x = "c_snd (c_fst z)"
      let ?y = "loc_upb ?n ?x"
      have S5_1: "c_assoc_have_key (pr_gr ?y) (c_pair ?n ?x) = 0" by (rule loc_upb_main)
      have S5_2: "c_assoc_value (pr_gr ?y) (c_pair ?n ?x) = univ_for_pr (c_pair ?n ?x)" by (rule pr_gr_value)
      from S5_1 have S5_3: "c_assoc_have_key (pr_gr ?y) (c_fst z) = 0" by simp
      from S5_2 A have S5_4: "c_assoc_value (pr_gr ?y) (c_fst z) = c_snd z" by simp
      from S5_3 S5_4 have "p z ?y = 0" by (simp add: p_def)
      thus " y. p z y = 0" ..
    next
      assume A: "y. p z y = 0"
      then obtain y where S5_1: "p z y = 0" ..
      have S5_2: "c_assoc_have_key (pr_gr y) (c_fst z) = 0"
      proof (rule ccontr)
        assume A_1: "c_assoc_have_key (pr_gr y) (c_fst z)  0"
        then have "p z y = 1" by (simp add: p_def)
        with S5_1 show False by auto
      qed
      then have S5_3: "p z y = (if c_assoc_value (pr_gr y) (c_fst z) = c_snd z then (0::nat) else 1)" by (simp add: p_def)
      have S5_4: "c_assoc_value (pr_gr y) (c_fst z) = c_snd z"
      proof (rule ccontr)
        assume A_2: "c_assoc_value (pr_gr y) (c_fst z)  c_snd z"
        then have "p z y = 1" by (simp add: p_def)
        with S5_1 show False by auto
      qed
      have S5_5: "c_is_sub_fun (pr_gr y) univ_for_pr" by (rule pr_gr_1)
      from S5_5 S5_2 have S5_6: "c_assoc_value (pr_gr y) (c_fst z) = univ_for_pr (c_fst z)" by (rule c_is_sub_fun_lm_1)
      with S5_4 show "univ_for_pr (c_fst z) = c_snd z" by auto
    qed
  qed
  from S5 S4 have "A = {z.  y. p z y = 0}" by auto
  then have "A = fn_to_set p" by (simp add: fn_to_set_def)
  moreover from p_is_pr have "fn_to_set p  ce_sets" by (rule ce_set_lm_1)
  ultimately have "A  ce_sets" by auto
  with A_def show ?thesis by auto
qed

theorem univ_for_pr_tot_rec: "total_recursive univ_for_pr"
proof -
  have "c_graph univ_for_pr  ce_sets" by (rule univ_for_pr_tot_rec_lm)
  then show ?thesis by (unfold total_recursive_def1, auto)
qed

subsection ‹Computable sets, Post's theorem›

definition
  computable :: "nat set  bool" where
  "computable = (λ A. A  ce_sets  -A  ce_sets)"

lemma computable_complement_1: "computable A  computable (- A)"
proof -
  assume "computable A"
  then show ?thesis by (unfold computable_def, auto)
qed

lemma computable_complement_2: "computable (- A)  computable A"
proof -
  assume "computable (- A)"
  then show ?thesis by (unfold computable_def, auto)
qed

lemma computable_complement_3: "(computable A) = (computable (- A))" by (unfold computable_def, auto)

theorem comp_impl_tot_rec: "computable A  total_recursive (chf A)"
proof -
  assume A: "computable A"
  from A have A1: "A  ce_sets" by (unfold computable_def, simp)
  from A have A2: "-A  ce_sets" by (unfold computable_def, simp)
  define p where "p x = c_pair x 0" for x
  define q where "q x = c_pair x 1" for x
  from p_def have p_is_pr: "p  PrimRec1" unfolding p_def by prec
  from q_def have q_is_pr: "q  PrimRec1" unfolding q_def by prec
  define U0 where "U0 = {p x | x. x  A}"
  define U1 where "U1 = {q x | x. x  - A}"
  from A1 p_is_pr have U0_ce: "U0  ce_sets" by(unfold U0_def, rule ce_set_lm_7)
  from A2 q_is_pr have U1_ce: "U1  ce_sets" by(unfold U1_def, rule ce_set_lm_7)
  define U where "U = U0  U1"
  from U0_ce U1_ce have U_ce: "U  ce_sets" by (unfold U_def, rule ce_union)
  define V where "V = c_graph (chf A)"
  have V_1: "V = { c_pair x (chf A x) | x. x  UNIV}" by (simp add: V_def c_graph_def)
  from U0_def p_def have U0_1: "U0 = { c_pair x y | x y. x  A  y=0}" by auto
  from U1_def q_def have U1_1: "U1 = { c_pair x y | x y. x  A  y=1}" by auto
  from U0_1 U1_1 U_def have U_1: "U = { c_pair x y | x y. (x  A  y=0)  (x  A  y=1)}" by auto
  from V_1 have V_2: "V = { c_pair x y | x y. y = chf A x}" by auto
  have L1: " x y. ((x  A  y=0)  (x  A  y=1)) = (y = chf A x)"
  proof -
    fix x y
    show "((x  A  y=0)  (x  A  y=1)) = (y = chf A x)" by(unfold chf_def, auto)
  qed
  from V_2 U_1 L1 have "U=V" by simp
  with U_ce have V_ce: "V  ce_sets" by auto
  with V_def have "c_graph (chf A)  ce_sets" by auto
  then show ?thesis by (unfold total_recursive_def1)
qed

theorem tot_rec_impl_comp: "total_recursive (chf A)  computable A"
proof -
  assume A: "total_recursive (chf A)"
  then have A1: "c_graph (chf A)  ce_sets" by (unfold total_recursive_def1)
  let ?U = "c_graph (chf A)"
  have L1: "?U = { c_pair x (chf A x) | x. x  UNIV}" by (simp add: c_graph_def)
  have L2: " x y. ((x  A  y=0)  (x  A  y=1)) = (y = chf A x)"
  proof - fix x y show "((x  A  y=0)  (x  A  y=1)) = (y = chf A x)" by(unfold chf_def, auto)
  qed
  from L1 L2 have L3: "?U = { c_pair x y | x y. (x  A  y=0)  (x  A  y=1)}" by auto
  define p where "p x = c_pair x 0" for x
  define q where "q x = c_pair x 1" for x
  have p_is_pr: "p  PrimRec1" unfolding p_def by prec
  have q_is_pr: "q  PrimRec1" unfolding q_def by prec
  define V where "V = { c_pair x y | x y. (x  A  y=0)  (x  A  y=1)}"
  from V_def L3 A1 have V_ce: "V  ce_sets" by auto
  from V_def have L4: " z. (z  V) = ( x y. z = c_pair x y   ((x  A  y=0)  (x  A  y=1)))" by blast
  have L5: " x. (p x  V) = (x  A)"
  proof - fix x show "(p x  V) = (x  A)"
    proof
      assume A: "p x  V"
      then have "c_pair x 0  V" by (unfold p_def)
      with V_def obtain x1 y1 where L5_2: "c_pair x 0 = c_pair x1 y1"
        and L5_3: "((x1  A  y1=0)  (x1  A  y1=1))" by auto
      from L5_2 have X_eq_X1: "x=x1" by (rule c_pair_inj1)
      from L5_2 have Y1_eq_0: "0=y1" by (rule c_pair_inj2)
      from L5_3 X_eq_X1 Y1_eq_0 show "x  A" by auto
    next
      assume A: "x  A"
      let ?z = "c_pair x 0"
      from A have L5_1: " x1 y1. c_pair x 0 = c_pair x1 y1   ((x1  A  y1=0)  (x1  A  y1=1))" by auto
      with V_def have "c_pair x 0  V" by auto
      with p_def show "p x  V" by simp
    qed
  qed
  then have A_eq: "A = { x. p x  V}" by auto
  from V_ce p_is_pr have "{ x. p x  V}  ce_sets" by (rule ce_set_lm_5)
  with A_eq have A_ce: "A  ce_sets" by simp
  have CA_eq: "- A = {x. q x  V}"
  proof -
    have " x. (q x  V) = (x  A)"
    proof - fix x show "(q x  V) = (x  A)"
      proof
        assume A: "q x  V"
        then have "c_pair x 1  V" by (unfold q_def)
        with V_def obtain x1 y1 where L5_2: "c_pair x 1 = c_pair x1 y1"
          and L5_3: "((x1  A  y1=0)  (x1  A  y1=1))" by auto
        from L5_2 have X_eq_X1: "x=x1" by (rule c_pair_inj1)
        from L5_2 have Y1_eq_1: "1=y1" by (rule c_pair_inj2)
        from L5_3 X_eq_X1 Y1_eq_1 show "x  A" by auto
      next
        assume A: "x  A"
        from A have L5_1: " x1 y1. c_pair x 1 = c_pair x1 y1   ((x1  A  y1=0)  (x1  A  y1=1))" by auto
        with V_def have "c_pair x 1  V" by auto
        with q_def show "q x  V" by simp
      qed
    qed
    then show ?thesis by auto
  qed
  from V_ce q_is_pr have "{ x. q x  V}  ce_sets" by (rule ce_set_lm_5)
  with CA_eq have CA_ce: "- A  ce_sets" by simp
  from A_ce CA_ce show ?thesis by (simp add: computable_def)
qed

theorem post_th_0: "(computable A) = (total_recursive (chf A))"
proof
  assume "computable A" then show "total_recursive (chf A)" by (rule comp_impl_tot_rec)
next
  assume "total_recursive (chf A)" then show "computable A" by (rule tot_rec_impl_comp)
qed

subsection ‹Universal computably enumerable set›

definition
  univ_ce :: "nat set" where
  "univ_ce = { c_pair n x | n x. x  nat_to_ce_set n }"

lemma univ_for_pr_lm: "univ_for_pr (c_pair n x) = (nat_to_pr n) x"
  by (simp add: univ_for_pr_def pr_conv_2_to_1_def)

theorem univ_is_ce: "univ_ce  ce_sets"
proof -
  define A where "A = c_graph univ_for_pr"
  then have "A  ce_sets" by (simp add: univ_for_pr_tot_rec_lm)
  then have " pA  PrimRec2. A = fn_to_set pA" by (rule ce_set_lm_3)
  then obtain pA where pA_is_pr: "pA  PrimRec2" and S1: "A = fn_to_set pA" by auto
  from S1 have S2: "A = { x.  y. pA x y = 0 }" by (simp add: fn_to_set_def)
  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
  from pA_is_pr have p_is_pr: "p  PrimRec2" unfolding p_def by prec
  have " z. ( n x. z = c_pair n x  x  nat_to_ce_set n) = (c_snd z  nat_to_ce_set (c_fst z))"
  proof -
    fix z show "( n x. z = c_pair n x  x  nat_to_ce_set n) = (c_snd z  nat_to_ce_set (c_fst z))"
    proof
      assume A: "n x. z = c_pair n x  x  nat_to_ce_set n"
      then obtain n x where L1: "z = c_pair n x  x  nat_to_ce_set n" by auto
      from L1 have L2: "z = c_pair n x" by auto
      from L1 have L3: "x  nat_to_ce_set n" by auto
      from L1 have L4: "c_fst z = n" by simp
      from L1 have L5: "c_snd z = x" by simp
      from L3 L4 L5 show "c_snd z  nat_to_ce_set (c_fst z)" by auto
    next
      assume A: "c_snd z  nat_to_ce_set (c_fst z)"
      let ?n = "c_fst z"
      let ?x = "c_snd z"
      have L1: "z = c_pair ?n ?x" by simp
      from L1 A have "z = c_pair ?n ?x  ?x  nat_to_ce_set ?n" by auto
      thus "n x. z = c_pair n x  x  nat_to_ce_set n" by blast
    qed
  qed
  then have "{ c_pair n x | n x. x  nat_to_ce_set n } = { z. c_snd z  nat_to_ce_set (c_fst z)}" by auto
  then have S3: "univ_ce  = { z. c_snd z  nat_to_ce_set (c_fst z)}" by (simp add: univ_ce_def)
  have S4: " z. (c_snd z  nat_to_ce_set (c_fst z)) = ( y. p z y = 0)"
  proof -
    fix z show "(c_snd z  nat_to_ce_set (c_fst z)) = ( y. p z y = 0)"
    proof
      assume A: "c_snd z  nat_to_ce_set (c_fst z)"
      have "nat_to_ce_set (c_fst z) = { x .  y. (nat_to_pr (c_fst z)) (c_pair x y) = 0 }" by (simp add: nat_to_ce_set_lm_1)
      with A obtain u where S4_1: "(nat_to_pr (c_fst z)) (c_pair (c_snd z) u) = 0"  by auto
      then have S4_2: "univ_for_pr (c_pair (c_fst z) (c_pair (c_snd z) u)) = 0" by (simp add: univ_for_pr_lm)
      from A_def have S4_3: "A = { c_pair x (univ_for_pr x) | x. x  UNIV }" by (simp add: c_graph_def)
      then have S4_4: " x. c_pair x (univ_for_pr x)  A" by auto
      then 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)))  A" by auto
      with S4_2 have S4_5: "c_pair (c_pair (c_fst z) (c_pair (c_snd z) u)) 0  A" by auto
      with S2 obtain v where S4_6: "pA (c_pair (c_pair (c_fst z) (c_pair (c_snd z) u)) 0) v = 0" 
        by auto
      define y where "y = c_pair u v"
      from y_def have S4_7: "u = c_fst y" by simp
      from y_def have S4_8: "v = c_snd y" by simp
      from S4_6 S4_7 S4_8 p_def have "p z y = 0" by simp
      thus " y. p z y = 0" ..
    next
      assume A: "y. p z y = 0"
      then obtain y where S4_1: "p z y = 0" ..
      from S4_1 p_def have S4_2: "pA (c_pair (c_pair (c_fst z) (c_pair (c_snd z) (c_fst y))) 0) (c_snd y) = 0" by simp
      with S2 have S4_3: "c_pair (c_pair (c_fst z) (c_pair (c_snd z) (c_fst y))) 0  A" by auto
      with A_def have "c_pair (c_pair (c_fst z) (c_pair (c_snd z) (c_fst y))) 0  c_graph univ_for_pr" by simp
      then have S4_4: "0 = univ_for_pr (c_pair (c_fst z) (c_pair (c_snd z) (c_fst y)))" by (rule c_graph_lm_1)
      then have S4_5: "univ_for_pr (c_pair (c_fst z) (c_pair (c_snd z) (c_fst y))) = 0" by auto
      then have S4_6: "(nat_to_pr (c_fst z)) (c_pair (c_snd z) (c_fst y)) = 0" by (simp add: univ_for_pr_lm)
      then have S4_7: " y. (nat_to_pr (c_fst z)) (c_pair (c_snd z) y) = 0" ..
      have S4_8: "nat_to_ce_set (c_fst z) = { x .  y. (nat_to_pr (c_fst z)) (c_pair x y) = 0 }" by (simp add: nat_to_ce_set_lm_1)
      from S4_7 have S4_9: "c_snd z  { x .  y. (nat_to_pr (c_fst z)) (c_pair x y) = 0 }" by auto
      with S4_8 show "c_snd z  nat_to_ce_set (c_fst z)" by auto
    qed
  qed
  with S3 have "univ_ce = {z.  y. p z y = 0}" by auto
  then have "univ_ce = fn_to_set p" by (simp add: fn_to_set_def)
  moreover from p_is_pr have "fn_to_set p  ce_sets" by (rule ce_set_lm_1)
  ultimately show "univ_ce  ce_sets" by auto
qed

lemma univ_ce_lm_1: "(c_pair n x  univ_ce) = (x  nat_to_ce_set n)"
proof -
  from univ_ce_def have S1: "univ_ce = {z .  n x. z = c_pair n x  x  nat_to_ce_set n}" by auto
  have S2: "( n1 x1. c_pair n x = c_pair n1 x1  x1  nat_to_ce_set n1) = (x  nat_to_ce_set n)"
  proof
    assume "n1 x1. c_pair n x = c_pair n1 x1  x1  nat_to_ce_set n1"
    then obtain n1 x1 where L1: "c_pair n x = c_pair n1 x1" and L2: "x1  nat_to_ce_set n1" by auto
    from L1 have L3: "n = n1" by (rule c_pair_inj1)
    from L1 have L4: "x = x1" by (rule c_pair_inj2)
    from L2 L3 L4 show "x  nat_to_ce_set n" by auto
  next
    assume A: "x  nat_to_ce_set n"
    then have "c_pair n x = c_pair n x  x  nat_to_ce_set n" by auto
    thus " n1 x1. c_pair n x = c_pair n1 x1  x1  nat_to_ce_set n1" by blast
  qed
  with S1 show ?thesis by auto
qed

theorem univ_ce_is_not_comp1: "- univ_ce  ce_sets"
proof (rule ccontr)
  assume "¬ - univ_ce  ce_sets"
  then have A: "- univ_ce  ce_sets" by auto
  define p where "p x = c_pair x x" for x
  have p_is_pr: "p  PrimRec1" unfolding p_def by prec
  define A where "A = { x. p x  - univ_ce }"
  from A p_is_pr have "{ x. p x  - univ_ce }  ce_sets" by (rule ce_set_lm_5)
  with A_def have S1: "A  ce_sets" by auto
  then have " n. A = nat_to_ce_set n" by (rule nat_to_ce_set_srj)
  then obtain n where S2: "A = nat_to_ce_set n" ..
  from A_def have "(n  A) = (p n  - univ_ce)" by auto
  with p_def have "(n  A) = (c_pair n n  univ_ce)" by auto
  with univ_ce_def univ_ce_lm_1 have "(n  A) = (n  nat_to_ce_set n)" by auto
  with S2 have "(n  A) = (n  A)" by auto
  thus False by auto
qed

theorem univ_ce_is_not_comp2: "¬ total_recursive (chf univ_ce)"
proof
  assume "total_recursive (chf univ_ce)"
  then have "computable univ_ce" by (rule tot_rec_impl_comp)
  then have "- univ_ce  ce_sets" by (unfold computable_def, auto)
  with univ_ce_is_not_comp1 show False by auto
qed

theorem univ_ce_is_not_comp3: "¬ computable univ_ce"
proof (rule ccontr)
  assume "¬ ¬ computable univ_ce"
  then have "computable univ_ce" by auto
  then have "total_recursive (chf univ_ce)" by (rule comp_impl_tot_rec)
  with univ_ce_is_not_comp2 show False by auto
qed

subsection ‹s-1-1 theorem, one-one and many-one reducibilities›

definition
  index_of_r_to_l :: nat where
  "index_of_r_to_l =
  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)"

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"
  apply(unfold index_of_r_to_l_def)
  apply(simp add: pair_by_index_main)
  apply(unfold c_f_pair_def)
  apply(simp add: index_of_c_fst_main)
  apply(simp add: comp_by_index_main)
  apply(simp add: index_of_c_fst_main)
  apply(simp add: index_of_c_snd_main)
done

definition
  s_ce :: "nat  nat  nat" where
  "s_ce == (λ e x. s1_1 (comp_by_index e index_of_r_to_l) x)"

lemma s_ce_is_pr: "s_ce  PrimRec2"
  unfolding s_ce_def using comp_by_index_is_pr s1_1_is_pr by prec

lemma s_ce_inj: "s_ce e1 x1 = s_ce e2 x2  e1=e2  x1=x2"
proof -
  let ?n1 = "index_of_r_to_l"
  assume "s_ce e1 x1 = s_ce e2 x2"
  then have "s1_1 (comp_by_index e1 ?n1) x1 = s1_1 (comp_by_index e2 ?n1) x2" by (unfold s_ce_def)
  then have L1: "comp_by_index e1 ?n1 = comp_by_index e2 ?n1  x1=x2" by (rule s1_1_inj)
  from L1 have "comp_by_index e1 ?n1 = comp_by_index e2 ?n1" ..
  then have "e1=e2" by (rule comp_by_index_inj1)
  moreover from L1 have "x1=x2" by auto
  ultimately show ?thesis by auto
qed

lemma s_ce_inj1: "s_ce e1 x = s_ce e2 x  e1=e2"
proof -
  assume "s_ce e1 x = s_ce e2 x"
  then have "e1=e2  x=x" by (rule s_ce_inj)
  then show "e1=e2" by auto
qed

lemma s_ce_inj2: "s_ce e x1 = s_ce e x2  x1=x2"
proof -
  assume "s_ce e x1 = s_ce e x2"
  then have "e=e  x1=x2" by (rule s_ce_inj)
  then show "x1=x2" by auto
qed

theorem s1_1_th1: " n x y. ((nat_to_pr n) (c_pair x y)) = (nat_to_pr (s1_1 n x)) y"
proof (rule allI, rule allI, rule allI)
  fix n x y show "nat_to_pr n (c_pair x y) = nat_to_pr (s1_1 n x) y"
  proof -
    have "(λ y. (nat_to_pr n) (c_pair x y)) = nat_to_pr (s1_1 n x)" by (rule s1_1_th)
    then show ?thesis by (simp add: fun_eq_iff)
  qed
qed

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 -
  let ?n1 = "index_of_r_to_l"
  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)" by (unfold s_ce_def, simp)
  also have " = (nat_to_pr (comp_by_index e ?n1)) (c_pair x (c_pair y z))" by (simp add: s1_1_th1)
  also have " = (nat_to_pr e) ((nat_to_pr ?n1) (c_pair x (c_pair y z)))" by (simp add: comp_by_index_main)
  finally show ?thesis by (simp add: index_of_r_to_l_lm)
qed

theorem s_ce_1_1_th: "(c_pair x y  nat_to_ce_set e) = (y  nat_to_ce_set (s_ce e x))"
proof
  assume A: "c_pair x y  nat_to_ce_set e"
  then obtain z where L1: "(nat_to_pr e) (c_pair (c_pair x y) z) = 0" 
    by (auto simp add: nat_to_ce_set_lm_1)
  have "(nat_to_pr (s_ce e x)) (c_pair y z) = 0" by (simp add: s_lm L1)
  with nat_to_ce_set_lm_1 show "y  nat_to_ce_set (s_ce e x)" by auto
next
  assume A: "y  nat_to_ce_set (s_ce e x)"
  then obtain z where L1: "(nat_to_pr (s_ce e x)) (c_pair y z) = 0" 
    by (auto simp add: nat_to_ce_set_lm_1)
  then have "(nat_to_pr e) (c_pair (c_pair x y) z) = 0" by (simp add: s_lm)
  with nat_to_ce_set_lm_1 show "c_pair x y  nat_to_ce_set e" by auto
qed

definition
  one_reducible_to_via :: "(nat set)  (nat set)  (nat  nat)  bool" where
  "one_reducible_to_via = (λ A B f. total_recursive f  inj f  ( x. (x  A) = (f x  B)))"

definition
  one_reducible_to :: "(nat set)  (nat set)  bool" where
  "one_reducible_to = (λ A B.  f. one_reducible_to_via A B f)"

definition
  many_reducible_to_via :: "(nat set)  (nat set)  (nat  nat)  bool" where
  "many_reducible_to_via = (λ A B f. total_recursive f  ( x. (x  A) = (f x  B)))"

definition
  many_reducible_to :: "(nat set)  (nat set)  bool" where
  "many_reducible_to = (λ A B.  f. many_reducible_to_via A B f)"

lemma one_reducible_to_via_trans: " one_reducible_to_via A B f; one_reducible_to_via B C g   one_reducible_to_via A C (g o f)"
proof -
  assume A1: "one_reducible_to_via A B f"
  assume A2: "one_reducible_to_via B C g"
  from A1 have f_tr: "total_recursive f" by (unfold one_reducible_to_via_def, auto)
  from A1 have f_inj: "inj f" by (unfold one_reducible_to_via_def, auto)
  from A1 have L1: " x. (x  A) = (f x  B)" by (unfold one_reducible_to_via_def, auto)
  from A2 have g_tr: "total_recursive g" by (unfold one_reducible_to_via_def, auto)
  from A2 have g_inj: "inj g" by (unfold one_reducible_to_via_def, auto)
  from A2 have L2: " x. (x  B) = (g x  C)" by (unfold one_reducible_to_via_def, auto)
  from g_tr f_tr have fg_tr: "total_recursive (g o f)" by (rule comp_tot_rec)
  from g_inj f_inj have fg_inj: "inj (g o f)" by (rule inj_compose)
  from L1 L2 have L3: "( x. (x  A) = ((g o f) x  C))" by auto
  with fg_tr fg_inj show ?thesis by (unfold one_reducible_to_via_def, auto)
qed

lemma one_reducible_to_trans: " one_reducible_to A B; one_reducible_to B C   one_reducible_to A C"
proof -
  assume "one_reducible_to A B"
  then obtain f where A1: "one_reducible_to_via A B f" unfolding one_reducible_to_def by auto
  assume "one_reducible_to B C"
  then obtain g where A2: "one_reducible_to_via B C g" unfolding one_reducible_to_def by auto
  from A1 A2 have "one_reducible_to_via A C (g o f)" by (rule one_reducible_to_via_trans)
  then show ?thesis unfolding one_reducible_to_def by auto
qed

lemma one_reducible_to_via_refl: "one_reducible_to_via A A (λ x. x)"
proof -
  have is_pr: "(λ x. x)  PrimRec1" by (rule pr_id1_1)
  then have is_tr: "total_recursive (λ x. x)" by (rule pr_is_total_rec)
  have is_inj: "inj (λ x. x)" by simp
  have L1: " x. (x  A) = (((λ x. x) x)  A)" by simp
  with is_tr is_inj show ?thesis by (unfold one_reducible_to_via_def, auto)
qed

lemma one_reducible_to_refl: "one_reducible_to A A"
proof -
  have "one_reducible_to_via A A (λ x. x)" by (rule one_reducible_to_via_refl)
  then show ?thesis by (unfold one_reducible_to_def, auto)
qed

lemma many_reducible_to_via_trans: " many_reducible_to_via A B f; many_reducible_to_via B C g   many_reducible_to_via A C (g o f)"
proof -
  assume A1: "many_reducible_to_via A B f"
  assume A2: "many_reducible_to_via B C g"
  from A1 have f_tr: "total_recursive f" by (unfold many_reducible_to_via_def, auto)
  from A1 have L1: " x. (x  A) = (f x  B)" by (unfold many_reducible_to_via_def, auto)
  from A2 have g_tr: "total_recursive g" by (unfold many_reducible_to_via_def, auto)
  from A2 have L2: " x. (x  B) = (g x  C)" by (unfold many_reducible_to_via_def, auto)
  from g_tr f_tr have fg_tr: "total_recursive (g o f)" by (rule comp_tot_rec)
  from L1 L2 have L3: "( x. (x  A) = ((g o f) x  C))" by auto
  with fg_tr show ?thesis by (unfold many_reducible_to_via_def, auto)
qed

lemma many_reducible_to_trans: " many_reducible_to A B; many_reducible_to B C   many_reducible_to A C"
proof -
  assume "many_reducible_to A B"
  then obtain f where A1: "many_reducible_to_via A B f"
    unfolding many_reducible_to_def by auto
  assume "many_reducible_to B C"
  then obtain g where A2: "many_reducible_to_via B C g"
    unfolding many_reducible_to_def by auto
  from A1 A2 have "many_reducible_to_via A C (g o f)" by (rule many_reducible_to_via_trans)
  then show ?thesis unfolding many_reducible_to_def by auto
qed

lemma one_reducibility_via_is_many: "one_reducible_to_via A B f  many_reducible_to_via A B f"
proof -
  assume A: "one_reducible_to_via A B f"
  from A have f_tr: "total_recursive f" by (unfold one_reducible_to_via_def, auto)
  from A have " x. (x  A) = (f x  B)" by (unfold one_reducible_to_via_def, auto)
  with f_tr show ?thesis by (unfold many_reducible_to_via_def, auto)
qed

lemma one_reducibility_is_many: "one_reducible_to A B  many_reducible_to A B"
proof -
  assume "one_reducible_to A B"
  then obtain f where A: "one_reducible_to_via A B f" 
    unfolding one_reducible_to_def by auto
  then have "many_reducible_to_via A B f" by (rule one_reducibility_via_is_many)
  then show ?thesis unfolding many_reducible_to_def by auto
qed

lemma many_reducible_to_via_refl: "many_reducible_to_via A A (λ x. x)"
proof -
  have "one_reducible_to_via A A (λ x. x)" by (rule one_reducible_to_via_refl)
  then show ?thesis by (rule one_reducibility_via_is_many)
qed

lemma many_reducible_to_refl: "many_reducible_to A A"
proof -
  have "one_reducible_to A A" by (rule one_reducible_to_refl)
  then show ?thesis by (rule one_reducibility_is_many)
qed

theorem m_red_to_comp: " many_reducible_to A B; computable B   computable A"
proof -
  assume "many_reducible_to A B"
  then obtain f where A1: "many_reducible_to_via A B f" 
    unfolding many_reducible_to_def by auto
  from A1 have f_tr: "total_recursive f" by (unfold many_reducible_to_via_def, auto)
  from A1 have L1: " x. (x  A) = (f x  B)" by (unfold many_reducible_to_via_def, auto)
  assume "computable B"
  then have L2: "total_recursive (chf B)" by (rule comp_impl_tot_rec)
  have L3: "chf A = (chf B) o f"
  proof fix x
    have "chf A x = (chf B) (f x)"
    proof cases
      assume A: "x  A"
      then have L3_1: "chf A x = 0" by (simp add: chf_lm_2)
      from A L1 have "f x  B" by auto
      then have L3_2: "(chf B) (f x) = 0" by (simp add: chf_lm_2)
      from L3_1 L3_2 show "chf A x = (chf B) (f x)" by auto
    next
      assume A: "x  A"
      then have L3_1: "chf A x = 1" by (simp add: chf_lm_3)
      from A L1 have "f x  B" by auto
      then have L3_2: "(chf B) (f x) = 1" by (simp add: chf_lm_3)
      from L3_1 L3_2 show "chf A x = (chf B) (f x)" by auto
    qed
    then show "chf A x = (chf B  f) x" by auto
  qed
  from L2 f_tr have "total_recursive (chf B  f)" by (rule comp_tot_rec)
  with L3 have "total_recursive (chf A)" by auto
  then show ?thesis by (rule tot_rec_impl_comp)
qed

lemma many_reducible_lm_1: "many_reducible_to univ_ce A  ¬ computable A"
proof (rule ccontr)
  assume A1: "many_reducible_to univ_ce A"
  assume "¬ ¬ computable A"
  then have A2: "computable A" by auto
  from A1 A2 have "computable univ_ce" by (rule m_red_to_comp)
  with univ_ce_is_not_comp3 show False by auto
qed

lemma one_reducible_lm_1: "one_reducible_to univ_ce A  ¬ computable A"
proof -
  assume "one_reducible_to univ_ce A"
  then have "many_reducible_to univ_ce A" by (rule one_reducibility_is_many)
  then show ?thesis by (rule many_reducible_lm_1)
qed

lemma one_reducible_lm_2: "one_reducible_to_via (nat_to_ce_set n) univ_ce (λ x. c_pair n x)"
proof -
  define f where "f x = c_pair n x" for x
  have f_is_pr: "f  PrimRec1" unfolding f_def by prec
  then have f_tr: "total_recursive f" by (rule pr_is_total_rec)
  have f_inj: "inj f"
  proof (rule injI)
    fix x y assume A: "f x = f y"
    then have "c_pair n x = c_pair n y" by (unfold f_def)
    then show "x = y" by (rule c_pair_inj2)
  qed
  have " x. (x  (nat_to_ce_set n)) = (f x  univ_ce)"
  proof fix x show "(x  nat_to_ce_set n) = (f x  univ_ce)" by (unfold f_def, simp add: univ_ce_lm_1)
  qed
  with f_tr f_inj show ?thesis by (unfold f_def, unfold one_reducible_to_via_def, auto)
qed

lemma one_reducible_lm_3: "one_reducible_to (nat_to_ce_set n) univ_ce"
proof -
  have "one_reducible_to_via (nat_to_ce_set n) univ_ce (λ x. c_pair n x)" by (rule one_reducible_lm_2)
  then show ?thesis by (unfold one_reducible_to_def, auto)
qed

lemma one_reducible_lm_4: "A  ce_sets  one_reducible_to A univ_ce"
proof -
  assume "A  ce_sets"
  then have " n. A = nat_to_ce_set n" by (rule nat_to_ce_set_srj)
  then obtain n where "A = nat_to_ce_set n" by auto
  with one_reducible_lm_3 show ?thesis by auto
qed

subsection ‹One-complete sets›

definition
  one_complete :: "nat set  bool" where
  "one_complete = (λ A. A  ce_sets  ( B. B  ce_sets  one_reducible_to B A))"

theorem univ_is_complete: "one_complete univ_ce"
proof (unfold one_complete_def)
  show "univ_ce  ce_sets  (B. B  ce_sets  one_reducible_to B univ_ce)"
  proof
    show "univ_ce  ce_sets" by (rule univ_is_ce)
  next
    show "B. B  ce_sets  one_reducible_to B univ_ce"
    proof (rule allI, rule impI)
      fix B assume "B  ce_sets" then show "one_reducible_to B univ_ce" by (rule one_reducible_lm_4)
    qed
  qed
qed

subsection ‹Index sets, Rice's theorem›

definition
  index_set :: "nat set  bool" where
  "index_set = (λ A.  n m. n  A  (nat_to_ce_set n = nat_to_ce_set m)  m  A)"

lemma index_set_lm_1: " index_set A; n A; nat_to_ce_set n = nat_to_ce_set m   m  A"
proof -
  assume A1: "index_set A"
  assume A2: "n  A"
  assume A3: "nat_to_ce_set n = nat_to_ce_set m"
  from A2 A3 have L1: "n  A  (nat_to_ce_set n = nat_to_ce_set m)" by auto
  from A1 have L2: " n m. n  A  (nat_to_ce_set n = nat_to_ce_set m)  m  A" by (unfold index_set_def)
  from L1 L2 show ?thesis by auto
qed

lemma index_set_lm_2: "index_set A  index_set (-A)"
proof -
  assume A: "index_set A"
  show "index_set (-A)"
  proof (unfold index_set_def)
    show "n m. n  - A  nat_to_ce_set n = nat_to_ce_set m  m  - A"
    proof (rule allI, rule allI, rule impI)
      fix n m assume A1: "n  - A  nat_to_ce_set n = nat_to_ce_set m"
      from A1 have A2: "n  -A" by auto
      from A1 have A3: "nat_to_ce_set m = nat_to_ce_set n" by auto
      show "m  - A"
      proof
        assume "m  A"
        from A this A3 have "n  A" by (rule index_set_lm_1)
        with A2 show False by auto
      qed
    qed
  qed
qed

lemma Rice_lm_1: " index_set A; A  {}; A  UNIV;  n  A. nat_to_ce_set n = {}   one_reducible_to univ_ce (- A)"
proof -
  assume A1: "index_set A"
  assume A2: "A  {}"
  assume A3: "A  UNIV"
  assume " n  A. nat_to_ce_set n = {}"
  then obtain e_0 where e_0_in_A: "e_0  A" and e_0_empty: "nat_to_ce_set e_0 = {}" by auto
  from e_0_in_A A3 obtain e_1 where e_1_not_in_A: "e_1  (- A)" by auto
  with e_0_in_A have e_0_neq_e_1: "e_0  e_1" by auto
  have "nat_to_ce_set e_0  nat_to_ce_set e_1"
  proof
    assume "nat_to_ce_set e_0 = nat_to_ce_set e_1"
    with A1 e_0_in_A have "e_1  A" by (rule index_set_lm_1)
    with e_1_not_in_A show False by auto
  qed
  with e_0_empty have e1_not_empty: "nat_to_ce_set e_1  {}" by auto
  define we_1 where "we_1 = nat_to_ce_set e_1"
  from e1_not_empty have we_1_not_empty: "we_1  {}" by (unfold we_1_def)
  define r where "r = univ_ce × we_1"
  have loc_lm_1: " x. x  univ_ce   y. (y  we_1) = ((x,y)  r)" by (unfold r_def, auto)
  have loc_lm_2: " x. x  univ_ce   y. (y  {}) = ((x,y)  r)" by (unfold r_def, auto)
  have r_ce: "r  ce_rels"
  proof (unfold r_def, rule ce_rel_lm_29)
    show "univ_ce  ce_sets" by (rule univ_is_ce)
    show "we_1  ce_sets" by (unfold we_1_def, rule nat_to_ce_set_into_ce)
  qed
  define we_n where "we_n = ce_rel_to_set r"
  from r_ce have we_n_ce: "we_n  ce_sets" by (unfold we_n_def, rule ce_rel_lm_6)
  then have " n. we_n = nat_to_ce_set n" by (rule nat_to_ce_set_srj)
  then obtain n where we_n_df1: "we_n = nat_to_ce_set n" by auto
  define f where "f x = s_ce n x" for x
  from s_ce_is_pr have f_is_pr: "f  PrimRec1" unfolding f_def by prec
  then have f_tr: "total_recursive f" by (rule pr_is_total_rec)
  have f_inj: "inj f"
  proof (rule injI)
    fix x y
    assume "f x = f y"
    then have "s_ce n x = s_ce n y" by (unfold f_def)
    then show "x = y" by (rule s_ce_inj2)
  qed
  have loc_lm_3: " x y. (c_pair x y  we_n) = (y  nat_to_ce_set (f x))"
  proof (rule allI, rule allI)
    fix x y show "(c_pair x y  we_n) = (y  nat_to_ce_set (f x))" by (unfold f_def, unfold we_n_df1, simp add: s_ce_1_1_th)
  qed
  from A1 have loc_lm_4: "index_set (- A)" by (rule index_set_lm_2)
  have loc_lm_5: " x. (x  univ_ce) = (f x  -A)"
  proof fix x show "(x  univ_ce) = (f x  -A)"
    proof
      assume A: "x  univ_ce"
      then have S1: " y. (y  we_1) = ((x,y)  r)" by (rule loc_lm_1)
      from ce_rel_lm_12 have " y. (c_pair x y  ce_rel_to_set r) = ((x,y)  r)" by auto
      then have " y. ((x,y)  r) = (c_pair x y  we_n)" by (unfold we_n_def, auto)
      with S1 have " y. (y  we_1) = (c_pair x y  we_n)" by auto
      with loc_lm_3 have " y. (y  we_1) = (y  nat_to_ce_set (f x))" by auto
      then have S2: "we_1 = nat_to_ce_set (f x)" by auto
      then have "nat_to_ce_set e_1 = nat_to_ce_set (f x)" by (unfold we_1_def)
      with loc_lm_4 e_1_not_in_A show "f x  -A" by (rule index_set_lm_1)
    next
      show " f x  - A  x  univ_ce"
      proof (rule ccontr)
        assume fx_in_A: "f x  - A"
        assume x_not_in_univ: "x  univ_ce"
        then have S1: " y. (y  {}) = ((x,y)  r)" by (rule loc_lm_2)
        from ce_rel_lm_12 have " y. (c_pair x y  ce_rel_to_set r) = ((x,y)  r)" by auto
        then have " y. ((x,y)  r) = (c_pair x y  we_n)" by (unfold we_n_def, auto)
        with S1 have " y. (y  {}) = (c_pair x y  we_n)" by auto
        with loc_lm_3 have " y. (y  {}) = (y  nat_to_ce_set (f x))" by auto
        then have S2: "{} = nat_to_ce_set (f x)" by auto
        then have "nat_to_ce_set e_0 = nat_to_ce_set (f x)" by (unfold e_0_empty)
        with A1 e_0_in_A have "f x  A" by (rule index_set_lm_1)
        with fx_in_A show False by auto
      qed
    qed
  qed
  with f_tr f_inj have "one_reducible_to_via univ_ce (-A) f" by (unfold one_reducible_to_via_def, auto)
  then show ?thesis by (unfold one_reducible_to_def, auto)
qed

lemma Rice_lm_2: " index_set A; A  {}; A  UNIV; n  A;  nat_to_ce_set n = {}   one_reducible_to univ_ce (- A)"
proof -
  assume A1: "index_set A"
  assume A2: "A  {}"
  assume A3: "A  UNIV"
  assume A4: "n  A"
  assume A5: "nat_to_ce_set n = {}"
  from A4 A5 have S1: " n  A. nat_to_ce_set n = {}" by auto
  from A1 A2 A3 S1 show ?thesis by (rule Rice_lm_1)
qed

theorem Rice_1: " index_set A; A  {}; A  UNIV   one_reducible_to univ_ce A  one_reducible_to univ_ce (- A)"
proof -
  assume A1: "index_set A"
  assume A2: "A  {}"
  assume A3: "A  UNIV"
  from ce_empty have " n. {} = nat_to_ce_set n" by (rule nat_to_ce_set_srj)
  then obtain n where n_empty: "nat_to_ce_set n = {}" by auto
  show ?thesis
  proof cases
    assume A: "n  A"
    from A1 A2 A3 A n_empty have "one_reducible_to univ_ce (- A)" by (rule Rice_lm_2)
    then show ?thesis by auto
  next
    assume "n  A" then have A: "n  - A" by auto
    from A1 have S1: "index_set (- A)" by (rule index_set_lm_2)
    from A3 have S2: "- A  {}" by auto
    from A2 have S3: "- A  UNIV" by auto
    from S1 S2 S3 A n_empty have "one_reducible_to univ_ce (- (- A))" by (rule Rice_lm_2)
    then have "one_reducible_to univ_ce A" by simp
    then show ?thesis by auto
  qed
qed

theorem Rice_2: " index_set A; A  {}; A  UNIV   ¬ computable A"
proof -
  assume A1: "index_set A"
  assume A2: "A  {}"
  assume A3: "A  UNIV"
  from A1 A2 A3 have "one_reducible_to univ_ce A  one_reducible_to univ_ce (- A)" by (rule Rice_1)
  then have S1: "¬ one_reducible_to univ_ce A  one_reducible_to univ_ce (- A)" by auto
  show ?thesis
  proof cases
    assume "one_reducible_to univ_ce A"
    then show "¬ computable A" by (rule one_reducible_lm_1)
  next
    assume "¬ one_reducible_to univ_ce A"
    with S1 have "one_reducible_to univ_ce (- A)" by auto
    then have "¬ computable (- A)" by (rule one_reducible_lm_1)
    with computable_complement_3 show "¬ computable A" by auto
  qed
qed

theorem Rice_3: " C  ce_sets; computable { n. nat_to_ce_set n  C}   C = {}  C = ce_sets"
proof (rule ccontr)
  assume A1: "C  ce_sets"
  assume A2: "computable { n. nat_to_ce_set n  C}"
  assume A3: "¬ (C = {}  C = ce_sets)"
  from A3 have A4: "C  {}" by auto
  from A3 have A5: "C  ce_sets" by auto
  define A where "A = { n. nat_to_ce_set n  C}"
  have S1: "index_set A"
  proof (unfold index_set_def)
    show "n m. n  A  nat_to_ce_set n = nat_to_ce_set m  m  A"
    proof (rule allI, rule allI, rule impI)
      fix n m assume A1_1: "n  A  nat_to_ce_set n = nat_to_ce_set m"
      from A1_1 have "n  A" by auto
      then have S1_1: "nat_to_ce_set n  C" by (unfold A_def, auto)
      from A1_1 have "nat_to_ce_set n = nat_to_ce_set m" by auto
      with S1_1 have "nat_to_ce_set m  C" by auto
      then show "m  A" by (unfold A_def, auto)
    qed
  qed
  have S2: "A  {}"
  proof -
    from A4 obtain B where S2_1: "B  C" by auto
    with A1 have "B  ce_sets" by auto
    then have " n. B = nat_to_ce_set n" by (rule nat_to_ce_set_srj)
    then obtain n where "B = nat_to_ce_set n" ..
    with S2_1 have "nat_to_ce_set n  C" by auto
    then show ?thesis by (unfold A_def, auto)
  qed
  have S3: "A  UNIV"
  proof -
    from A1 A5 obtain B where S2_1: "B  C" and S2_2: "B  ce_sets" by auto
    from S2_2 have " n. B = nat_to_ce_set n" by (rule nat_to_ce_set_srj)
    then obtain n where "B = nat_to_ce_set n" ..
    with S2_1 have "nat_to_ce_set n  C" by auto
    then show ?thesis by (unfold A_def, auto)
  qed
  from S1 S2 S3 have "¬ computable A" by (rule Rice_2)
  with A2 show False unfolding A_def by auto
qed

end