# Theory R1_BC

section ‹@{term "ℛ"} is not in BC\label{s:r1_bc}›

theory R1_BC
imports Lemma_R
CP_FIN_NUM  (* for V0 *)
begin

text ‹We show that @{term "U⇩0 ∪ V⇩0"} is not in BC,
which implies @{term "ℛ ∉ BC"}.

The proof is by contradiction. Assume there is a strategy $S$ learning @{term
"U⇩0 ∪ V⇩0"} behaviorally correct in the limit with respect to our
standard Gödel numbering $\varphi$. Thanks to Lemma~R for BC we can assume
$S$ to be total. Then we construct a function in @{term "U⇩0 ∪ V⇩0"} for
which $S$ fails.

As usual, there is a computable process building prefixes of functions
$\psi_j$. For every $j$ it starts with the singleton prefix $b = [j]$ and
computes the next prefix from a given prefix $b$ as follows:

\begin{enumerate}
\item Simulate $\varphi_{S(b0^k)}(|b| + k)$ for increasing $k$ for an
increasing number of steps.
\item Once a $k$ with $\varphi_{S(b0^k)}(|b| + k) = 0$ is found, extend the
prefix by $0^k1$.
\end{enumerate}

There is always such a $k$ because by assumption $S$ learns $b0^\infty \in U_0$ and thus outputs a hypothesis for $b0^\infty$ on almost all of its
prefixes. Therefore for almost all prefixes of the form $b0^k$, we have
$\varphi_{S(b0^k)} = b0^\infty$ and hence $\varphi_{S(b0^k)}(|b| + k) = 0$.
But Step~2 constructs $\psi_j$ such that $\psi_j(|b| + k) = 1$. Therefore $S$
does not hypothesize $\psi_j$ on the prefix $b0^k$ of $\psi_j$. And since the
process runs forever, $S$ outputs infinitely many incorrect hypotheses for
$\psi_j$ and thus does not learn $\psi_j$.

Applying Kleene's fixed-point theorem to @{term "ψ ∈ ℛ⇧2"}
yields a $j$ with $\varphi_j = \psi_j$ and thus $\psi_j \in V_0$. But $S$
does not learn any $\psi_j$, contradicting our assumption.

The result @{prop "ℛ ∉ BC"} can be obtained more directly by
running the process with the empty prefix, thereby constructing only one
function instead of a numbering. This function is in @{term R1}, and $S$
fails to learn it by the same reasoning as above. The stronger statement
about @{term "U⇩0 ∪ V⇩0"} will be exploited in
Section~\ref{s:union}.

In the following locale the assumption that $S$ learns @{term "U⇩0"}
suffices for analyzing the process. However, in order to arrive at the
desired contradiction this assumption is too weak because the functions built
by the process are not in @{term "U⇩0"}.›

locale r1_bc =
fixes s :: partial1
assumes s_in_R1: "s ∈ ℛ" and s_learn_U0: "learn_bc φ U⇩0 s"
begin

lemma s_learn_prenum: "⋀b. learn_bc φ {prenum b} s"
using s_learn_U0 U0_altdef learn_bc_closed_subseteq by blast

text ‹A @{typ recf} for the strategy:›

definition r_s :: recf where
"r_s ≡ SOME rs. recfn 1 rs ∧  total rs ∧ s = (λx. eval rs [x])"

lemma r_s_recfn [simp]: "recfn 1 r_s"
and r_s_total: "⋀x. eval r_s [x] ↓"
and eval_r_s: "⋀x. s x = eval r_s [x]"
using r_s_def R1_SOME[OF s_in_R1, of r_s] by simp_all

text ‹We begin with the function that finds the $k$ from Step~1 of the
construction of $\psi$.›

definition "r_find_k ≡
let k = Cn 2 r_pdec1 [Id 2 0];
r = Cn 2 r_result1
[Cn 2 r_pdec2 [Id 2 0],
Cn 2 r_s [Cn 2 r_append_zeros [Id 2 1, k]],
Cn 2 r_add [Cn 2 r_length [Id 2 1], k]]
in Cn 1 r_pdec1 [Mn 1 (Cn 2 r_eq [r, r_constn 1 1])]"

lemma r_find_k_recfn [simp]: "recfn 1 r_find_k"
unfolding r_find_k_def by (simp add: Let_def)

text ‹There is always a suitable $k$, since the strategy learns
$b0^\infty$ for all $b$.›

