---

Step * of Lemma simple_fan_theorem-ext

∀[X:n:ℕ ⟶ (ℕn ⟶ 𝔹) ⟶ ℙ]
  (∀n:ℕ. ∀s:ℕn ⟶ 𝔹.  Dec(X[n;s])) ⇒ (∃k:ℕ [(∀f:ℕ ⟶ 𝔹. ∃n:ℕk. X[n;f])]) supposing ∀f:ℕ ⟶ 𝔹. (↓∃n:ℕ. X[n;f])
BY
{ Extract of Obid: simple_fan_theorem
  not unfolding  bar_recursion btrue bfalse
  finishing with (Try (Fold `bottom` 0)
                  THEN SqequalSqle
                  THEN RepeatFor 3 (SqLeCD)
                  THEN SqReasoning
                  THEN RevHypSubst (-1) 0
                  THEN AutoSplit)
  normalizes to:
  
  λd.bar_recursion(d;
                   λn,s,f. 1;
                   λn,s,f. eval a = f tt in eval b = f ff in   if (a) < (b)  then 1 + b  else (1 + a);
                   0;λm.eval x = m in
                        ⊥) }

---

Latex:

---

Latex:
\mforall{}[X:n:\mBbbN{}  {}\mrightarrow{}  (\mBbbN{}n  {}\mrightarrow{}  \mBbbB{})  {}\mrightarrow{}  \mBbbP{}]
    (\mforall{}n:\mBbbN{}.  \mforall{}s:\mBbbN{}n  {}\mrightarrow{}  \mBbbB{}.    Dec(X[n;s]))  {}\mRightarrow{}  (\mexists{}k:\mBbbN{}  [(\mforall{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbB{}.  \mexists{}n:\mBbbN{}k.  X[n;f])]) 
    supposing  \mforall{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbB{}.  (\mdownarrow{}\mexists{}n:\mBbbN{}.  X[n;f])


By

---

Latex:
Extract  of  Obid:  simple\_fan\_theorem
not  unfolding    bar\_recursion  btrue  bfalse
finishing  with  (Try  (Fold  `bottom`  0)
                                THEN  SqequalSqle
                                THEN  RepeatFor  3  (SqLeCD)
                                THEN  SqReasoning
                                THEN  RevHypSubst  (-1)  0
                                THEN  AutoSplit)
normalizes  to:

\mlambda{}d.bar\_recursion(d;
                                  \mlambda{}n,s,f.  1;
                                  \mlambda{}n,s,f.  eval  a  =  f  tt  in  eval  b  =  f  ff  in      if  (a)  <  (b)    then  1  +  b    else  (1  +  a);
                                  0;\mlambda{}m.eval  x  =  m  in
                                            \mbot{})

---

Home Index