section ‹CONS is a proper subset of LIM\label{s:cons_lim}› theory CONS_LIM imports Inductive_Inference_Basics begin text ‹That there are classes in @{term "LIM - CONS"} was noted by Barzdin~\<^cite>‹"b-iiafp-74" and "b-iiafp-77"› and Blum and Blum~\<^cite>‹"bb-tmtii-75"›. It was proven by Wiehagen~\<^cite>‹"w-lerfss-76"› (see also Wiehagen and Zeugmann~\<^cite>‹"wz-idmowle-94"›). The proof uses this class:› definition U_LIMCONS :: "partial1 set" ("U⇘_{LIM-CONS}⇙") where "U⇘_{LIM-CONS}⇙ ≡ {vs @ [j] ⊙ p| vs j p. j ≥ 2 ∧ p ∈ ℛ⇩_{0}⇩_{1}∧ φ j = vs @ [j] ⊙ p}" text ‹Every function in @{term "U⇘_{LIM-CONS}⇙"} carries a Gödel number greater or equal two of itself, after which only zeros and ones occur. Thus, a strategy that always outputs the rightmost value greater or equal two in the given prefix will converge to this Gödel number. The next function searches an encoded list for the rightmost element greater or equal two.› definition rmge2 :: partial1 where "rmge2 e ≡ if ∀i<e_length e. e_nth e i < 2 then Some 0 else Some (e_nth e (GREATEST i. i < e_length e ∧ e_nth e i ≥ 2))" lemma rmge2: assumes "xs = list_decode e" shows "rmge2 e = (if ∀i<length xs. xs ! i < 2 then Some 0 else Some (xs ! (GREATEST i. i < length xs ∧ xs ! i ≥ 2)))" proof - have "(i < e_length e ∧ e_nth e i ≥ 2) = (i < length xs ∧ xs ! i ≥ 2)" for i using assms by simp then have "(GREATEST i. i < e_length e ∧ e_nth e i ≥ 2) = (GREATEST i. i < length xs ∧ xs ! i ≥ 2)" by simp moreover have "(∀i<length xs. xs ! i < 2) = (∀i<e_length e. e_nth e i < 2)" using assms by simp moreover have "(GREATEST i. i < length xs ∧ xs ! i ≥ 2) < length xs" (is "Greatest ?P < _") if "¬ (∀i<length xs. xs ! i < 2)" using that GreatestI_ex_nat[of ?P] le_less_linear order.asym by blast ultimately show ?thesis using rmge2_def assms by auto qed lemma rmge2_init: "rmge2 (f ▹ n) = (if ∀i<Suc n. the (f i) < 2 then Some 0 else Some (the (f (GREATEST i. i < Suc n ∧ the (f i) ≥ 2))))" proof - let ?xs = "prefix f n" have "f ▹ n = list_encode ?xs" by (simp add: init_def) moreover have "(∀i<Suc n. the (f i) < 2) = (∀i<length ?xs. ?xs ! i < 2)" by simp moreover have "(GREATEST i. i < Suc n ∧ the (f i) ≥ 2) = (GREATEST i. i < length ?xs ∧ ?xs ! i ≥ 2)" using length_prefix[of f n] prefix_nth[of _ n f] by metis moreover have "(GREATEST i. i < Suc n ∧ the (f i) ≥ 2) < Suc n" if "¬ (∀i<Suc n. the (f i) < 2)" using that GreatestI_ex_nat[of "λi. i<Suc n ∧ the (f i) ≥ 2" n] by fastforce ultimately show ?thesis using rmge2 by auto qed corollary rmge2_init_total: assumes "total1 f" shows "rmge2 (f ▹ n) = (if ∀i<Suc n. the (f i) < 2 then Some 0 else f (GREATEST i. i < Suc n ∧ the (f i) ≥ 2))" using assms total1_def rmge2_init by auto lemma rmge2_in_R1: "rmge2 ∈ ℛ" proof - define g where "g = Cn 3 r_ifle [r_constn 2 2, Cn 3 r_nth [Id 3 2, Id 3 0], Cn 3 r_nth [Id 3 2, Id 3 0], Id 3 1]" then have "recfn 3 g" by simp then have g: "eval g [j, r, e] ↓= (if 2 ≤ e_nth e j then e_nth e j else r)" for j r e using g_def by simp let ?h = "Pr 1 Z g" have "recfn 2 ?h" by (simp add: ‹recfn 3 g›) have h: "eval ?h [j, e] = (if ∀i<j. e_nth e i < 2 then Some 0 else Some (e_nth e (GREATEST i. i < j ∧ e_nth e i ≥ 2)))" for j e proof (induction j) case 0 then show ?case using ‹recfn 2 ?h› by auto next case (Suc j) then have "eval ?h [Suc j, e] = eval g [j, the (eval ?h [j, e]), e]" using ‹recfn 2 ?h› by auto then have *: "eval ?h [Suc j, e] ↓= (if 2 ≤ e_nth e j then e_nth e j else if ∀i<j. e_nth e i < 2 then 0 else (e_nth e (GREATEST i. i < j ∧ e_nth e i ≥ 2)))" using g Suc by auto show ?case proof (cases "∀i<Suc j. e_nth e i < 2") case True then show ?thesis using * by auto next case ex: False show ?thesis proof (cases "2 ≤ e_nth e j") case True then have "eval ?h [Suc j, e] ↓= e_nth e j" using * by simp moreover have "(GREATEST i. i < Suc j ∧ e_nth e i ≥ 2) = j" using ex True Greatest_equality[of "λi. i < Suc j ∧ e_nth e i ≥ 2"] by simp ultimately show ?thesis using ex by auto next case False then have "∃i<j. e_nth e i ≥ 2" using ex leI less_Suc_eq by blast with * have "eval ?h [Suc j, e] ↓= e_nth e (GREATEST i. i < j ∧ e_nth e i ≥ 2)" using False by (smt leD) moreover have "(GREATEST i. i < Suc j ∧ e_nth e i ≥ 2) = (GREATEST i. i < j ∧ e_nth e i ≥ 2)" using False ex by (metis less_SucI less_Suc_eq less_antisym numeral_2_eq_2) ultimately show ?thesis using ex by metis qed qed qed let ?hh = "Cn 1 ?h [Cn 1 r_length [Id 1 0], Id 1 0]" have "recfn 1 ?hh" using ‹recfn 2 ?h› by simp with h have hh: "eval ?hh [e] ↓= (if ∀i<e_length e. e_nth e i < 2 then 0 else e_nth e (GREATEST i. i < e_length e ∧ e_nth e i ≥ 2))" for e by auto then have "eval ?hh [e] = rmge2 e" for e unfolding rmge2_def by auto moreover have "total ?hh" using hh totalI1 ‹recfn 1 ?hh› by simp ultimately show ?thesis using ‹recfn 1 ?hh› by blast qed text ‹The first part of the main result is that @{term "U⇘_{LIM-CONS}⇙ ∈ LIM"}.› lemma U_LIMCONS_in_Lim: "U⇘_{LIM-CONS}⇙ ∈ LIM" proof - have "U⇘_{LIM-CONS}⇙ ⊆ ℛ" unfolding U_LIMCONS_def using prepend_in_R1 RPred1_subseteq_R1 by blast have "learn_lim φ U⇘_{LIM-CONS}⇙ rmge2" proof (rule learn_limI) show "environment φ U⇘_{LIM-CONS}⇙ rmge2" using ‹U_LIMCONS ⊆ ℛ› phi_in_P2 rmge2_def rmge2_in_R1 by simp show "∃i. φ i = f ∧ (∀⇧^{∞}n. rmge2 (f ▹ n) ↓= i)" if "f ∈ U⇘_{LIM-CONS}⇙" for f proof - from that obtain vs j p where j: "j ≥ 2" and p: "p ∈ ℛ⇩_{0}⇩_{1}" and s: "φ j = vs @ [j] ⊙ p" and f: "f = vs @ [j] ⊙ p" unfolding U_LIMCONS_def by auto then have "φ j = f" by simp from that have "total1 f" using ‹U⇘_{LIM-CONS}⇙ ⊆ ℛ› R1_imp_total1 total1_def by auto define n⇩_{0}where "n⇩_{0}= length vs" have f_gr_n0: "f n ↓= 0 ∨ f n ↓= 1" if "n > n⇩_{0}" for n proof - have "f n = p (n - n⇩_{0}- 1)" using that n⇩_{0}_def f by simp with RPred1_def p show ?thesis by auto qed have "rmge2 (f ▹ n) ↓= j" if "n ≥ n⇩_{0}" for n proof - have n0_greatest: "(GREATEST i. i < Suc n ∧ the (f i) ≥ 2) = n⇩_{0}" proof (rule Greatest_equality) show "n⇩_{0}< Suc n ∧ the (f n⇩_{0}) ≥ 2" using n⇩_{0}_def f that j by simp show "⋀y. y < Suc n ∧ the (f y) ≥ 2 ⟹ y ≤ n⇩_{0}" proof - fix y assume "y < Suc n ∧ 2 ≤ the (f y)" moreover have "p ∈ ℛ ∧ (∀n. p n ↓= 0 ∨ p n ↓= 1)" using RPred1_def p by blast ultimately show "y ≤ n⇩_{0}" using f_gr_n0 by (metis Suc_1 Suc_n_not_le_n Zero_neq_Suc le_less_linear le_zero_eq option.sel) qed qed have "f n⇩_{0}↓= j" using n⇩_{0}_def f by simp then have "¬ (∀i<Suc n. the (f i) < 2)" using j that less_Suc_eq_le by auto then have "rmge2 (f ▹ n) = f (GREATEST i. i < Suc n ∧ the (f i) ≥ 2)" using rmge2_init_total ‹total1 f› by auto with n0_greatest ‹f n⇩_{0}↓= j› show ?thesis by simp qed with ‹φ j = f› show ?thesis by auto qed qed then show ?thesis using Lim_def by auto qed text ‹The class @{term "U_LIMCONS"} is \emph{prefix-complete}, which means that every non-empty list is the prefix of some function in @{term "U_LIMCONS"}. To show this we use an auxiliary lemma: For every $f \in \mathcal{R}$ and $k \in \mathbb{N}$ the value of $f$ at $k$ can be replaced by a Gödel number of the function resulting from the replacement.› lemma goedel_at: fixes m :: nat and k :: nat assumes "f ∈ ℛ" shows "∃n≥m. φ n = (λx. if x = k then Some n else f x)" proof - define psi :: "partial1 ⇒ nat ⇒ partial2" where "psi = (λf k i x. (if x = k then Some i else f x))" have "psi f k ∈ ℛ⇧^{2}" proof - obtain r where r: "recfn 1 r" "total r" "eval r [x] = f x" for x using assms by auto define r_psi where "r_psi = Cn 2 r_ifeq [Id 2 1, r_dummy 1 (r_const k), Id 2 0, Cn 2 r [Id 2 1]]" show ?thesis proof (rule R2I[of r_psi]) from r_psi_def show "recfn 2 r_psi" using r(1) by simp have "eval r_psi [i, x] = (if x = k then Some i else f x)" for i x proof - have "eval (Cn 2 r [Id 2 1]) [i, x] = f x" using r by simp then have "eval r_psi [i, x] = eval r_ifeq [x, k, i, the (f x)]" unfolding r_psi_def using ‹recfn 2 r_psi› r R1_imp_total1[OF assms] by simp then show ?thesis using assms by simp qed then show "⋀x y. eval r_psi [x, y] = psi f k x y" unfolding psi_def by simp then show "total r_psi" using totalI2[of r_psi] ‹recfn 2 r_psi› assms psi_def by fastforce qed qed then obtain n where "n ≥ m" "φ n = psi f k n" using assms kleene_fixed_point[of "psi f k" m] by auto then show ?thesis unfolding psi_def by auto qed lemma U_LIMCONS_prefix_complete: assumes "length vs > 0" shows "∃f∈U⇘_{LIM-CONS}⇙. prefix f (length vs - 1) = vs" proof - let ?p = "λ_. Some 0" let ?f = "vs @ [0] ⊙ ?p" have "?f ∈ ℛ" using prepend_in_R1 RPred1_subseteq_R1 const0_in_RPred1 by blast with goedel_at[of ?f 2 "length vs"] obtain j where j: "j ≥ 2" "φ j = (λx. if x = length vs then Some j else ?f x)" (is "_ = ?g") by auto moreover have g: "?g x = (vs @ [j] ⊙ ?p) x" for x by (simp add: nth_append) ultimately have "?g ∈ U⇘_{LIM-CONS}⇙" unfolding U_LIMCONS_def using const0_in_RPred1 by fastforce moreover have "prefix ?g (length vs - 1) = vs" using g assms prefixI prepend_associative by auto ultimately show ?thesis by auto qed text ‹Roughly speaking, a strategy learning a prefix-complete class must be total because it must be defined for every prefix in the class. Technically, however, the empty list is not a prefix, and thus a strategy may diverge on input 0. We can work around this by showing that if there is a strategy learning a prefix-complete class then there is also a total strategy learning this class. We need the result only for consistent learning.› lemma U_prefix_complete_imp_total_strategy: assumes "⋀vs. length vs > 0 ⟹ ∃f∈U. prefix f (length vs - 1) = vs" and "learn_cons ψ U s" shows "∃t. total1 t ∧ learn_cons ψ U t" proof - define t where "t = (λe. if e = 0 then Some 0 else s e)" have "s e ↓" if "e > 0" for e proof - from that have "list_decode e ≠ []" (is "?vs ≠ _") using list_encode_0 list_encode_decode by (metis less_imp_neq) then have "length ?vs > 0" by simp with assms(1) obtain f where f: "f ∈ U" "prefix f (length ?vs - 1) = ?vs" by auto with learn_cons_def learn_limE have "s (f ▹ (length ?vs - 1)) ↓" using assms(2) by auto then show "s e ↓" using f(2) init_def by auto qed then have "total1 t" using t_def by auto have "t ∈ 𝒫" proof - from assms(2) have "s ∈ 𝒫" using learn_consE by simp then obtain rs where rs: "recfn 1 rs" "eval rs [x] = s x" for x by auto define rt where "rt = Cn 1 (r_lifz Z rs) [Id 1 0, Id 1 0]" then have "recfn 1 rt" using rs by auto moreover have "eval rt [x] = t x" for x using rs rt_def t_def by simp ultimately show ?thesis by blast qed have "s (f ▹ n) = t (f ▹ n)" if "f ∈ U" for f n unfolding t_def by (simp add: init_neq_zero) then have "learn_cons ψ U t" using ‹t ∈ 𝒫› assms(2) learn_consE[of ψ U s] learn_consI[of ψ U t] by simp with ‹total1 t› show ?thesis by auto qed text ‹The proof of @{prop "U⇘_{LIM-CONS}⇙ ∉ CONS"} is by contradiction. Assume there is a consistent learning strategy $S$. By the previous lemma $S$ can be assumed to be total. Moreover it outputs a consistent hypothesis for every prefix. Thus for every $e \in \mathbb{N}^+$, $S(e) \neq S(e0)$ or $S(e) \neq S(e1)$ because $S(e)$ cannot be consistent with both $e0$ and $e1$. We use this property of $S$ to construct a function in @{term "U⇘_{LIM-CONS}⇙"} for which $S$ fails as a learning strategy. To this end we define a numbering $\psi \in \mathcal{R}^2$ with $\psi_i(0) = i$ and \[ \psi_i(x + 1) = \left\{\begin{array}{ll} 0 & \mbox{if } S(\psi_i^x0) \neq S(\psi_i^x),\\ 1 & \mbox{otherwise}. \end{array}\right. \] This numbering is recursive because $S$ is total. The ``otherwise'' case is equivalent to $S(\psi_i^x1) \neq S(\psi_i^x)$ because $S(\psi_i^x)$ cannot be consistent with both $\psi_i^x0$ and $\psi_i^x1$. Therefore every prefix $\psi_i^x$ is extended in such a way that $S$ changes its hypothesis. Hence $S$ does not learn $\psi_i$ in the limit. Kleene's fixed-point theorem ensures that for some $j \geq 2$, $\varphi_j = \psi_j$. This $\psi_j$ is the sought function in @{term "U⇘_{LIM-CONS}⇙"}. The following locale formalizes the construction of $\psi$ for a total strategy $S$.› locale cons_lim = fixes s :: partial1 assumes s_in_R1: "s ∈ ℛ" begin text ‹A @{typ recf} computing the strategy:› definition r_s :: recf where "r_s ≡ SOME r_s. recfn 1 r_s ∧ total r_s ∧ s = (λx. eval r_s [x])" lemma r_s_recfn [simp]: "recfn 1 r_s" and r_s_total [simp]: "⋀x. eval r_s [x] ↓" and eval_r_s: "s = (λx. eval r_s [x])" using r_s_def R1_SOME[OF s_in_R1, of r_s] by simp_all text ‹The next function represents the prefixes of $\psi_i$.› fun prefixes :: "nat ⇒ nat ⇒ nat list" where "prefixes i 0 = [i]" | "prefixes i (Suc x) = (prefixes i x) @ [if s (e_snoc (list_encode (prefixes i x)) 0) = s (list_encode (prefixes i x)) then 1 else 0]" definition "r_prefixes_aux ≡ Cn 3 r_ifeq [Cn 3 r_s [Cn 3 r_snoc [Id 3 1, r_constn 2 0]], Cn 3 r_s [Id 3 1], Cn 3 r_snoc [Id 3 1, r_constn 2 1], Cn 3 r_snoc [Id 3 1, r_constn 2 0]]" lemma r_prefixes_aux_recfn: "recfn 3 r_prefixes_aux" unfolding r_prefixes_aux_def by simp lemma r_prefixes_aux: "eval r_prefixes_aux [j, v, i] ↓= e_snoc v (if eval r_s [e_snoc v 0] = eval r_s [v] then 1 else 0)" unfolding r_prefixes_aux_def by auto definition "r_prefixes ≡ r_swap (Pr 1 r_singleton_encode r_prefixes_aux)" lemma r_prefixes_recfn: "recfn 2 r_prefixes" unfolding r_prefixes_def r_prefixes_aux_def by simp lemma r_prefixes: "eval r_prefixes [i, n] ↓= list_encode (prefixes i n)" proof - let ?h = "Pr 1 r_singleton_encode r_prefixes_aux" have "eval ?h [n, i] ↓= list_encode (prefixes i n)" proof (induction n) case 0 then show ?case using r_prefixes_def r_prefixes_aux_recfn r_singleton_encode by simp next case (Suc n) then show ?case using r_prefixes_aux_recfn r_prefixes_aux eval_r_s by auto metis+ qed moreover have "eval ?h [n, i] = eval r_prefixes [i, n]" for i n unfolding r_prefixes_def by (simp add: r_prefixes_aux_recfn) ultimately show ?thesis by simp qed lemma prefixes_neq_nil: "length (prefixes i x) > 0" by (induction x) auto text ‹The actual numbering can then be defined via @{term prefixes}.› definition psi :: "partial2" ("ψ") where "ψ i x ≡ Some (last (prefixes i x))" lemma psi_in_R2: "ψ ∈ ℛ⇧^{2}" proof define r_psi where "r_psi ≡ Cn 2 r_last [r_prefixes]" have "recfn 2 r_psi" unfolding r_psi_def by (simp add: r_prefixes_recfn) then have "eval r_psi [i, n] ↓= last (prefixes i n)" for n i unfolding r_psi_def using r_prefixes r_prefixes_recfn prefixes_neq_nil by simp then have "(λi x. Some (last (prefixes i x))) ∈ 𝒫⇧^{2}" using ‹recfn 2 r_psi› P2I[of "r_psi"] by simp with psi_def show "ψ ∈ 𝒫⇧^{2}" by presburger moreover show "total2 psi" unfolding psi_def by auto qed lemma psi_0_or_1: assumes "n > 0" shows "ψ i n ↓= 0 ∨ ψ i n ↓= 1" proof - from assms obtain m where "n = Suc m" using gr0_implies_Suc by blast then have "last (prefixes i (Suc m)) = 0 ∨ last (prefixes i (Suc m)) = 1" by simp then show ?thesis using ‹n = Suc m› psi_def by simp qed text ‹The function @{term "prefixes"} does indeed provide the prefixes for @{term "ψ"}.› lemma psi_init: "(ψ i) ▹ x = list_encode (prefixes i x)" proof - have "prefix (ψ i) x = prefixes i x" unfolding psi_def by (induction x) (simp_all add: prefix_0 prefix_Suc) with init_def show ?thesis by simp qed text ‹One of the functions $\psi_i$ is in @{term "U⇘_{LIM-CONS}⇙"}.› lemma ex_psi_in_U: "∃j. ψ j ∈ U⇘_{LIM-CONS}⇙" proof - obtain j where j: "j ≥ 2" "ψ j = φ j" using kleene_fixed_point[of ψ] psi_in_R2 R2_imp_P2 by metis then have "ψ j ∈ 𝒫" by (simp add: phi_in_P2) define p where "p = (λx. ψ j (x + 1))" have "p ∈ ℛ⇩_{0}⇩_{1}" proof - from p_def ‹ψ j ∈ 𝒫› skip_P1 have "p ∈ 𝒫" by blast from psi_in_R2 have "total1 (ψ j)" by simp with p_def have "total1 p" by (simp add: total1_def) with psi_0_or_1 have "p n ↓= 0 ∨ p n ↓= 1" for n using psi_def p_def by simp then show ?thesis by (simp add: RPred1_def P1_total_imp_R1 ‹p ∈ 𝒫› ‹total1 p›) qed moreover have "ψ j = [j] ⊙ p" proof fix x show "ψ j x = ([j] ⊙ p) x" proof (cases "x = 0") case True then show ?thesis using psi_def psi_def prepend_at_less by simp next case False then show ?thesis using p_def by simp qed qed ultimately have "ψ j ∈ U⇘_{LIM-CONS}⇙" using j U_LIMCONS_def by (metis (mono_tags, lifting) append_Nil mem_Collect_eq) then show ?thesis by auto qed text ‹The strategy fails to learn @{term U_LIMCONS} because it changes its hypothesis all the time on functions $\psi_j \in V_0$.› lemma U_LIMCONS_not_learn_cons: "¬ learn_cons φ U⇘_{LIM-CONS}⇙ s" proof assume learn: "learn_cons φ U⇘_{LIM-CONS}⇙ s" have "s (list_encode (vs @ [0])) ≠ s (list_encode (vs @ [1]))" for vs proof - obtain f⇩_{0}where f0: "f⇩_{0}∈ U⇘_{LIM-CONS}⇙" "prefix f⇩_{0}(length vs) = vs @ [0]" using U_LIMCONS_prefix_complete[of "vs @ [0]"] by auto obtain f⇩_{1}where f1: "f⇩_{1}∈ U⇘_{LIM-CONS}⇙" "prefix f⇩_{1}(length vs) = vs @ [1]" using U_LIMCONS_prefix_complete[of "vs @ [1]"] by auto have "f⇩_{0}(length vs) ≠ f⇩_{1}(length vs)" using f0 f1 by (metis lessI nth_append_length prefix_nth zero_neq_one) moreover have "φ (the (s (f⇩_{0}▹ length vs))) (length vs) = f⇩_{0}(length vs)" using learn_consE(3)[of φ U_LIMCONS s, OF learn, of f⇩_{0}"length vs", OF f0(1)] by simp moreover have "φ (the (s (f⇩_{1}▹ length vs))) (length vs) = f⇩_{1}(length vs)" using learn_consE(3)[of φ U_LIMCONS s, OF learn, of f⇩_{1}"length vs", OF f1(1)] by simp ultimately have "the (s (f⇩_{0}▹ length vs)) ≠ the (s (f⇩_{1}▹ length vs))" by auto then have "s (f⇩_{0}▹ length vs) ≠ s (f⇩_{1}▹ length vs)" by auto with f0(2) f1(2) show ?thesis by (simp add: init_def) qed then have "s (list_encode (vs @ [0])) ≠ s (list_encode vs) ∨ s (list_encode (vs @ [1])) ≠ s (list_encode vs)" for vs by metis then have "s (list_encode (prefixes i (Suc x))) ≠ s (list_encode (prefixes i x))" for i x by simp then have "¬ learn_lim φ {ψ i} s" for i using psi_def psi_init always_hyp_change_not_Lim by simp then have "¬ learn_lim φ U_LIMCONS s" using ex_psi_in_U learn_lim_closed_subseteq by blast then show False using learn learn_cons_def by simp qed end text ‹With the locale we can now show the second part of the main result:› lemma U_LIMCONS_not_in_CONS: "U⇘_{LIM-CONS}⇙ ∉ CONS" proof assume "U⇘_{LIM-CONS}⇙ ∈ CONS" then have "U⇘_{LIM-CONS}⇙ ∈ CONS_wrt φ" by (simp add: CONS_wrt_phi_eq_CONS) then obtain almost_s where "learn_cons φ U⇘_{LIM-CONS}⇙ almost_s" using CONS_wrt_def by auto then obtain s where s: "total1 s" "learn_cons φ U⇘_{LIM-CONS}⇙ s" using U_LIMCONS_prefix_complete U_prefix_complete_imp_total_strategy by blast then have "s ∈ ℛ" using learn_consE(1) P1_total_imp_R1 by blast with cons_lim_def interpret cons_lim s by simp show False using s(2) U_LIMCONS_not_learn_cons by simp qed text ‹The main result of this section:› theorem CONS_subset_Lim: "CONS ⊂ LIM" using U_LIMCONS_in_Lim U_LIMCONS_not_in_CONS CONS_subseteq_Lim by auto end