lemma learn_bc_prenum_eventually_zero:
"∃k. φ (the (s (e_append_zeros b k))) (e_length b + k) ↓= 0"
proof -
let ?f = "prenum b"
have "∃n≥e_length b. φ (the (s (?f ▹ n))) = ?f"
using learn_bcE s_learn_prenum by (meson le_cases singletonI)
then obtain n where n: "n ≥ e_length b" "φ (the (s (?f ▹ n))) = ?f"
by auto
define k where "k = Suc n - e_length b"
let ?e = "e_append_zeros b k"
have len: "e_length ?e = Suc n"
using k_def n e_append_zeros_length by simp
have "?f ▹ n = ?e"
proof -
have "e_length ?e > 0"
using len n(1) by simp
moreover have "?f x ↓= e_nth ?e x" for x
proof (cases "x < e_length b")
case True
then show ?thesis using e_nth_append_zeros by simp
next
case False
then have "?f x ↓= 0" by simp
moreover from False have "e_nth ?e x = 0"
using e_nth_append_zeros_big by simp
ultimately show ?thesis by simp
qed
ultimately show ?thesis using initI[of "?e"] len by simp
qed
with n(2) have "φ (the (s ?e)) = ?f" by simp
then have "φ (the (s ?e)) (e_length ?e) ↓= 0"
using len n(1) by auto
then show ?thesis using e_append_zeros_length by auto
qed

lemma if_eq_eq: "(if v = 1 then (0 :: nat) else 1) = 0 ⟹ v = 1"
by presburger

lemma r_find_k:
shows "eval r_find_k [b] ↓"
and "let k = the (eval r_find_k [b])
in φ (the (s (e_append_zeros b k))) (e_length b + k) ↓= 0"
proof -
let ?k = "Cn 2 r_pdec1 [Id 2 0]"
let ?argt = "Cn 2 r_pdec2 [Id 2 0]"
let ?argi = "Cn 2 r_s [Cn 2 r_append_zeros [Id 2 1, ?k]]"
let ?argx = "Cn 2 r_add [Cn 2 r_length [Id 2 1], ?k]"
let ?r = "Cn 2 r_result1 [?argt, ?argi, ?argx]"
define f where "f ≡
let k = Cn 2 r_pdec1 [Id 2 0];
r = Cn 2 r_result1
[Cn 2 r_pdec2 [Id 2 0],
Cn 2 r_s [Cn 2 r_append_zeros [Id 2 1, k]],
Cn 2 r_add [Cn 2 r_length [Id 2 1], k]]
in Cn 2 r_eq [r, r_constn 1 1]"
then have "recfn 2 f" by (simp add: Let_def)
have "total r_s"
then have "total f"
unfolding f_def using Cn_total Mn_free_imp_total by (simp add: Let_def)

have "eval ?argi [z, b] = s (e_append_zeros b (pdec1 z))" for z
using r_append_zeros ‹recfn 2 f› eval_r_s by auto
then have "eval ?argi [z, b] ↓= the (s (e_append_zeros b (pdec1 z)))" for z
using eval_r_s r_s_total by simp
moreover have "recfn 2 ?r" using ‹recfn 2 f› by auto
ultimately have r: "eval ?r [z, b] =
eval r_result1 [pdec2 z, the (s (e_append_zeros b (pdec1 z))), e_length b + pdec1 z]"
for z
by simp
then have f: "eval f [z, b] ↓= (if the (eval ?r [z, b]) = 1 then 0 else 1)" for z
using f_def ‹recfn 2 f› prim_recfn_total by (auto simp add: Let_def)

have "∃k. φ (the (s (e_append_zeros b k))) (e_length b + k) ↓= 0"
using s_learn_prenum learn_bc_prenum_eventually_zero by auto
then obtain k where "φ (the (s (e_append_zeros b k))) (e_length b + k) ↓= 0"
by auto
then obtain t where "eval r_result1 [t, the (s (e_append_zeros b k)), e_length b + k] ↓= Suc 0"
using r_result1_converg_phi(1) by blast
then have t: "eval r_result1 [t, the (s (e_append_zeros b k)), e_length b + k] ↓= Suc 0"
by simp

