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" by (simp add: r_s_total totalI1) 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" by (simp add: r_result1_some_phi) 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' by (simp add: less_eq_Suc_le order_trans_rules(23)) 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] by (simp add: prefixes_def r_prefixes_0) 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' by (simp add: r1_bc_def s'(1)) 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