let ?z = "prod_encode (k, t)"
have "eval ?r [?z, b] ↓= Suc 0"
using t r by (metis fst_conv prod_encode_inverse snd_conv)
with f have fzb: "eval f [?z, b] ↓= 0" by simp
moreover have "eval (Mn 1 f) [b] =
(if (∃z. eval f ([z, b]) ↓= 0)
then Some (LEAST z. eval f [z, b] ↓= 0)
else None)"
using eval_Mn_total[of 1 f "[b]"] ‹total f› ‹recfn 2 f› by simp
ultimately have mn1f: "eval (Mn 1 f) [b] ↓= (LEAST z. eval f [z, b] ↓= 0)"
by auto
with fzb have "eval f [the (eval (Mn 1 f) [b]), b] ↓= 0" (is "eval f [?zz, b] ↓= 0")
using ‹total f› ‹recfn 2 f› LeastI_ex[of "%z. eval f [z, b] ↓= 0"] by auto
moreover have "eval f [?zz, b] ↓= (if the (eval ?r [?zz, b]) = 1 then 0 else 1)"
using f by simp
ultimately have "(if the (eval ?r [?zz, b]) = 1 then (0 :: nat) else 1) = 0" by auto
then have "the (eval ?r [?zz, b]) = 1"
using if_eq_eq[of "the (eval ?r [?zz, b])"] by simp
then have
"eval r_result1
[pdec2 ?zz, the (s (e_append_zeros b (pdec1 ?zz))), e_length b + pdec1 ?zz] ↓=
1"
using r r_result1_total r_result1_prim totalE
by (metis length_Cons list.size(3) numeral_3_eq_3 option.collapse)
then have *: "φ (the (s (e_append_zeros b (pdec1 ?zz)))) (e_length b + pdec1 ?zz) ↓= 0"

define Mn1f where "Mn1f = Mn 1 f"
then have "eval Mn1f [b] ↓= ?zz"
using mn1f by auto
moreover have "recfn 1 (Cn 1 r_pdec1 [Mn1f])"
using ‹recfn 2 f› Mn1f_def by simp
ultimately have "eval (Cn 1 r_pdec1 [Mn1f]) [b] = eval r_pdec1 [the (eval (Mn1f) [b])]"
by auto
then have "eval (Cn 1 r_pdec1 [Mn1f]) [b] = eval r_pdec1 [?zz]"
using Mn1f_def by blast
then have 1: "eval (Cn 1 r_pdec1 [Mn1f]) [b] ↓= pdec1 ?zz"
by simp
moreover have "recfn 1 (Cn 1 S [Cn 1 r_pdec1 [Mn1f]])"
using ‹recfn 2 f› Mn1f_def by simp
ultimately have "eval (Cn 1 S [Cn 1 r_pdec1 [Mn1f]]) [b] =
eval S [the (eval (Cn 1 r_pdec1 [Mn1f]) [b])]"
by simp
then have "eval (Cn 1 S [Cn 1 r_pdec1 [Mn1f]]) [b] = eval S [pdec1 ?zz]"
using 1 by simp
then have "eval (Cn 1 S [Cn 1 r_pdec1 [Mn1f]]) [b] ↓= Suc (pdec1 ?zz)"
by simp
moreover have "eval r_find_k [b] = eval (Cn 1 r_pdec1 [Mn1f]) [b]"
unfolding r_find_k_def Mn1f_def f_def by metis
ultimately have r_find_ksb: "eval r_find_k [b] ↓= pdec1 ?zz"
using 1 by simp
then show "eval r_find_k [b] ↓" by simp_all

from r_find_ksb have "the (eval r_find_k [b]) = pdec1 ?zz"
by simp
moreover have "φ (the (s (e_append_zeros b (pdec1 ?zz)))) (e_length b + pdec1 ?zz) ↓= 0"
using * by simp
ultimately show "let k = the (eval r_find_k [b])
in φ (the (s (e_append_zeros b k))) (e_length b + k) ↓= 0"
by simp
qed

lemma r_find_k_total: "total r_find_k"
by (simp add: s_learn_prenum r_find_k(1) totalI1)

text ‹The following function represents one iteration of the
process.›

abbreviation "r_next ≡
Cn 3 r_snoc [Cn 3 r_append_zeros [Id 3 1, Cn 3 r_find_k [Id 3 1]], r_constn 2 1]"

text ‹Using @{term r_next} we define the function @{term r_prefixes}
that computes the prefix after every iteration of the process.›

definition r_prefixes :: recf where
"r_prefixes ≡ Pr 1 r_singleton_encode r_next"

lemma r_prefixes_recfn: "recfn 2 r_prefixes"
unfolding r_prefixes_def by simp

lemma r_prefixes_total: "total r_prefixes"
proof -
have "recfn 3 r_next" by simp
then have "total r_next"
using ‹recfn 3 r_next› r_find_k_total Cn_total Mn_free_imp_total by auto
then show ?thesis
by (simp add: Mn_free_imp_total Pr_total r_prefixes_def)
qed

lemma r_prefixes_0: "eval r_prefixes [0, j] ↓= list_encode [j]"
unfolding r_prefixes_def by simp

lemma r_prefixes_Suc:
"eval r_prefixes [Suc n, j] ↓=
(let b = the (eval r_prefixes [n, j])
in e_snoc (e_append_zeros b (the (eval r_find_k [b]))) 1)"
proof -
have "recfn 3 r_next" by simp
then have "total r_next"
using ‹recfn 3 r_next› r_find_k_total Cn_total Mn_free_imp_total by auto
have eval_next: "eval r_next [t, v, j] ↓=
e_snoc (e_append_zeros v (the (eval r_find_k [v]))) 1"
for t v j
using r_find_k_total ‹recfn 3 r_next› r_append_zeros by simp
then have "eval r_prefixes [Suc n, j] = eval r_next [n, the (eval r_prefixes [n, j]), j]"
using r_prefixes_total by (simp add: r_prefixes_def)
then show "eval r_prefixes [Suc n, j] ↓=
(let b = the (eval r_prefixes [n, j])
in e_snoc (e_append_zeros b (the (eval r_find_k [b]))) 1)"
using eval_next by metis
qed

text ‹Since @{term r_prefixes} is total, we can get away with
introducing a total function.›

definition prefixes :: "nat ⇒ nat ⇒ nat" where
"prefixes j t ≡ the (eval r_prefixes [t, j])"

lemma prefixes_Suc:
"prefixes j (Suc t) =
e_snoc (e_append_zeros (prefixes j t) (the (eval r_find_k [prefixes j t]))) 1"
unfolding prefixes_def using r_prefixes_Suc by (simp_all add: Let_def)

lemma prefixes_Suc_length:
"e_length (prefixes j (Suc t)) =
Suc (e_length (prefixes j t) + the (eval r_find_k [prefixes j t]))"
using e_append_zeros_length prefixes_Suc by simp

lemma prefixes_length_mono: "e_length (prefixes j t) < e_length (prefixes j (Suc t))"
using prefixes_Suc_length by simp

lemma prefixes_length_mono': "e_length (prefixes j t) ≤ e_length (prefixes j (t + d))"
proof (induction d)
case 0
then show ?case by simp
next
case (Suc d)
then show ?case using prefixes_length_mono le_less_trans by fastforce
qed

lemma prefixes_length_lower_bound: "e_length (prefixes j t) ≥ Suc t"
proof (induction t)
case 0
then show ?case by (simp add: prefixes_def r_prefixes_0)
next
case (Suc t)
moreover have "Suc (e_length (prefixes j t)) ≤ e_length (prefixes j (Suc t))"
using prefixes_length_mono by (simp add: Suc_leI)
ultimately show ?case by simp
qed

lemma prefixes_Suc_nth:
assumes "x < e_length (prefixes j t)"
shows "e_nth (prefixes j t) x = e_nth (prefixes j (Suc t)) x"
proof -
define k where "k = the (eval r_find_k [prefixes j t])"
let ?u = "e_append_zeros (prefixes j t) k"
have "prefixes j (Suc t) =
e_snoc (e_append_zeros (prefixes j t) (the (eval r_find_k [prefixes j t]))) 1"
using prefixes_Suc by simp
with k_def have "prefixes j (Suc t) = e_snoc ?u 1"
by simp
then have "e_nth (prefixes j (Suc t)) x = e_nth (e_snoc ?u 1) x"
by simp
moreover have "x < e_length ?u"
using assms e_append_zeros_length by auto
ultimately have "e_nth (prefixes j (Suc t)) x = e_nth ?u x"
using e_nth_snoc_small by simp
moreover have "e_nth ?u x = e_nth (prefixes j t) x"
using assms e_nth_append_zeros by simp
ultimately show "e_nth (prefixes j t) x = e_nth (prefixes j (Suc t)) x"
by simp
qed

lemma prefixes_Suc_last: "e_nth (prefixes j (Suc t)) (e_length (prefixes j (Suc t)) - 1) = 1"
using prefixes_Suc by simp

lemma prefixes_le_nth:
assumes "x < e_length (prefixes j t)"
shows "e_nth (prefixes j t) x = e_nth (prefixes j (t + d)) x"
proof (induction d)
case 0
then show ?case by simp
next
case (Suc d)
have "x < e_length (prefixes j (t + d))"
using s_learn_prenum assms prefixes_length_mono'
then have "e_nth (prefixes j (t + d)) x = e_nth (prefixes j (t + Suc d)) x"
using prefixes_Suc_nth by simp
with Suc show ?case by simp
qed

text ‹The numbering $\psi$ is defined via @{term[names_short] prefixes}.›

definition psi :: partial2 ("ψ") where
"ψ j x ≡ Some (e_nth (prefixes j (Suc x)) x)"

lemma psi_in_R2: "ψ ∈ ℛ⇧2"
proof
define r where "r ≡  Cn 2 r_nth [Cn 2 r_prefixes [Cn 2 S [Id 2 1], Id 2 0], Id 2 1]"
then have "recfn 2 r"
using r_prefixes_recfn by simp
then have "eval r [j, x] ↓= e_nth (prefixes j (Suc x)) x" for j x
unfolding r_def prefixes_def using r_prefixes_total r_prefixes_recfn e_nth by simp
then have "eval r [j, x] = ψ j x" for j x
unfolding psi_def by simp
then show "ψ ∈ 𝒫⇧2"
using ‹recfn 2 r› by auto
show "total2 ψ"
unfolding psi_def by auto
qed

lemma psi_eq_nth_prefixes:
assumes "x < e_length (prefixes j t)"
shows "ψ j x ↓= e_nth (prefixes j t) x"
proof (cases "Suc x < t")
case True
have "x ≤ e_length (prefixes j x)"
using prefixes_length_lower_bound by (simp add: Suc_leD)
also have "... < e_length (prefixes j (Suc x))"
using prefixes_length_mono s_learn_prenum by simp
finally have "x < e_length (prefixes j (Suc x))" .
with True have "e_nth (prefixes j (Suc x)) x = e_nth (prefixes j t) x"
using prefixes_le_nth[of x j "Suc x" "t - Suc x"] by simp
then show ?thesis using psi_def by simp
next
case False
then have "e_nth (prefixes j (Suc x)) x = e_nth (prefixes j t) x"
using prefixes_le_nth[of x j t "Suc x - t"] assms by simp
then show ?thesis using psi_def by simp
qed

lemma psi_at_0: "ψ j 0 ↓= j"
using psi_eq_nth_prefixes[of 0 j 0] prefixes_length_lower_bound[of 0 j]

text ‹The prefixes output by the process @{term[names_short] "prefixes j"} are
indeed prefixes of $\psi_j$.›

lemma prefixes_init_psi: "ψ j ▹ (e_length (prefixes j (Suc t)) - 1) = prefixes j (Suc t)"
proof (rule initI[of "prefixes j (Suc t)"])
let ?e = "prefixes j (Suc t)"
show "e_length ?e > 0"
using prefixes_length_lower_bound[of "Suc t" j] by auto
show "⋀x. x < e_length ?e ⟹ ψ j x ↓= e_nth ?e x"
using prefixes_Suc_nth psi_eq_nth_prefixes by simp
qed

text ‹Every prefix of $\psi_j$ generated by the process
@{term[names_short] "prefixes j"} (except for the initial one) is of the form
$b0^k1$. But $k$ is chosen such that $\varphi_{S(b0^k)}(|b|+k) = 0 \neq 1 = b0^k1_{|b|+k}$. Therefore the hypothesis $S(b0^k)$ is incorrect for
$\psi_j$.›

lemma hyp_wrong_at_last:
"φ (the (s (e_butlast (prefixes j (Suc t))))) (e_length (prefixes j (Suc t)) - 1) ≠
ψ j (e_length (prefixes j (Suc t)) - 1)"
(is "?lhs ≠ ?rhs")
proof -
let ?b = "prefixes j t"
let ?k = "the (eval r_find_k [?b])"
let ?x = "e_length (prefixes j (Suc t)) - 1"
have "e_butlast (prefixes j (Suc t)) = e_append_zeros ?b ?k"
using s_learn_prenum prefixes_Suc by simp
then have "?lhs = φ (the (s (e_append_zeros ?b ?k))) ?x"
by simp
moreover have "?x = e_length ?b + ?k"
using prefixes_Suc_length by simp
ultimately have "?lhs = φ (the (s (e_append_zeros ?b ?k))) (e_length ?b + ?k)"
by simp
then have "?lhs ↓= 0"
using r_find_k(2) r_s_total s_learn_prenum by metis
moreover have "?x < e_length (prefixes j (Suc t))"
using prefixes_length_lower_bound le_less_trans linorder_not_le s_learn_prenum
by fastforce
ultimately have "?rhs ↓= e_nth (prefixes j (Suc t)) ?x"
using psi_eq_nth_prefixes[of ?x j "Suc t"] by simp
moreover have "e_nth (prefixes j (Suc t)) ?x = 1"
using prefixes_Suc prefixes_Suc_last by simp
ultimately have "?rhs ↓= 1" by simp
with ‹?lhs ↓= 0› show ?thesis by simp
qed

corollary hyp_wrong: "φ (the (s (e_butlast (prefixes j (Suc t))))) ≠ ψ j"
using hyp_wrong_at_last[of j t] by auto

text ‹For all $j$, the strategy $S$ outputs infinitely many wrong hypotheses for
$\psi_j$›

lemma infinite_hyp_wrong: "∃m>n. φ (the (s (ψ j ▹ m))) ≠ ψ j"
proof -
let ?b = "prefixes j (Suc (Suc n))"
let ?bb = "e_butlast ?b"
have len_b: "e_length ?b > Suc (Suc n)"
using prefixes_length_lower_bound by (simp add: Suc_le_lessD)
then have len_bb: "e_length ?bb > Suc n" by simp
define m where "m = e_length ?bb - 1"
with len_bb have "m > n" by simp
have "ψ j ▹ m = ?bb"
proof -
have "ψ j ▹ (e_length ?b - 1) = ?b"
using prefixes_init_psi by simp
then have "ψ j ▹ (e_length ?b - 2) = ?bb"
using init_butlast_init psi_in_R2 R2_proj_R1 R1_imp_total1 len_bb length_init
by (metis Suc_1 diff_diff_left length_butlast length_greater_0_conv
list.size(3) list_decode_encode not_less0 plus_1_eq_Suc)
then show ?thesis by (metis diff_Suc_1 length_init m_def)
qed
moreover have "φ (the (s ?bb)) ≠ ψ j"
using hyp_wrong by simp
ultimately have "φ (the (s (ψ j ▹ m))) ≠ ψ j"
by simp
with ‹m > n› show ?thesis by auto
qed

lemma U0_V0_not_learn_bc: "¬ learn_bc φ (U⇩0 ∪ V⇩0) s"
proof -
obtain j where j: "φ j = ψ j"
using R2_imp_P2 kleene_fixed_point psi_in_R2 by blast
moreover have "∃m>n. φ (the (s ((ψ j) ▹ m))) ≠ ψ j" for n
using infinite_hyp_wrong[of _ j] by simp
ultimately have "¬ learn_bc φ {ψ j} s"
using infinite_hyp_wrong_not_BC by simp
moreover have "ψ j ∈ V⇩0"
proof -
have "ψ j ∈ ℛ" (is "?f ∈ ℛ")
using psi_in_R2 by simp
moreover have "φ (the (?f 0)) = ?f"
using j psi_at_0[of j] by simp
ultimately show ?thesis by (simp add: V0_def)
qed
ultimately show "¬ learn_bc φ (U⇩0 ∪ V⇩0) s"
using learn_bc_closed_subseteq by auto
qed

end

lemma U0_V0_not_in_BC: "U⇩0 ∪ V⇩0 ∉ BC"
proof
assume in_BC: "U⇩0 ∪ V⇩0 ∈ BC"
then have "U⇩0 ∪ V⇩0 ∈ BC_wrt φ"
using BC_wrt_phi_eq_BC by simp
then obtain s where "learn_bc φ (U⇩0 ∪ V⇩0) s"
using BC_wrt_def by auto
then obtain s' where s': "s' ∈ ℛ" "learn_bc φ (U⇩0 ∪ V⇩0) s'"
using lemma_R_for_BC_simple by blast
then have learn_U0: "learn_bc φ U⇩0 s'"
using learn_bc_closed_subseteq[of φ "U⇩0 ∪ V⇩0" "s'"] by simp
then interpret r1_bc s'
have "¬ learn_bc φ (U⇩0 ∪ V⇩0) s'"
using learn_bc_closed_subseteq U0_V0_not_learn_bc by simp
with s'(2) show False by simp
qed

theorem R1_not_in_BC: "ℛ ∉ BC"
proof -
have "U⇩0 ∪ V⇩0 ⊆ ℛ"
using V0_def U0_in_NUM by auto
then show ?thesis
using U0_V0_not_in_BC BC_closed_subseteq by auto
qed

end